Metamath Proof Explorer

Theorem scott0b

Description: Applying Scott's trick yields the empty set iff it was applied to the empty set. (Contributed by NM, 15-Oct-2003) Use the Scott operation. (Revised by BTernaryTau, 19-Jul-2026)

Ref Expression
Assertion scott0b ( 𝐴 = ∅ ↔ Scott 𝐴 = ∅ )

Proof

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