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

Metamath Proof Explorer

Theorem scott0

Description: Scott's trick collects all sets that have a certain property and are of the smallest possible rank. This theorem shows that the resulting collection, expressed as in Equation 9.3 of Jech p. 72, contains at least one representative with the property, if there is one. In other words, the collection is empty iff no set has the property (i.e. A is empty). (Contributed by NM, 15-Oct-2003)

Ref Expression
Assertion scott0 ( 𝐴 = ∅ ↔ { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } = ∅ )

Proof

Step Hyp Ref Expression
1 rabeq ⊢ ( 𝐴 = ∅ → { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } = { 𝑥 ∈ ∅ ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } )
2 rab0 ⊢ { 𝑥 ∈ ∅ ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } = ∅
3 1 2 eqtrdi ⊢ ( 𝐴 = ∅ → { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } = ∅ )
4 n0 ⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑥 𝑥 ∈ 𝐴 )
5 nfre1 ⊢ Ⅎ 𝑥 ∃ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) = ( rank ‘ 𝑥 )
6 eqid ⊢ ( rank ‘ 𝑥 ) = ( rank ‘ 𝑥 )
7 rspe ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( rank ‘ 𝑥 ) = ( rank ‘ 𝑥 ) ) → ∃ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) = ( rank ‘ 𝑥 ) )
8 6 7 mpan2 ⊢ ( 𝑥 ∈ 𝐴 → ∃ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) = ( rank ‘ 𝑥 ) )
9 5 8 exlimi ⊢ ( ∃ 𝑥 𝑥 ∈ 𝐴 → ∃ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) = ( rank ‘ 𝑥 ) )
10 4 9 sylbi ⊢ ( 𝐴 ≠ ∅ → ∃ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) = ( rank ‘ 𝑥 ) )
11 fvex ⊢ ( rank ‘ 𝑥 ) ∈ V
12 eqeq1 ⊢ ( 𝑦 = ( rank ‘ 𝑥 ) → ( 𝑦 = ( rank ‘ 𝑥 ) ↔ ( rank ‘ 𝑥 ) = ( rank ‘ 𝑥 ) ) )
13 12 anbi2d ⊢ ( 𝑦 = ( rank ‘ 𝑥 ) → ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( rank ‘ 𝑥 ) ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( rank ‘ 𝑥 ) = ( rank ‘ 𝑥 ) ) ) )
14 11 13 spcev ⊢ ( ( 𝑥 ∈ 𝐴 ∧ ( rank ‘ 𝑥 ) = ( rank ‘ 𝑥 ) ) → ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( rank ‘ 𝑥 ) ) )
15 14 eximi ⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ( rank ‘ 𝑥 ) = ( rank ‘ 𝑥 ) ) → ∃ 𝑥 ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( rank ‘ 𝑥 ) ) )
16 excom ⊢ ( ∃ 𝑦 ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( rank ‘ 𝑥 ) ) ↔ ∃ 𝑥 ∃ 𝑦 ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( rank ‘ 𝑥 ) ) )
17 15 16 sylibr ⊢ ( ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ( rank ‘ 𝑥 ) = ( rank ‘ 𝑥 ) ) → ∃ 𝑦 ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( rank ‘ 𝑥 ) ) )
18 df-rex ⊢ ( ∃ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) = ( rank ‘ 𝑥 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ ( rank ‘ 𝑥 ) = ( rank ‘ 𝑥 ) ) )
19 df-rex ⊢ ( ∃ 𝑥 ∈ 𝐴 𝑦 = ( rank ‘ 𝑥 ) ↔ ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( rank ‘ 𝑥 ) ) )
20 19 exbii ⊢ ( ∃ 𝑦 ∃ 𝑥 ∈ 𝐴 𝑦 = ( rank ‘ 𝑥 ) ↔ ∃ 𝑦 ∃ 𝑥 ( 𝑥 ∈ 𝐴 ∧ 𝑦 = ( rank ‘ 𝑥 ) ) )
21 17 18 20 3imtr4i ⊢ ( ∃ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) = ( rank ‘ 𝑥 ) → ∃ 𝑦 ∃ 𝑥 ∈ 𝐴 𝑦 = ( rank ‘ 𝑥 ) )
22 10 21 syl ⊢ ( 𝐴 ≠ ∅ → ∃ 𝑦 ∃ 𝑥 ∈ 𝐴 𝑦 = ( rank ‘ 𝑥 ) )
23 abn0 ⊢ ( { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( rank ‘ 𝑥 ) } ≠ ∅ ↔ ∃ 𝑦 ∃ 𝑥 ∈ 𝐴 𝑦 = ( rank ‘ 𝑥 ) )
24 22 23 sylibr ⊢ ( 𝐴 ≠ ∅ → { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( rank ‘ 𝑥 ) } ≠ ∅ )
25 11 dfiin2 ⊢ ∩ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) = ∩ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( rank ‘ 𝑥 ) }
26 rankon ⊢ ( rank ‘ 𝑥 ) ∈ On
27 eleq1 ⊢ ( 𝑦 = ( rank ‘ 𝑥 ) → ( 𝑦 ∈ On ↔ ( rank ‘ 𝑥 ) ∈ On ) )
28 26 27 mpbiri ⊢ ( 𝑦 = ( rank ‘ 𝑥 ) → 𝑦 ∈ On )
29 28 rexlimivw ⊢ ( ∃ 𝑥 ∈ 𝐴 𝑦 = ( rank ‘ 𝑥 ) → 𝑦 ∈ On )
30 29 abssi ⊢ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( rank ‘ 𝑥 ) } ⊆ On
31 onint ⊢ ( ( { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( rank ‘ 𝑥 ) } ⊆ On ∧ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( rank ‘ 𝑥 ) } ≠ ∅ ) → ∩ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( rank ‘ 𝑥 ) } ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( rank ‘ 𝑥 ) } )
32 30 31 mpan ⊢ ( { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( rank ‘ 𝑥 ) } ≠ ∅ → ∩ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( rank ‘ 𝑥 ) } ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( rank ‘ 𝑥 ) } )
33 25 32 eqeltrid ⊢ ( { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( rank ‘ 𝑥 ) } ≠ ∅ → ∩ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( rank ‘ 𝑥 ) } )
34 nfii1 ⊢ Ⅎ 𝑥 ∩ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 )
35 34 nfeq2 ⊢ Ⅎ 𝑥 𝑦 = ∩ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 )
36 eqeq1 ⊢ ( 𝑦 = ∩ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) → ( 𝑦 = ( rank ‘ 𝑥 ) ↔ ∩ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) = ( rank ‘ 𝑥 ) ) )
37 35 36 rexbid ⊢ ( 𝑦 = ∩ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) → ( ∃ 𝑥 ∈ 𝐴 𝑦 = ( rank ‘ 𝑥 ) ↔ ∃ 𝑥 ∈ 𝐴 ∩ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) = ( rank ‘ 𝑥 ) ) )
38 37 elabg ⊢ ( ∩ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( rank ‘ 𝑥 ) } → ( ∩ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( rank ‘ 𝑥 ) } ↔ ∃ 𝑥 ∈ 𝐴 ∩ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) = ( rank ‘ 𝑥 ) ) )
39 38 ibi ⊢ ( ∩ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ∈ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = ( rank ‘ 𝑥 ) } → ∃ 𝑥 ∈ 𝐴 ∩ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) = ( rank ‘ 𝑥 ) )
40 ssid ⊢ ( rank ‘ 𝑦 ) ⊆ ( rank ‘ 𝑦 )
41 fveq2 ⊢ ( 𝑥 = 𝑦 → ( rank ‘ 𝑥 ) = ( rank ‘ 𝑦 ) )
42 41 sseq1d ⊢ ( 𝑥 = 𝑦 → ( ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ↔ ( rank ‘ 𝑦 ) ⊆ ( rank ‘ 𝑦 ) ) )
43 42 rspcev ⊢ ( ( 𝑦 ∈ 𝐴 ∧ ( rank ‘ 𝑦 ) ⊆ ( rank ‘ 𝑦 ) ) → ∃ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) )
44 40 43 mpan2 ⊢ ( 𝑦 ∈ 𝐴 → ∃ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) )
45 iinss ⊢ ( ∃ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) → ∩ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) )
46 44 45 syl ⊢ ( 𝑦 ∈ 𝐴 → ∩ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) )
47 sseq1 ⊢ ( ∩ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) = ( rank ‘ 𝑥 ) → ( ∩ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ↔ ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) )
48 46 47 imbitrid ⊢ ( ∩ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) = ( rank ‘ 𝑥 ) → ( 𝑦 ∈ 𝐴 → ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) ) )
49 48 ralrimiv ⊢ ( ∩ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) = ( rank ‘ 𝑥 ) → ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) )
50 49 reximi ⊢ ( ∃ 𝑥 ∈ 𝐴 ∩ 𝑥 ∈ 𝐴 ( rank ‘ 𝑥 ) = ( rank ‘ 𝑥 ) → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) )
51 24 33 39 50 4syl ⊢ ( 𝐴 ≠ ∅ → ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) )
52 rabn0 ⊢ ( { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } ≠ ∅ ↔ ∃ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) )
53 51 52 sylibr ⊢ ( 𝐴 ≠ ∅ → { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } ≠ ∅ )
54 53 necon4i ⊢ ( { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } = ∅ → 𝐴 = ∅ )
55 3 54 impbii ⊢ ( 𝐴 = ∅ ↔ { 𝑥 ∈ 𝐴 ∣ ∀ 𝑦 ∈ 𝐴 ( rank ‘ 𝑥 ) ⊆ ( rank ‘ 𝑦 ) } = ∅ )