dfnns2

Description: Alternate definition of the positive surreal integers. Compare df-nn . (Contributed by Scott Fenton, 6-Aug-2025)

		Ref	Expression
	Assertion	dfnns2	$⊢ ℕ_{s} = rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) [ω]$

Proof

Step	Hyp	Ref	Expression
1		elnns	$⊢ i \in ℕ_{s} \leftrightarrow (i \in ℕ_{0s} \land i \neq 0_{s})$
2		df-ne	$⊢ i \neq 0_{s} \leftrightarrow \neg i = 0_{s}$
3		n0s0suc	$⊢ i \in ℕ_{0s} \to (i = 0_{s} \lor \exists j \in ℕ_{0s} i = j +_{s} 1_{s})$
4	3	ord	$⊢ i \in ℕ_{0s} \to (\neg i = 0_{s} \to \exists j \in ℕ_{0s} i = j +_{s} 1_{s})$
5	2 4	biimtrid	$⊢ i \in ℕ_{0s} \to (i \neq 0_{s} \to \exists j \in ℕ_{0s} i = j +_{s} 1_{s})$
6	5	imp	$⊢ (i \in ℕ_{0s} \land i \neq 0_{s}) \to \exists j \in ℕ_{0s} i = j +_{s} 1_{s}$
7		oveq1	$⊢ i = 0_{s} \to i +_{s} 1_{s} = 0_{s} +_{s} 1_{s}$
8		1sno	$⊢ 1_{s} \in No$
9		addslid	$⊢ 1_{s} \in No \to 0_{s} +_{s} 1_{s} = 1_{s}$
10	8 9	ax-mp	$⊢ 0_{s} +_{s} 1_{s} = 1_{s}$
11	7 10	eqtrdi	$⊢ i = 0_{s} \to i +_{s} 1_{s} = 1_{s}$
12	11	eqeq2d	$⊢ i = 0_{s} \to (({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (y) = i +_{s} 1_{s} \leftrightarrow ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (y) = 1_{s})$
13	12	rexbidv	$⊢ i = 0_{s} \to (\exists y \in ω ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (y) = i +_{s} 1_{s} \leftrightarrow \exists y \in ω ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (y) = 1_{s})$
14		oveq1	$⊢ i = k \to i +_{s} 1_{s} = k +_{s} 1_{s}$
15	14	eqeq2d	$⊢ i = k \to (({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (y) = i +_{s} 1_{s} \leftrightarrow ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (y) = k +_{s} 1_{s})$
16	15	rexbidv	$⊢ i = k \to (\exists y \in ω ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (y) = i +_{s} 1_{s} \leftrightarrow \exists y \in ω ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (y) = k +_{s} 1_{s})$
17		oveq1	$⊢ i = k +_{s} 1_{s} \to i +_{s} 1_{s} = (k +_{s} 1_{s}) +_{s} 1_{s}$
18	17	eqeq2d	$⊢ i = k +_{s} 1_{s} \to (({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (y) = i +_{s} 1_{s} \leftrightarrow ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (y) = (k +_{s} 1_{s}) +_{s} 1_{s})$
19	18	rexbidv	$⊢ i = k +_{s} 1_{s} \to (\exists y \in ω ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (y) = i +_{s} 1_{s} \leftrightarrow \exists y \in ω ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (y) = (k +_{s} 1_{s}) +_{s} 1_{s})$
20		fveqeq2	$⊢ y = z \to (({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (y) = (k +_{s} 1_{s}) +_{s} 1_{s} \leftrightarrow ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (z) = (k +_{s} 1_{s}) +_{s} 1_{s})$
21	20	cbvrexvw	$⊢ \exists y \in ω ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (y) = (k +_{s} 1_{s}) +_{s} 1_{s} \leftrightarrow \exists z \in ω ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (z) = (k +_{s} 1_{s}) +_{s} 1_{s}$
22	19 21	bitrdi	$⊢ i = k +_{s} 1_{s} \to (\exists y \in ω ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (y) = i +_{s} 1_{s} \leftrightarrow \exists z \in ω ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (z) = (k +_{s} 1_{s}) +_{s} 1_{s})$
23		oveq1	$⊢ i = j \to i +_{s} 1_{s} = j +_{s} 1_{s}$
24	23	eqeq2d	$⊢ i = j \to (({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (y) = i +_{s} 1_{s} \leftrightarrow ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (y) = j +_{s} 1_{s})$
25	24	rexbidv	$⊢ i = j \to (\exists y \in ω ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (y) = i +_{s} 1_{s} \leftrightarrow \exists y \in ω ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (y) = j +_{s} 1_{s})$
26		peano1	$⊢ \emptyset \in ω$
27		1nns	$⊢ 1_{s} \in ℕ_{s}$
28		fr0g	$⊢ 1_{s} \in ℕ_{s} \to ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (\emptyset) = 1_{s}$
29	27 28	ax-mp	$⊢ ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (\emptyset) = 1_{s}$
30		fveqeq2	$⊢ y = \emptyset \to (({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (y) = 1_{s} \leftrightarrow ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (\emptyset) = 1_{s})$
31	30	rspcev	$⊢ (\emptyset \in ω \land ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (\emptyset) = 1_{s}) \to \exists y \in ω ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (y) = 1_{s}$
32	26 29 31	mp2an	$⊢ \exists y \in ω ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (y) = 1_{s}$
33		fveqeq2	$⊢ z = suc y \to (({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (z) = ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (y) +_{s} 1_{s} \leftrightarrow ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (suc y) = ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (y) +_{s} 1_{s})$
34		peano2	$⊢ y \in ω \to suc y \in ω$
35		ovex	$⊢ ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (y) +_{s} 1_{s} \in V$
36		eqid	$⊢ {rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω} = {rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}$
37		oveq1	$⊢ z = x \to z +_{s} 1_{s} = x +_{s} 1_{s}$
38		oveq1	$⊢ z = ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (y) \to z +_{s} 1_{s} = ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (y) +_{s} 1_{s}$
39	36 37 38	frsucmpt2	$⊢ (y \in ω \land ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (y) +_{s} 1_{s} \in V) \to ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (suc y) = ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (y) +_{s} 1_{s}$
40	35 39	mpan2	$⊢ y \in ω \to ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (suc y) = ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (y) +_{s} 1_{s}$
41	33 34 40	rspcedvdw	$⊢ y \in ω \to \exists z \in ω ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (z) = ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (y) +_{s} 1_{s}$
42	41	adantl	$⊢ (k \in ℕ_{0s} \land y \in ω) \to \exists z \in ω ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (z) = ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (y) +_{s} 1_{s}$
43		oveq1	$⊢ ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (y) = k +_{s} 1_{s} \to ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (y) +_{s} 1_{s} = (k +_{s} 1_{s}) +_{s} 1_{s}$
44	43	eqeq2d	$⊢ ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (y) = k +_{s} 1_{s} \to (({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (z) = ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (y) +_{s} 1_{s} \leftrightarrow ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (z) = (k +_{s} 1_{s}) +_{s} 1_{s})$
45	44	rexbidv	$⊢ ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (y) = k +_{s} 1_{s} \to (\exists z \in ω ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (z) = ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (y) +_{s} 1_{s} \leftrightarrow \exists z \in ω ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (z) = (k +_{s} 1_{s}) +_{s} 1_{s})$
46	42 45	syl5ibcom	$⊢ (k \in ℕ_{0s} \land y \in ω) \to (({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (y) = k +_{s} 1_{s} \to \exists z \in ω ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (z) = (k +_{s} 1_{s}) +_{s} 1_{s})$
47	46	rexlimdva	$⊢ k \in ℕ_{0s} \to (\exists y \in ω ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (y) = k +_{s} 1_{s} \to \exists z \in ω ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (z) = (k +_{s} 1_{s}) +_{s} 1_{s})$
48	13 16 22 25 32 47	n0sind	$⊢ j \in ℕ_{0s} \to \exists y \in ω ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (y) = j +_{s} 1_{s}$
49		frfnom	$⊢ ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) Fn ω$
50		fvelrnb	$⊢ ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) Fn ω \to (j +_{s} 1_{s} \in ran ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) \leftrightarrow \exists y \in ω ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (y) = j +_{s} 1_{s})$
51	49 50	ax-mp	$⊢ j +_{s} 1_{s} \in ran ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) \leftrightarrow \exists y \in ω ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (y) = j +_{s} 1_{s}$
52	48 51	sylibr	$⊢ j \in ℕ_{0s} \to j +_{s} 1_{s} \in ran ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω})$
53		df-ima	$⊢ rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) [ω] = ran ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω})$
54	52 53	eleqtrrdi	$⊢ j \in ℕ_{0s} \to j +_{s} 1_{s} \in rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) [ω]$
55		eleq1	$⊢ i = j +_{s} 1_{s} \to (i \in rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) [ω] \leftrightarrow j +_{s} 1_{s} \in rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) [ω])$
56	54 55	syl5ibrcom	$⊢ j \in ℕ_{0s} \to (i = j +_{s} 1_{s} \to i \in rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) [ω])$
57	56	rexlimiv	$⊢ \exists j \in ℕ_{0s} i = j +_{s} 1_{s} \to i \in rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) [ω]$
58	6 57	syl	$⊢ (i \in ℕ_{0s} \land i \neq 0_{s}) \to i \in rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) [ω]$
59	1 58	sylbi	$⊢ i \in ℕ_{s} \to i \in rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) [ω]$
60	59	ssriv	$⊢ ℕ_{s} \subseteq rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) [ω]$
61		fveq2	$⊢ k = \emptyset \to ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (k) = ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (\emptyset)$
62	61	eleq1d	$⊢ k = \emptyset \to (({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (k) \in ℕ_{s} \leftrightarrow ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (\emptyset) \in ℕ_{s})$
63		fveq2	$⊢ k = j \to ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (k) = ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (j)$
64	63	eleq1d	$⊢ k = j \to (({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (k) \in ℕ_{s} \leftrightarrow ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (j) \in ℕ_{s})$
65		fveq2	$⊢ k = suc j \to ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (k) = ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (suc j)$
66	65	eleq1d	$⊢ k = suc j \to (({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (k) \in ℕ_{s} \leftrightarrow ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (suc j) \in ℕ_{s})$
67		fveq2	$⊢ k = i \to ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (k) = ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (i)$
68	67	eleq1d	$⊢ k = i \to (({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (k) \in ℕ_{s} \leftrightarrow ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (i) \in ℕ_{s})$
69	29 27	eqeltri	$⊢ ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (\emptyset) \in ℕ_{s}$
70		peano2nns	$⊢ ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (j) \in ℕ_{s} \to ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (j) +_{s} 1_{s} \in ℕ_{s}$
71		ovex	$⊢ ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (j) +_{s} 1_{s} \in V$
72		oveq1	$⊢ y = x \to y +_{s} 1_{s} = x +_{s} 1_{s}$
73		oveq1	$⊢ y = ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (j) \to y +_{s} 1_{s} = ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (j) +_{s} 1_{s}$
74	36 72 73	frsucmpt2	$⊢ (j \in ω \land ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (j) +_{s} 1_{s} \in V) \to ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (suc j) = ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (j) +_{s} 1_{s}$
75	71 74	mpan2	$⊢ j \in ω \to ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (suc j) = ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (j) +_{s} 1_{s}$
76	75	eleq1d	$⊢ j \in ω \to (({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (suc j) \in ℕ_{s} \leftrightarrow ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (j) +_{s} 1_{s} \in ℕ_{s})$
77	70 76	imbitrrid	$⊢ j \in ω \to (({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (j) \in ℕ_{s} \to ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (suc j) \in ℕ_{s})$
78	62 64 66 68 69 77	finds	$⊢ i \in ω \to ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (i) \in ℕ_{s}$
79	78	rgen	$⊢ \forall i \in ω ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (i) \in ℕ_{s}$
80		fnfvrnss	$⊢ (({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) Fn ω \land \forall i \in ω ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) (i) \in ℕ_{s}) \to ran ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) \subseteq ℕ_{s}$
81	49 79 80	mp2an	$⊢ ran ({rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) ↾}_{ω}) \subseteq ℕ_{s}$
82	53 81	eqsstri	$⊢ rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) [ω] \subseteq ℕ_{s}$
83	60 82	eqssi	$⊢ ℕ_{s} = rec ((x \in V ⟼ x +_{s} 1_{s}), 1_{s}) [ω]$

Metamath Proof Explorer

Theorem dfnns2

Proof