Metamath Proof Explorer


Theorem bday0b

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

Ref Expression
Assertion bday0b Could not format assertion : No typesetting found for |- ( X e. No -> ( ( bday ` X ) = (/) <-> X = 0s ) ) with typecode |-

Proof

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