Metamath Proof Explorer

Theorem 0elscott

Description: If the empty set is an element of the input class, then the Scott's trick set is the singleton of the empty set. (Contributed by BTernaryTau, 23-Aug-2026)

Ref Expression
Assertion 0elscott 
|- ( (/) e. A -> Scott A = { (/) } )

Proof

Step Hyp Ref Expression
1 fveq2 
 |-  ( y = (/) -> ( rank ` y ) = ( rank ` (/) ) )
2 1 sseq2d 
 |-  ( y = (/) -> ( ( rank ` x ) C_ ( rank ` y ) <-> ( rank ` x ) C_ ( rank ` (/) ) ) )
3 ss0b 
 |-  ( ( rank ` x ) C_ (/) <-> ( rank ` x ) = (/) )
4 0elon 
 |-  (/) e. On
5 onrankid 
 |-  ( (/) e. On <-> ( rank ` (/) ) = (/) )
6 4 5 mpbi 
 |-  ( rank ` (/) ) = (/)
7 6 sseq2i 
 |-  ( ( rank ` x ) C_ ( rank ` (/) ) <-> ( rank ` x ) C_ (/) )
8 vex 
 |-  x e. _V
9 8 rankeq0 
 |-  ( x = (/) <-> ( rank ` x ) = (/) )
10 3 7 9 3bitr4i 
 |-  ( ( rank ` x ) C_ ( rank ` (/) ) <-> x = (/) )
11 2 10 bitrdi 
 |-  ( y = (/) -> ( ( rank ` x ) C_ ( rank ` y ) <-> x = (/) ) )
12 11 rspcv 
 |-  ( (/) e. A -> ( A. y e. A ( rank ` x ) C_ ( rank ` y ) -> x = (/) ) )
13 12 ralrimivw 
 |-  ( (/) e. A -> A. x e. A ( A. y e. A ( rank ` x ) C_ ( rank ` y ) -> x = (/) ) )
14 df-scott 
 |-  Scott A = { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) }
15 14 sseq1i 
 |-  ( Scott A C_ { (/) } <-> { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } C_ { (/) } )
16 rabsssn 
 |-  ( { x e. A | A. y e. A ( rank ` x ) C_ ( rank ` y ) } C_ { (/) } <-> A. x e. A ( A. y e. A ( rank ` x ) C_ ( rank ` y ) -> x = (/) ) )
17 15 16 bitri 
 |-  ( Scott A C_ { (/) } <-> A. x e. A ( A. y e. A ( rank ` x ) C_ ( rank ` y ) -> x = (/) ) )
18 13 17 sylibr 
 |-  ( (/) e. A -> Scott A C_ { (/) } )
19 sssn 
 |-  ( Scott A C_ { (/) } <-> ( Scott A = (/) \/ Scott A = { (/) } ) )
20 18 19 sylib 
 |-  ( (/) e. A -> ( Scott A = (/) \/ Scott A = { (/) } ) )
21 elscottn0 
 |-  ( (/) e. A -> Scott A =/= (/) )
22 21 neneqd 
 |-  ( (/) e. A -> -. Scott A = (/) )
23 20 22 orcnd 
 |-  ( (/) e. A -> Scott A = { (/) } )