Metamath Proof Explorer

Metamath Proof Explorer

< Previous Next >
Related theorems
GIF version

Theorem indpi 3828

Description: Principle of Finite Induction on positive integers.

**Hypotheses**
Ref	Expression
indpi.1	⊢ (x = 1_o → (φ ↔ ψ))
indpi.2	⊢ (x = y → (φ ↔ χ))
indpi.3	⊢ (x = (y +_N 1_o) → (φ ↔ θ))
indpi.4	⊢ (x = A → (φ ↔ τ))
indpi.5	⊢ ψ
indpi.6	⊢ (y ∈ N → (χ → θ))

**Assertion**
Ref	Expression
indpi	⊢ (A ∈ N → τ)

Distinct variable group(s): x,y x,A ψ,x χ,x θ,x τ,x φ,y

**Proof of Theorem indpi**
Step	Hyp	Ref	Expression
1		nlt1pi 3827	. . . 4 ⊢ ¬ A <_N 1_o
2		1pi 3805	. . . . 5 ⊢ 1_o ∈ N
3		ltsopi 3810	. . . . . 6 ⊢ <_N Or N
4		sotric 2148	. . . . . 6 ⊢ (( <_N Or N ∧ (A ∈ N ∧ 1_o ∈ N)) → (A <_N 1_o ↔ ¬ (A = 1_o ∨ 1_o <_N A)))
5	3, 4	mpan 518	. . . . 5 ⊢ ((A ∈ N ∧ 1_o ∈ N) → (A <_N 1_o ↔ ¬ (A = 1_o ∨ 1_o <_N A)))
6	2, 5	mpan2 519	. . . 4 ⊢ (A ∈ N → (A <_N 1_o ↔ ¬ (A = 1_o ∨ 1_o <_N A)))
7	1, 6	mtbii 538	. . 3 ⊢ (A ∈ N → ¬ ¬ (A = 1_o ∨ 1_o <_N A))
8		nega 78	. . 3 ⊢ (¬ ¬ (A = 1_o ∨ 1_o <_N A) → (A = 1_o ∨ 1_o <_N A))
9	7, 8	syl 12	. 2 ⊢ (A ∈ N → (A = 1_o ∨ 1_o <_N A))
10	2	elisseti 1355	. . . . . . 7 ⊢ 1_o ∈ V
11	10	eqvinc 1407	. . . . . 6 ⊢ (1_o = A ↔ ∃x(x = 1_o ∧ x = A))
12		indpi.4	. . . . . 6 ⊢ (x = A → (φ ↔ τ))
13		indpi.5	. . . . . . 7 ⊢ ψ
14		indpi.1	. . . . . . 7 ⊢ (x = 1_o → (φ ↔ ψ))
15	13, 14	mpbiri 169	. . . . . 6 ⊢ (x = 1_o → φ)
16	11, 12, 15	gencl 1365	. . . . 5 ⊢ (1_o = A → τ)
17	16	cleqcoms 1104	. . . 4 ⊢ (A = 1_o → τ)
18	17	a1i 7	. . 3 ⊢ (A ∈ N → (A = 1_o → τ))
19		1onn 3193	. . . . . . 7 ⊢ 1_o ∈ ω
20		eleq1 1149	. . . . . . . . . 10 ⊢ (x = 1_o → (x ∈ N ↔ 1_o ∈ N))
21		breq2 2066	. . . . . . . . . 10 ⊢ (x = 1_o → (1_o <_N x ↔ 1_o <_N 1_o))
22	20, 21	anbi12d 476	. . . . . . . . 9 ⊢ (x = 1_o → ((x ∈ N ∧ 1_o <_N x) ↔ (1_o ∈ N ∧ 1_o <_N 1_o)))
23	22, 14	imbi12d 474	. . . . . . . 8 ⊢ (x = 1_o → (((x ∈ N ∧ 1_o <_N x) → φ) ↔ ((1_o ∈ N ∧ 1_o <_N 1_o) → ψ)))
24		eleq1 1149	. . . . . . . . . 10 ⊢ (x = y → (x ∈ N ↔ y ∈ N))
25		breq2 2066	. . . . . . . . . 10 ⊢ (x = y → (1_o <_N x ↔ 1_o <_N y))
26	24, 25	anbi12d 476	. . . . . . . . 9 ⊢ (x = y → ((x ∈ N ∧ 1_o <_N x) ↔ (y ∈ N ∧ 1_o <_N y)))
27		indpi.2	. . . . . . . . 9 ⊢ (x = y → (φ ↔ χ))
28	26, 27	imbi12d 474	. . . . . . . 8 ⊢ (x = y → (((x ∈ N ∧ 1_o <_N x) → φ) ↔ ((y ∈ N ∧ 1_o <_N y) → χ)))
29		eleq1 1149	. . . . . . . . . . . . . . . . 17 ⊢ (x = suc y → (x ∈ ω ↔ suc y ∈ ω))
30		peano2b 2388	. . . . . . . . . . . . . . . . 17 ⊢ (y ∈ ω ↔ suc y ∈ ω)
31	29, 30	syl6bbr 416	. . . . . . . . . . . . . . . 16 ⊢ (x = suc y → (x ∈ ω ↔ y ∈ ω))
32		pinn 3800	. . . . . . . . . . . . . . . 16 ⊢ (x ∈ N → x ∈ ω)
33	31, 32	syl5bi 183	. . . . . . . . . . . . . . 15 ⊢ (x = suc y → (x ∈ N → y ∈ ω))
34	33	adantrd 308	. . . . . . . . . . . . . 14 ⊢ (x = suc y → ((x ∈ N ∧ 1_o <_N x) → y ∈ ω))
35		eleq2 1150	. . . . . . . . . . . . . . . 16 ⊢ (x = suc y → (1_o ∈ x ↔ 1_o ∈ suc y))
36		elsuci 2289	. . . . . . . . . . . . . . . . 17 ⊢ (1_o ∈ suc y → (1_o ∈ y ∨ 1_o = y))
37		n0i 1712	. . . . . . . . . . . . . . . . . 18 ⊢ (1_o ∈ y → ¬ y = ∅)
38		0ex 1745	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ∅ ∈ V
39	38	sucid 2304	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ∅ ∈ suc ∅
40		df-1o 3104	. . . . . . . . . . . . . . . . . . . . 21 ⊢ 1_o = suc ∅
41	39, 40	eleqtrr 1162	. . . . . . . . . . . . . . . . . . . 20 ⊢ ∅ ∈ 1_o
42		eleq2 1150	. . . . . . . . . . . . . . . . . . . 20 ⊢ (1_o = y → (∅ ∈ 1_o ↔ ∅ ∈ y))
43	41, 42	mpbii 168	. . . . . . . . . . . . . . . . . . 19 ⊢ (1_o = y → ∅ ∈ y)
44		n0i 1712	. . . . . . . . . . . . . . . . . . 19 ⊢ (∅ ∈ y → ¬ y = ∅)
45	43, 44	syl 12	. . . . . . . . . . . . . . . . . 18 ⊢ (1_o = y → ¬ y = ∅)
46	37, 45	jaoi 275	. . . . . . . . . . . . . . . . 17 ⊢ ((1_o ∈ y ∨ 1_o = y) → ¬ y = ∅)
47	36, 46	syl 12	. . . . . . . . . . . . . . . 16 ⊢ (1_o ∈ suc y → ¬ y = ∅)
48	35, 47	syl6bi 187	. . . . . . . . . . . . . . 15 ⊢ (x = suc y → (1_o ∈ x → ¬ y = ∅))
49		ltpiord 3809	. . . . . . . . . . . . . . . . 17 ⊢ ((1_o ∈ N ∧ x ∈ N) → (1_o <_N x ↔ 1_o ∈ x))
50	2, 49	mpan 518	. . . . . . . . . . . . . . . 16 ⊢ (x ∈ N → (1_o <_N x ↔ 1_o ∈ x))
51	50	biimpa 324	. . . . . . . . . . . . . . 15 ⊢ ((x ∈ N ∧ 1_o <_N x) → 1_o ∈ x)
52	48, 51	syl5 22	. . . . . . . . . . . . . 14 ⊢ (x = suc y → ((x ∈ N ∧ 1_o <_N x) → ¬ y = ∅))
53	34, 52	jcad 455	. . . . . . . . . . . . 13 ⊢ (x = suc y → ((x ∈ N ∧ 1_o <_N x) → (y ∈ ω ∧ ¬ y = ∅)))
54		elni 3798	. . . . . . . . . . . . 13 ⊢ (y ∈ N ↔ (y ∈ ω ∧ ¬ y = ∅))
55	53, 54	syl6ibr 186	. . . . . . . . . . . 12 ⊢ (x = suc y → ((x ∈ N ∧ 1_o <_N x) → y ∈ N))
56		breq2 2066	. . . . . . . . . . . . 13 ⊢ (x = suc y → (1_o <_N x ↔ 1_o <_N suc y))
57		pm3.27 260	. . . . . . . . . . . . 13 ⊢ ((x ∈ N ∧ 1_o <_N x) → 1_o <_N x)
58	56, 57	syl5bi 183	. . . . . . . . . . . 12 ⊢ (x = suc y → ((x ∈ N ∧ 1_o <_N x) → 1_o <_N suc y))
59	55, 58	jcad 455	. . . . . . . . . . 11 ⊢ (x = suc y → ((x ∈ N ∧ 1_o <_N x) → (y ∈ N ∧ 1_o <_N suc y)))
60		addpiord 3806	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((y ∈ N ∧ 1_o ∈ N) → (y +_N 1_o) = (y +_o 1_o))
61	2, 60	mpan2 519	. . . . . . . . . . . . . . . . . . 19 ⊢ (y ∈ N → (y +_N 1_o) = (y +_o 1_o))
62		pion 3801	. . . . . . . . . . . . . . . . . . . 20 ⊢ (y ∈ N → y ∈ On)
63		oa1suc 3132	. . . . . . . . . . . . . . . . . . . 20 ⊢ (y ∈ On → (y +_o 1_o) = suc y)
64	62, 63	syl 12	. . . . . . . . . . . . . . . . . . 19 ⊢ (y ∈ N → (y +_o 1_o) = suc y)
65	61, 64	eqtrd 1128	. . . . . . . . . . . . . . . . . 18 ⊢ (y ∈ N → (y +_N 1_o) = suc y)
66	65	cleq2d 1112	. . . . . . . . . . . . . . . . 17 ⊢ (y ∈ N → (x = (y +_N 1_o) ↔ x = suc y))
67	66	biimparc 327	. . . . . . . . . . . . . . . 16 ⊢ ((x = suc y ∧ y ∈ N) → x = (y +_N 1_o))
68	67	eleq1d 1155	. . . . . . . . . . . . . . 15 ⊢ ((x = suc y ∧ y ∈ N) → (x ∈ N ↔ (y +_N 1_o) ∈ N))
69		addclpi 3814	. . . . . . . . . . . . . . . 16 ⊢ ((y ∈ N ∧ 1_o ∈ N) → (y +_N 1_o) ∈ N)
70	2, 69	mpan2 519	. . . . . . . . . . . . . . 15 ⊢ (y ∈ N → (y +_N 1_o) ∈ N)
71	68, 70	syl5bir 184	. . . . . . . . . . . . . 14 ⊢ ((x = suc y ∧ y ∈ N) → (y ∈ N → x ∈ N))
72	71	exp 291	. . . . . . . . . . . . 13 ⊢ (x = suc y → (y ∈ N → (y ∈ N → x ∈ N)))
73	72	pm2.43d 59	. . . . . . . . . . . 12 ⊢ (x = suc y → (y ∈ N → x ∈ N))
74	56	biimprd 136	. . . . . . . . . . . 12 ⊢ (x = suc y → (1_o <_N suc y → 1_o <_N x))
75	73, 74	anim12d 431	. . . . . . . . . . 11 ⊢ (x = suc y → ((y ∈ N ∧ 1_o <_N suc y) → (x ∈ N ∧ 1_o <_N x)))
76	59, 75	impbid 397	. . . . . . . . . 10 ⊢ (x = suc y → ((x ∈ N ∧ 1_o <_N x) ↔ (y ∈ N ∧ 1_o <_N suc y)))
77	76	imbi1d 465	. . . . . . . . 9 ⊢ (x = suc y → (((x ∈ N ∧ 1_o <_N x) → φ) ↔ ((y ∈ N ∧ 1_o <_N suc y) → φ)))
78		indpi.3	. . . . . . . . . . . . 13 ⊢ (x = (y +_N 1_o) → (φ ↔ θ))
79	66, 78	syl6bir 188	. . . . . . . . . . . 12 ⊢ (y ∈ N → (x = suc y → (φ ↔ θ)))
80	79	adantr 306	. . . . . . . . . . 11 ⊢ ((y ∈ N ∧ 1_o <_N suc y) → (x = suc y → (φ ↔ θ)))
81	80	com12 13	. . . . . . . . . 10 ⊢ (x = suc y → ((y ∈ N ∧ 1_o <_N suc y) → (φ ↔ θ)))
82	81	pm5.74d 444	. . . . . . . . 9 ⊢ (x = suc y → (((y ∈ N ∧ 1_o <_N suc y) → φ) ↔ ((y ∈ N ∧ 1_o <_N suc y) → θ)))
83	77, 82	bitrd 406	. . . . . . . 8 ⊢ (x = suc y → (((x ∈ N ∧ 1_o <_N x) → φ) ↔ ((y ∈ N ∧ 1_o <_N suc y) → θ)))
84		eleq1 1149	. . . . . . . . . 10 ⊢ (x = A → (x ∈ N ↔ A ∈ N))
85		breq2 2066	. . . . . . . . . 10 ⊢ (x = A → (1_o <_N x ↔ 1_o <_N A))
86	84, 85	anbi12d 476	. . . . . . . . 9 ⊢ (x = A → ((x ∈ N ∧ 1_o <_N x) ↔ (A ∈ N ∧ 1_o <_N A)))
87	86, 12	imbi12d 474	. . . . . . . 8 ⊢ (x = A → (((x ∈ N ∧ 1_o <_N x) → φ) ↔ ((A ∈ N ∧ 1_o <_N A) → τ)))
88	13	a1i 7	. . . . . . . . 9 ⊢ ((1_o ∈ N ∧ 1_o <_N 1_o) → ψ)
89	88	a1i 7	. . . . . . . 8 ⊢ (1_o ∈ ω → ((1_o ∈ N ∧ 1_o <_N 1_o) → ψ))
90		pm3.2 232	. . . . . . . . . . . . . . 15 ⊢ (y ∈ N → (1_o ∈ y → (y ∈ N ∧ 1_o ∈ y)))
91		ltpiord 3809	. . . . . . . . . . . . . . . . 17 ⊢ ((1_o ∈ N ∧ y ∈ N) → (1_o <_N y ↔ 1_o ∈ y))
92	2, 91	mpan 518	. . . . . . . . . . . . . . . 16 ⊢ (y ∈ N → (1_o <_N y ↔ 1_o ∈ y))
93	92	pm5.32i 489	. . . . . . . . . . . . . . 15 ⊢ ((y ∈ N ∧ 1_o <_N y) ↔ (y ∈ N ∧ 1_o ∈ y))
94	90, 93	syl6ibr 186	. . . . . . . . . . . . . 14 ⊢ (y ∈ N → (1_o ∈ y → (y ∈ N ∧ 1_o <_N y)))
95	94	syl4d 28	. . . . . . . . . . . . 13 ⊢ (y ∈ N → (((y ∈ N ∧ 1_o <_N y) → χ) → (1_o ∈ y → χ)))
96	10	eqvinc 1407	. . . . . . . . . . . . . . . . 17 ⊢ (1_o = y ↔ ∃x(x = 1_o ∧ x = y))
97	96, 27, 15	gencl 1365	. . . . . . . . . . . . . . . 16 ⊢ (1_o = y → χ)
98		jao 274	. . . . . . . . . . . . . . . 16 ⊢ ((1_o ∈ y → χ) → ((1_o = y → χ) → ((1_o ∈ y ∨ 1_o = y) → χ)))
99	97, 98	mpi 44	. . . . . . . . . . . . . . 15 ⊢ ((1_o ∈ y → χ) → ((1_o ∈ y ∨ 1_o = y) → χ))
100	99, 36	syl5 22	. . . . . . . . . . . . . 14 ⊢ ((1_o ∈ y → χ) → (1_o ∈ suc y → χ))
101		visset 1350	. . . . . . . . . . . . . . . . . 18 ⊢ y ∈ V
102	101	sucex 2303	. . . . . . . . . . . . . . . . 17 ⊢ suc y ∈ V
103		ltrelpi 3811	. . . . . . . . . . . . . . . . 17 ⊢ <_N ⊆ (N × N)
104	102, 103	brel 2459	. . . . . . . . . . . . . . . 16 ⊢ (1_o <_N suc y → (1_o ∈ N ∧ suc y ∈ N))
105		ltpiord 3809	. . . . . . . . . . . . . . . 16 ⊢ ((1_o ∈ N ∧ suc y ∈ N) → (1_o <_N suc y ↔ 1_o ∈ suc y))
106	104, 105	syl 12	. . . . . . . . . . . . . . 15 ⊢ (1_o <_N suc y → (1_o <_N suc y ↔ 1_o ∈ suc y))
107	106	ibi 449	. . . . . . . . . . . . . 14 ⊢ (1_o <_N suc y → 1_o ∈ suc y)
108	100, 107	syl5 22	. . . . . . . . . . . . 13 ⊢ ((1_o ∈ y → χ) → (1_o <_N suc y → χ))
109	95, 108	syl6 23	. . . . . . . . . . . 12 ⊢ (y ∈ N → (((y ∈ N ∧ 1_o <_N y) → χ) → (1_o <_N suc y → χ)))
110	109	com12 13	. . . . . . . . . . 11 ⊢ (((y ∈ N ∧ 1_o <_N y) → χ) → (y ∈ N → (1_o <_N suc y → χ)))
111	110	imp3a 279	. . . . . . . . . 10 ⊢ (((y ∈ N ∧ 1_o <_N y) → χ) → ((y ∈ N ∧ 1_o <_N suc y) → χ))
112		elni2 3799	. . . . . . . . . . . 12 ⊢ (y ∈ N ↔ (y ∈ ω ∧ ∅ ∈ y))
113		indpi.6	. . . . . . . . . . . 12 ⊢ (y ∈ N → (χ → θ))
114	112, 113	sylbir 176	. . . . . . . . . . 11 ⊢ ((y ∈ ω ∧ ∅ ∈ y) → (χ → θ))
115	40	sseq1i 1524	. . . . . . . . . . . 12 ⊢ (1_o ⊆ y ↔ suc ∅ ⊆ y)
116		sucssel 2321	. . . . . . . . . . . . 13 ⊢ (∅ ∈ V → (suc ∅ ⊆ y → ∅ ∈ y))
117	38, 116	ax-mp 6	. . . . . . . . . . . 12 ⊢ (suc ∅ ⊆ y → ∅ ∈ y)
118	115, 117	sylbi 174	. . . . . . . . . . 11 ⊢ (1_o ⊆ y → ∅ ∈ y)
119	114, 118	sylan2 346	. . . . . . . . . 10 ⊢ ((y ∈ ω ∧ 1_o ⊆ y) → (χ → θ))
120	111, 119	syl9r 56	. . . . . . . . 9 ⊢ ((y ∈ ω ∧ 1_o ⊆ y) → (((y ∈ N ∧ 1_o <_N y) → χ) → ((y ∈ N ∧ 1_o <_N suc y) → θ)))
121	120	adantlr 310	. . . . . . . 8 ⊢ (((y ∈ ω ∧ 1_o ∈ ω) ∧ 1_o ⊆ y) → (((y ∈ N ∧ 1_o <_N y) → χ) → ((y ∈ N ∧ 1_o <_N suc y) → θ)))
122	23, 28, 83, 87, 89, 121	findsg 2398	. . . . . . 7 ⊢ (((A ∈ ω ∧ 1_o ∈ ω) ∧ 1_o ⊆ A) → ((A ∈ N ∧ 1_o <_N A) → τ))
123	19, 122	mpan12 530	. . . . . 6 ⊢ ((A ∈ ω ∧ 1_o ⊆ A) → ((A ∈ N ∧ 1_o <_N A) → τ))
124		pinn 3800	. . . . . 6 ⊢ (A ∈ N → A ∈ ω)
125		elni2 3799	. . . . . . 7 ⊢ (A ∈ N ↔ (A ∈ ω ∧ ∅ ∈ A))
126		nnord 2381	. . . . . . . . . 10 ⊢ (A ∈ ω → Ord A)
127		ordsucss 2320	. . . . . . . . . 10 ⊢ (Ord A → (∅ ∈ A → suc ∅ ⊆ A))
128	126, 127	syl 12	. . . . . . . . 9 ⊢ (A ∈ ω → (∅ ∈ A → suc ∅ ⊆ A))
129	40	sseq1i 1524	. . . . . . . . 9 ⊢ (1_o ⊆ A ↔ suc ∅ ⊆ A)
130	128, 129	syl6ibr 186	. . . . . . . 8 ⊢ (A ∈ ω → (∅ ∈ A → 1_o ⊆ A))
131	130	imp 277	. . . . . . 7 ⊢ ((A ∈ ω ∧ ∅ ∈ A) → 1_o ⊆ A)
132	125, 131	sylbi 174	. . . . . 6 ⊢ (A ∈ N → 1_o ⊆ A)
133	123, 124, 132	sylanc 361	. . . . 5 ⊢ (A ∈ N → ((A ∈ N ∧ 1_o <_N A) → τ))
134	133	exp3a 292	. . . 4 ⊢ (A ∈ N → (A ∈ N → (1_o <_N A → τ)))
135	134	pm2.43i 58	. . 3 ⊢ (A ∈ N → (1_o <_N A → τ))
136	18, 135	jaod 329	. 2 ⊢ (A ∈ N → ((A = 1_o ∨ 1_o <_N A) → τ))
137	9, 136	mpd 46	1 ⊢ (A ∈ N → τ)

Colors of variables: wff set class

Syntax hints: ¬ wn 1 → wi 2 ↔ wb 127 ∨ wo 195 ∧ wa 196 = weq 797 = wceq 1091 ∈ wcel 1092 Vcvv 1348 ⊆ wss 1487 ∅c0 1707 class class class wbr 2054 Or wor 2059 Ord word 2198 Oncon0 2199 suc csuc 2201 ωcom 2372 (class class class)co 3001 1_oc1o 3099 +_o coa 3101 Ncnpi 3766 +_N cpli 3767 <_N clti 3769

This theorem is referenced by: prlem934a 3931

This theorem was proved from axioms: ax-1 3 ax-2 4 ax-3 5 ax-mp 6 ax-4 673 ax-5 674 ax-6 675 ax-7 676 ax-gen 677 ax-8 798 ax-9 799 ax-10 800 ax-11 801 ax-12 802 ax-13 804 ax-14 805 ax-16 922 ax-17 925 ax-ext 1074 ax-rep 1075 ax-un 1076 ax-pow 1077

This theorem depends on definitions: df-bi 128 df-or 197 df-an 198 df-3or 582 df-3an 583 df-ex 679 df-sb 853 df-eu 1009 df-mo 1010 df-clab 1093 df-cleq 1097 df-clel 1099 df-ral 1205 df-rex 1206 df-rab 1208 df-v 1349 df-sbc 1441 df-dif 1489 df-un 1490 df-in 1491 df-ss 1492 df-nul 1708 df-if 1777 df-pw 1799 df-sn 1811 df-pr 1812 df-tp 1814 df-op 1815 df-uni 1920 df-iun 1996 df-tr 2042 df-br 2063 df-opab 2098 df-eprel 2122 df-id 2125 df-po 2128 df-so 2138 df-fr 2169 df-we 2186 df-ord 2202 df-on 2203 df-lim 2204 df-suc 2205 df-om 2373 df-xp 2424 df-rel 2425 df-cnv 2426 df-co 2427 df-dm 2428 df-rn 2429 df-res 2430 df-ima 2431 df-fun 2432 df-fn 2433 df-fv 2438 df-rdg 2970 df-opr 3003 df-oprab 3004 df-1o 3104 df-oadd 3106 df-ni 3794 df-pli 3795 df-lti 3797

metamath.org