n0fincut

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	n0fincut	$⊢ (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		ltsso	$⊢ <_{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		lenlts	$⊢ (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		nulsgts	$⊢ \{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		lesid	$⊢ 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	cutscld	$⊢ ((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		lltr	$⊢ 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	63 64 67 68	ltsrecd	$⊢ (((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)))$
70	61 69	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)$
71	50 51 52 56 70	leltstrd	$⊢ (((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)$
72		velsn	$⊢ w \in \{\{x\} \|_{s} \emptyset\} \leftrightarrow w = \{x\} \|_{s} \emptyset$
73		breq2	$⊢ w = \{x\} \|_{s} \emptyset \to (z <_{s} w \leftrightarrow z <_{s} (\{x\} \|_{s} \emptyset))$
74	72 73	sylbi	$⊢ w \in \{\{x\} \|_{s} \emptyset\} \to (z <_{s} w \leftrightarrow z <_{s} (\{x\} \|_{s} \emptyset))$
75	71 74	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)$
76	75	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$
77	44 46 47 49 76	sltsd	$⊢ ((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\}$
78		snelpwi	$⊢ \{x\} \|_{s} \emptyset \in No \to \{\{x\} \|_{s} \emptyset\} \in 𝒫 No$
79		nulsgts	$⊢ \{\{x\} \|_{s} \emptyset\} \in 𝒫 No \to \{\{x\} \|_{s} \emptyset\} ≪_{s} \emptyset$
80	48 78 79	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$
81	31 41 43 77 80	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$
82	81	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$
83		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}$
84	83 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}$
85	84	peano2n0sd	$⊢ ((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}$
86		n0cut	$⊢ x +_{s} 1_{s} \in ℕ_{0s} \to x +_{s} 1_{s} = \{(x +_{s} 1_{s}) -_{s} 1_{s}\} \|_{s} \emptyset$
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} = \{(x +_{s} 1_{s}) -_{s} 1_{s}\} \|_{s} \emptyset$
88		1no	$⊢ 1_{s} \in No$
89		pncans	$⊢ (x \in No \land 1_{s} \in No) \to (x +_{s} 1_{s}) -_{s} 1_{s} = x$
90	28 88 89	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$
91	90	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\}$
92	91	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$
93	87 92	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}$
94	93 85	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}$
95	82 94	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}$
96	95	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})$
97	25 96	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})$
98	97	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})$
99	17 98	mpd	$⊢ (A \neq \emptyset \land (A \subseteq ℕ_{0s} \land A \in Fin)) \to A \|_{s} \emptyset \in ℕ_{0s}$
100	99	ex	$⊢ A \neq \emptyset \to ((A \subseteq ℕ_{0s} \land A \in Fin) \to A \|_{s} \emptyset \in ℕ_{0s})$
101	6 100	pm2.61ine	$⊢ (A \subseteq ℕ_{0s} \land A \in Fin) \to A \|_{s} \emptyset \in ℕ_{0s}$

Metamath Proof Explorer

Theorem n0fincut

Proof