This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem scott0s

Description: Theorem scheme version of scott0 . The collection of all x of minimum rank such that ph ( x ) is true, is not empty iff there is an x such that ph ( x ) holds. (Contributed by NM, 13-Oct-2003)

Ref Expression
Assertion scott0s ( ∃ 𝑥 𝜑 ↔ { 𝑥 ∣ ( 𝜑 ∧ ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) } ≠ ∅ )

Proof

Step Hyp Ref Expression
1 abn0 ⊢ ( { 𝑥 ∣ 𝜑 } ≠ ∅ ↔ ∃ 𝑥 𝜑 )
2 scott0 ⊢ ( { 𝑥 ∣ 𝜑 } = ∅ ↔ { 𝑧 ∈ { 𝑥 ∣ 𝜑 } ∣ ∀ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) } = ∅ )
3 nfcv ⊢ Ⅎ 𝑧 { 𝑥 ∣ 𝜑 }
4 nfab1 ⊢ Ⅎ 𝑥 { 𝑥 ∣ 𝜑 }
5 nfv ⊢ Ⅎ 𝑥 ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 )
6 4 5 nfralw ⊢ Ⅎ 𝑥 ∀ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 )
7 nfv ⊢ Ⅎ 𝑧 ∀ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 )
8 fveq2 ⊢ ( 𝑧 = 𝑥 → ( rank ‘ 𝑧 ) = ( rank ‘ 𝑥 ) )
9 8 sseq1d ⊢ ( 𝑧 = 𝑥 → ( ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) ↔ ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) )
10 9 ralbidv ⊢ ( 𝑧 = 𝑥 → ( ∀ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) ↔ ∀ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) )
11 3 4 6 7 10 cbvrabw ⊢ { 𝑧 ∈ { 𝑥 ∣ 𝜑 } ∣ ∀ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) } = { 𝑥 ∈ { 𝑥 ∣ 𝜑 } ∣ ∀ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) }
12 df-rab ⊢ { 𝑥 ∈ { 𝑥 ∣ 𝜑 } ∣ ∀ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } = { 𝑥 ∣ ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ∧ ∀ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) }
13 abid ⊢ ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ↔ 𝜑 )
14 df-ral ⊢ ( ∀ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ↔ ∀ 𝑦 ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) )
15 df-sbc ⊢ ( [ 𝑦 / 𝑥 ] 𝜑 ↔ 𝑦 ∈ { 𝑥 ∣ 𝜑 } )
16 15 imbi1i ⊢ ( ( [ 𝑦 / 𝑥 ] 𝜑 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ↔ ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) )
17 16 albii ⊢ ( ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ↔ ∀ 𝑦 ( 𝑦 ∈ { 𝑥 ∣ 𝜑 } → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) )
18 14 17 bitr4i ⊢ ( ∀ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ↔ ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) )
19 13 18 anbi12i ⊢ ( ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ∧ ∀ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ↔ ( 𝜑 ∧ ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) )
20 19 abbii ⊢ { 𝑥 ∣ ( 𝑥 ∈ { 𝑥 ∣ 𝜑 } ∧ ∀ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) } = { 𝑥 ∣ ( 𝜑 ∧ ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) }
21 11 12 20 3eqtri ⊢ { 𝑧 ∈ { 𝑥 ∣ 𝜑 } ∣ ∀ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) } = { 𝑥 ∣ ( 𝜑 ∧ ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) }
22 21 eqeq1i ⊢ ( { 𝑧 ∈ { 𝑥 ∣ 𝜑 } ∣ ∀ 𝑦 ∈ { 𝑥 ∣ 𝜑 } ( rank ‘ 𝑧 ) ⊆ ( rank ‘ 𝑦 ) } = ∅ ↔ { 𝑥 ∣ ( 𝜑 ∧ ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) } = ∅ )
23 2 22 bitri ⊢ ( { 𝑥 ∣ 𝜑 } = ∅ ↔ { 𝑥 ∣ ( 𝜑 ∧ ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) } = ∅ )
24 23 necon3bii ⊢ ( { 𝑥 ∣ 𝜑 } ≠ ∅ ↔ { 𝑥 ∣ ( 𝜑 ∧ ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) } ≠ ∅ )
25 1 24 bitr3i ⊢ ( ∃ 𝑥 𝜑 ↔ { 𝑥 ∣ ( 𝜑 ∧ ∀ 𝑦 ( [ 𝑦 / 𝑥 ] 𝜑 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) ) } ≠ ∅ )