peano5uzs

Description: Peano's inductive postulate for upper surreal integers. (Contributed by Scott Fenton, 25-Jul-2025)

	Ref	Expression
Hypotheses	peano5uzs.1	$⊢ φ \to N \in ℤ_{s}$
	peano5uzs.2	$⊢ φ \to N \in A$
	peano5uzs.3	$⊢ (φ \land x \in A) \to x +_{s} 1_{s} \in A$
Assertion	peano5uzs	$⊢ φ \to \{k \in ℤ_{s} \| N \leq_{s} k\} \subseteq A$

Proof

Step	Hyp	Ref	Expression
1		peano5uzs.1	$⊢ φ \to N \in ℤ_{s}$
2		peano5uzs.2	$⊢ φ \to N \in A$
3		peano5uzs.3	$⊢ (φ \land x \in A) \to x +_{s} 1_{s} \in A$
4		breq2	$⊢ k = n \to (N \leq_{s} k \leftrightarrow N \leq_{s} n)$
5	4	elrab	$⊢ n \in \{k \in ℤ_{s} \| N \leq_{s} k\} \leftrightarrow (n \in ℤ_{s} \land N \leq_{s} n)$
6		zno	$⊢ n \in ℤ_{s} \to n \in No$
7	6	adantr	$⊢ (n \in ℤ_{s} \land N \leq_{s} n) \to n \in No$
8	1	znod	$⊢ φ \to N \in No$
9		npcans	$⊢ (n \in No \land N \in No) \to (n -_{s} N) +_{s} N = n$
10	7 8 9	syl2anr	$⊢ (φ \land (n \in ℤ_{s} \land N \leq_{s} n)) \to (n -_{s} N) +_{s} N = n$
11		simprl	$⊢ (φ \land (n \in ℤ_{s} \land N \leq_{s} n)) \to n \in ℤ_{s}$
12	1	adantr	$⊢ (φ \land (n \in ℤ_{s} \land N \leq_{s} n)) \to N \in ℤ_{s}$
13	11 12	zsubscld	$⊢ (φ \land (n \in ℤ_{s} \land N \leq_{s} n)) \to n -_{s} N \in ℤ_{s}$
14	6	adantl	$⊢ (φ \land n \in ℤ_{s}) \to n \in No$
15	8	adantr	$⊢ (φ \land n \in ℤ_{s}) \to N \in No$
16	14 15	subsge0d	$⊢ (φ \land n \in ℤ_{s}) \to (0_{s} \leq_{s} (n -_{s} N) \leftrightarrow N \leq_{s} n)$
17	16	biimpar	$⊢ ((φ \land n \in ℤ_{s}) \land N \leq_{s} n) \to 0_{s} \leq_{s} (n -_{s} N)$
18	17	anasss	$⊢ (φ \land (n \in ℤ_{s} \land N \leq_{s} n)) \to 0_{s} \leq_{s} (n -_{s} N)$
19	13 18	jca	$⊢ (φ \land (n \in ℤ_{s} \land N \leq_{s} n)) \to (n -_{s} N \in ℤ_{s} \land 0_{s} \leq_{s} (n -_{s} N))$
20		eln0zs	$⊢ n -_{s} N \in ℕ_{0s} \leftrightarrow (n -_{s} N \in ℤ_{s} \land 0_{s} \leq_{s} (n -_{s} N))$
21	19 20	sylibr	$⊢ (φ \land (n \in ℤ_{s} \land N \leq_{s} n)) \to n -_{s} N \in ℕ_{0s}$
22	21	ex	$⊢ φ \to ((n \in ℤ_{s} \land N \leq_{s} n) \to n -_{s} N \in ℕ_{0s})$
23		oveq1	$⊢ z = 0_{s} \to z +_{s} N = 0_{s} +_{s} N$
24	23	eleq1d	$⊢ z = 0_{s} \to (z +_{s} N \in A \leftrightarrow 0_{s} +_{s} N \in A)$
25	24	imbi2d	$⊢ z = 0_{s} \to ((φ \to z +_{s} N \in A) \leftrightarrow (φ \to 0_{s} +_{s} N \in A))$
26		oveq1	$⊢ z = y \to z +_{s} N = y +_{s} N$
27	26	eleq1d	$⊢ z = y \to (z +_{s} N \in A \leftrightarrow y +_{s} N \in A)$
28	27	imbi2d	$⊢ z = y \to ((φ \to z +_{s} N \in A) \leftrightarrow (φ \to y +_{s} N \in A))$
29		oveq1	$⊢ z = y +_{s} 1_{s} \to z +_{s} N = (y +_{s} 1_{s}) +_{s} N$
30	29	eleq1d	$⊢ z = y +_{s} 1_{s} \to (z +_{s} N \in A \leftrightarrow (y +_{s} 1_{s}) +_{s} N \in A)$
31	30	imbi2d	$⊢ z = y +_{s} 1_{s} \to ((φ \to z +_{s} N \in A) \leftrightarrow (φ \to (y +_{s} 1_{s}) +_{s} N \in A))$
32		oveq1	$⊢ z = n -_{s} N \to z +_{s} N = (n -_{s} N) +_{s} N$
33	32	eleq1d	$⊢ z = n -_{s} N \to (z +_{s} N \in A \leftrightarrow (n -_{s} N) +_{s} N \in A)$
34	33	imbi2d	$⊢ z = n -_{s} N \to ((φ \to z +_{s} N \in A) \leftrightarrow (φ \to (n -_{s} N) +_{s} N \in A))$
35		addslid	$⊢ N \in No \to 0_{s} +_{s} N = N$
36	8 35	syl	$⊢ φ \to 0_{s} +_{s} N = N$
37	36 2	eqeltrd	$⊢ φ \to 0_{s} +_{s} N \in A$
38	3	ralrimiva	$⊢ φ \to \forall x \in A x +_{s} 1_{s} \in A$
39		oveq1	$⊢ x = y +_{s} N \to x +_{s} 1_{s} = (y +_{s} N) +_{s} 1_{s}$
40	39	eleq1d	$⊢ x = y +_{s} N \to (x +_{s} 1_{s} \in A \leftrightarrow (y +_{s} N) +_{s} 1_{s} \in A)$
41	40	rspccv	$⊢ \forall x \in A x +_{s} 1_{s} \in A \to (y +_{s} N \in A \to (y +_{s} N) +_{s} 1_{s} \in A)$
42	38 41	syl	$⊢ φ \to (y +_{s} N \in A \to (y +_{s} N) +_{s} 1_{s} \in A)$
43	42	adantl	$⊢ (y \in ℕ_{0s} \land φ) \to (y +_{s} N \in A \to (y +_{s} N) +_{s} 1_{s} \in A)$
44		n0sno	$⊢ y \in ℕ_{0s} \to y \in No$
45	44	adantr	$⊢ (y \in ℕ_{0s} \land φ) \to y \in No$
46		1sno	$⊢ 1_{s} \in No$
47	46	a1i	$⊢ (y \in ℕ_{0s} \land φ) \to 1_{s} \in No$
48	8	adantl	$⊢ (y \in ℕ_{0s} \land φ) \to N \in No$
49	45 47 48	adds32d	$⊢ (y \in ℕ_{0s} \land φ) \to (y +_{s} 1_{s}) +_{s} N = (y +_{s} N) +_{s} 1_{s}$
50	49	eleq1d	$⊢ (y \in ℕ_{0s} \land φ) \to ((y +_{s} 1_{s}) +_{s} N \in A \leftrightarrow (y +_{s} N) +_{s} 1_{s} \in A)$
51	43 50	sylibrd	$⊢ (y \in ℕ_{0s} \land φ) \to (y +_{s} N \in A \to (y +_{s} 1_{s}) +_{s} N \in A)$
52	51	ex	$⊢ y \in ℕ_{0s} \to (φ \to (y +_{s} N \in A \to (y +_{s} 1_{s}) +_{s} N \in A))$
53	52	a2d	$⊢ y \in ℕ_{0s} \to ((φ \to y +_{s} N \in A) \to (φ \to (y +_{s} 1_{s}) +_{s} N \in A))$
54	25 28 31 34 37 53	n0sind	$⊢ n -_{s} N \in ℕ_{0s} \to (φ \to (n -_{s} N) +_{s} N \in A)$
55	54	com12	$⊢ φ \to (n -_{s} N \in ℕ_{0s} \to (n -_{s} N) +_{s} N \in A)$
56	22 55	syld	$⊢ φ \to ((n \in ℤ_{s} \land N \leq_{s} n) \to (n -_{s} N) +_{s} N \in A)$
57	56	imp	$⊢ (φ \land (n \in ℤ_{s} \land N \leq_{s} n)) \to (n -_{s} N) +_{s} N \in A$
58	10 57	eqeltrrd	$⊢ (φ \land (n \in ℤ_{s} \land N \leq_{s} n)) \to n \in A$
59	58	ex	$⊢ φ \to ((n \in ℤ_{s} \land N \leq_{s} n) \to n \in A)$
60	5 59	biimtrid	$⊢ φ \to (n \in \{k \in ℤ_{s} \| N \leq_{s} k\} \to n \in A)$
61	60	ssrdv	$⊢ φ \to \{k \in ℤ_{s} \| N \leq_{s} k\} \subseteq A$

Metamath Proof Explorer

Theorem peano5uzs

Proof