Metamath Proof Explorer

Theorem bday0b

Description: The only surreal with birthday (/) is 0s . (Contributed by Scott Fenton, 8-Aug-2024)

Ref Expression
Assertion bday0b 
|- ( X e. No -> ( ( bday ` X ) = (/) <-> X = 0s ) )

Proof

Step Hyp Ref Expression
1 df-0s 
 |-  0s = ( (/) |s (/) )
2 snelpwi 
 |-  ( X e. No -> { X } e. ~P No )
3 nulsslt 
 |-  ( { X } e. ~P No -> (/) <
4 2 3 syl 
 |-  ( X e. No -> (/) <
5 4 adantr 
 |-  ( ( X e. No /\ ( bday ` X ) = (/) ) -> (/) <
6 nulssgt 
 |-  ( { X } e. ~P No -> { X } <
7 2 6 syl 
 |-  ( X e. No -> { X } <
8 7 adantr 
 |-  ( ( X e. No /\ ( bday ` X ) = (/) ) -> { X } <
9 id 
 |-  ( ( bday ` X ) = (/) -> ( bday ` X ) = (/) )
10 0ss 
 |-  (/) C_ ( bday ` x )
11 9 10 eqsstrdi 
 |-  ( ( bday ` X ) = (/) -> ( bday ` X ) C_ ( bday ` x ) )
12 11 a1d 
 |-  ( ( bday ` X ) = (/) -> ( ( (/) < ( bday ` X ) C_ ( bday ` x ) ) )
13 12 adantl 
 |-  ( ( X e. No /\ ( bday ` X ) = (/) ) -> ( ( (/) < ( bday ` X ) C_ ( bday ` x ) ) )
14 13 ralrimivw 
 |-  ( ( X e. No /\ ( bday ` X ) = (/) ) -> A. x e. No ( ( (/) < ( bday ` X ) C_ ( bday ` x ) ) )
15 0elpw 
 |-  (/) e. ~P No
16 nulssgt 
 |-  ( (/) e. ~P No -> (/) <
17 15 16 ax-mp 
 |-  (/) <
18 eqscut2 
 |-  ( ( (/) < ( ( (/) |s (/) ) = X <-> ( (/) < ( bday ` X ) C_ ( bday ` x ) ) ) ) )
19 17 18 mpan 
 |-  ( X e. No -> ( ( (/) |s (/) ) = X <-> ( (/) < ( bday ` X ) C_ ( bday ` x ) ) ) ) )
20 19 adantr 
 |-  ( ( X e. No /\ ( bday ` X ) = (/) ) -> ( ( (/) |s (/) ) = X <-> ( (/) < ( bday ` X ) C_ ( bday ` x ) ) ) ) )
21 5 8 14 20 mpbir3and 
 |-  ( ( X e. No /\ ( bday ` X ) = (/) ) -> ( (/) |s (/) ) = X )
22 1 21 eqtr2id 
 |-  ( ( X e. No /\ ( bday ` X ) = (/) ) -> X = 0s )
23 22 ex 
 |-  ( X e. No -> ( ( bday ` X ) = (/) -> X = 0s ) )
24 fveq2 
 |-  ( X = 0s -> ( bday ` X ) = ( bday ` 0s ) )
25 bday0s 
 |-  ( bday ` 0s ) = (/)
26 24 25 eqtrdi 
 |-  ( X = 0s -> ( bday ` X ) = (/) )
27 23 26 impbid1 
 |-  ( X e. No -> ( ( bday ` X ) = (/) <-> X = 0s ) )