Theorem scutcut

Description: Cut properties of the surreal cut operation. (Contributed by Scott Fenton, 8-Dec-2021)

	Ref	Expression
Assertion	scutcut	⊢ ( 𝐴 <<s 𝐵 → ( ( 𝐴 |s 𝐵 ) ∈ No ∧ 𝐴 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		scutval	⊢ ( 𝐴 <<s 𝐵 → ( 𝐴 |s 𝐵 ) = ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) )
2		conway	⊢ ( 𝐴 <<s 𝐵 → ∃! 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) )
3		riotacl	⊢ ( ∃! 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) → ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } )
4	2 3	syl	⊢ ( 𝐴 <<s 𝐵 → ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ) ) ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } )
5	1 4	eqeltrd	⊢ ( 𝐴 <<s 𝐵 → ( 𝐴 |s 𝐵 ) ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } )
6		sneq	⊢ ( 𝑦 = ( 𝐴 |s 𝐵 ) → { 𝑦 } = { ( 𝐴 |s 𝐵 ) } )
7	6	breq2d	⊢ ( 𝑦 = ( 𝐴 |s 𝐵 ) → ( 𝐴 <<s { 𝑦 } ↔ 𝐴 <<s { ( 𝐴 |s 𝐵 ) } ) )
8	6	breq1d	⊢ ( 𝑦 = ( 𝐴 |s 𝐵 ) → ( { 𝑦 } <<s 𝐵 ↔ { ( 𝐴 |s 𝐵 ) } <<s 𝐵 ) )
9	7 8	anbi12d	⊢ ( 𝑦 = ( 𝐴 |s 𝐵 ) → ( ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) ↔ ( 𝐴 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐵 ) ) )
10	9	elrab	⊢ ( ( 𝐴 |s 𝐵 ) ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ↔ ( ( 𝐴 |s 𝐵 ) ∈ No ∧ ( 𝐴 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐵 ) ) )
11		3anass	⊢ ( ( ( 𝐴 |s 𝐵 ) ∈ No ∧ 𝐴 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐵 ) ↔ ( ( 𝐴 |s 𝐵 ) ∈ No ∧ ( 𝐴 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐵 ) ) )
12	10 11	bitr4i	⊢ ( ( 𝐴 |s 𝐵 ) ∈ { 𝑦 ∈ No ∣ ( 𝐴 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝐵 ) } ↔ ( ( 𝐴 |s 𝐵 ) ∈ No ∧ 𝐴 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐵 ) )
13	5 12	sylib	⊢ ( 𝐴 <<s 𝐵 → ( ( 𝐴 |s 𝐵 ) ∈ No ∧ 𝐴 <<s { ( 𝐴 |s 𝐵 ) } ∧ { ( 𝐴 |s 𝐵 ) } <<s 𝐵 ) )