Theorem bday1

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

	Ref	Expression
Assertion	bday1	⊢ ( bday ‘ 1s ) = 1o

Proof

Step	Hyp	Ref	Expression
1		df-1s	⊢ 1s = ( { 0s } |s ∅ )
2	1	fveq2i	⊢ ( bday ‘ 1s ) = ( bday ‘ ( { 0s } |s ∅ ) )
3		0no	⊢ 0s ∈ No
4		snelpwi	⊢ ( 0s ∈ No → { 0s } ∈ 𝒫 No )
5	3 4	ax-mp	⊢ { 0s } ∈ 𝒫 No
6		nulsgts	⊢ ( { 0s } ∈ 𝒫 No → { 0s } <<s ∅ )
7	5 6	ax-mp	⊢ { 0s } <<s ∅
8		cutbdaybnd2	⊢ ( { 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		bday0	⊢ ( 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		ltsirr	⊢ ( 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	imbitrrid	⊢ ( 𝑦 ∈ No → ( 0s <s 𝑦 → ( bday ‘ 𝑦 ) ≠ ∅ ) )
43		bdayon	⊢ ( 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	imbitrrdi	⊢ ( 𝑦 ∈ No → ( 0s <s 𝑦 → 1o ⊆ ( bday ‘ 𝑦 ) ) )
48		sltssep	⊢ ( { 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		cutbday	⊢ ( { 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