Metamath Proof Explorer

Theorem bday1s

Description: The birthday of surreal one is ordinal one. (Contributed by Scott Fenton, 8-Aug-2024)

Ref Expression
Assertion bday1s ( bday ‘ 1s ) = 1o

Proof

Step Hyp Ref Expression
1 df-1s ⊢ 1s = ( { 0s } |s ∅ )
2 1 fveq2i ⊢ ( bday ‘ 1s ) = ( bday ‘ ( { 0s } |s ∅ ) )
3 0sno ⊢ 0s ∈ No
4 snelpwi ⊢ ( 0s ∈ No → { 0s } ∈ 𝒫 No )
5 3 4 ax-mp ⊢ { 0s } ∈ 𝒫 No
6 nulssgt ⊢ ( { 0s } ∈ 𝒫 No → { 0s } <<s ∅ )
7 5 6 ax-mp ⊢ { 0s } <<s ∅
8 scutbdaybnd2 ⊢ ( { 0s } <<s ∅ → ( bday ‘ ( { 0s } |s ∅ ) ) ⊆ suc ∪ ( bday “ ( { 0s } ∪ ∅ ) ) )
9 7 8 ax-mp ⊢ ( bday ‘ ( { 0s } |s ∅ ) ) ⊆ suc ∪ ( bday “ ( { 0s } ∪ ∅ ) )
10 un0 ⊢ ( { 0s } ∪ ∅ ) = { 0s }
11 10 imaeq2i ⊢ ( bday “ ( { 0s } ∪ ∅ ) ) = ( bday “ { 0s } )
12 bdayfn ⊢ bday Fn No
13 fnsnfv ⊢ ( ( bday Fn No ∧ 0s ∈ No ) → { ( bday ‘ 0s ) } = ( bday “ { 0s } ) )
14 12 3 13 mp2an ⊢ { ( bday ‘ 0s ) } = ( bday “ { 0s } )
15 bday0s ⊢ ( bday ‘ 0s ) = ∅
16 15 sneqi ⊢ { ( bday ‘ 0s ) } = { ∅ }
17 11 14 16 3eqtr2i ⊢ ( bday “ ( { 0s } ∪ ∅ ) ) = { ∅ }
18 17 unieqi ⊢ ∪ ( bday “ ( { 0s } ∪ ∅ ) ) = ∪ { ∅ }
19 0ex ⊢ ∅ ∈ V
20 19 unisn ⊢ ∪ { ∅ } = ∅
21 18 20 eqtri ⊢ ∪ ( bday “ ( { 0s } ∪ ∅ ) ) = ∅
22 suceq ⊢ ( ∪ ( bday “ ( { 0s } ∪ ∅ ) ) = ∅ → suc ∪ ( bday “ ( { 0s } ∪ ∅ ) ) = suc ∅ )
23 21 22 ax-mp ⊢ suc ∪ ( bday “ ( { 0s } ∪ ∅ ) ) = suc ∅
24 df-1o ⊢ 1o = suc ∅
25 23 24 eqtr4i ⊢ suc ∪ ( bday “ ( { 0s } ∪ ∅ ) ) = 1o
26 9 25 sseqtri ⊢ ( bday ‘ ( { 0s } |s ∅ ) ) ⊆ 1o
27 ssrab2 ⊢ { 𝑥 ∈ No ∣ ( { 0s } <<s { 𝑥 } ∧ { 𝑥 } <<s ∅ ) } ⊆ No
28 fnssintima ⊢ ( ( bday Fn No ∧ { 𝑥 ∈ No ∣ ( { 0s } <<s { 𝑥 } ∧ { 𝑥 } <<s ∅ ) } ⊆ No ) → ( 1o ⊆ ∩ ( bday “ { 𝑥 ∈ No ∣ ( { 0s } <<s { 𝑥 } ∧ { 𝑥 } <<s ∅ ) } ) ↔ ∀ 𝑦 ∈ { 𝑥 ∈ No ∣ ( { 0s } <<s { 𝑥 } ∧ { 𝑥 } <<s ∅ ) } 1o ⊆ ( bday ‘ 𝑦 ) ) )
29 12 27 28 mp2an ⊢ ( 1o ⊆ ∩ ( bday “ { 𝑥 ∈ No ∣ ( { 0s } <<s { 𝑥 } ∧ { 𝑥 } <<s ∅ ) } ) ↔ ∀ 𝑦 ∈ { 𝑥 ∈ No ∣ ( { 0s } <<s { 𝑥 } ∧ { 𝑥 } <<s ∅ ) } 1o ⊆ ( bday ‘ 𝑦 ) )
30 sneq ⊢ ( 𝑥 = 𝑦 → { 𝑥 } = { 𝑦 } )
31 30 breq2d ⊢ ( 𝑥 = 𝑦 → ( { 0s } <<s { 𝑥 } ↔ { 0s } <<s { 𝑦 } ) )
32 30 breq1d ⊢ ( 𝑥 = 𝑦 → ( { 𝑥 } <<s ∅ ↔ { 𝑦 } <<s ∅ ) )
33 31 32 anbi12d ⊢ ( 𝑥 = 𝑦 → ( ( { 0s } <<s { 𝑥 } ∧ { 𝑥 } <<s ∅ ) ↔ ( { 0s } <<s { 𝑦 } ∧ { 𝑦 } <<s ∅ ) ) )
34 33 elrab ⊢ ( 𝑦 ∈ { 𝑥 ∈ No ∣ ( { 0s } <<s { 𝑥 } ∧ { 𝑥 } <<s ∅ ) } ↔ ( 𝑦 ∈ No ∧ ( { 0s } <<s { 𝑦 } ∧ { 𝑦 } <<s ∅ ) ) )
35 sltirr ⊢ ( 0s ∈ No → ¬ 0s <s 0s )
36 3 35 ax-mp ⊢ ¬ 0s <s 0s
37 breq2 ⊢ ( 𝑦 = 0s → ( 0s <s 𝑦 ↔ 0s <s 0s ) )
38 36 37 mtbiri ⊢ ( 𝑦 = 0s → ¬ 0s <s 𝑦 )
39 38 necon2ai ⊢ ( 0s <s 𝑦 → 𝑦 ≠ 0s )
40 bday0b ⊢ ( 𝑦 ∈ No → ( ( bday ‘ 𝑦 ) = ∅ ↔ 𝑦 = 0s ) )
41 40 necon3bid ⊢ ( 𝑦 ∈ No → ( ( bday ‘ 𝑦 ) ≠ ∅ ↔ 𝑦 ≠ 0s ) )
42 39 41 syl5ibr ⊢ ( 𝑦 ∈ No → ( 0s <s 𝑦 → ( bday ‘ 𝑦 ) ≠ ∅ ) )
43 bdayelon ⊢ ( bday ‘ 𝑦 ) ∈ On
44 43 onordi ⊢ Ord ( bday ‘ 𝑦 )
45 ordge1n0 ⊢ ( Ord ( bday ‘ 𝑦 ) → ( 1o ⊆ ( bday ‘ 𝑦 ) ↔ ( bday ‘ 𝑦 ) ≠ ∅ ) )
46 44 45 ax-mp ⊢ ( 1o ⊆ ( bday ‘ 𝑦 ) ↔ ( bday ‘ 𝑦 ) ≠ ∅ )
47 42 46 syl6ibr ⊢ ( 𝑦 ∈ No → ( 0s <s 𝑦 → 1o ⊆ ( bday ‘ 𝑦 ) ) )
48 ssltsep ⊢ ( { 0s } <<s { 𝑦 } → ∀ 𝑥 ∈ { 0s } ∀ 𝑧 ∈ { 𝑦 } 𝑥 <s 𝑧 )
49 vex ⊢ 𝑦 ∈ V
50 breq2 ⊢ ( 𝑧 = 𝑦 → ( 𝑥 <s 𝑧 ↔ 𝑥 <s 𝑦 ) )
51 49 50 ralsn ⊢ ( ∀ 𝑧 ∈ { 𝑦 } 𝑥 <s 𝑧 ↔ 𝑥 <s 𝑦 )
52 51 ralbii ⊢ ( ∀ 𝑥 ∈ { 0s } ∀ 𝑧 ∈ { 𝑦 } 𝑥 <s 𝑧 ↔ ∀ 𝑥 ∈ { 0s } 𝑥 <s 𝑦 )
53 3 elexi ⊢ 0s ∈ V
54 breq1 ⊢ ( 𝑥 = 0s → ( 𝑥 <s 𝑦 ↔ 0s <s 𝑦 ) )
55 53 54 ralsn ⊢ ( ∀ 𝑥 ∈ { 0s } 𝑥 <s 𝑦 ↔ 0s <s 𝑦 )
56 52 55 bitri ⊢ ( ∀ 𝑥 ∈ { 0s } ∀ 𝑧 ∈ { 𝑦 } 𝑥 <s 𝑧 ↔ 0s <s 𝑦 )
57 48 56 sylib ⊢ ( { 0s } <<s { 𝑦 } → 0s <s 𝑦 )
58 47 57 impel ⊢ ( ( 𝑦 ∈ No ∧ { 0s } <<s { 𝑦 } ) → 1o ⊆ ( bday ‘ 𝑦 ) )
59 58 adantrr ⊢ ( ( 𝑦 ∈ No ∧ ( { 0s } <<s { 𝑦 } ∧ { 𝑦 } <<s ∅ ) ) → 1o ⊆ ( bday ‘ 𝑦 ) )
60 34 59 sylbi ⊢ ( 𝑦 ∈ { 𝑥 ∈ No ∣ ( { 0s } <<s { 𝑥 } ∧ { 𝑥 } <<s ∅ ) } → 1o ⊆ ( bday ‘ 𝑦 ) )
61 29 60 mprgbir ⊢ 1o ⊆ ∩ ( bday “ { 𝑥 ∈ No ∣ ( { 0s } <<s { 𝑥 } ∧ { 𝑥 } <<s ∅ ) } )
62 scutbday ⊢ ( { 0s } <<s ∅ → ( bday ‘ ( { 0s } |s ∅ ) ) = ∩ ( bday “ { 𝑥 ∈ No ∣ ( { 0s } <<s { 𝑥 } ∧ { 𝑥 } <<s ∅ ) } ) )
63 7 62 ax-mp ⊢ ( bday ‘ ( { 0s } |s ∅ ) ) = ∩ ( bday “ { 𝑥 ∈ No ∣ ( { 0s } <<s { 𝑥 } ∧ { 𝑥 } <<s ∅ ) } )
64 61 63 sseqtrri ⊢ 1o ⊆ ( bday ‘ ( { 0s } |s ∅ ) )
65 26 64 eqssi ⊢ ( bday ‘ ( { 0s } |s ∅ ) ) = 1o
66 2 65 eqtri ⊢ ( bday ‘ 1s ) = 1o