This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 adantr 
 |-  ( ( y e. A /\ x e. A ) -> ( A. y e. A ( rank ` x ) C_ ( rank ` y ) -> ( rank ` x ) C_ ( rank ` y ) ) )
14 13 ss2rabdv 
 |-  ( y e. A -> { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } C_ { x e. A | ( rank ` x ) C_ ( rank ` y ) } )
15 rankon 
 |-  ( rank ` y ) e. On
16 fveq2 
 |-  ( x = w -> ( rank ` x ) = ( rank ` w ) )
17 16 sseq1d 
 |-  ( x = w -> ( ( rank ` x ) C_ ( rank ` y ) <-> ( rank ` w ) C_ ( rank ` y ) ) )
18 17 elrab 
 |-  ( w e. { x e. A | ( rank ` x ) C_ ( rank ` y ) } <-> ( w e. A /\ ( rank ` w ) C_ ( rank ` y ) ) )
19 18 simprbi 
 |-  ( w e. { x e. A | ( rank ` x ) C_ ( rank ` y ) } -> ( rank ` w ) C_ ( rank ` y ) )
20 19 rgen 
 |-  A. w e. { x e. A | ( rank ` x ) C_ ( rank ` y ) } ( rank ` w ) C_ ( rank ` y )
21 sseq2 
 |-  ( z = ( rank ` y ) -> ( ( rank ` w ) C_ z <-> ( rank ` w ) C_ ( rank ` y ) ) )
22 21 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 ) ) )
23 22 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 )
24 15 20 23 mp2an 
 |-  E. z e. On A. w e. { x e. A | ( rank ` x ) C_ ( rank ` y ) } ( rank ` w ) C_ z
25 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 )
26 24 25 ax-mp 
 |-  { x e. A | ( rank ` x ) C_ ( rank ` y ) } e. _V
27 26 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 )
28 14 27 syl 
 |-  ( y e. A -> { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } e. _V )
29 10 28 exlimi 
 |-  ( E. y y e. A -> { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } e. _V )
30 6 29 sylbi 
 |-  ( -. A = (/) -> { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } e. _V )
31 5 30 pm2.61i 
 |-  { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } e. _V