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 
|- ( A = (/) <-> Scott A = (/) )

Proof

Step Hyp Ref Expression
1 scotteq 
 |-  ( A = (/) -> Scott A = Scott (/) )
2 scott0 
 |-  Scott (/) = (/)
3 1 2 eqtrdi 
 |-  ( A = (/) -> Scott A = (/) )
4 df-scott 
 |-  Scott A = { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) }
5 4 eqeq1i 
 |-  ( Scott A = (/) <-> { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } = (/) )
6 n0 
 |-  ( A =/= (/) <-> E. x x e. A )
7 nfre1 
 |-  F/ x E. x e. A ( rank ` x ) = ( rank ` x )
8 eqid 
 |-  ( rank ` x ) = ( rank ` x )
9 rspe 
 |-  ( ( x e. A /\ ( rank ` x ) = ( rank ` x ) ) -> E. x e. A ( rank ` x ) = ( rank ` x ) )
10 8 9 mpan2 
 |-  ( x e. A -> E. x e. A ( rank ` x ) = ( rank ` x ) )
11 7 10 exlimi 
 |-  ( E. x x e. A -> E. x e. A ( rank ` x ) = ( rank ` x ) )
12 6 11 sylbi 
 |-  ( A =/= (/) -> E. x e. A ( rank ` x ) = ( rank ` x ) )
13 fvex 
 |-  ( rank ` x ) e. _V
14 eqeq1 
 |-  ( y = ( rank ` x ) -> ( y = ( rank ` x ) <-> ( rank ` x ) = ( rank ` x ) ) )
15 14 anbi2d 
 |-  ( y = ( rank ` x ) -> ( ( x e. A /\ y = ( rank ` x ) ) <-> ( x e. A /\ ( rank ` x ) = ( rank ` x ) ) ) )
16 13 15 spcev 
 |-  ( ( x e. A /\ ( rank ` x ) = ( rank ` x ) ) -> E. y ( x e. A /\ y = ( rank ` x ) ) )
17 16 eximi 
 |-  ( E. x ( x e. A /\ ( rank ` x ) = ( rank ` x ) ) -> E. x E. y ( x e. A /\ y = ( rank ` x ) ) )
18 excom 
 |-  ( E. y E. x ( x e. A /\ y = ( rank ` x ) ) <-> E. x E. y ( x e. A /\ y = ( rank ` x ) ) )
19 17 18 sylibr 
 |-  ( E. x ( x e. A /\ ( rank ` x ) = ( rank ` x ) ) -> E. y E. x ( x e. A /\ y = ( rank ` x ) ) )
20 df-rex 
 |-  ( E. x e. A ( rank ` x ) = ( rank ` x ) <-> E. x ( x e. A /\ ( rank ` x ) = ( rank ` x ) ) )
21 df-rex 
 |-  ( E. x e. A y = ( rank ` x ) <-> E. x ( x e. A /\ y = ( rank ` x ) ) )
22 21 exbii 
 |-  ( E. y E. x e. A y = ( rank ` x ) <-> E. y E. x ( x e. A /\ y = ( rank ` x ) ) )
23 19 20 22 3imtr4i 
 |-  ( E. x e. A ( rank ` x ) = ( rank ` x ) -> E. y E. x e. A y = ( rank ` x ) )
24 12 23 syl 
 |-  ( A =/= (/) -> E. y E. x e. A y = ( rank ` x ) )
25 abn0 
 |-  ( { y | E. x e. A y = ( rank ` x ) } =/= (/) <-> E. y E. x e. A y = ( rank ` x ) )
26 24 25 sylibr 
 |-  ( A =/= (/) -> { y | E. x e. A y = ( rank ` x ) } =/= (/) )
27 13 dfiin2 
 |-  |^|_ x e. A ( rank ` x ) = |^| { y | E. x e. A y = ( rank ` x ) }
28 rankon 
 |-  ( rank ` x ) e. On
29 eleq1 
 |-  ( y = ( rank ` x ) -> ( y e. On <-> ( rank ` x ) e. On ) )
30 28 29 mpbiri 
 |-  ( y = ( rank ` x ) -> y e. On )
31 30 rexlimivw 
 |-  ( E. x e. A y = ( rank ` x ) -> y e. On )
32 31 abssi 
 |-  { y | E. x e. A y = ( rank ` x ) } C_ On
33 onint 
 |-  ( ( { y | E. x e. A y = ( rank ` x ) } C_ On /\ { y | E. x e. A y = ( rank ` x ) } =/= (/) ) -> |^| { y | E. x e. A y = ( rank ` x ) } e. { y | E. x e. A y = ( rank ` x ) } )
34 32 33 mpan 
 |-  ( { y | E. x e. A y = ( rank ` x ) } =/= (/) -> |^| { y | E. x e. A y = ( rank ` x ) } e. { y | E. x e. A y = ( rank ` x ) } )
35 27 34 eqeltrid 
 |-  ( { y | E. x e. A y = ( rank ` x ) } =/= (/) -> |^|_ x e. A ( rank ` x ) e. { y | E. x e. A y = ( rank ` x ) } )
36 nfii1 
 |-  F/_ x |^|_ x e. A ( rank ` x )
37 36 nfeq2 
 |-  F/ x y = |^|_ x e. A ( rank ` x )
38 eqeq1 
 |-  ( y = |^|_ x e. A ( rank ` x ) -> ( y = ( rank ` x ) <-> |^|_ x e. A ( rank ` x ) = ( rank ` x ) ) )
39 37 38 rexbid 
 |-  ( y = |^|_ x e. A ( rank ` x ) -> ( E. x e. A y = ( rank ` x ) <-> E. x e. A |^|_ x e. A ( rank ` x ) = ( rank ` x ) ) )
40 39 elabg 
 |-  ( |^|_ x e. A ( rank ` x ) e. { y | E. x e. A y = ( rank ` x ) } -> ( |^|_ x e. A ( rank ` x ) e. { y | E. x e. A y = ( rank ` x ) } <-> E. x e. A |^|_ x e. A ( rank ` x ) = ( rank ` x ) ) )
41 40 ibi 
 |-  ( |^|_ x e. A ( rank ` x ) e. { y | E. x e. A y = ( rank ` x ) } -> E. x e. A |^|_ x e. A ( rank ` x ) = ( rank ` x ) )
42 ssid 
 |-  ( rank ` y ) C_ ( rank ` y )
43 fveq2 
 |-  ( x = y -> ( rank ` x ) = ( rank ` y ) )
44 43 sseq1d 
 |-  ( x = y -> ( ( rank ` x ) C_ ( rank ` y ) <-> ( rank ` y ) C_ ( rank ` y ) ) )
45 44 rspcev 
 |-  ( ( y e. A /\ ( rank ` y ) C_ ( rank ` y ) ) -> E. x e. A ( rank ` x ) C_ ( rank ` y ) )
46 42 45 mpan2 
 |-  ( y e. A -> E. x e. A ( rank ` x ) C_ ( rank ` y ) )
47 iinss 
 |-  ( E. x e. A ( rank ` x ) C_ ( rank ` y ) -> |^|_ x e. A ( rank ` x ) C_ ( rank ` y ) )
48 46 47 syl 
 |-  ( y e. A -> |^|_ x e. A ( rank ` x ) C_ ( rank ` y ) )
49 sseq1 
 |-  ( |^|_ x e. A ( rank ` x ) = ( rank ` x ) -> ( |^|_ x e. A ( rank ` x ) C_ ( rank ` y ) <-> ( rank ` x ) C_ ( rank ` y ) ) )
50 48 49 imbitrid 
 |-  ( |^|_ x e. A ( rank ` x ) = ( rank ` x ) -> ( y e. A -> ( rank ` x ) C_ ( rank ` y ) ) )
51 50 ralrimiv 
 |-  ( |^|_ x e. A ( rank ` x ) = ( rank ` x ) -> A. y e. A ( rank ` x ) C_ ( rank ` y ) )
52 51 reximi 
 |-  ( E. x e. A |^|_ x e. A ( rank ` x ) = ( rank ` x ) -> E. x e. A A. y e. A ( rank ` x ) C_ ( rank ` y ) )
53 26 35 41 52 4syl 
 |-  ( A =/= (/) -> E. x e. A A. y e. A ( rank ` x ) C_ ( rank ` y ) )
54 rabn0 
 |-  ( { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } =/= (/) <-> E. x e. A A. y e. A ( rank ` x ) C_ ( rank ` y ) )
55 53 54 sylibr 
 |-  ( A =/= (/) -> { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } =/= (/) )
56 55 necon4i 
 |-  ( { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } = (/) -> A = (/) )
57 5 56 sylbi 
 |-  ( Scott A = (/) -> A = (/) )
58 3 57 impbii 
 |-  ( A = (/) <-> Scott A = (/) )