n0sfincut

Description: The simplest number greater than a finite set of non-negative surreal integers is a non-negative surreal integer. (Contributed by Scott Fenton, 5-Nov-2025)

		Ref	Expression
	Assertion	n0sfincut	$⊢ (A \subseteq ℕ_{0s} \land A \in Fin) \to A \|_{s} \emptyset \in ℕ_{0s}$

Proof

Step	Hyp	Ref	Expression
1		oveq1	$⊢ A = \emptyset \to A \|_{s} \emptyset = \emptyset \|_{s} \emptyset$
2		df-0s	$⊢ 0_{s} = \emptyset \|_{s} \emptyset$
3		0n0s	$⊢ 0_{s} \in ℕ_{0s}$
4	2 3	eqeltrri	$⊢ \emptyset \|_{s} \emptyset \in ℕ_{0s}$
5	1 4	eqeltrdi	$⊢ A = \emptyset \to A \|_{s} \emptyset \in ℕ_{0s}$
6	5	a1d	$⊢ A = \emptyset \to ((A \subseteq ℕ_{0s} \land A \in Fin) \to A \|_{s} \emptyset \in ℕ_{0s})$
7		n0ssno	$⊢ ℕ_{0s} \subseteq No$
8		sstr	$⊢ (A \subseteq ℕ_{0s} \land ℕ_{0s} \subseteq No) \to A \subseteq No$
9	7 8	mpan2	$⊢ A \subseteq ℕ_{0s} \to A \subseteq No$
10		sltso	$⊢ <_{s} Or No$
11		soss	$⊢ A \subseteq No \to (<_{s} Or No \to <_{s} Or A)$
12	9 10 11	mpisyl	$⊢ A \subseteq ℕ_{0s} \to <_{s} Or A$
13	12	ad2antrl	$⊢ (A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \to <_{s} Or A$
14		simprr	$⊢ (A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \to A \in Fin$
15		simpl	$⊢ (A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \to A \neq \emptyset$
16		fimax2g	$⊢ (<_{s} Or A \land A \in Fin \land A \neq \emptyset) \to \exists x \in A \forall y \in A \neg x <_{s} y$
17	13 14 15 16	syl3anc	$⊢ (A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \to \exists x \in A \forall y \in A \neg x <_{s} y$
18	9	ad2antrl	$⊢ (A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \to A \subseteq No$
19	18	adantr	$⊢ ((A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \land x \in A) \to A \subseteq No$
20	19	sselda	$⊢ (((A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \land x \in A) \land y \in A) \to y \in No$
21	18	sselda	$⊢ ((A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \land x \in A) \to x \in No$
22	21	adantr	$⊢ (((A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \land x \in A) \land y \in A) \to x \in No$
23		slenlt	$⊢ (y \in No \land x \in No) \to (y \leq_{s} x \leftrightarrow \neg x <_{s} y)$
24	20 22 23	syl2anc	$⊢ (((A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \land x \in A) \land y \in A) \to (y \leq_{s} x \leftrightarrow \neg x <_{s} y)$
25	24	ralbidva	$⊢ ((A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \land x \in A) \to (\forall y \in A y \leq_{s} x \leftrightarrow \forall y \in A \neg x <_{s} y)$
26		simpl	$⊢ (x \in A \land \forall y \in A y \leq_{s} x) \to x \in A$
27		ssel2	$⊢ (A \subseteq No \land x \in A) \to x \in No$
28	18 26 27	syl2an	$⊢ ((A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \land (x \in A \land \forall y \in A y \leq_{s} x)) \to x \in No$
29		snelpwi	$⊢ x \in No \to \{x\} \in 𝒫 No$
30		nulssgt	$⊢ \{x\} \in 𝒫 No \to \{x\} ≪_{s} \emptyset$
31	28 29 30	3syl	$⊢ ((A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \land (x \in A \land \forall y \in A y \leq_{s} x)) \to \{x\} ≪_{s} \emptyset$
32		breq2	$⊢ w = x \to (x \leq_{s} w \leftrightarrow x \leq_{s} x)$
33		simprl	$⊢ ((A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \land (x \in A \land \forall y \in A y \leq_{s} x)) \to x \in A$
34		slerflex	$⊢ x \in No \to x \leq_{s} x$
35	28 34	syl	$⊢ ((A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \land (x \in A \land \forall y \in A y \leq_{s} x)) \to x \leq_{s} x$
36	32 33 35	rspcedvdw	$⊢ ((A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \land (x \in A \land \forall y \in A y \leq_{s} x)) \to \exists w \in A x \leq_{s} w$
37		vex	$⊢ x \in V$
38		breq1	$⊢ z = x \to (z \leq_{s} w \leftrightarrow x \leq_{s} w)$
39	38	rexbidv	$⊢ z = x \to (\exists w \in A z \leq_{s} w \leftrightarrow \exists w \in A x \leq_{s} w)$
40	37 39	ralsn	$⊢ \forall z \in \{x\} \exists w \in A z \leq_{s} w \leftrightarrow \exists w \in A x \leq_{s} w$
41	36 40	sylibr	$⊢ ((A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \land (x \in A \land \forall y \in A y \leq_{s} x)) \to \forall z \in \{x\} \exists w \in A z \leq_{s} w$
42		ral0	$⊢ \forall z \in \emptyset \exists w \in \emptyset w \leq_{s} z$
43	42	a1i	$⊢ ((A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \land (x \in A \land \forall y \in A y \leq_{s} x)) \to \forall z \in \emptyset \exists w \in \emptyset w \leq_{s} z$
44		simplrr	$⊢ ((A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \land (x \in A \land \forall y \in A y \leq_{s} x)) \to A \in Fin$
45		snex	$⊢ \{\{x\} \|_{s} \emptyset\} \in V$
46	45	a1i	$⊢ ((A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \land (x \in A \land \forall y \in A y \leq_{s} x)) \to \{\{x\} \|_{s} \emptyset\} \in V$
47	18	adantr	$⊢ ((A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \land (x \in A \land \forall y \in A y \leq_{s} x)) \to A \subseteq No$
48	31	scutcld	$⊢ ((A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \land (x \in A \land \forall y \in A y \leq_{s} x)) \to \{x\} \|_{s} \emptyset \in No$
49	48	snssd	$⊢ ((A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \land (x \in A \land \forall y \in A y \leq_{s} x)) \to \{\{x\} \|_{s} \emptyset\} \subseteq No$
50	47	sselda	$⊢ (((A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \land (x \in A \land \forall y \in A y \leq_{s} x)) \land z \in A) \to z \in No$
51	28	adantr	$⊢ (((A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \land (x \in A \land \forall y \in A y \leq_{s} x)) \land z \in A) \to x \in No$
52	48	adantr	$⊢ (((A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \land (x \in A \land \forall y \in A y \leq_{s} x)) \land z \in A) \to \{x\} \|_{s} \emptyset \in No$
53		breq1	$⊢ y = z \to (y \leq_{s} x \leftrightarrow z \leq_{s} x)$
54		simplrr	$⊢ (((A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \land (x \in A \land \forall y \in A y \leq_{s} x)) \land z \in A) \to \forall y \in A y \leq_{s} x$
55		simpr	$⊢ (((A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \land (x \in A \land \forall y \in A y \leq_{s} x)) \land z \in A) \to z \in A$
56	53 54 55	rspcdva	$⊢ (((A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \land (x \in A \land \forall y \in A y \leq_{s} x)) \land z \in A) \to z \leq_{s} x$
57	51 34	syl	$⊢ (((A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \land (x \in A \land \forall y \in A y \leq_{s} x)) \land z \in A) \to x \leq_{s} x$
58		breq2	$⊢ z = x \to (x \leq_{s} z \leftrightarrow x \leq_{s} x)$
59	37 58	rexsn	$⊢ \exists z \in \{x\} x \leq_{s} z \leftrightarrow x \leq_{s} x$
60	57 59	sylibr	$⊢ (((A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \land (x \in A \land \forall y \in A y \leq_{s} x)) \land z \in A) \to \exists z \in \{x\} x \leq_{s} z$
61	60	orcd	$⊢ (((A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \land (x \in A \land \forall y \in A y \leq_{s} x)) \land z \in A) \to (\exists z \in \{x\} x \leq_{s} z \lor \exists w \in R (x) w \leq_{s} (\{x\} \|_{s} \emptyset))$
62		lltropt	$⊢ L (x) ≪_{s} R (x)$
63	62	a1i	$⊢ (((A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \land (x \in A \land \forall y \in A y \leq_{s} x)) \land z \in A) \to L (x) ≪_{s} R (x)$
64	31	adantr	$⊢ (((A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \land (x \in A \land \forall y \in A y \leq_{s} x)) \land z \in A) \to \{x\} ≪_{s} \emptyset$
65		lrcut	$⊢ x \in No \to L (x) \|_{s} R (x) = x$
66	51 65	syl	$⊢ (((A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \land (x \in A \land \forall y \in A y \leq_{s} x)) \land z \in A) \to L (x) \|_{s} R (x) = x$
67	66	eqcomd	$⊢ (((A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \land (x \in A \land \forall y \in A y \leq_{s} x)) \land z \in A) \to x = L (x) \|_{s} R (x)$
68		eqidd	$⊢ (((A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \land (x \in A \land \forall y \in A y \leq_{s} x)) \land z \in A) \to \{x\} \|_{s} \emptyset = \{x\} \|_{s} \emptyset$
69		sltrec	$⊢ ((L (x) ≪_{s} R (x) \land \{x\} ≪_{s} \emptyset) \land (x = L (x) \|_{s} R (x) \land \{x\} \|_{s} \emptyset = \{x\} \|_{s} \emptyset)) \to (x <_{s} (\{x\} \|_{s} \emptyset) \leftrightarrow (\exists z \in \{x\} x \leq_{s} z \lor \exists w \in R (x) w \leq_{s} (\{x\} \|_{s} \emptyset)))$
70	63 64 67 68 69	syl22anc	$⊢ (((A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \land (x \in A \land \forall y \in A y \leq_{s} x)) \land z \in A) \to (x <_{s} (\{x\} \|_{s} \emptyset) \leftrightarrow (\exists z \in \{x\} x \leq_{s} z \lor \exists w \in R (x) w \leq_{s} (\{x\} \|_{s} \emptyset)))$
71	61 70	mpbird	$⊢ (((A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \land (x \in A \land \forall y \in A y \leq_{s} x)) \land z \in A) \to x <_{s} (\{x\} \|_{s} \emptyset)$
72	50 51 52 56 71	slelttrd	$⊢ (((A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \land (x \in A \land \forall y \in A y \leq_{s} x)) \land z \in A) \to z <_{s} (\{x\} \|_{s} \emptyset)$
73		velsn	$⊢ w \in \{\{x\} \|_{s} \emptyset\} \leftrightarrow w = \{x\} \|_{s} \emptyset$
74		breq2	$⊢ w = \{x\} \|_{s} \emptyset \to (z <_{s} w \leftrightarrow z <_{s} (\{x\} \|_{s} \emptyset))$
75	73 74	sylbi	$⊢ w \in \{\{x\} \|_{s} \emptyset\} \to (z <_{s} w \leftrightarrow z <_{s} (\{x\} \|_{s} \emptyset))$
76	72 75	syl5ibrcom	$⊢ (((A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \land (x \in A \land \forall y \in A y \leq_{s} x)) \land z \in A) \to (w \in \{\{x\} \|_{s} \emptyset\} \to z <_{s} w)$
77	76	3impia	$⊢ (((A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \land (x \in A \land \forall y \in A y \leq_{s} x)) \land z \in A \land w \in \{\{x\} \|_{s} \emptyset\}) \to z <_{s} w$
78	44 46 47 49 77	ssltd	$⊢ ((A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \land (x \in A \land \forall y \in A y \leq_{s} x)) \to A ≪_{s} \{\{x\} \|_{s} \emptyset\}$
79		snelpwi	$⊢ \{x\} \|_{s} \emptyset \in No \to \{\{x\} \|_{s} \emptyset\} \in 𝒫 No$
80		nulssgt	$⊢ \{\{x\} \|_{s} \emptyset\} \in 𝒫 No \to \{\{x\} \|_{s} \emptyset\} ≪_{s} \emptyset$
81	48 79 80	3syl	$⊢ ((A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \land (x \in A \land \forall y \in A y \leq_{s} x)) \to \{\{x\} \|_{s} \emptyset\} ≪_{s} \emptyset$
82	31 41 43 78 81	cofcut1d	$⊢ ((A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \land (x \in A \land \forall y \in A y \leq_{s} x)) \to \{x\} \|_{s} \emptyset = A \|_{s} \emptyset$
83	82	eqcomd	$⊢ ((A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \land (x \in A \land \forall y \in A y \leq_{s} x)) \to A \|_{s} \emptyset = \{x\} \|_{s} \emptyset$
84		simplrl	$⊢ ((A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \land (x \in A \land \forall y \in A y \leq_{s} x)) \to A \subseteq ℕ_{0s}$
85	84 33	sseldd	$⊢ ((A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \land (x \in A \land \forall y \in A y \leq_{s} x)) \to x \in ℕ_{0s}$
86		peano2n0s	$⊢ x \in ℕ_{0s} \to x +_{s} 1_{s} \in ℕ_{0s}$
87	85 86	syl	$⊢ ((A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \land (x \in A \land \forall y \in A y \leq_{s} x)) \to x +_{s} 1_{s} \in ℕ_{0s}$
88		n0scut	$⊢ x +_{s} 1_{s} \in ℕ_{0s} \to x +_{s} 1_{s} = \{(x +_{s} 1_{s}) -_{s} 1_{s}\} \|_{s} \emptyset$
89	87 88	syl	$⊢ ((A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \land (x \in A \land \forall y \in A y \leq_{s} x)) \to x +_{s} 1_{s} = \{(x +_{s} 1_{s}) -_{s} 1_{s}\} \|_{s} \emptyset$
90		1sno	$⊢ 1_{s} \in No$
91		pncans	$⊢ (x \in No \land 1_{s} \in No) \to (x +_{s} 1_{s}) -_{s} 1_{s} = x$
92	28 90 91	sylancl	$⊢ ((A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \land (x \in A \land \forall y \in A y \leq_{s} x)) \to (x +_{s} 1_{s}) -_{s} 1_{s} = x$
93	92	sneqd	$⊢ ((A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \land (x \in A \land \forall y \in A y \leq_{s} x)) \to \{(x +_{s} 1_{s}) -_{s} 1_{s}\} = \{x\}$
94	93	oveq1d	$⊢ ((A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \land (x \in A \land \forall y \in A y \leq_{s} x)) \to \{(x +_{s} 1_{s}) -_{s} 1_{s}\} \|_{s} \emptyset = \{x\} \|_{s} \emptyset$
95	89 94	eqtr2d	$⊢ ((A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \land (x \in A \land \forall y \in A y \leq_{s} x)) \to \{x\} \|_{s} \emptyset = x +_{s} 1_{s}$
96	95 87	eqeltrd	$⊢ ((A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \land (x \in A \land \forall y \in A y \leq_{s} x)) \to \{x\} \|_{s} \emptyset \in ℕ_{0s}$
97	83 96	eqeltrd	$⊢ ((A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \land (x \in A \land \forall y \in A y \leq_{s} x)) \to A \|_{s} \emptyset \in ℕ_{0s}$
98	97	expr	$⊢ ((A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \land x \in A) \to (\forall y \in A y \leq_{s} x \to A \|_{s} \emptyset \in ℕ_{0s})$
99	25 98	sylbird	$⊢ ((A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \land x \in A) \to (\forall y \in A \neg x <_{s} y \to A \|_{s} \emptyset \in ℕ_{0s})$
100	99	rexlimdva	$⊢ (A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \to (\exists x \in A \forall y \in A \neg x <_{s} y \to A \|_{s} \emptyset \in ℕ_{0s})$
101	17 100	mpd	$⊢ (A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \to A \|_{s} \emptyset \in ℕ_{0s}$
102	101	ex	$⊢ A \neq \emptyset \to ((A \subseteq ℕ_{0s} \land A \in Fin) \to A \|_{s} \emptyset \in ℕ_{0s})$
103	6 102	pm2.61ine	$⊢ (A \subseteq ℕ_{0s} \land A \in Fin) \to A \|_{s} \emptyset \in ℕ_{0s}$

Metamath Proof Explorer

Theorem n0sfincut

Proof