eqscut2

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

		Ref	Expression
	Assertion	eqscut2	$⊢ (L ≪_{s} R \land X \in No) \to (L \|_{s} R = X \leftrightarrow (L ≪_{s} \{X\} \land \{X\} ≪_{s} R \land \forall y \in No ((L ≪_{s} \{y\} \land \{y\} ≪_{s} R) \to bday (X) \subseteq bday (y))))$

Proof

Step	Hyp	Ref	Expression
1		eqscut	$⊢ (L ≪_{s} R \land X \in No) \to (L \|_{s} R = X \leftrightarrow (L ≪_{s} \{X\} \land \{X\} ≪_{s} R \land bday (X) = ⋂ bday [\{x \in No \| (L ≪_{s} \{x\} \land \{x\} ≪_{s} R)\}]))$
2		eqss	$⊢ bday (X) = ⋂ bday [\{x \in No \| (L ≪_{s} \{x\} \land \{x\} ≪_{s} R)\}] \leftrightarrow (bday (X) \subseteq ⋂ bday [\{x \in No \| (L ≪_{s} \{x\} \land \{x\} ≪_{s} R)\}] \land ⋂ bday [\{x \in No \| (L ≪_{s} \{x\} \land \{x\} ≪_{s} R)\}] \subseteq bday (X))$
3		sneq	$⊢ x = X \to \{x\} = \{X\}$
4	3	breq2d	$⊢ x = X \to (L ≪_{s} \{x\} \leftrightarrow L ≪_{s} \{X\})$
5	3	breq1d	$⊢ x = X \to (\{x\} ≪_{s} R \leftrightarrow \{X\} ≪_{s} R)$
6	4 5	anbi12d	$⊢ x = X \to ((L ≪_{s} \{x\} \land \{x\} ≪_{s} R) \leftrightarrow (L ≪_{s} \{X\} \land \{X\} ≪_{s} R))$
7	6	elrab3	$⊢ X \in No \to (X \in \{x \in No \| (L ≪_{s} \{x\} \land \{x\} ≪_{s} R)\} \leftrightarrow (L ≪_{s} \{X\} \land \{X\} ≪_{s} R))$
8	7	adantl	$⊢ (L ≪_{s} R \land X \in No) \to (X \in \{x \in No \| (L ≪_{s} \{x\} \land \{x\} ≪_{s} R)\} \leftrightarrow (L ≪_{s} \{X\} \land \{X\} ≪_{s} R))$
9	8	biimpar	$⊢ ((L ≪_{s} R \land X \in No) \land (L ≪_{s} \{X\} \land \{X\} ≪_{s} R)) \to X \in \{x \in No \| (L ≪_{s} \{x\} \land \{x\} ≪_{s} R)\}$
10		bdayfn	$⊢ bday Fn No$
11		ssrab2	$⊢ \{x \in No \| (L ≪_{s} \{x\} \land \{x\} ≪_{s} R)\} \subseteq No$
12		fnfvima	$⊢ (bday Fn No \land \{x \in No \| (L ≪_{s} \{x\} \land \{x\} ≪_{s} R)\} \subseteq No \land X \in \{x \in No \| (L ≪_{s} \{x\} \land \{x\} ≪_{s} R)\}) \to bday (X) \in bday [\{x \in No \| (L ≪_{s} \{x\} \land \{x\} ≪_{s} R)\}]$
13	10 11 12	mp3an12	$⊢ X \in \{x \in No \| (L ≪_{s} \{x\} \land \{x\} ≪_{s} R)\} \to bday (X) \in bday [\{x \in No \| (L ≪_{s} \{x\} \land \{x\} ≪_{s} R)\}]$
14		intss1	$⊢ bday (X) \in bday [\{x \in No \| (L ≪_{s} \{x\} \land \{x\} ≪_{s} R)\}] \to ⋂ bday [\{x \in No \| (L ≪_{s} \{x\} \land \{x\} ≪_{s} R)\}] \subseteq bday (X)$
15	9 13 14	3syl	$⊢ ((L ≪_{s} R \land X \in No) \land (L ≪_{s} \{X\} \land \{X\} ≪_{s} R)) \to ⋂ bday [\{x \in No \| (L ≪_{s} \{x\} \land \{x\} ≪_{s} R)\}] \subseteq bday (X)$
16	15	biantrud	$⊢ ((L ≪_{s} R \land X \in No) \land (L ≪_{s} \{X\} \land \{X\} ≪_{s} R)) \to (bday (X) \subseteq ⋂ bday [\{x \in No \| (L ≪_{s} \{x\} \land \{x\} ≪_{s} R)\}] \leftrightarrow (bday (X) \subseteq ⋂ bday [\{x \in No \| (L ≪_{s} \{x\} \land \{x\} ≪_{s} R)\}] \land ⋂ bday [\{x \in No \| (L ≪_{s} \{x\} \land \{x\} ≪_{s} R)\}] \subseteq bday (X)))$
17		ssint	$⊢ bday (X) \subseteq ⋂ bday [\{x \in No \| (L ≪_{s} \{x\} \land \{x\} ≪_{s} R)\}] \leftrightarrow \forall z \in bday [\{x \in No \| (L ≪_{s} \{x\} \land \{x\} ≪_{s} R)\}] bday (X) \subseteq z$
18		fvelimab	$⊢ (bday Fn No \land \{x \in No \| (L ≪_{s} \{x\} \land \{x\} ≪_{s} R)\} \subseteq No) \to (z \in bday [\{x \in No \| (L ≪_{s} \{x\} \land \{x\} ≪_{s} R)\}] \leftrightarrow \exists y \in \{x \in No \| (L ≪_{s} \{x\} \land \{x\} ≪_{s} R)\} bday (y) = z)$
19	10 11 18	mp2an	$⊢ z \in bday [\{x \in No \| (L ≪_{s} \{x\} \land \{x\} ≪_{s} R)\}] \leftrightarrow \exists y \in \{x \in No \| (L ≪_{s} \{x\} \land \{x\} ≪_{s} R)\} bday (y) = z$
20		sneq	$⊢ x = y \to \{x\} = \{y\}$
21	20	breq2d	$⊢ x = y \to (L ≪_{s} \{x\} \leftrightarrow L ≪_{s} \{y\})$
22	20	breq1d	$⊢ x = y \to (\{x\} ≪_{s} R \leftrightarrow \{y\} ≪_{s} R)$
23	21 22	anbi12d	$⊢ x = y \to ((L ≪_{s} \{x\} \land \{x\} ≪_{s} R) \leftrightarrow (L ≪_{s} \{y\} \land \{y\} ≪_{s} R))$
24	23	rexrab	$⊢ \exists y \in \{x \in No \| (L ≪_{s} \{x\} \land \{x\} ≪_{s} R)\} bday (y) = z \leftrightarrow \exists y \in No ((L ≪_{s} \{y\} \land \{y\} ≪_{s} R) \land bday (y) = z)$
25	19 24	bitri	$⊢ z \in bday [\{x \in No \| (L ≪_{s} \{x\} \land \{x\} ≪_{s} R)\}] \leftrightarrow \exists y \in No ((L ≪_{s} \{y\} \land \{y\} ≪_{s} R) \land bday (y) = z)$
26	25	imbi1i	$⊢ (z \in bday [\{x \in No \| (L ≪_{s} \{x\} \land \{x\} ≪_{s} R)\}] \to bday (X) \subseteq z) \leftrightarrow (\exists y \in No ((L ≪_{s} \{y\} \land \{y\} ≪_{s} R) \land bday (y) = z) \to bday (X) \subseteq z)$
27		r19.23v	$⊢ \forall y \in No (((L ≪_{s} \{y\} \land \{y\} ≪_{s} R) \land bday (y) = z) \to bday (X) \subseteq z) \leftrightarrow (\exists y \in No ((L ≪_{s} \{y\} \land \{y\} ≪_{s} R) \land bday (y) = z) \to bday (X) \subseteq z)$
28		eqcom	$⊢ bday (y) = z \leftrightarrow z = bday (y)$
29	28	anbi1ci	$⊢ ((L ≪_{s} \{y\} \land \{y\} ≪_{s} R) \land bday (y) = z) \leftrightarrow (z = bday (y) \land (L ≪_{s} \{y\} \land \{y\} ≪_{s} R))$
30	29	imbi1i	$⊢ (((L ≪_{s} \{y\} \land \{y\} ≪_{s} R) \land bday (y) = z) \to bday (X) \subseteq z) \leftrightarrow ((z = bday (y) \land (L ≪_{s} \{y\} \land \{y\} ≪_{s} R)) \to bday (X) \subseteq z)$
31		impexp	$⊢ ((z = bday (y) \land (L ≪_{s} \{y\} \land \{y\} ≪_{s} R)) \to bday (X) \subseteq z) \leftrightarrow (z = bday (y) \to ((L ≪_{s} \{y\} \land \{y\} ≪_{s} R) \to bday (X) \subseteq z))$
32	30 31	bitri	$⊢ (((L ≪_{s} \{y\} \land \{y\} ≪_{s} R) \land bday (y) = z) \to bday (X) \subseteq z) \leftrightarrow (z = bday (y) \to ((L ≪_{s} \{y\} \land \{y\} ≪_{s} R) \to bday (X) \subseteq z))$
33	32	ralbii	$⊢ \forall y \in No (((L ≪_{s} \{y\} \land \{y\} ≪_{s} R) \land bday (y) = z) \to bday (X) \subseteq z) \leftrightarrow \forall y \in No (z = bday (y) \to ((L ≪_{s} \{y\} \land \{y\} ≪_{s} R) \to bday (X) \subseteq z))$
34	26 27 33	3bitr2i	$⊢ (z \in bday [\{x \in No \| (L ≪_{s} \{x\} \land \{x\} ≪_{s} R)\}] \to bday (X) \subseteq z) \leftrightarrow \forall y \in No (z = bday (y) \to ((L ≪_{s} \{y\} \land \{y\} ≪_{s} R) \to bday (X) \subseteq z))$
35	34	albii	$⊢ \forall z (z \in bday [\{x \in No \| (L ≪_{s} \{x\} \land \{x\} ≪_{s} R)\}] \to bday (X) \subseteq z) \leftrightarrow \forall z \forall y \in No (z = bday (y) \to ((L ≪_{s} \{y\} \land \{y\} ≪_{s} R) \to bday (X) \subseteq z))$
36		df-ral	$⊢ \forall z \in bday [\{x \in No \| (L ≪_{s} \{x\} \land \{x\} ≪_{s} R)\}] bday (X) \subseteq z \leftrightarrow \forall z (z \in bday [\{x \in No \| (L ≪_{s} \{x\} \land \{x\} ≪_{s} R)\}] \to bday (X) \subseteq z)$
37		ralcom4	$⊢ \forall y \in No \forall z (z = bday (y) \to ((L ≪_{s} \{y\} \land \{y\} ≪_{s} R) \to bday (X) \subseteq z)) \leftrightarrow \forall z \forall y \in No (z = bday (y) \to ((L ≪_{s} \{y\} \land \{y\} ≪_{s} R) \to bday (X) \subseteq z))$
38	35 36 37	3bitr4i	$⊢ \forall z \in bday [\{x \in No \| (L ≪_{s} \{x\} \land \{x\} ≪_{s} R)\}] bday (X) \subseteq z \leftrightarrow \forall y \in No \forall z (z = bday (y) \to ((L ≪_{s} \{y\} \land \{y\} ≪_{s} R) \to bday (X) \subseteq z))$
39		fvex	$⊢ bday (y) \in V$
40		sseq2	$⊢ z = bday (y) \to (bday (X) \subseteq z \leftrightarrow bday (X) \subseteq bday (y))$
41	40	imbi2d	$⊢ z = bday (y) \to (((L ≪_{s} \{y\} \land \{y\} ≪_{s} R) \to bday (X) \subseteq z) \leftrightarrow ((L ≪_{s} \{y\} \land \{y\} ≪_{s} R) \to bday (X) \subseteq bday (y)))$
42	39 41	ceqsalv	$⊢ \forall z (z = bday (y) \to ((L ≪_{s} \{y\} \land \{y\} ≪_{s} R) \to bday (X) \subseteq z)) \leftrightarrow ((L ≪_{s} \{y\} \land \{y\} ≪_{s} R) \to bday (X) \subseteq bday (y))$
43	42	ralbii	$⊢ \forall y \in No \forall z (z = bday (y) \to ((L ≪_{s} \{y\} \land \{y\} ≪_{s} R) \to bday (X) \subseteq z)) \leftrightarrow \forall y \in No ((L ≪_{s} \{y\} \land \{y\} ≪_{s} R) \to bday (X) \subseteq bday (y))$
44	38 43	bitri	$⊢ \forall z \in bday [\{x \in No \| (L ≪_{s} \{x\} \land \{x\} ≪_{s} R)\}] bday (X) \subseteq z \leftrightarrow \forall y \in No ((L ≪_{s} \{y\} \land \{y\} ≪_{s} R) \to bday (X) \subseteq bday (y))$
45	17 44	bitri	$⊢ bday (X) \subseteq ⋂ bday [\{x \in No \| (L ≪_{s} \{x\} \land \{x\} ≪_{s} R)\}] \leftrightarrow \forall y \in No ((L ≪_{s} \{y\} \land \{y\} ≪_{s} R) \to bday (X) \subseteq bday (y))$
46	16 45	bitr3di	$⊢ ((L ≪_{s} R \land X \in No) \land (L ≪_{s} \{X\} \land \{X\} ≪_{s} R)) \to ((bday (X) \subseteq ⋂ bday [\{x \in No \| (L ≪_{s} \{x\} \land \{x\} ≪_{s} R)\}] \land ⋂ bday [\{x \in No \| (L ≪_{s} \{x\} \land \{x\} ≪_{s} R)\}] \subseteq bday (X)) \leftrightarrow \forall y \in No ((L ≪_{s} \{y\} \land \{y\} ≪_{s} R) \to bday (X) \subseteq bday (y)))$
47	2 46	syl5bb	$⊢ ((L ≪_{s} R \land X \in No) \land (L ≪_{s} \{X\} \land \{X\} ≪_{s} R)) \to (bday (X) = ⋂ bday [\{x \in No \| (L ≪_{s} \{x\} \land \{x\} ≪_{s} R)\}] \leftrightarrow \forall y \in No ((L ≪_{s} \{y\} \land \{y\} ≪_{s} R) \to bday (X) \subseteq bday (y)))$
48	47	pm5.32da	$⊢ (L ≪_{s} R \land X \in No) \to (((L ≪_{s} \{X\} \land \{X\} ≪_{s} R) \land bday (X) = ⋂ bday [\{x \in No \| (L ≪_{s} \{x\} \land \{x\} ≪_{s} R)\}]) \leftrightarrow ((L ≪_{s} \{X\} \land \{X\} ≪_{s} R) \land \forall y \in No ((L ≪_{s} \{y\} \land \{y\} ≪_{s} R) \to bday (X) \subseteq bday (y))))$
49		df-3an	$⊢ (L ≪_{s} \{X\} \land \{X\} ≪_{s} R \land bday (X) = ⋂ bday [\{x \in No \| (L ≪_{s} \{x\} \land \{x\} ≪_{s} R)\}]) \leftrightarrow ((L ≪_{s} \{X\} \land \{X\} ≪_{s} R) \land bday (X) = ⋂ bday [\{x \in No \| (L ≪_{s} \{x\} \land \{x\} ≪_{s} R)\}])$
50		df-3an	$⊢ (L ≪_{s} \{X\} \land \{X\} ≪_{s} R \land \forall y \in No ((L ≪_{s} \{y\} \land \{y\} ≪_{s} R) \to bday (X) \subseteq bday (y))) \leftrightarrow ((L ≪_{s} \{X\} \land \{X\} ≪_{s} R) \land \forall y \in No ((L ≪_{s} \{y\} \land \{y\} ≪_{s} R) \to bday (X) \subseteq bday (y)))$
51	48 49 50	3bitr4g	$⊢ (L ≪_{s} R \land X \in No) \to ((L ≪_{s} \{X\} \land \{X\} ≪_{s} R \land bday (X) = ⋂ bday [\{x \in No \| (L ≪_{s} \{x\} \land \{x\} ≪_{s} R)\}]) \leftrightarrow (L ≪_{s} \{X\} \land \{X\} ≪_{s} R \land \forall y \in No ((L ≪_{s} \{y\} \land \{y\} ≪_{s} R) \to bday (X) \subseteq bday (y))))$
52	1 51	bitrd	$⊢ (L ≪_{s} R \land X \in No) \to (L \|_{s} R = X \leftrightarrow (L ≪_{s} \{X\} \land \{X\} ≪_{s} R \land \forall y \in No ((L ≪_{s} \{y\} \land \{y\} ≪_{s} R) \to bday (X) \subseteq bday (y))))$

Metamath Proof Explorer

Theorem eqscut2

Proof