cuteq1

Description: Condition for a surreal cut to equal one. (Contributed by Scott Fenton, 12-Mar-2025)

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

Proof

Step	Hyp	Ref	Expression
1		cuteq1.1	$⊢ φ \to 0_{s} \in A$
2		cuteq1.2	$⊢ φ \to A ≪_{s} \{1_{s}\}$
3		cuteq1.3	$⊢ φ \to \{1_{s}\} ≪_{s} B$
4		bday1	$⊢ bday (1_{s}) = 1_{𝑜}$
5		df-1o	$⊢ 1_{𝑜} = suc \emptyset$
6	4 5	eqtri	$⊢ bday (1_{s}) = suc \emptyset$
7		sltssep	$⊢ A ≪_{s} \{0_{s}\} \to \forall x \in A \forall y \in \{0_{s}\} x <_{s} y$
8		dfral2	$⊢ \forall y \in \{0_{s}\} x <_{s} y \leftrightarrow \neg \exists y \in \{0_{s}\} \neg x <_{s} y$
9	8	ralbii	$⊢ \forall x \in A \forall y \in \{0_{s}\} x <_{s} y \leftrightarrow \forall x \in A \neg \exists y \in \{0_{s}\} \neg x <_{s} y$
10		ralnex	$⊢ \forall x \in A \neg \exists y \in \{0_{s}\} \neg x <_{s} y \leftrightarrow \neg \exists x \in A \exists y \in \{0_{s}\} \neg x <_{s} y$
11	9 10	bitri	$⊢ \forall x \in A \forall y \in \{0_{s}\} x <_{s} y \leftrightarrow \neg \exists x \in A \exists y \in \{0_{s}\} \neg x <_{s} y$
12	7 11	sylib	$⊢ A ≪_{s} \{0_{s}\} \to \neg \exists x \in A \exists y \in \{0_{s}\} \neg x <_{s} y$
13		0no	$⊢ 0_{s} \in No$
14		ltsirr	$⊢ 0_{s} \in No \to \neg 0_{s} <_{s} 0_{s}$
15	13 14	ax-mp	$⊢ \neg 0_{s} <_{s} 0_{s}$
16		breq1	$⊢ x = 0_{s} \to (x <_{s} 0_{s} \leftrightarrow 0_{s} <_{s} 0_{s})$
17	16	notbid	$⊢ x = 0_{s} \to (\neg x <_{s} 0_{s} \leftrightarrow \neg 0_{s} <_{s} 0_{s})$
18	17	rspcev	$⊢ (0_{s} \in A \land \neg 0_{s} <_{s} 0_{s}) \to \exists x \in A \neg x <_{s} 0_{s}$
19	1 15 18	sylancl	$⊢ φ \to \exists x \in A \neg x <_{s} 0_{s}$
20	13	elexi	$⊢ 0_{s} \in V$
21		breq2	$⊢ y = 0_{s} \to (x <_{s} y \leftrightarrow x <_{s} 0_{s})$
22	21	notbid	$⊢ y = 0_{s} \to (\neg x <_{s} y \leftrightarrow \neg x <_{s} 0_{s})$
23	20 22	rexsn	$⊢ \exists y \in \{0_{s}\} \neg x <_{s} y \leftrightarrow \neg x <_{s} 0_{s}$
24	23	rexbii	$⊢ \exists x \in A \exists y \in \{0_{s}\} \neg x <_{s} y \leftrightarrow \exists x \in A \neg x <_{s} 0_{s}$
25	19 24	sylibr	$⊢ φ \to \exists x \in A \exists y \in \{0_{s}\} \neg x <_{s} y$
26	12 25	nsyl3	$⊢ φ \to \neg A ≪_{s} \{0_{s}\}$
27	26	adantr	$⊢ (φ \land x \in No) \to \neg A ≪_{s} \{0_{s}\}$
28		sneq	$⊢ x = 0_{s} \to \{x\} = \{0_{s}\}$
29	28	breq2d	$⊢ x = 0_{s} \to (A ≪_{s} \{x\} \leftrightarrow A ≪_{s} \{0_{s}\})$
30	29	notbid	$⊢ x = 0_{s} \to (\neg A ≪_{s} \{x\} \leftrightarrow \neg A ≪_{s} \{0_{s}\})$
31	27 30	syl5ibrcom	$⊢ (φ \land x \in No) \to (x = 0_{s} \to \neg A ≪_{s} \{x\})$
32	31	necon2ad	$⊢ (φ \land x \in No) \to (A ≪_{s} \{x\} \to x \neq 0_{s})$
33	32	adantrd	$⊢ (φ \land x \in No) \to ((A ≪_{s} \{x\} \land \{x\} ≪_{s} B) \to x \neq 0_{s})$
34	33	impr	$⊢ (φ \land (x \in No \land (A ≪_{s} \{x\} \land \{x\} ≪_{s} B))) \to x \neq 0_{s}$
35		bday0b	$⊢ x \in No \to (bday (x) = \emptyset \leftrightarrow x = 0_{s})$
36	35	ad2antrl	$⊢ (φ \land (x \in No \land (A ≪_{s} \{x\} \land \{x\} ≪_{s} B))) \to (bday (x) = \emptyset \leftrightarrow x = 0_{s})$
37	36	necon3bid	$⊢ (φ \land (x \in No \land (A ≪_{s} \{x\} \land \{x\} ≪_{s} B))) \to (bday (x) \neq \emptyset \leftrightarrow x \neq 0_{s})$
38	34 37	mpbird	$⊢ (φ \land (x \in No \land (A ≪_{s} \{x\} \land \{x\} ≪_{s} B))) \to bday (x) \neq \emptyset$
39		bdayon	$⊢ bday (x) \in On$
40	39	onordi	$⊢ Ord bday (x)$
41		ord0eln0	$⊢ Ord bday (x) \to (\emptyset \in bday (x) \leftrightarrow bday (x) \neq \emptyset)$
42	40 41	ax-mp	$⊢ \emptyset \in bday (x) \leftrightarrow bday (x) \neq \emptyset$
43		0elon	$⊢ \emptyset \in On$
44	43 39	onsucssi	$⊢ \emptyset \in bday (x) \leftrightarrow suc \emptyset \subseteq bday (x)$
45	42 44	bitr3i	$⊢ bday (x) \neq \emptyset \leftrightarrow suc \emptyset \subseteq bday (x)$
46	38 45	sylib	$⊢ (φ \land (x \in No \land (A ≪_{s} \{x\} \land \{x\} ≪_{s} B))) \to suc \emptyset \subseteq bday (x)$
47	6 46	eqsstrid	$⊢ (φ \land (x \in No \land (A ≪_{s} \{x\} \land \{x\} ≪_{s} B))) \to bday (1_{s}) \subseteq bday (x)$
48	47	expr	$⊢ (φ \land x \in No) \to ((A ≪_{s} \{x\} \land \{x\} ≪_{s} B) \to bday (1_{s}) \subseteq bday (x))$
49	48	ralrimiva	$⊢ φ \to \forall x \in No ((A ≪_{s} \{x\} \land \{x\} ≪_{s} B) \to bday (1_{s}) \subseteq bday (x))$
50		1no	$⊢ 1_{s} \in No$
51	50	elexi	$⊢ 1_{s} \in V$
52	51	snnz	$⊢ \{1_{s}\} \neq \emptyset$
53		sltstr	$⊢ (A ≪_{s} \{1_{s}\} \land \{1_{s}\} ≪_{s} B \land \{1_{s}\} \neq \emptyset) \to A ≪_{s} B$
54	52 53	mp3an3	$⊢ (A ≪_{s} \{1_{s}\} \land \{1_{s}\} ≪_{s} B) \to A ≪_{s} B$
55	2 3 54	syl2anc	$⊢ φ \to A ≪_{s} B$
56		eqcuts2	$⊢ (A ≪_{s} B \land 1_{s} \in No) \to (A \|_{s} B = 1_{s} \leftrightarrow (A ≪_{s} \{1_{s}\} \land \{1_{s}\} ≪_{s} B \land \forall x \in No ((A ≪_{s} \{x\} \land \{x\} ≪_{s} B) \to bday (1_{s}) \subseteq bday (x))))$
57	55 50 56	sylancl	$⊢ φ \to (A \|_{s} B = 1_{s} \leftrightarrow (A ≪_{s} \{1_{s}\} \land \{1_{s}\} ≪_{s} B \land \forall x \in No ((A ≪_{s} \{x\} \land \{x\} ≪_{s} B) \to bday (1_{s}) \subseteq bday (x))))$
58	2 3 49 57	mpbir3and	$⊢ φ \to A \|_{s} B = 1_{s}$

Metamath Proof Explorer

Theorem cuteq1

Proof