Theorem cutsf

Description: Functionality statement for the surreal cut operator. (Contributed by Scott Fenton, 15-Dec-2021)

	Ref	Expression
Assertion	cutsf	⊢ |s : <<s ⟶ No

Proof

Step	Hyp	Ref	Expression
1		df-cuts	⊢ |s = ( 𝑎 ∈ 𝒫 No , 𝑏 ∈ ( <<s “ { 𝑎 } ) ↦ ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) )
2	1	mpofun	⊢ Fun |s
3		dmcuts	⊢ dom |s = <<s
4		df-fn	⊢ ( |s Fn <<s ↔ ( Fun |s ∧ dom |s = <<s ) )
5	2 3 4	mpbir2an	⊢ |s Fn <<s
6	1	rnmpo	⊢ ran |s = { 𝑧 ∣ ∃ 𝑎 ∈ 𝒫 No ∃ 𝑏 ∈ ( <<s “ { 𝑎 } ) 𝑧 = ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) }
7		vex	⊢ 𝑎 ∈ V
8		vex	⊢ 𝑏 ∈ V
9	7 8	elimasn	⊢ ( 𝑏 ∈ ( <<s “ { 𝑎 } ) ↔ ⟨ 𝑎 , 𝑏 ⟩ ∈ <<s )
10		df-br	⊢ ( 𝑎 <<s 𝑏 ↔ ⟨ 𝑎 , 𝑏 ⟩ ∈ <<s )
11	9 10	bitr4i	⊢ ( 𝑏 ∈ ( <<s “ { 𝑎 } ) ↔ 𝑎 <<s 𝑏 )
12		cutsval	⊢ ( 𝑎 <<s 𝑏 → ( 𝑎 |s 𝑏 ) = ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) )
13		cutscl	⊢ ( 𝑎 <<s 𝑏 → ( 𝑎 |s 𝑏 ) ∈ No )
14	12 13	eqeltrrd	⊢ ( 𝑎 <<s 𝑏 → ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) ∈ No )
15	11 14	sylbi	⊢ ( 𝑏 ∈ ( <<s “ { 𝑎 } ) → ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) ∈ No )
16		eleq1a	⊢ ( ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) ∈ No → ( 𝑧 = ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) → 𝑧 ∈ No ) )
17	15 16	syl	⊢ ( 𝑏 ∈ ( <<s “ { 𝑎 } ) → ( 𝑧 = ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) → 𝑧 ∈ No ) )
18	17	adantl	⊢ ( ( 𝑎 ∈ 𝒫 No ∧ 𝑏 ∈ ( <<s “ { 𝑎 } ) ) → ( 𝑧 = ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) → 𝑧 ∈ No ) )
19	18	rexlimivv	⊢ ( ∃ 𝑎 ∈ 𝒫 No ∃ 𝑏 ∈ ( <<s “ { 𝑎 } ) 𝑧 = ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) → 𝑧 ∈ No )
20	19	abssi	⊢ { 𝑧 ∣ ∃ 𝑎 ∈ 𝒫 No ∃ 𝑏 ∈ ( <<s “ { 𝑎 } ) 𝑧 = ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) } ⊆ No
21	6 20	eqsstri	⊢ ran |s ⊆ No
22		df-f	⊢ ( |s : <<s ⟶ No ↔ ( |s Fn <<s ∧ ran |s ⊆ No ) )
23	5 21 22	mpbir2an	⊢ |s : <<s ⟶ No