cuteq0

Description: Condition for a surreal cut to equal zero. (Contributed by Scott Fenton, 3-Feb-2025)

	Ref	Expression
Hypotheses	cuteq0.1	$⊢ φ \to A ≪_{s} \{0_{s}\}$
	cuteq0.2	$⊢ φ \to \{0_{s}\} ≪_{s} B$
Assertion	cuteq0	$⊢ φ \to A \|_{s} B = 0_{s}$

Proof

Step	Hyp	Ref	Expression
1		cuteq0.1	$⊢ φ \to A ≪_{s} \{0_{s}\}$
2		cuteq0.2	$⊢ φ \to \{0_{s}\} ≪_{s} B$
3		bday0	$⊢ bday (0_{s}) = \emptyset$
4	3	a1i	$⊢ φ \to bday (0_{s}) = \emptyset$
5		0no	$⊢ 0_{s} \in No$
6		sneq	$⊢ y = 0_{s} \to \{y\} = \{0_{s}\}$
7	6	breq2d	$⊢ y = 0_{s} \to (A ≪_{s} \{y\} \leftrightarrow A ≪_{s} \{0_{s}\})$
8	6	breq1d	$⊢ y = 0_{s} \to (\{y\} ≪_{s} B \leftrightarrow \{0_{s}\} ≪_{s} B)$
9	7 8	anbi12d	$⊢ y = 0_{s} \to ((A ≪_{s} \{y\} \land \{y\} ≪_{s} B) \leftrightarrow (A ≪_{s} \{0_{s}\} \land \{0_{s}\} ≪_{s} B))$
10		fveqeq2	$⊢ y = 0_{s} \to (bday (y) = \emptyset \leftrightarrow bday (0_{s}) = \emptyset)$
11	9 10	anbi12d	$⊢ y = 0_{s} \to (((A ≪_{s} \{y\} \land \{y\} ≪_{s} B) \land bday (y) = \emptyset) \leftrightarrow ((A ≪_{s} \{0_{s}\} \land \{0_{s}\} ≪_{s} B) \land bday (0_{s}) = \emptyset))$
12	11	rspcev	$⊢ (0_{s} \in No \land ((A ≪_{s} \{0_{s}\} \land \{0_{s}\} ≪_{s} B) \land bday (0_{s}) = \emptyset)) \to \exists y \in No ((A ≪_{s} \{y\} \land \{y\} ≪_{s} B) \land bday (y) = \emptyset)$
13	5 12	mpan	$⊢ ((A ≪_{s} \{0_{s}\} \land \{0_{s}\} ≪_{s} B) \land bday (0_{s}) = \emptyset) \to \exists y \in No ((A ≪_{s} \{y\} \land \{y\} ≪_{s} B) \land bday (y) = \emptyset)$
14	1 2 4 13	syl21anc	$⊢ φ \to \exists y \in No ((A ≪_{s} \{y\} \land \{y\} ≪_{s} B) \land bday (y) = \emptyset)$
15		bdayfn	$⊢ bday Fn No$
16		ssrab2	$⊢ \{x \in No \| (A ≪_{s} \{x\} \land \{x\} ≪_{s} B)\} \subseteq No$
17		fvelimab	$⊢ (bday Fn No \land \{x \in No \| (A ≪_{s} \{x\} \land \{x\} ≪_{s} B)\} \subseteq No) \to (\emptyset \in bday [\{x \in No \| (A ≪_{s} \{x\} \land \{x\} ≪_{s} B)\}] \leftrightarrow \exists y \in \{x \in No \| (A ≪_{s} \{x\} \land \{x\} ≪_{s} B)\} bday (y) = \emptyset)$
18	15 16 17	mp2an	$⊢ \emptyset \in bday [\{x \in No \| (A ≪_{s} \{x\} \land \{x\} ≪_{s} B)\}] \leftrightarrow \exists y \in \{x \in No \| (A ≪_{s} \{x\} \land \{x\} ≪_{s} B)\} bday (y) = \emptyset$
19		sneq	$⊢ x = y \to \{x\} = \{y\}$
20	19	breq2d	$⊢ x = y \to (A ≪_{s} \{x\} \leftrightarrow A ≪_{s} \{y\})$
21	19	breq1d	$⊢ x = y \to (\{x\} ≪_{s} B \leftrightarrow \{y\} ≪_{s} B)$
22	20 21	anbi12d	$⊢ x = y \to ((A ≪_{s} \{x\} \land \{x\} ≪_{s} B) \leftrightarrow (A ≪_{s} \{y\} \land \{y\} ≪_{s} B))$
23	22	rexrab	$⊢ \exists y \in \{x \in No \| (A ≪_{s} \{x\} \land \{x\} ≪_{s} B)\} bday (y) = \emptyset \leftrightarrow \exists y \in No ((A ≪_{s} \{y\} \land \{y\} ≪_{s} B) \land bday (y) = \emptyset)$
24	18 23	bitri	$⊢ \emptyset \in bday [\{x \in No \| (A ≪_{s} \{x\} \land \{x\} ≪_{s} B)\}] \leftrightarrow \exists y \in No ((A ≪_{s} \{y\} \land \{y\} ≪_{s} B) \land bday (y) = \emptyset)$
25	14 24	sylibr	$⊢ φ \to \emptyset \in bday [\{x \in No \| (A ≪_{s} \{x\} \land \{x\} ≪_{s} B)\}]$
26		int0el	$⊢ \emptyset \in bday [\{x \in No \| (A ≪_{s} \{x\} \land \{x\} ≪_{s} B)\}] \to ⋂ bday [\{x \in No \| (A ≪_{s} \{x\} \land \{x\} ≪_{s} B)\}] = \emptyset$
27	25 26	syl	$⊢ φ \to ⋂ bday [\{x \in No \| (A ≪_{s} \{x\} \land \{x\} ≪_{s} B)\}] = \emptyset$
28	3 27	eqtr4id	$⊢ φ \to bday (0_{s}) = ⋂ bday [\{x \in No \| (A ≪_{s} \{x\} \land \{x\} ≪_{s} B)\}]$
29	5	elexi	$⊢ 0_{s} \in V$
30	29	snnz	$⊢ \{0_{s}\} \neq \emptyset$
31		sltstr	$⊢ (A ≪_{s} \{0_{s}\} \land \{0_{s}\} ≪_{s} B \land \{0_{s}\} \neq \emptyset) \to A ≪_{s} B$
32	30 31	mp3an3	$⊢ (A ≪_{s} \{0_{s}\} \land \{0_{s}\} ≪_{s} B) \to A ≪_{s} B$
33	1 2 32	syl2anc	$⊢ φ \to A ≪_{s} B$
34		eqcuts	$⊢ (A ≪_{s} B \land 0_{s} \in No) \to (A \|_{s} B = 0_{s} \leftrightarrow (A ≪_{s} \{0_{s}\} \land \{0_{s}\} ≪_{s} B \land bday (0_{s}) = ⋂ bday [\{x \in No \| (A ≪_{s} \{x\} \land \{x\} ≪_{s} B)\}]))$
35	33 5 34	sylancl	$⊢ φ \to (A \|_{s} B = 0_{s} \leftrightarrow (A ≪_{s} \{0_{s}\} \land \{0_{s}\} ≪_{s} B \land bday (0_{s}) = ⋂ bday [\{x \in No \| (A ≪_{s} \{x\} \land \{x\} ≪_{s} B)\}]))$
36	1 2 28 35	mpbir3and	$⊢ φ \to A \|_{s} B = 0_{s}$

Metamath Proof Explorer

Theorem cuteq0

Proof