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 a b c | a 𝒫 No b s a c = ι x y No | a s y y s b | bday x = bday y No | a s y y s b = a b | c a 𝒫 No b s a c = ι x y No | a s y y s b | bday x = bday y No | a s y y s b
2 df-scut | s = a 𝒫 No , b s a ι x y No | a s y y s b | bday x = bday y No | a s y y s b
3 df-mpo a 𝒫 No , b s a ι x y No | a s y y s b | bday x = bday y No | a s y y s b = a b c | a 𝒫 No b s a c = ι x y No | a s y y s b | bday x = bday y No | a s y y s b
4 2 3 eqtri | s = a b c | a 𝒫 No b s a c = ι x y No | a s y y s b | bday x = bday y No | a s y y s b
5 4 dmeqi dom | s = dom a b c | a 𝒫 No b s a c = ι x y No | a s y y s b | bday x = bday y No | a s y y s b
6 df-sslt s = a b | a No b No x a y b x < s y
7 6 relopabiv Rel s
8 19.42v c a 𝒫 No b s a c = ι x y No | a s y y s b | bday x = bday y No | a s y y s b a 𝒫 No b s a c c = ι x y No | a s y y s b | bday x = bday y No | a s y y s b
9 ssltss1 a s b a No
10 velpw a 𝒫 No a No
11 9 10 sylibr a s b a 𝒫 No
12 11 pm4.71ri a s b a 𝒫 No a s b
13 vex a V
14 vex b V
15 13 14 elimasn b s a a b s
16 df-br a s b a b s
17 15 16 bitr4i b s a a s b
18 17 anbi2i a 𝒫 No b s a a 𝒫 No a s b
19 riotaex ι x y No | a s y y s b | bday x = bday y No | a s y y s b V
20 19 isseti c c = ι x y No | a s y y s b | bday x = bday y No | a s y y s b
21 20 biantru a 𝒫 No b s a a 𝒫 No b s a c c = ι x y No | a s y y s b | bday x = bday y No | a s y y s b
22 12 18 21 3bitr2i a s b a 𝒫 No b s a c c = ι x y No | a s y y s b | bday x = bday y No | a s y y s b
23 8 22 16 3bitr2ri a b s c a 𝒫 No b s a c = ι x y No | a s y y s b | bday x = bday y No | a s y y s b
24 23 a1i a b s c a 𝒫 No b s a c = ι x y No | a s y y s b | bday x = bday y No | a s y y s b
25 7 24 opabbi2dv s = a b | c a 𝒫 No b s a c = ι x y No | a s y y s b | bday x = bday y No | a s y y s b
26 25 mptru s = a b | c a 𝒫 No b s a c = ι x y No | a s y y s b | bday x = bday y No | a s y y s b
27 1 5 26 3eqtr4i dom | s = s