Theorem bday0s

Description: Calculate the birthday of surreal zero. (Contributed by Scott Fenton, 7-Aug-2024)

	Ref	Expression
Assertion	bday0s	⊢ ( bday ‘ 0s ) = ∅

Proof

Step	Hyp	Ref	Expression
1		df-0s	⊢ 0s = ( ∅ |s ∅ )
2	1	fveq2i	⊢ ( bday ‘ 0s ) = ( bday ‘ ( ∅ |s ∅ ) )
3		0elpw	⊢ ∅ ∈ 𝒫 No
4		nulssgt	⊢ ( ∅ ∈ 𝒫 No → ∅ <<s ∅ )
5		scutbday	⊢ ( ∅ <<s ∅ → ( bday ‘ ( ∅ |s ∅ ) ) = ∩ ( bday “ { 𝑥 ∈ No ∣ ( ∅ <<s { 𝑥 } ∧ { 𝑥 } <<s ∅ ) } ) )
6	3 4 5	mp2b	⊢ ( bday ‘ ( ∅ |s ∅ ) ) = ∩ ( bday “ { 𝑥 ∈ No ∣ ( ∅ <<s { 𝑥 } ∧ { 𝑥 } <<s ∅ ) } )
7	2 6	eqtri	⊢ ( bday ‘ 0s ) = ∩ ( bday “ { 𝑥 ∈ No ∣ ( ∅ <<s { 𝑥 } ∧ { 𝑥 } <<s ∅ ) } )
8		snelpwi	⊢ ( 𝑥 ∈ No → { 𝑥 } ∈ 𝒫 No )
9		nulsslt	⊢ ( { 𝑥 } ∈ 𝒫 No → ∅ <<s { 𝑥 } )
10		nulssgt	⊢ ( { 𝑥 } ∈ 𝒫 No → { 𝑥 } <<s ∅ )
11	9 10	jca	⊢ ( { 𝑥 } ∈ 𝒫 No → ( ∅ <<s { 𝑥 } ∧ { 𝑥 } <<s ∅ ) )
12	8 11	syl	⊢ ( 𝑥 ∈ No → ( ∅ <<s { 𝑥 } ∧ { 𝑥 } <<s ∅ ) )
13	12	rabeqc	⊢ { 𝑥 ∈ No ∣ ( ∅ <<s { 𝑥 } ∧ { 𝑥 } <<s ∅ ) } = No
14		bdaydm	⊢ dom bday = No
15	13 14	eqtr4i	⊢ { 𝑥 ∈ No ∣ ( ∅ <<s { 𝑥 } ∧ { 𝑥 } <<s ∅ ) } = dom bday
16	15	imaeq2i	⊢ ( bday “ { 𝑥 ∈ No ∣ ( ∅ <<s { 𝑥 } ∧ { 𝑥 } <<s ∅ ) } ) = ( bday “ dom bday )
17		imadmrn	⊢ ( bday “ dom bday ) = ran bday
18		bdayrn	⊢ ran bday = On
19	16 17 18	3eqtri	⊢ ( bday “ { 𝑥 ∈ No ∣ ( ∅ <<s { 𝑥 } ∧ { 𝑥 } <<s ∅ ) } ) = On
20	19	inteqi	⊢ ∩ ( bday “ { 𝑥 ∈ No ∣ ( ∅ <<s { 𝑥 } ∧ { 𝑥 } <<s ∅ ) } ) = ∩ On
21		inton	⊢ ∩ On = ∅
22	7 20 21	3eqtri	⊢ ( bday ‘ 0s ) = ∅