Theorem ssltbday

Description: Birthday comparison rule for surreals. (Contributed by Scott Fenton, 23-Feb-2026)

	Ref	Expression
Hypotheses	ssltbday.1	⊢ ( 𝜑 → 𝐴 = ( 𝐿 |s 𝑅 ) )
	ssltbday.2	⊢ ( 𝜑 → 𝐵 ∈ No )
	ssltbday.3	⊢ ( 𝜑 → 𝐿 <<s { 𝐵 } )
	ssltbday.4	⊢ ( 𝜑 → { 𝐵 } <<s 𝑅 )
Assertion	ssltbday	⊢ ( 𝜑 → ( bday ‘ 𝐴 ) ⊆ ( bday ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		ssltbday.1	⊢ ( 𝜑 → 𝐴 = ( 𝐿 |s 𝑅 ) )
2		ssltbday.2	⊢ ( 𝜑 → 𝐵 ∈ No )
3		ssltbday.3	⊢ ( 𝜑 → 𝐿 <<s { 𝐵 } )
4		ssltbday.4	⊢ ( 𝜑 → { 𝐵 } <<s 𝑅 )
5	1	fveq2d	⊢ ( 𝜑 → ( bday ‘ 𝐴 ) = ( bday ‘ ( 𝐿 |s 𝑅 ) ) )
6	2	snn0d	⊢ ( 𝜑 → { 𝐵 } ≠ ∅ )
7		sslttr	⊢ ( ( 𝐿 <<s { 𝐵 } ∧ { 𝐵 } <<s 𝑅 ∧ { 𝐵 } ≠ ∅ ) → 𝐿 <<s 𝑅 )
8	3 4 6 7	syl3anc	⊢ ( 𝜑 → 𝐿 <<s 𝑅 )
9		scutbday	⊢ ( 𝐿 <<s 𝑅 → ( bday ‘ ( 𝐿 |s 𝑅 ) ) = ∩ ( bday “ { 𝑥 ∈ No ∣ ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) } ) )
10	8 9	syl	⊢ ( 𝜑 → ( bday ‘ ( 𝐿 |s 𝑅 ) ) = ∩ ( bday “ { 𝑥 ∈ No ∣ ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) } ) )
11		bdayfn	⊢ bday Fn No
12		ssrab2	⊢ { 𝑥 ∈ No ∣ ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) } ⊆ No
13		sneq	⊢ ( 𝑥 = 𝐵 → { 𝑥 } = { 𝐵 } )
14	13	breq2d	⊢ ( 𝑥 = 𝐵 → ( 𝐿 <<s { 𝑥 } ↔ 𝐿 <<s { 𝐵 } ) )
15	13	breq1d	⊢ ( 𝑥 = 𝐵 → ( { 𝑥 } <<s 𝑅 ↔ { 𝐵 } <<s 𝑅 ) )
16	14 15	anbi12d	⊢ ( 𝑥 = 𝐵 → ( ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) ↔ ( 𝐿 <<s { 𝐵 } ∧ { 𝐵 } <<s 𝑅 ) ) )
17	3 4	jca	⊢ ( 𝜑 → ( 𝐿 <<s { 𝐵 } ∧ { 𝐵 } <<s 𝑅 ) )
18	16 2 17	elrabd	⊢ ( 𝜑 → 𝐵 ∈ { 𝑥 ∈ No ∣ ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) } )
19		fnfvima	⊢ ( ( bday Fn No ∧ { 𝑥 ∈ No ∣ ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) } ⊆ No ∧ 𝐵 ∈ { 𝑥 ∈ No ∣ ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) } ) → ( bday ‘ 𝐵 ) ∈ ( bday “ { 𝑥 ∈ No ∣ ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) } ) )
20	11 12 18 19	mp3an12i	⊢ ( 𝜑 → ( bday ‘ 𝐵 ) ∈ ( bday “ { 𝑥 ∈ No ∣ ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) } ) )
21		intss1	⊢ ( ( bday ‘ 𝐵 ) ∈ ( bday “ { 𝑥 ∈ No ∣ ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) } ) → ∩ ( bday “ { 𝑥 ∈ No ∣ ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) } ) ⊆ ( bday ‘ 𝐵 ) )
22	20 21	syl	⊢ ( 𝜑 → ∩ ( bday “ { 𝑥 ∈ No ∣ ( 𝐿 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝑅 ) } ) ⊆ ( bday ‘ 𝐵 ) )
23	10 22	eqsstrd	⊢ ( 𝜑 → ( bday ‘ ( 𝐿 |s 𝑅 ) ) ⊆ ( bday ‘ 𝐵 ) )
24	5 23	eqsstrd	⊢ ( 𝜑 → ( bday ‘ 𝐴 ) ⊆ ( bday ‘ 𝐵 ) )