Theorem cutbdaybnd

Description: An upper bound on the birthday of a surreal cut. (Contributed by Scott Fenton, 10-Aug-2024)

	Ref	Expression
Assertion	cutbdaybnd	⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ 𝑂 )

Proof

Step	Hyp	Ref	Expression
1		etaslts	⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) → ∃ 𝑥 ∈ No ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday ‘ 𝑥 ) ⊆ 𝑂 ) )
2		simpl1	⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) ∧ ( 𝑥 ∈ No ∧ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday ‘ 𝑥 ) ⊆ 𝑂 ) ) ) → 𝐴 <<s 𝐵 )
3		cutbday	⊢ ( 𝐴 <<s 𝐵 → ( bday ‘ ( 𝐴 |s 𝐵 ) ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) )
4	2 3	syl	⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) ∧ ( 𝑥 ∈ No ∧ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday ‘ 𝑥 ) ⊆ 𝑂 ) ) ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) )
5		bdayfn	⊢ bday Fn No
6		ssrab2	⊢ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ⊆ No
7		sneq	⊢ ( 𝑦 = 𝑥 → { 𝑦 } = { 𝑥 } )
8	7	breq2d	⊢ ( 𝑦 = 𝑥 → ( 𝐴 <<s { 𝑦 } ↔ 𝐴 <<s { 𝑥 } ) )
9	7	breq1d	⊢ ( 𝑦 = 𝑥 → ( { 𝑦 } <<s 𝐵 ↔ { 𝑥 } <<s 𝐵 ) )
10	8 9	anbi12d	⊢ ( 𝑦 = 𝑥 → ( ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) ↔ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) ) )
11		simprl	⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) ∧ ( 𝑥 ∈ No ∧ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday ‘ 𝑥 ) ⊆ 𝑂 ) ) ) → 𝑥 ∈ No )
12		simprr1	⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) ∧ ( 𝑥 ∈ No ∧ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday ‘ 𝑥 ) ⊆ 𝑂 ) ) ) → 𝐴 <<s { 𝑥 } )
13		simprr2	⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) ∧ ( 𝑥 ∈ No ∧ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday ‘ 𝑥 ) ⊆ 𝑂 ) ) ) → { 𝑥 } <<s 𝐵 )
14	12 13	jca	⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) ∧ ( 𝑥 ∈ No ∧ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday ‘ 𝑥 ) ⊆ 𝑂 ) ) ) → ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) )
15	10 11 14	elrabd	⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) ∧ ( 𝑥 ∈ No ∧ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday ‘ 𝑥 ) ⊆ 𝑂 ) ) ) → 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } )
16		fnfvima	⊢ ( ( bday Fn No ∧ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ⊆ No ∧ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) → ( bday ‘ 𝑥 ) ∈ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) )
17	5 6 15 16	mp3an12i	⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) ∧ ( 𝑥 ∈ No ∧ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday ‘ 𝑥 ) ⊆ 𝑂 ) ) ) → ( bday ‘ 𝑥 ) ∈ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) )
18		intss1	⊢ ( ( bday ‘ 𝑥 ) ∈ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) → ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ⊆ ( bday ‘ 𝑥 ) )
19	17 18	syl	⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) ∧ ( 𝑥 ∈ No ∧ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday ‘ 𝑥 ) ⊆ 𝑂 ) ) ) → ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ⊆ ( bday ‘ 𝑥 ) )
20	4 19	eqsstrd	⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) ∧ ( 𝑥 ∈ No ∧ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday ‘ 𝑥 ) ⊆ 𝑂 ) ) ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ ( bday ‘ 𝑥 ) )
21		simprr3	⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) ∧ ( 𝑥 ∈ No ∧ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday ‘ 𝑥 ) ⊆ 𝑂 ) ) ) → ( bday ‘ 𝑥 ) ⊆ 𝑂 )
22	20 21	sstrd	⊢ ( ( ( 𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) ∧ ( 𝑥 ∈ No ∧ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ∧ ( bday ‘ 𝑥 ) ⊆ 𝑂 ) ) ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ 𝑂 )
23	1 22	rexlimddv	⊢ ( ( 𝐴 <<s 𝐵 ∧ 𝑂 ∈ On ∧ ( bday “ ( 𝐴 ∪ 𝐵 ) ) ⊆ 𝑂 ) → ( bday ‘ ( 𝐴 |s 𝐵 ) ) ⊆ 𝑂 )