Metamath Proof Explorer

Theorem scottex

Description: Scott's trick produces a set. (Contributed by NM, 13-Oct-2003) Use the Scott operation. (Revised by BTernaryTau, 18-Jul-2026)

Ref Expression
Assertion scottex 
|- Scott A e. _V

Proof

Step Hyp Ref Expression
1 df-scott 
 |-  Scott A = { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) }
2 0ex 
 |-  (/) e. _V
3 eleq1 
 |-  ( A = (/) -> ( A e. _V <-> (/) e. _V ) )
4 2 3 mpbiri 
 |-  ( A = (/) -> A e. _V )
5 rabexg 
 |-  ( A e. _V -> { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } e. _V )
6 4 5 syl 
 |-  ( A = (/) -> { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } e. _V )
7 neq0 
 |-  ( -. A = (/) <-> E. v v e. A )
8 fveq2 
 |-  ( y = v -> ( rank ` y ) = ( rank ` v ) )
9 8 sseq2d 
 |-  ( y = v -> ( ( rank ` x ) C_ ( rank ` y ) <-> ( rank ` x ) C_ ( rank ` v ) ) )
10 9 rspcv 
 |-  ( v e. A -> ( A. y e. A ( rank ` x ) C_ ( rank ` y ) -> ( rank ` x ) C_ ( rank ` v ) ) )
11 10 adantr 
 |-  ( ( v e. A /\ x e. A ) -> ( A. y e. A ( rank ` x ) C_ ( rank ` y ) -> ( rank ` x ) C_ ( rank ` v ) ) )
12 11 ss2rabdv 
 |-  ( v e. A -> { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } C_ { x e. A | ( rank ` x ) C_ ( rank ` v ) } )
13 rankon 
 |-  ( rank ` v ) e. On
14 fveq2 
 |-  ( x = w -> ( rank ` x ) = ( rank ` w ) )
15 14 sseq1d 
 |-  ( x = w -> ( ( rank ` x ) C_ ( rank ` v ) <-> ( rank ` w ) C_ ( rank ` v ) ) )
16 15 elrab 
 |-  ( w e. { x e. A | ( rank ` x ) C_ ( rank ` v ) } <-> ( w e. A /\ ( rank ` w ) C_ ( rank ` v ) ) )
17 16 simprbi 
 |-  ( w e. { x e. A | ( rank ` x ) C_ ( rank ` v ) } -> ( rank ` w ) C_ ( rank ` v ) )
18 17 rgen 
 |-  A. w e. { x e. A | ( rank ` x ) C_ ( rank ` v ) } ( rank ` w ) C_ ( rank ` v )
19 sseq2 
 |-  ( z = ( rank ` v ) -> ( ( rank ` w ) C_ z <-> ( rank ` w ) C_ ( rank ` v ) ) )
20 19 ralbidv 
 |-  ( z = ( rank ` v ) -> ( A. w e. { x e. A | ( rank ` x ) C_ ( rank ` v ) } ( rank ` w ) C_ z <-> A. w e. { x e. A | ( rank ` x ) C_ ( rank ` v ) } ( rank ` w ) C_ ( rank ` v ) ) )
21 20 rspcev 
 |-  ( ( ( rank ` v ) e. On /\ A. w e. { x e. A | ( rank ` x ) C_ ( rank ` v ) } ( rank ` w ) C_ ( rank ` v ) ) -> E. z e. On A. w e. { x e. A | ( rank ` x ) C_ ( rank ` v ) } ( rank ` w ) C_ z )
22 13 18 21 mp2an 
 |-  E. z e. On A. w e. { x e. A | ( rank ` x ) C_ ( rank ` v ) } ( rank ` w ) C_ z
23 bndrank 
 |-  ( E. z e. On A. w e. { x e. A | ( rank ` x ) C_ ( rank ` v ) } ( rank ` w ) C_ z -> { x e. A | ( rank ` x ) C_ ( rank ` v ) } e. _V )
24 22 23 ax-mp 
 |-  { x e. A | ( rank ` x ) C_ ( rank ` v ) } e. _V
25 24 ssex 
 |-  ( { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } C_ { x e. A | ( rank ` x ) C_ ( rank ` v ) } -> { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } e. _V )
26 12 25 syl 
 |-  ( v e. A -> { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } e. _V )
27 26 exlimiv 
 |-  ( E. v v e. A -> { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } e. _V )
28 7 27 sylbi 
 |-  ( -. A = (/) -> { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } e. _V )
29 6 28 pm2.61i 
 |-  { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } e. _V
30 1 29 eqeltri 
 |-  Scott A e. _V