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 
|- ( A = (/) <-> { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } = (/) )

Proof

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