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 syl5ib
 |-  ( |^|_ 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 ) } = (/) )