Theorem dmcuts

Description: The domain of the surreal cut operation is all separated surreal sets. (Contributed by Scott Fenton, 8-Dec-2021)

	Ref	Expression
Assertion	dmcuts	⊢ dom |s = <<s

Proof

Step	Hyp	Ref	Expression
1		dmoprab	⊢ dom { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ∣ ( ( 𝑎 ∈ 𝒫 No ∧ 𝑏 ∈ ( <<s “ { 𝑎 } ) ) ∧ 𝑐 = ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) ) } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ( ( 𝑎 ∈ 𝒫 No ∧ 𝑏 ∈ ( <<s “ { 𝑎 } ) ) ∧ 𝑐 = ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) ) }
2		df-cuts	⊢ |s = ( 𝑎 ∈ 𝒫 No , 𝑏 ∈ ( <<s “ { 𝑎 } ) ↦ ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) )
3		df-mpo	⊢ ( 𝑎 ∈ 𝒫 No , 𝑏 ∈ ( <<s “ { 𝑎 } ) ↦ ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) ) = { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ∣ ( ( 𝑎 ∈ 𝒫 No ∧ 𝑏 ∈ ( <<s “ { 𝑎 } ) ) ∧ 𝑐 = ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) ) }
4	2 3	eqtri	⊢ |s = { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ∣ ( ( 𝑎 ∈ 𝒫 No ∧ 𝑏 ∈ ( <<s “ { 𝑎 } ) ) ∧ 𝑐 = ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) ) }
5	4	dmeqi	⊢ dom |s = dom { ⟨ ⟨ 𝑎 , 𝑏 ⟩ , 𝑐 ⟩ ∣ ( ( 𝑎 ∈ 𝒫 No ∧ 𝑏 ∈ ( <<s “ { 𝑎 } ) ) ∧ 𝑐 = ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) ) }
6		df-slts	⊢ <<s = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ⊆ No ∧ 𝑏 ⊆ No ∧ ∀ 𝑥 ∈ 𝑎 ∀ 𝑦 ∈ 𝑏 𝑥 <s 𝑦 ) }
7	6	relopabiv	⊢ Rel <<s
8		19.42v	⊢ ( ∃ 𝑐 ( ( 𝑎 ∈ 𝒫 No ∧ 𝑏 ∈ ( <<s “ { 𝑎 } ) ) ∧ 𝑐 = ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) ) ↔ ( ( 𝑎 ∈ 𝒫 No ∧ 𝑏 ∈ ( <<s “ { 𝑎 } ) ) ∧ ∃ 𝑐 𝑐 = ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) ) )
9		sltsss1	⊢ ( 𝑎 <<s 𝑏 → 𝑎 ⊆ No )
10		velpw	⊢ ( 𝑎 ∈ 𝒫 No ↔ 𝑎 ⊆ No )
11	9 10	sylibr	⊢ ( 𝑎 <<s 𝑏 → 𝑎 ∈ 𝒫 No )
12	11	pm4.71ri	⊢ ( 𝑎 <<s 𝑏 ↔ ( 𝑎 ∈ 𝒫 No ∧ 𝑎 <<s 𝑏 ) )
13		vex	⊢ 𝑎 ∈ V
14		vex	⊢ 𝑏 ∈ V
15	13 14	elimasn	⊢ ( 𝑏 ∈ ( <<s “ { 𝑎 } ) ↔ ⟨ 𝑎 , 𝑏 ⟩ ∈ <<s )
16		df-br	⊢ ( 𝑎 <<s 𝑏 ↔ ⟨ 𝑎 , 𝑏 ⟩ ∈ <<s )
17	15 16	bitr4i	⊢ ( 𝑏 ∈ ( <<s “ { 𝑎 } ) ↔ 𝑎 <<s 𝑏 )
18	17	anbi2i	⊢ ( ( 𝑎 ∈ 𝒫 No ∧ 𝑏 ∈ ( <<s “ { 𝑎 } ) ) ↔ ( 𝑎 ∈ 𝒫 No ∧ 𝑎 <<s 𝑏 ) )
19		riotaex	⊢ ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) ∈ V
20	19	isseti	⊢ ∃ 𝑐 𝑐 = ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) )
21	20	biantru	⊢ ( ( 𝑎 ∈ 𝒫 No ∧ 𝑏 ∈ ( <<s “ { 𝑎 } ) ) ↔ ( ( 𝑎 ∈ 𝒫 No ∧ 𝑏 ∈ ( <<s “ { 𝑎 } ) ) ∧ ∃ 𝑐 𝑐 = ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) ) )
22	12 18 21	3bitr2i	⊢ ( 𝑎 <<s 𝑏 ↔ ( ( 𝑎 ∈ 𝒫 No ∧ 𝑏 ∈ ( <<s “ { 𝑎 } ) ) ∧ ∃ 𝑐 𝑐 = ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) ) )
23	8 22 16	3bitr2ri	⊢ ( ⟨ 𝑎 , 𝑏 ⟩ ∈ <<s ↔ ∃ 𝑐 ( ( 𝑎 ∈ 𝒫 No ∧ 𝑏 ∈ ( <<s “ { 𝑎 } ) ) ∧ 𝑐 = ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) ) )
24	23	a1i	⊢ ( ⊤ → ( ⟨ 𝑎 , 𝑏 ⟩ ∈ <<s ↔ ∃ 𝑐 ( ( 𝑎 ∈ 𝒫 No ∧ 𝑏 ∈ ( <<s “ { 𝑎 } ) ) ∧ 𝑐 = ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) ) ) )
25	7 24	opabbi2dv	⊢ ( ⊤ → <<s = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ( ( 𝑎 ∈ 𝒫 No ∧ 𝑏 ∈ ( <<s “ { 𝑎 } ) ) ∧ 𝑐 = ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) ) } )
26	25	mptru	⊢ <<s = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ∃ 𝑐 ( ( 𝑎 ∈ 𝒫 No ∧ 𝑏 ∈ ( <<s “ { 𝑎 } ) ) ∧ 𝑐 = ( ℩ 𝑥 ∈ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ( bday ‘ 𝑥 ) = ∩ ( bday “ { 𝑦 ∈ No ∣ ( 𝑎 <<s { 𝑦 } ∧ { 𝑦 } <<s 𝑏 ) } ) ) ) }
27	1 5 26	3eqtr4i	⊢ dom |s = <<s