Theorem cutbday

Description: The birthday of the surreal cut is equal to the minimum birthday in the gap. (Contributed by Scott Fenton, 8-Dec-2021)

	Ref	Expression
Assertion	cutbday	⊢ ( 𝐴 <<s 𝐵 → ( bday ‘ ( 𝐴 |s 𝐵 ) ) = ∩ ( bday “ { 𝑥 ∈ No ∣ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) } ) )

Proof

Step	Hyp	Ref	Expression
1		cutsval	⊢ ( 𝐴 <<s 𝐵 → ( 𝐴 |s 𝐵 ) = ( ℩ 𝑦 ∈ { 𝑥 ∈ No ∣ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) } ( bday ‘ 𝑦 ) = ∩ ( bday “ { 𝑥 ∈ No ∣ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) } ) ) )
2	1	eqcomd	⊢ ( 𝐴 <<s 𝐵 → ( ℩ 𝑦 ∈ { 𝑥 ∈ No ∣ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) } ( bday ‘ 𝑦 ) = ∩ ( bday “ { 𝑥 ∈ No ∣ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) } ) ) = ( 𝐴 |s 𝐵 ) )
3		cutcuts	⊢ ( 𝐴 <<s 𝐵 → ( ( 𝐴 |s 𝐵 ) ∈ No ∧ 𝐴 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐵 ) )
4		sneq	⊢ ( 𝑥 = ( 𝐴 |s 𝐵 ) → { 𝑥 } = { ( 𝐴 |s 𝐵 ) } )
5	4	breq2d	⊢ ( 𝑥 = ( 𝐴 |s 𝐵 ) → ( 𝐴 <<s { 𝑥 } ↔ 𝐴 <<s { ( 𝐴 |s 𝐵 ) } ) )
6	4	breq1d	⊢ ( 𝑥 = ( 𝐴 |s 𝐵 ) → ( { 𝑥 } <<s 𝐵 ↔ { ( 𝐴 |s 𝐵 ) } <<s 𝐵 ) )
7	5 6	anbi12d	⊢ ( 𝑥 = ( 𝐴 |s 𝐵 ) → ( ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) ↔ ( 𝐴 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐵 ) ) )
8	7	elrab	⊢ ( ( 𝐴 |s 𝐵 ) ∈ { 𝑥 ∈ No ∣ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) } ↔ ( ( 𝐴 |s 𝐵 ) ∈ No ∧ ( 𝐴 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐵 ) ) )
9		3anass	⊢ ( ( ( 𝐴 |s 𝐵 ) ∈ No ∧ 𝐴 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐵 ) ↔ ( ( 𝐴 |s 𝐵 ) ∈ No ∧ ( 𝐴 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐵 ) ) )
10	8 9	bitr4i	⊢ ( ( 𝐴 |s 𝐵 ) ∈ { 𝑥 ∈ No ∣ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) } ↔ ( ( 𝐴 |s 𝐵 ) ∈ No ∧ 𝐴 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐵 ) )
11	3 10	sylibr	⊢ ( 𝐴 <<s 𝐵 → ( 𝐴 |s 𝐵 ) ∈ { 𝑥 ∈ No ∣ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) } )
12		conway	⊢ ( 𝐴 <<s 𝐵 → ∃! 𝑦 ∈ { 𝑥 ∈ No ∣ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) } ( bday ‘ 𝑦 ) = ∩ ( bday “ { 𝑥 ∈ No ∣ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) } ) )
13		fveqeq2	⊢ ( 𝑦 = ( 𝐴 |s 𝐵 ) → ( ( bday ‘ 𝑦 ) = ∩ ( bday “ { 𝑥 ∈ No ∣ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) } ) ↔ ( bday ‘ ( 𝐴 |s 𝐵 ) ) = ∩ ( bday “ { 𝑥 ∈ No ∣ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) } ) ) )
14	13	riota2	⊢ ( ( ( 𝐴 |s 𝐵 ) ∈ { 𝑥 ∈ No ∣ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) } ∧ ∃! 𝑦 ∈ { 𝑥 ∈ No ∣ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) } ( bday ‘ 𝑦 ) = ∩ ( bday “ { 𝑥 ∈ No ∣ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) } ) ) → ( ( bday ‘ ( 𝐴 |s 𝐵 ) ) = ∩ ( bday “ { 𝑥 ∈ No ∣ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) } ) ↔ ( ℩ 𝑦 ∈ { 𝑥 ∈ No ∣ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) } ( bday ‘ 𝑦 ) = ∩ ( bday “ { 𝑥 ∈ No ∣ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) } ) ) = ( 𝐴 |s 𝐵 ) ) )
15	11 12 14	syl2anc	⊢ ( 𝐴 <<s 𝐵 → ( ( bday ‘ ( 𝐴 |s 𝐵 ) ) = ∩ ( bday “ { 𝑥 ∈ No ∣ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) } ) ↔ ( ℩ 𝑦 ∈ { 𝑥 ∈ No ∣ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) } ( bday ‘ 𝑦 ) = ∩ ( bday “ { 𝑥 ∈ No ∣ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) } ) ) = ( 𝐴 |s 𝐵 ) ) )
16	2 15	mpbird	⊢ ( 𝐴 <<s 𝐵 → ( bday ‘ ( 𝐴 |s 𝐵 ) ) = ∩ ( bday “ { 𝑥 ∈ No ∣ ( 𝐴 <<s { 𝑥 } ∧ { 𝑥 } <<s 𝐵 ) } ) )