eqcuts

Description: Condition for equality to a surreal cut. (Contributed by Scott Fenton, 8-Aug-2024)

		Ref	Expression
	Assertion	eqcuts	$⊢ (L ≪_{s} R \land X \in No) \to (L \|_{s} R = X \leftrightarrow (L ≪_{s} \{X\} \land \{X\} ≪_{s} R \land bday (X) = ⋂ bday [\{y \in No \| (L ≪_{s} \{y\} \land \{y\} ≪_{s} R)\}]))$

Proof

Step	Hyp	Ref	Expression
1		cutsval	$⊢ L ≪_{s} R \to L \|_{s} R = (ι x \in \{y \in No \| (L ≪_{s} \{y\} \land \{y\} ≪_{s} R)\} \| bday (x) = ⋂ bday [\{y \in No \| (L ≪_{s} \{y\} \land \{y\} ≪_{s} R)\}])$
2	1	adantr	$⊢ (L ≪_{s} R \land X \in No) \to L \|_{s} R = (ι x \in \{y \in No \| (L ≪_{s} \{y\} \land \{y\} ≪_{s} R)\} \| bday (x) = ⋂ bday [\{y \in No \| (L ≪_{s} \{y\} \land \{y\} ≪_{s} R)\}])$
3		sneq	$⊢ x = y \to \{x\} = \{y\}$
4	3	breq2d	$⊢ x = y \to (L ≪_{s} \{x\} \leftrightarrow L ≪_{s} \{y\})$
5	3	breq1d	$⊢ x = y \to (\{x\} ≪_{s} R \leftrightarrow \{y\} ≪_{s} R)$
6	4 5	anbi12d	$⊢ x = y \to ((L ≪_{s} \{x\} \land \{x\} ≪_{s} R) \leftrightarrow (L ≪_{s} \{y\} \land \{y\} ≪_{s} R))$
7	6	riotarab	$⊢ (ι x \in \{y \in No \| (L ≪_{s} \{y\} \land \{y\} ≪_{s} R)\} \| bday (x) = ⋂ bday [\{y \in No \| (L ≪_{s} \{y\} \land \{y\} ≪_{s} R)\}]) = (ι x \in No \| ((L ≪_{s} \{x\} \land \{x\} ≪_{s} R) \land bday (x) = ⋂ bday [\{y \in No \| (L ≪_{s} \{y\} \land \{y\} ≪_{s} R)\}]))$
8	2 7	eqtrdi	$⊢ (L ≪_{s} R \land X \in No) \to L \|_{s} R = (ι x \in No \| ((L ≪_{s} \{x\} \land \{x\} ≪_{s} R) \land bday (x) = ⋂ bday [\{y \in No \| (L ≪_{s} \{y\} \land \{y\} ≪_{s} R)\}]))$
9	8	eqeq1d	$⊢ (L ≪_{s} R \land X \in No) \to (L \|_{s} R = X \leftrightarrow (ι x \in No \| ((L ≪_{s} \{x\} \land \{x\} ≪_{s} R) \land bday (x) = ⋂ bday [\{y \in No \| (L ≪_{s} \{y\} \land \{y\} ≪_{s} R)\}])) = X)$
10		conway	$⊢ L ≪_{s} R \to \exists! x \in \{y \in No \| (L ≪_{s} \{y\} \land \{y\} ≪_{s} R)\} bday (x) = ⋂ bday [\{y \in No \| (L ≪_{s} \{y\} \land \{y\} ≪_{s} R)\}]$
11	6	reurab	$⊢ \exists! x \in \{y \in No \| (L ≪_{s} \{y\} \land \{y\} ≪_{s} R)\} bday (x) = ⋂ bday [\{y \in No \| (L ≪_{s} \{y\} \land \{y\} ≪_{s} R)\}] \leftrightarrow \exists! x \in No ((L ≪_{s} \{x\} \land \{x\} ≪_{s} R) \land bday (x) = ⋂ bday [\{y \in No \| (L ≪_{s} \{y\} \land \{y\} ≪_{s} R)\}])$
12	10 11	sylib	$⊢ L ≪_{s} R \to \exists! x \in No ((L ≪_{s} \{x\} \land \{x\} ≪_{s} R) \land bday (x) = ⋂ bday [\{y \in No \| (L ≪_{s} \{y\} \land \{y\} ≪_{s} R)\}])$
13		df-3an	$⊢ (L ≪_{s} \{x\} \land \{x\} ≪_{s} R \land bday (x) = ⋂ bday [\{y \in No \| (L ≪_{s} \{y\} \land \{y\} ≪_{s} R)\}]) \leftrightarrow ((L ≪_{s} \{x\} \land \{x\} ≪_{s} R) \land bday (x) = ⋂ bday [\{y \in No \| (L ≪_{s} \{y\} \land \{y\} ≪_{s} R)\}])$
14		sneq	$⊢ x = X \to \{x\} = \{X\}$
15	14	breq2d	$⊢ x = X \to (L ≪_{s} \{x\} \leftrightarrow L ≪_{s} \{X\})$
16	14	breq1d	$⊢ x = X \to (\{x\} ≪_{s} R \leftrightarrow \{X\} ≪_{s} R)$
17		fveqeq2	$⊢ x = X \to (bday (x) = ⋂ bday [\{y \in No \| (L ≪_{s} \{y\} \land \{y\} ≪_{s} R)\}] \leftrightarrow bday (X) = ⋂ bday [\{y \in No \| (L ≪_{s} \{y\} \land \{y\} ≪_{s} R)\}])$
18	15 16 17	3anbi123d	$⊢ x = X \to ((L ≪_{s} \{x\} \land \{x\} ≪_{s} R \land bday (x) = ⋂ bday [\{y \in No \| (L ≪_{s} \{y\} \land \{y\} ≪_{s} R)\}]) \leftrightarrow (L ≪_{s} \{X\} \land \{X\} ≪_{s} R \land bday (X) = ⋂ bday [\{y \in No \| (L ≪_{s} \{y\} \land \{y\} ≪_{s} R)\}]))$
19	13 18	bitr3id	$⊢ x = X \to (((L ≪_{s} \{x\} \land \{x\} ≪_{s} R) \land bday (x) = ⋂ bday [\{y \in No \| (L ≪_{s} \{y\} \land \{y\} ≪_{s} R)\}]) \leftrightarrow (L ≪_{s} \{X\} \land \{X\} ≪_{s} R \land bday (X) = ⋂ bday [\{y \in No \| (L ≪_{s} \{y\} \land \{y\} ≪_{s} R)\}]))$
20	19	riota2	$⊢ (X \in No \land \exists! x \in No ((L ≪_{s} \{x\} \land \{x\} ≪_{s} R) \land bday (x) = ⋂ bday [\{y \in No \| (L ≪_{s} \{y\} \land \{y\} ≪_{s} R)\}])) \to ((L ≪_{s} \{X\} \land \{X\} ≪_{s} R \land bday (X) = ⋂ bday [\{y \in No \| (L ≪_{s} \{y\} \land \{y\} ≪_{s} R)\}]) \leftrightarrow (ι x \in No \| ((L ≪_{s} \{x\} \land \{x\} ≪_{s} R) \land bday (x) = ⋂ bday [\{y \in No \| (L ≪_{s} \{y\} \land \{y\} ≪_{s} R)\}])) = X)$
21	20	ancoms	$⊢ (\exists! x \in No ((L ≪_{s} \{x\} \land \{x\} ≪_{s} R) \land bday (x) = ⋂ bday [\{y \in No \| (L ≪_{s} \{y\} \land \{y\} ≪_{s} R)\}]) \land X \in No) \to ((L ≪_{s} \{X\} \land \{X\} ≪_{s} R \land bday (X) = ⋂ bday [\{y \in No \| (L ≪_{s} \{y\} \land \{y\} ≪_{s} R)\}]) \leftrightarrow (ι x \in No \| ((L ≪_{s} \{x\} \land \{x\} ≪_{s} R) \land bday (x) = ⋂ bday [\{y \in No \| (L ≪_{s} \{y\} \land \{y\} ≪_{s} R)\}])) = X)$
22	12 21	sylan	$⊢ (L ≪_{s} R \land X \in No) \to ((L ≪_{s} \{X\} \land \{X\} ≪_{s} R \land bday (X) = ⋂ bday [\{y \in No \| (L ≪_{s} \{y\} \land \{y\} ≪_{s} R)\}]) \leftrightarrow (ι x \in No \| ((L ≪_{s} \{x\} \land \{x\} ≪_{s} R) \land bday (x) = ⋂ bday [\{y \in No \| (L ≪_{s} \{y\} \land \{y\} ≪_{s} R)\}])) = X)$
23	9 22	bitr4d	$⊢ (L ≪_{s} R \land X \in No) \to (L \|_{s} R = X \leftrightarrow (L ≪_{s} \{X\} \land \{X\} ≪_{s} R \land bday (X) = ⋂ bday [\{y \in No \| (L ≪_{s} \{y\} \land \{y\} ≪_{s} R)\}]))$

Metamath Proof Explorer

Theorem eqcuts

Proof