indpi

Description: Principle of Finite Induction on positive integers. (Contributed by NM, 23-Mar-1996) (New usage is discouraged.)

	Ref	Expression
Hypotheses	indpi.1	$⊢ x = 1_{𝑜} \to (φ \leftrightarrow ψ)$
	indpi.2	$⊢ x = y \to (φ \leftrightarrow χ)$
	indpi.3	$⊢ x = y +_{𝑵} 1_{𝑜} \to (φ \leftrightarrow θ)$
	indpi.4	$⊢ x = A \to (φ \leftrightarrow τ)$
	indpi.5	$⊢ ψ$
	indpi.6	$⊢ y \in 𝑵 \to (χ \to θ)$
Assertion	indpi	$⊢ A \in 𝑵 \to τ$

Proof

Step	Hyp	Ref	Expression
1		indpi.1	$⊢ x = 1_{𝑜} \to (φ \leftrightarrow ψ)$
2		indpi.2	$⊢ x = y \to (φ \leftrightarrow χ)$
3		indpi.3	$⊢ x = y +_{𝑵} 1_{𝑜} \to (φ \leftrightarrow θ)$
4		indpi.4	$⊢ x = A \to (φ \leftrightarrow τ)$
5		indpi.5	$⊢ ψ$
6		indpi.6	$⊢ y \in 𝑵 \to (χ \to θ)$
7		1oex	$⊢ 1_{𝑜} \in V$
8	7	eqvinc	$⊢ 1_{𝑜} = A \leftrightarrow \exists x (x = 1_{𝑜} \land x = A)$
9	5 1	mpbiri	$⊢ x = 1_{𝑜} \to φ$
10	8 4 9	gencl	$⊢ 1_{𝑜} = A \to τ$
11	10	eqcoms	$⊢ A = 1_{𝑜} \to τ$
12	11	a1i	$⊢ A \in 𝑵 \to (A = 1_{𝑜} \to τ)$
13		pinn	$⊢ A \in 𝑵 \to A \in ω$
14		elni2	$⊢ A \in 𝑵 \leftrightarrow (A \in ω \land \emptyset \in A)$
15		nnord	$⊢ A \in ω \to Ord A$
16		ordsucss	$⊢ Ord A \to (\emptyset \in A \to suc \emptyset \subseteq A)$
17	15 16	syl	$⊢ A \in ω \to (\emptyset \in A \to suc \emptyset \subseteq A)$
18		df-1o	$⊢ 1_{𝑜} = suc \emptyset$
19	18	sseq1i	$⊢ 1_{𝑜} \subseteq A \leftrightarrow suc \emptyset \subseteq A$
20	17 19	imbitrrdi	$⊢ A \in ω \to (\emptyset \in A \to 1_{𝑜} \subseteq A)$
21	20	imp	$⊢ (A \in ω \land \emptyset \in A) \to 1_{𝑜} \subseteq A$
22	14 21	sylbi	$⊢ A \in 𝑵 \to 1_{𝑜} \subseteq A$
23		1onn	$⊢ 1_{𝑜} \in ω$
24		eleq1	$⊢ x = 1_{𝑜} \to (x \in 𝑵 \leftrightarrow 1_{𝑜} \in 𝑵)$
25		breq2	$⊢ x = 1_{𝑜} \to (1_{𝑜} <_{𝑵} x \leftrightarrow 1_{𝑜} <_{𝑵} 1_{𝑜})$
26	24 25	anbi12d	$⊢ x = 1_{𝑜} \to ((x \in 𝑵 \land 1_{𝑜} <_{𝑵} x) \leftrightarrow (1_{𝑜} \in 𝑵 \land 1_{𝑜} <_{𝑵} 1_{𝑜}))$
27	26 1	imbi12d	$⊢ x = 1_{𝑜} \to (((x \in 𝑵 \land 1_{𝑜} <_{𝑵} x) \to φ) \leftrightarrow ((1_{𝑜} \in 𝑵 \land 1_{𝑜} <_{𝑵} 1_{𝑜}) \to ψ))$
28		eleq1	$⊢ x = y \to (x \in 𝑵 \leftrightarrow y \in 𝑵)$
29		breq2	$⊢ x = y \to (1_{𝑜} <_{𝑵} x \leftrightarrow 1_{𝑜} <_{𝑵} y)$
30	28 29	anbi12d	$⊢ x = y \to ((x \in 𝑵 \land 1_{𝑜} <_{𝑵} x) \leftrightarrow (y \in 𝑵 \land 1_{𝑜} <_{𝑵} y))$
31	30 2	imbi12d	$⊢ x = y \to (((x \in 𝑵 \land 1_{𝑜} <_{𝑵} x) \to φ) \leftrightarrow ((y \in 𝑵 \land 1_{𝑜} <_{𝑵} y) \to χ))$
32		pinn	$⊢ x \in 𝑵 \to x \in ω$
33		eleq1	$⊢ x = suc y \to (x \in ω \leftrightarrow suc y \in ω)$
34		peano2b	$⊢ y \in ω \leftrightarrow suc y \in ω$
35	33 34	bitr4di	$⊢ x = suc y \to (x \in ω \leftrightarrow y \in ω)$
36	32 35	imbitrid	$⊢ x = suc y \to (x \in 𝑵 \to y \in ω)$
37	36	adantrd	$⊢ x = suc y \to ((x \in 𝑵 \land 1_{𝑜} <_{𝑵} x) \to y \in ω)$
38		1pi	$⊢ 1_{𝑜} \in 𝑵$
39		ltpiord	$⊢ (1_{𝑜} \in 𝑵 \land x \in 𝑵) \to (1_{𝑜} <_{𝑵} x \leftrightarrow 1_{𝑜} \in x)$
40	38 39	mpan	$⊢ x \in 𝑵 \to (1_{𝑜} <_{𝑵} x \leftrightarrow 1_{𝑜} \in x)$
41	40	biimpa	$⊢ (x \in 𝑵 \land 1_{𝑜} <_{𝑵} x) \to 1_{𝑜} \in x$
42		eleq2	$⊢ x = suc y \to (1_{𝑜} \in x \leftrightarrow 1_{𝑜} \in suc y)$
43		elsuci	$⊢ 1_{𝑜} \in suc y \to (1_{𝑜} \in y \lor 1_{𝑜} = y)$
44		ne0i	$⊢ 1_{𝑜} \in y \to y \neq \emptyset$
45		0lt1o	$⊢ \emptyset \in 1_{𝑜}$
46		eleq2	$⊢ 1_{𝑜} = y \to (\emptyset \in 1_{𝑜} \leftrightarrow \emptyset \in y)$
47	45 46	mpbii	$⊢ 1_{𝑜} = y \to \emptyset \in y$
48	47	ne0d	$⊢ 1_{𝑜} = y \to y \neq \emptyset$
49	44 48	jaoi	$⊢ (1_{𝑜} \in y \lor 1_{𝑜} = y) \to y \neq \emptyset$
50	43 49	syl	$⊢ 1_{𝑜} \in suc y \to y \neq \emptyset$
51	42 50	biimtrdi	$⊢ x = suc y \to (1_{𝑜} \in x \to y \neq \emptyset)$
52	41 51	syl5	$⊢ x = suc y \to ((x \in 𝑵 \land 1_{𝑜} <_{𝑵} x) \to y \neq \emptyset)$
53	37 52	jcad	$⊢ x = suc y \to ((x \in 𝑵 \land 1_{𝑜} <_{𝑵} x) \to (y \in ω \land y \neq \emptyset))$
54		elni	$⊢ y \in 𝑵 \leftrightarrow (y \in ω \land y \neq \emptyset)$
55	53 54	imbitrrdi	$⊢ x = suc y \to ((x \in 𝑵 \land 1_{𝑜} <_{𝑵} x) \to y \in 𝑵)$
56		simpr	$⊢ (x \in 𝑵 \land 1_{𝑜} <_{𝑵} x) \to 1_{𝑜} <_{𝑵} x$
57		breq2	$⊢ x = suc y \to (1_{𝑜} <_{𝑵} x \leftrightarrow 1_{𝑜} <_{𝑵} suc y)$
58	56 57	imbitrid	$⊢ x = suc y \to ((x \in 𝑵 \land 1_{𝑜} <_{𝑵} x) \to 1_{𝑜} <_{𝑵} suc y)$
59	55 58	jcad	$⊢ x = suc y \to ((x \in 𝑵 \land 1_{𝑜} <_{𝑵} x) \to (y \in 𝑵 \land 1_{𝑜} <_{𝑵} suc y))$
60		addclpi	$⊢ (y \in 𝑵 \land 1_{𝑜} \in 𝑵) \to y +_{𝑵} 1_{𝑜} \in 𝑵$
61	38 60	mpan2	$⊢ y \in 𝑵 \to y +_{𝑵} 1_{𝑜} \in 𝑵$
62		addpiord	$⊢ (y \in 𝑵 \land 1_{𝑜} \in 𝑵) \to y +_{𝑵} 1_{𝑜} = y +_{𝑜} 1_{𝑜}$
63	38 62	mpan2	$⊢ y \in 𝑵 \to y +_{𝑵} 1_{𝑜} = y +_{𝑜} 1_{𝑜}$
64		pion	$⊢ y \in 𝑵 \to y \in On$
65		oa1suc	$⊢ y \in On \to y +_{𝑜} 1_{𝑜} = suc y$
66	64 65	syl	$⊢ y \in 𝑵 \to y +_{𝑜} 1_{𝑜} = suc y$
67	63 66	eqtrd	$⊢ y \in 𝑵 \to y +_{𝑵} 1_{𝑜} = suc y$
68	67	eqeq2d	$⊢ y \in 𝑵 \to (x = y +_{𝑵} 1_{𝑜} \leftrightarrow x = suc y)$
69	68	biimparc	$⊢ (x = suc y \land y \in 𝑵) \to x = y +_{𝑵} 1_{𝑜}$
70	69	eleq1d	$⊢ (x = suc y \land y \in 𝑵) \to (x \in 𝑵 \leftrightarrow y +_{𝑵} 1_{𝑜} \in 𝑵)$
71	61 70	imbitrrid	$⊢ (x = suc y \land y \in 𝑵) \to (y \in 𝑵 \to x \in 𝑵)$
72	71	ex	$⊢ x = suc y \to (y \in 𝑵 \to (y \in 𝑵 \to x \in 𝑵))$
73	72	pm2.43d	$⊢ x = suc y \to (y \in 𝑵 \to x \in 𝑵)$
74	57	biimprd	$⊢ x = suc y \to (1_{𝑜} <_{𝑵} suc y \to 1_{𝑜} <_{𝑵} x)$
75	73 74	anim12d	$⊢ x = suc y \to ((y \in 𝑵 \land 1_{𝑜} <_{𝑵} suc y) \to (x \in 𝑵 \land 1_{𝑜} <_{𝑵} x))$
76	59 75	impbid	$⊢ x = suc y \to ((x \in 𝑵 \land 1_{𝑜} <_{𝑵} x) \leftrightarrow (y \in 𝑵 \land 1_{𝑜} <_{𝑵} suc y))$
77	76	imbi1d	$⊢ x = suc y \to (((x \in 𝑵 \land 1_{𝑜} <_{𝑵} x) \to φ) \leftrightarrow ((y \in 𝑵 \land 1_{𝑜} <_{𝑵} suc y) \to φ))$
78	68 3	biimtrrdi	$⊢ y \in 𝑵 \to (x = suc y \to (φ \leftrightarrow θ))$
79	78	adantr	$⊢ (y \in 𝑵 \land 1_{𝑜} <_{𝑵} suc y) \to (x = suc y \to (φ \leftrightarrow θ))$
80	79	com12	$⊢ x = suc y \to ((y \in 𝑵 \land 1_{𝑜} <_{𝑵} suc y) \to (φ \leftrightarrow θ))$
81	80	pm5.74d	$⊢ x = suc y \to (((y \in 𝑵 \land 1_{𝑜} <_{𝑵} suc y) \to φ) \leftrightarrow ((y \in 𝑵 \land 1_{𝑜} <_{𝑵} suc y) \to θ))$
82	77 81	bitrd	$⊢ x = suc y \to (((x \in 𝑵 \land 1_{𝑜} <_{𝑵} x) \to φ) \leftrightarrow ((y \in 𝑵 \land 1_{𝑜} <_{𝑵} suc y) \to θ))$
83		eleq1	$⊢ x = A \to (x \in 𝑵 \leftrightarrow A \in 𝑵)$
84		breq2	$⊢ x = A \to (1_{𝑜} <_{𝑵} x \leftrightarrow 1_{𝑜} <_{𝑵} A)$
85	83 84	anbi12d	$⊢ x = A \to ((x \in 𝑵 \land 1_{𝑜} <_{𝑵} x) \leftrightarrow (A \in 𝑵 \land 1_{𝑜} <_{𝑵} A))$
86	85 4	imbi12d	$⊢ x = A \to (((x \in 𝑵 \land 1_{𝑜} <_{𝑵} x) \to φ) \leftrightarrow ((A \in 𝑵 \land 1_{𝑜} <_{𝑵} A) \to τ))$
87	5	2a1i	$⊢ 1_{𝑜} \in ω \to ((1_{𝑜} \in 𝑵 \land 1_{𝑜} <_{𝑵} 1_{𝑜}) \to ψ)$
88		ltpiord	$⊢ (1_{𝑜} \in 𝑵 \land y \in 𝑵) \to (1_{𝑜} <_{𝑵} y \leftrightarrow 1_{𝑜} \in y)$
89	38 88	mpan	$⊢ y \in 𝑵 \to (1_{𝑜} <_{𝑵} y \leftrightarrow 1_{𝑜} \in y)$
90	89	pm5.32i	$⊢ (y \in 𝑵 \land 1_{𝑜} <_{𝑵} y) \leftrightarrow (y \in 𝑵 \land 1_{𝑜} \in y)$
91	90	simplbi2	$⊢ y \in 𝑵 \to (1_{𝑜} \in y \to (y \in 𝑵 \land 1_{𝑜} <_{𝑵} y))$
92	91	imim1d	$⊢ y \in 𝑵 \to (((y \in 𝑵 \land 1_{𝑜} <_{𝑵} y) \to χ) \to (1_{𝑜} \in y \to χ))$
93		ltrelpi	$⊢ <_{𝑵} \subseteq 𝑵 \times 𝑵$
94	93	brel	$⊢ 1_{𝑜} <_{𝑵} suc y \to (1_{𝑜} \in 𝑵 \land suc y \in 𝑵)$
95		ltpiord	$⊢ (1_{𝑜} \in 𝑵 \land suc y \in 𝑵) \to (1_{𝑜} <_{𝑵} suc y \leftrightarrow 1_{𝑜} \in suc y)$
96	94 95	syl	$⊢ 1_{𝑜} <_{𝑵} suc y \to (1_{𝑜} <_{𝑵} suc y \leftrightarrow 1_{𝑜} \in suc y)$
97	96	ibi	$⊢ 1_{𝑜} <_{𝑵} suc y \to 1_{𝑜} \in suc y$
98	7	eqvinc	$⊢ 1_{𝑜} = y \leftrightarrow \exists x (x = 1_{𝑜} \land x = y)$
99	98 2 9	gencl	$⊢ 1_{𝑜} = y \to χ$
100		jao	$⊢ (1_{𝑜} \in y \to χ) \to ((1_{𝑜} = y \to χ) \to ((1_{𝑜} \in y \lor 1_{𝑜} = y) \to χ))$
101	99 100	mpi	$⊢ (1_{𝑜} \in y \to χ) \to ((1_{𝑜} \in y \lor 1_{𝑜} = y) \to χ)$
102	43 101	syl5	$⊢ (1_{𝑜} \in y \to χ) \to (1_{𝑜} \in suc y \to χ)$
103	97 102	syl5	$⊢ (1_{𝑜} \in y \to χ) \to (1_{𝑜} <_{𝑵} suc y \to χ)$
104	92 103	syl6com	$⊢ ((y \in 𝑵 \land 1_{𝑜} <_{𝑵} y) \to χ) \to (y \in 𝑵 \to (1_{𝑜} <_{𝑵} suc y \to χ))$
105	104	impd	$⊢ ((y \in 𝑵 \land 1_{𝑜} <_{𝑵} y) \to χ) \to ((y \in 𝑵 \land 1_{𝑜} <_{𝑵} suc y) \to χ)$
106	18	sseq1i	$⊢ 1_{𝑜} \subseteq y \leftrightarrow suc \emptyset \subseteq y$
107		0ex	$⊢ \emptyset \in V$
108		sucssel	$⊢ \emptyset \in V \to (suc \emptyset \subseteq y \to \emptyset \in y)$
109	107 108	ax-mp	$⊢ suc \emptyset \subseteq y \to \emptyset \in y$
110	106 109	sylbi	$⊢ 1_{𝑜} \subseteq y \to \emptyset \in y$
111		elni2	$⊢ y \in 𝑵 \leftrightarrow (y \in ω \land \emptyset \in y)$
112	111 6	sylbir	$⊢ (y \in ω \land \emptyset \in y) \to (χ \to θ)$
113	110 112	sylan2	$⊢ (y \in ω \land 1_{𝑜} \subseteq y) \to (χ \to θ)$
114	105 113	syl9r	$⊢ (y \in ω \land 1_{𝑜} \subseteq y) \to (((y \in 𝑵 \land 1_{𝑜} <_{𝑵} y) \to χ) \to ((y \in 𝑵 \land 1_{𝑜} <_{𝑵} suc y) \to θ))$
115	114	adantlr	$⊢ ((y \in ω \land 1_{𝑜} \in ω) \land 1_{𝑜} \subseteq y) \to (((y \in 𝑵 \land 1_{𝑜} <_{𝑵} y) \to χ) \to ((y \in 𝑵 \land 1_{𝑜} <_{𝑵} suc y) \to θ))$
116	27 31 82 86 87 115	findsg	$⊢ ((A \in ω \land 1_{𝑜} \in ω) \land 1_{𝑜} \subseteq A) \to ((A \in 𝑵 \land 1_{𝑜} <_{𝑵} A) \to τ)$
117	23 116	mpanl2	$⊢ (A \in ω \land 1_{𝑜} \subseteq A) \to ((A \in 𝑵 \land 1_{𝑜} <_{𝑵} A) \to τ)$
118	13 22 117	syl2anc	$⊢ A \in 𝑵 \to ((A \in 𝑵 \land 1_{𝑜} <_{𝑵} A) \to τ)$
119	118	expd	$⊢ A \in 𝑵 \to (A \in 𝑵 \to (1_{𝑜} <_{𝑵} A \to τ))$
120	119	pm2.43i	$⊢ A \in 𝑵 \to (1_{𝑜} <_{𝑵} A \to τ)$
121		nlt1pi	$⊢ \neg A <_{𝑵} 1_{𝑜}$
122		ltsopi	$⊢ <_{𝑵} Or 𝑵$
123		sotric	$⊢ (<_{𝑵} Or 𝑵 \land (A \in 𝑵 \land 1_{𝑜} \in 𝑵)) \to (A <_{𝑵} 1_{𝑜} \leftrightarrow \neg (A = 1_{𝑜} \lor 1_{𝑜} <_{𝑵} A))$
124	122 123	mpan	$⊢ (A \in 𝑵 \land 1_{𝑜} \in 𝑵) \to (A <_{𝑵} 1_{𝑜} \leftrightarrow \neg (A = 1_{𝑜} \lor 1_{𝑜} <_{𝑵} A))$
125	38 124	mpan2	$⊢ A \in 𝑵 \to (A <_{𝑵} 1_{𝑜} \leftrightarrow \neg (A = 1_{𝑜} \lor 1_{𝑜} <_{𝑵} A))$
126	121 125	mtbii	$⊢ A \in 𝑵 \to \neg \neg (A = 1_{𝑜} \lor 1_{𝑜} <_{𝑵} A)$
127	126	notnotrd	$⊢ A \in 𝑵 \to (A = 1_{𝑜} \lor 1_{𝑜} <_{𝑵} A)$
128	12 120 127	mpjaod	$⊢ A \in 𝑵 \to τ$

Metamath Proof Explorer

Theorem indpi

Proof