Metamath Proof Explorer

Theorem dmscut

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

Ref Expression
Assertion dmscut 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-scut ⊢ |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-sslt ⊢ <<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 ssltss1 ⊢ ( 𝑎 <<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