Theorem bday0b

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

	Ref	Expression
Assertion	bday0b	⊢ ( 𝑋 ∈ No → ( ( bday ‘ 𝑋 ) = ∅ ↔ 𝑋 = 0s ) )

Proof

Step	Hyp	Ref	Expression
1		df-0s	⊢ 0s = ( ∅ |s ∅ )
2		snelpwi	⊢ ( 𝑋 ∈ No → { 𝑋 } ∈ 𝒫 No )
3		nulsslt	⊢ ( { 𝑋 } ∈ 𝒫 No → ∅ <<s { 𝑋 } )
4	2 3	syl	⊢ ( 𝑋 ∈ No → ∅ <<s { 𝑋 } )
5	4	adantr	⊢ ( ( 𝑋 ∈ No ∧ ( bday ‘ 𝑋 ) = ∅ ) → ∅ <<s { 𝑋 } )
6		nulssgt	⊢ ( { 𝑋 } ∈ 𝒫 No → { 𝑋 } <<s ∅ )
7	2 6	syl	⊢ ( 𝑋 ∈ No → { 𝑋 } <<s ∅ )
8	7	adantr	⊢ ( ( 𝑋 ∈ No ∧ ( bday ‘ 𝑋 ) = ∅ ) → { 𝑋 } <<s ∅ )
9		id	⊢ ( ( bday ‘ 𝑋 ) = ∅ → ( bday ‘ 𝑋 ) = ∅ )
10		0ss	⊢ ∅ ⊆ ( bday ‘ 𝑥 )
11	9 10	eqsstrdi	⊢ ( ( bday ‘ 𝑋 ) = ∅ → ( bday ‘ 𝑋 ) ⊆ ( bday ‘ 𝑥 ) )
12	11	a1d	⊢ ( ( bday ‘ 𝑋 ) = ∅ → ( ( ∅ <<s { 𝑥 } ∧ { 𝑥 } <<s ∅ ) → ( bday ‘ 𝑋 ) ⊆ ( bday ‘ 𝑥 ) ) )
13	12	adantl	⊢ ( ( 𝑋 ∈ No ∧ ( bday ‘ 𝑋 ) = ∅ ) → ( ( ∅ <<s { 𝑥 } ∧ { 𝑥 } <<s ∅ ) → ( bday ‘ 𝑋 ) ⊆ ( bday ‘ 𝑥 ) ) )
14	13	ralrimivw	⊢ ( ( 𝑋 ∈ No ∧ ( bday ‘ 𝑋 ) = ∅ ) → ∀ 𝑥 ∈ No ( ( ∅ <<s { 𝑥 } ∧ { 𝑥 } <<s ∅ ) → ( bday ‘ 𝑋 ) ⊆ ( bday ‘ 𝑥 ) ) )
15		0elpw	⊢ ∅ ∈ 𝒫 No
16		nulssgt	⊢ ( ∅ ∈ 𝒫 No → ∅ <<s ∅ )
17	15 16	ax-mp	⊢ ∅ <<s ∅
18		eqscut2	⊢ ( ( ∅ <<s ∅ ∧ 𝑋 ∈ No ) → ( ( ∅ |s ∅ ) = 𝑋 ↔ ( ∅ <<s { 𝑋 } ∧ { 𝑋 } <<s ∅ ∧ ∀ 𝑥 ∈ No ( ( ∅ <<s { 𝑥 } ∧ { 𝑥 } <<s ∅ ) → ( bday ‘ 𝑋 ) ⊆ ( bday ‘ 𝑥 ) ) ) ) )
19	17 18	mpan	⊢ ( 𝑋 ∈ No → ( ( ∅ |s ∅ ) = 𝑋 ↔ ( ∅ <<s { 𝑋 } ∧ { 𝑋 } <<s ∅ ∧ ∀ 𝑥 ∈ No ( ( ∅ <<s { 𝑥 } ∧ { 𝑥 } <<s ∅ ) → ( bday ‘ 𝑋 ) ⊆ ( bday ‘ 𝑥 ) ) ) ) )
20	19	adantr	⊢ ( ( 𝑋 ∈ No ∧ ( bday ‘ 𝑋 ) = ∅ ) → ( ( ∅ |s ∅ ) = 𝑋 ↔ ( ∅ <<s { 𝑋 } ∧ { 𝑋 } <<s ∅ ∧ ∀ 𝑥 ∈ No ( ( ∅ <<s { 𝑥 } ∧ { 𝑥 } <<s ∅ ) → ( bday ‘ 𝑋 ) ⊆ ( bday ‘ 𝑥 ) ) ) ) )
21	5 8 14 20	mpbir3and	⊢ ( ( 𝑋 ∈ No ∧ ( bday ‘ 𝑋 ) = ∅ ) → ( ∅ |s ∅ ) = 𝑋 )
22	1 21	syl5req	⊢ ( ( 𝑋 ∈ No ∧ ( bday ‘ 𝑋 ) = ∅ ) → 𝑋 = 0s )
23	22	ex	⊢ ( 𝑋 ∈ No → ( ( bday ‘ 𝑋 ) = ∅ → 𝑋 = 0s ) )
24		fveq2	⊢ ( 𝑋 = 0s → ( bday ‘ 𝑋 ) = ( bday ‘ 0s ) )
25		bday0s	⊢ ( bday ‘ 0s ) = ∅
26	24 25	eqtrdi	⊢ ( 𝑋 = 0s → ( bday ‘ 𝑋 ) = ∅ )
27	23 26	impbid1	⊢ ( 𝑋 ∈ No → ( ( bday ‘ 𝑋 ) = ∅ ↔ 𝑋 = 0s ) )