Metamath Proof Explorer

Theorem scottex

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, is a set. (Contributed by NM, 13-Oct-2003)

Ref Expression
Assertion scottex 
|- { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } e. _V

Proof

Step Hyp Ref Expression
1 0ex 
 |-  (/) e. _V
2 eleq1 
 |-  ( A = (/) -> ( A e. _V <-> (/) e. _V ) )
3 1 2 mpbiri 
 |-  ( A = (/) -> A e. _V )
4 rabexg 
 |-  ( A e. _V -> { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } e. _V )
5 3 4 syl 
 |-  ( A = (/) -> { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } e. _V )
6 neq0 
 |-  ( -. A = (/) <-> E. y y e. A )
7 nfra1 
 |-  F/ y A. y e. A ( rank ` x ) C_ ( rank ` y )
8 nfcv 
 |-  F/_ y A
9 7 8 nfrabw 
 |-  F/_ y { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) }
10 9 nfel1 
 |-  F/ y { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } e. _V
11 rsp 
 |-  ( A. y e. A ( rank ` x ) C_ ( rank ` y ) -> ( y e. A -> ( rank ` x ) C_ ( rank ` y ) ) )
12 11 com12 
 |-  ( y e. A -> ( A. y e. A ( rank ` x ) C_ ( rank ` y ) -> ( rank ` x ) C_ ( rank ` y ) ) )
13 12 ralrimivw 
 |-  ( y e. A -> A. x e. A ( A. y e. A ( rank ` x ) C_ ( rank ` y ) -> ( rank ` x ) C_ ( rank ` y ) ) )
14 ss2rab 
 |-  ( { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } C_ { x e. A | ( rank ` x ) C_ ( rank ` y ) } <-> A. x e. A ( A. y e. A ( rank ` x ) C_ ( rank ` y ) -> ( rank ` x ) C_ ( rank ` y ) ) )
15 13 14 sylibr 
 |-  ( y e. A -> { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } C_ { x e. A | ( rank ` x ) C_ ( rank ` y ) } )
16 rankon 
 |-  ( rank ` y ) e. On
17 fveq2 
 |-  ( x = w -> ( rank ` x ) = ( rank ` w ) )
18 17 sseq1d 
 |-  ( x = w -> ( ( rank ` x ) C_ ( rank ` y ) <-> ( rank ` w ) C_ ( rank ` y ) ) )
19 18 elrab 
 |-  ( w e. { x e. A | ( rank ` x ) C_ ( rank ` y ) } <-> ( w e. A /\ ( rank ` w ) C_ ( rank ` y ) ) )
20 19 simprbi 
 |-  ( w e. { x e. A | ( rank ` x ) C_ ( rank ` y ) } -> ( rank ` w ) C_ ( rank ` y ) )
21 20 rgen 
 |-  A. w e. { x e. A | ( rank ` x ) C_ ( rank ` y ) } ( rank ` w ) C_ ( rank ` y )
22 sseq2 
 |-  ( z = ( rank ` y ) -> ( ( rank ` w ) C_ z <-> ( rank ` w ) C_ ( rank ` y ) ) )
23 22 ralbidv 
 |-  ( z = ( rank ` y ) -> ( A. w e. { x e. A | ( rank ` x ) C_ ( rank ` y ) } ( rank ` w ) C_ z <-> A. w e. { x e. A | ( rank ` x ) C_ ( rank ` y ) } ( rank ` w ) C_ ( rank ` y ) ) )
24 23 rspcev 
 |-  ( ( ( rank ` y ) e. On /\ A. w e. { x e. A | ( rank ` x ) C_ ( rank ` y ) } ( rank ` w ) C_ ( rank ` y ) ) -> E. z e. On A. w e. { x e. A | ( rank ` x ) C_ ( rank ` y ) } ( rank ` w ) C_ z )
25 16 21 24 mp2an 
 |-  E. z e. On A. w e. { x e. A | ( rank ` x ) C_ ( rank ` y ) } ( rank ` w ) C_ z
26 bndrank 
 |-  ( E. z e. On A. w e. { x e. A | ( rank ` x ) C_ ( rank ` y ) } ( rank ` w ) C_ z -> { x e. A | ( rank ` x ) C_ ( rank ` y ) } e. _V )
27 25 26 ax-mp 
 |-  { x e. A | ( rank ` x ) C_ ( rank ` y ) } e. _V
28 27 ssex 
 |-  ( { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } C_ { x e. A | ( rank ` x ) C_ ( rank ` y ) } -> { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } e. _V )
29 15 28 syl 
 |-  ( y e. A -> { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } e. _V )
30 10 29 exlimi 
 |-  ( E. y y e. A -> { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } e. _V )
31 6 30 sylbi 
 |-  ( -. A = (/) -> { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } e. _V )
32 5 31 pm2.61i 
 |-  { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } e. _V