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 \in 𝒫 No \land b \in ≪_{s} [\{a\}]) \land c = (ι x \in \{y \in No \| (a ≪_{s} \{y\} \land \{y\} ≪_{s} b)\} \| bday (x) = ⋂ bday [\{y \in No \| (a ≪_{s} \{y\} \land \{y\} ≪_{s} b)\}]))\} = \{⟨a, b⟩ \| \exists c ((a \in 𝒫 No \land b \in ≪_{s} [\{a\}]) \land c = (ι x \in \{y \in No \| (a ≪_{s} \{y\} \land \{y\} ≪_{s} b)\} \| bday (x) = ⋂ bday [\{y \in No \| (a ≪_{s} \{y\} \land \{y\} ≪_{s} b)\}]))\}$
2		df-scut	$⊢ \|_{s} = (a \in 𝒫 No, b \in ≪_{s} [\{a\}] ⟼ (ι x \in \{y \in No \| (a ≪_{s} \{y\} \land \{y\} ≪_{s} b)\} \| bday (x) = ⋂ bday [\{y \in No \| (a ≪_{s} \{y\} \land \{y\} ≪_{s} b)\}]))$
3		df-mpo	$⊢ (a \in 𝒫 No, b \in ≪_{s} [\{a\}] ⟼ (ι x \in \{y \in No \| (a ≪_{s} \{y\} \land \{y\} ≪_{s} b)\} \| bday (x) = ⋂ bday [\{y \in No \| (a ≪_{s} \{y\} \land \{y\} ≪_{s} b)\}])) = \{⟨⟨a, b⟩, c⟩ \| ((a \in 𝒫 No \land b \in ≪_{s} [\{a\}]) \land c = (ι x \in \{y \in No \| (a ≪_{s} \{y\} \land \{y\} ≪_{s} b)\} \| bday (x) = ⋂ bday [\{y \in No \| (a ≪_{s} \{y\} \land \{y\} ≪_{s} b)\}]))\}$
4	2 3	eqtri	$⊢ \|_{s} = \{⟨⟨a, b⟩, c⟩ \| ((a \in 𝒫 No \land b \in ≪_{s} [\{a\}]) \land c = (ι x \in \{y \in No \| (a ≪_{s} \{y\} \land \{y\} ≪_{s} b)\} \| bday (x) = ⋂ bday [\{y \in No \| (a ≪_{s} \{y\} \land \{y\} ≪_{s} b)\}]))\}$
5	4	dmeqi	$⊢ dom \|_{s} = dom \{⟨⟨a, b⟩, c⟩ \| ((a \in 𝒫 No \land b \in ≪_{s} [\{a\}]) \land c = (ι x \in \{y \in No \| (a ≪_{s} \{y\} \land \{y\} ≪_{s} b)\} \| bday (x) = ⋂ bday [\{y \in No \| (a ≪_{s} \{y\} \land \{y\} ≪_{s} b)\}]))\}$
6		df-sslt	$⊢ ≪_{s} = \{⟨a, b⟩ \| (a \subseteq No \land b \subseteq No \land \forall x \in a \forall y \in b x <_{s} y)\}$
7	6	relopabiv	$⊢ Rel ≪_{s}$
8		19.42v	$⊢ \exists c ((a \in 𝒫 No \land b \in ≪_{s} [\{a\}]) \land c = (ι x \in \{y \in No \| (a ≪_{s} \{y\} \land \{y\} ≪_{s} b)\} \| bday (x) = ⋂ bday [\{y \in No \| (a ≪_{s} \{y\} \land \{y\} ≪_{s} b)\}])) \leftrightarrow ((a \in 𝒫 No \land b \in ≪_{s} [\{a\}]) \land \exists c c = (ι x \in \{y \in No \| (a ≪_{s} \{y\} \land \{y\} ≪_{s} b)\} \| bday (x) = ⋂ bday [\{y \in No \| (a ≪_{s} \{y\} \land \{y\} ≪_{s} b)\}]))$
9		ssltss1	$⊢ a ≪_{s} b \to a \subseteq No$
10		velpw	$⊢ a \in 𝒫 No \leftrightarrow a \subseteq No$
11	9 10	sylibr	$⊢ a ≪_{s} b \to a \in 𝒫 No$
12	11	pm4.71ri	$⊢ a ≪_{s} b \leftrightarrow (a \in 𝒫 No \land a ≪_{s} b)$
13		vex	$⊢ a \in V$
14		vex	$⊢ b \in V$
15	13 14	elimasn	$⊢ b \in ≪_{s} [\{a\}] \leftrightarrow ⟨a, b⟩ \in ≪_{s}$
16		df-br	$⊢ a ≪_{s} b \leftrightarrow ⟨a, b⟩ \in ≪_{s}$
17	15 16	bitr4i	$⊢ b \in ≪_{s} [\{a\}] \leftrightarrow a ≪_{s} b$
18	17	anbi2i	$⊢ (a \in 𝒫 No \land b \in ≪_{s} [\{a\}]) \leftrightarrow (a \in 𝒫 No \land a ≪_{s} b)$
19		riotaex	$⊢ (ι x \in \{y \in No \| (a ≪_{s} \{y\} \land \{y\} ≪_{s} b)\} \| bday (x) = ⋂ bday [\{y \in No \| (a ≪_{s} \{y\} \land \{y\} ≪_{s} b)\}]) \in V$
20	19	isseti	$⊢ \exists c c = (ι x \in \{y \in No \| (a ≪_{s} \{y\} \land \{y\} ≪_{s} b)\} \| bday (x) = ⋂ bday [\{y \in No \| (a ≪_{s} \{y\} \land \{y\} ≪_{s} b)\}])$
21	20	biantru	$⊢ (a \in 𝒫 No \land b \in ≪_{s} [\{a\}]) \leftrightarrow ((a \in 𝒫 No \land b \in ≪_{s} [\{a\}]) \land \exists c c = (ι x \in \{y \in No \| (a ≪_{s} \{y\} \land \{y\} ≪_{s} b)\} \| bday (x) = ⋂ bday [\{y \in No \| (a ≪_{s} \{y\} \land \{y\} ≪_{s} b)\}]))$
22	12 18 21	3bitr2i	$⊢ a ≪_{s} b \leftrightarrow ((a \in 𝒫 No \land b \in ≪_{s} [\{a\}]) \land \exists c c = (ι x \in \{y \in No \| (a ≪_{s} \{y\} \land \{y\} ≪_{s} b)\} \| bday (x) = ⋂ bday [\{y \in No \| (a ≪_{s} \{y\} \land \{y\} ≪_{s} b)\}]))$
23	8 22 16	3bitr2ri	$⊢ ⟨a, b⟩ \in ≪_{s} \leftrightarrow \exists c ((a \in 𝒫 No \land b \in ≪_{s} [\{a\}]) \land c = (ι x \in \{y \in No \| (a ≪_{s} \{y\} \land \{y\} ≪_{s} b)\} \| bday (x) = ⋂ bday [\{y \in No \| (a ≪_{s} \{y\} \land \{y\} ≪_{s} b)\}]))$
24	23	a1i	$⊢ ⊤ \to (⟨a, b⟩ \in ≪_{s} \leftrightarrow \exists c ((a \in 𝒫 No \land b \in ≪_{s} [\{a\}]) \land c = (ι x \in \{y \in No \| (a ≪_{s} \{y\} \land \{y\} ≪_{s} b)\} \| bday (x) = ⋂ bday [\{y \in No \| (a ≪_{s} \{y\} \land \{y\} ≪_{s} b)\}])))$
25	7 24	opabbi2dv	$⊢ ⊤ \to ≪_{s} = \{⟨a, b⟩ \| \exists c ((a \in 𝒫 No \land b \in ≪_{s} [\{a\}]) \land c = (ι x \in \{y \in No \| (a ≪_{s} \{y\} \land \{y\} ≪_{s} b)\} \| bday (x) = ⋂ bday [\{y \in No \| (a ≪_{s} \{y\} \land \{y\} ≪_{s} b)\}]))\}$
26	25	mptru	$⊢ ≪_{s} = \{⟨a, b⟩ \| \exists c ((a \in 𝒫 No \land b \in ≪_{s} [\{a\}]) \land c = (ι x \in \{y \in No \| (a ≪_{s} \{y\} \land \{y\} ≪_{s} b)\} \| bday (x) = ⋂ bday [\{y \in No \| (a ≪_{s} \{y\} \land \{y\} ≪_{s} b)\}]))\}$
27	1 5 26	3eqtr4i	$⊢ dom \|_{s} = ≪_{s}$

Metamath Proof Explorer

Theorem dmscut

Proof