Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  indpi Structured version   Visualization version   GIF version

Theorem indpi 9681
 Description: Principle of Finite Induction on positive integers. (Contributed by NM, 23-Mar-1996.) (New usage is discouraged.)
Hypotheses
Ref Expression
indpi.1 (𝑥 = 1𝑜 → (𝜑𝜓))
indpi.2 (𝑥 = 𝑦 → (𝜑𝜒))
indpi.3 (𝑥 = (𝑦 +N 1𝑜) → (𝜑𝜃))
indpi.4 (𝑥 = 𝐴 → (𝜑𝜏))
indpi.5 𝜓
indpi.6 (𝑦N → (𝜒𝜃))
Assertion
Ref Expression
indpi (𝐴N𝜏)
Distinct variable groups:   𝑥,𝑦   𝑥,𝐴   𝜓,𝑥   𝜒,𝑥   𝜃,𝑥   𝜏,𝑥   𝜑,𝑦
Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)   𝜒(𝑦)   𝜃(𝑦)   𝜏(𝑦)   𝐴(𝑦)

Proof of Theorem indpi
StepHypRef Expression
1 1pi 9657 . . . . . . 7 1𝑜N
21elexi 3202 . . . . . 6 1𝑜 ∈ V
32eqvinc 3317 . . . . 5 (1𝑜 = 𝐴 ↔ ∃𝑥(𝑥 = 1𝑜𝑥 = 𝐴))
4 indpi.4 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜏))
5 indpi.5 . . . . . 6 𝜓
6 indpi.1 . . . . . 6 (𝑥 = 1𝑜 → (𝜑𝜓))
75, 6mpbiri 248 . . . . 5 (𝑥 = 1𝑜𝜑)
83, 4, 7gencl 3224 . . . 4 (1𝑜 = 𝐴𝜏)
98eqcoms 2629 . . 3 (𝐴 = 1𝑜𝜏)
109a1i 11 . 2 (𝐴N → (𝐴 = 1𝑜𝜏))
11 pinn 9652 . . . . 5 (𝐴N𝐴 ∈ ω)
12 elni2 9651 . . . . . 6 (𝐴N ↔ (𝐴 ∈ ω ∧ ∅ ∈ 𝐴))
13 nnord 7027 . . . . . . . . 9 (𝐴 ∈ ω → Ord 𝐴)
14 ordsucss 6972 . . . . . . . . 9 (Ord 𝐴 → (∅ ∈ 𝐴 → suc ∅ ⊆ 𝐴))
1513, 14syl 17 . . . . . . . 8 (𝐴 ∈ ω → (∅ ∈ 𝐴 → suc ∅ ⊆ 𝐴))
16 df-1o 7512 . . . . . . . . 9 1𝑜 = suc ∅
1716sseq1i 3613 . . . . . . . 8 (1𝑜𝐴 ↔ suc ∅ ⊆ 𝐴)
1815, 17syl6ibr 242 . . . . . . 7 (𝐴 ∈ ω → (∅ ∈ 𝐴 → 1𝑜𝐴))
1918imp 445 . . . . . 6 ((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) → 1𝑜𝐴)
2012, 19sylbi 207 . . . . 5 (𝐴N → 1𝑜𝐴)
21 1onn 7671 . . . . . 6 1𝑜 ∈ ω
22 eleq1 2686 . . . . . . . . 9 (𝑥 = 1𝑜 → (𝑥N ↔ 1𝑜N))
23 breq2 4622 . . . . . . . . 9 (𝑥 = 1𝑜 → (1𝑜 <N 𝑥 ↔ 1𝑜 <N 1𝑜))
2422, 23anbi12d 746 . . . . . . . 8 (𝑥 = 1𝑜 → ((𝑥N ∧ 1𝑜 <N 𝑥) ↔ (1𝑜N ∧ 1𝑜 <N 1𝑜)))
2524, 6imbi12d 334 . . . . . . 7 (𝑥 = 1𝑜 → (((𝑥N ∧ 1𝑜 <N 𝑥) → 𝜑) ↔ ((1𝑜N ∧ 1𝑜 <N 1𝑜) → 𝜓)))
26 eleq1 2686 . . . . . . . . 9 (𝑥 = 𝑦 → (𝑥N𝑦N))
27 breq2 4622 . . . . . . . . 9 (𝑥 = 𝑦 → (1𝑜 <N 𝑥 ↔ 1𝑜 <N 𝑦))
2826, 27anbi12d 746 . . . . . . . 8 (𝑥 = 𝑦 → ((𝑥N ∧ 1𝑜 <N 𝑥) ↔ (𝑦N ∧ 1𝑜 <N 𝑦)))
29 indpi.2 . . . . . . . 8 (𝑥 = 𝑦 → (𝜑𝜒))
3028, 29imbi12d 334 . . . . . . 7 (𝑥 = 𝑦 → (((𝑥N ∧ 1𝑜 <N 𝑥) → 𝜑) ↔ ((𝑦N ∧ 1𝑜 <N 𝑦) → 𝜒)))
31 pinn 9652 . . . . . . . . . . . . . . 15 (𝑥N𝑥 ∈ ω)
32 eleq1 2686 . . . . . . . . . . . . . . . 16 (𝑥 = suc 𝑦 → (𝑥 ∈ ω ↔ suc 𝑦 ∈ ω))
33 peano2b 7035 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ω ↔ suc 𝑦 ∈ ω)
3432, 33syl6bbr 278 . . . . . . . . . . . . . . 15 (𝑥 = suc 𝑦 → (𝑥 ∈ ω ↔ 𝑦 ∈ ω))
3531, 34syl5ib 234 . . . . . . . . . . . . . 14 (𝑥 = suc 𝑦 → (𝑥N𝑦 ∈ ω))
3635adantrd 484 . . . . . . . . . . . . 13 (𝑥 = suc 𝑦 → ((𝑥N ∧ 1𝑜 <N 𝑥) → 𝑦 ∈ ω))
37 ltpiord 9661 . . . . . . . . . . . . . . . 16 ((1𝑜N𝑥N) → (1𝑜 <N 𝑥 ↔ 1𝑜𝑥))
381, 37mpan 705 . . . . . . . . . . . . . . 15 (𝑥N → (1𝑜 <N 𝑥 ↔ 1𝑜𝑥))
3938biimpa 501 . . . . . . . . . . . . . 14 ((𝑥N ∧ 1𝑜 <N 𝑥) → 1𝑜𝑥)
40 eleq2 2687 . . . . . . . . . . . . . . 15 (𝑥 = suc 𝑦 → (1𝑜𝑥 ↔ 1𝑜 ∈ suc 𝑦))
41 elsuci 5755 . . . . . . . . . . . . . . . 16 (1𝑜 ∈ suc 𝑦 → (1𝑜𝑦 ∨ 1𝑜 = 𝑦))
42 ne0i 3902 . . . . . . . . . . . . . . . . 17 (1𝑜𝑦𝑦 ≠ ∅)
43 0lt1o 7536 . . . . . . . . . . . . . . . . . . 19 ∅ ∈ 1𝑜
44 eleq2 2687 . . . . . . . . . . . . . . . . . . 19 (1𝑜 = 𝑦 → (∅ ∈ 1𝑜 ↔ ∅ ∈ 𝑦))
4543, 44mpbii 223 . . . . . . . . . . . . . . . . . 18 (1𝑜 = 𝑦 → ∅ ∈ 𝑦)
46 ne0i 3902 . . . . . . . . . . . . . . . . . 18 (∅ ∈ 𝑦𝑦 ≠ ∅)
4745, 46syl 17 . . . . . . . . . . . . . . . . 17 (1𝑜 = 𝑦𝑦 ≠ ∅)
4842, 47jaoi 394 . . . . . . . . . . . . . . . 16 ((1𝑜𝑦 ∨ 1𝑜 = 𝑦) → 𝑦 ≠ ∅)
4941, 48syl 17 . . . . . . . . . . . . . . 15 (1𝑜 ∈ suc 𝑦𝑦 ≠ ∅)
5040, 49syl6bi 243 . . . . . . . . . . . . . 14 (𝑥 = suc 𝑦 → (1𝑜𝑥𝑦 ≠ ∅))
5139, 50syl5 34 . . . . . . . . . . . . 13 (𝑥 = suc 𝑦 → ((𝑥N ∧ 1𝑜 <N 𝑥) → 𝑦 ≠ ∅))
5236, 51jcad 555 . . . . . . . . . . . 12 (𝑥 = suc 𝑦 → ((𝑥N ∧ 1𝑜 <N 𝑥) → (𝑦 ∈ ω ∧ 𝑦 ≠ ∅)))
53 elni 9650 . . . . . . . . . . . 12 (𝑦N ↔ (𝑦 ∈ ω ∧ 𝑦 ≠ ∅))
5452, 53syl6ibr 242 . . . . . . . . . . 11 (𝑥 = suc 𝑦 → ((𝑥N ∧ 1𝑜 <N 𝑥) → 𝑦N))
55 simpr 477 . . . . . . . . . . . 12 ((𝑥N ∧ 1𝑜 <N 𝑥) → 1𝑜 <N 𝑥)
56 breq2 4622 . . . . . . . . . . . 12 (𝑥 = suc 𝑦 → (1𝑜 <N 𝑥 ↔ 1𝑜 <N suc 𝑦))
5755, 56syl5ib 234 . . . . . . . . . . 11 (𝑥 = suc 𝑦 → ((𝑥N ∧ 1𝑜 <N 𝑥) → 1𝑜 <N suc 𝑦))
5854, 57jcad 555 . . . . . . . . . 10 (𝑥 = suc 𝑦 → ((𝑥N ∧ 1𝑜 <N 𝑥) → (𝑦N ∧ 1𝑜 <N suc 𝑦)))
59 addclpi 9666 . . . . . . . . . . . . . . 15 ((𝑦N ∧ 1𝑜N) → (𝑦 +N 1𝑜) ∈ N)
601, 59mpan2 706 . . . . . . . . . . . . . 14 (𝑦N → (𝑦 +N 1𝑜) ∈ N)
61 addpiord 9658 . . . . . . . . . . . . . . . . . . 19 ((𝑦N ∧ 1𝑜N) → (𝑦 +N 1𝑜) = (𝑦 +𝑜 1𝑜))
621, 61mpan2 706 . . . . . . . . . . . . . . . . . 18 (𝑦N → (𝑦 +N 1𝑜) = (𝑦 +𝑜 1𝑜))
63 pion 9653 . . . . . . . . . . . . . . . . . . 19 (𝑦N𝑦 ∈ On)
64 oa1suc 7563 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ On → (𝑦 +𝑜 1𝑜) = suc 𝑦)
6563, 64syl 17 . . . . . . . . . . . . . . . . . 18 (𝑦N → (𝑦 +𝑜 1𝑜) = suc 𝑦)
6662, 65eqtrd 2655 . . . . . . . . . . . . . . . . 17 (𝑦N → (𝑦 +N 1𝑜) = suc 𝑦)
6766eqeq2d 2631 . . . . . . . . . . . . . . . 16 (𝑦N → (𝑥 = (𝑦 +N 1𝑜) ↔ 𝑥 = suc 𝑦))
6867biimparc 504 . . . . . . . . . . . . . . 15 ((𝑥 = suc 𝑦𝑦N) → 𝑥 = (𝑦 +N 1𝑜))
6968eleq1d 2683 . . . . . . . . . . . . . 14 ((𝑥 = suc 𝑦𝑦N) → (𝑥N ↔ (𝑦 +N 1𝑜) ∈ N))
7060, 69syl5ibr 236 . . . . . . . . . . . . 13 ((𝑥 = suc 𝑦𝑦N) → (𝑦N𝑥N))
7170ex 450 . . . . . . . . . . . 12 (𝑥 = suc 𝑦 → (𝑦N → (𝑦N𝑥N)))
7271pm2.43d 53 . . . . . . . . . . 11 (𝑥 = suc 𝑦 → (𝑦N𝑥N))
7356biimprd 238 . . . . . . . . . . 11 (𝑥 = suc 𝑦 → (1𝑜 <N suc 𝑦 → 1𝑜 <N 𝑥))
7472, 73anim12d 585 . . . . . . . . . 10 (𝑥 = suc 𝑦 → ((𝑦N ∧ 1𝑜 <N suc 𝑦) → (𝑥N ∧ 1𝑜 <N 𝑥)))
7558, 74impbid 202 . . . . . . . . 9 (𝑥 = suc 𝑦 → ((𝑥N ∧ 1𝑜 <N 𝑥) ↔ (𝑦N ∧ 1𝑜 <N suc 𝑦)))
7675imbi1d 331 . . . . . . . 8 (𝑥 = suc 𝑦 → (((𝑥N ∧ 1𝑜 <N 𝑥) → 𝜑) ↔ ((𝑦N ∧ 1𝑜 <N suc 𝑦) → 𝜑)))
77 indpi.3 . . . . . . . . . . . 12 (𝑥 = (𝑦 +N 1𝑜) → (𝜑𝜃))
7867, 77syl6bir 244 . . . . . . . . . . 11 (𝑦N → (𝑥 = suc 𝑦 → (𝜑𝜃)))
7978adantr 481 . . . . . . . . . 10 ((𝑦N ∧ 1𝑜 <N suc 𝑦) → (𝑥 = suc 𝑦 → (𝜑𝜃)))
8079com12 32 . . . . . . . . 9 (𝑥 = suc 𝑦 → ((𝑦N ∧ 1𝑜 <N suc 𝑦) → (𝜑𝜃)))
8180pm5.74d 262 . . . . . . . 8 (𝑥 = suc 𝑦 → (((𝑦N ∧ 1𝑜 <N suc 𝑦) → 𝜑) ↔ ((𝑦N ∧ 1𝑜 <N suc 𝑦) → 𝜃)))
8276, 81bitrd 268 . . . . . . 7 (𝑥 = suc 𝑦 → (((𝑥N ∧ 1𝑜 <N 𝑥) → 𝜑) ↔ ((𝑦N ∧ 1𝑜 <N suc 𝑦) → 𝜃)))
83 eleq1 2686 . . . . . . . . 9 (𝑥 = 𝐴 → (𝑥N𝐴N))
84 breq2 4622 . . . . . . . . 9 (𝑥 = 𝐴 → (1𝑜 <N 𝑥 ↔ 1𝑜 <N 𝐴))
8583, 84anbi12d 746 . . . . . . . 8 (𝑥 = 𝐴 → ((𝑥N ∧ 1𝑜 <N 𝑥) ↔ (𝐴N ∧ 1𝑜 <N 𝐴)))
8685, 4imbi12d 334 . . . . . . 7 (𝑥 = 𝐴 → (((𝑥N ∧ 1𝑜 <N 𝑥) → 𝜑) ↔ ((𝐴N ∧ 1𝑜 <N 𝐴) → 𝜏)))
8752a1i 12 . . . . . . 7 (1𝑜 ∈ ω → ((1𝑜N ∧ 1𝑜 <N 1𝑜) → 𝜓))
88 ltpiord 9661 . . . . . . . . . . . . . . 15 ((1𝑜N𝑦N) → (1𝑜 <N 𝑦 ↔ 1𝑜𝑦))
891, 88mpan 705 . . . . . . . . . . . . . 14 (𝑦N → (1𝑜 <N 𝑦 ↔ 1𝑜𝑦))
9089pm5.32i 668 . . . . . . . . . . . . 13 ((𝑦N ∧ 1𝑜 <N 𝑦) ↔ (𝑦N ∧ 1𝑜𝑦))
9190simplbi2 654 . . . . . . . . . . . 12 (𝑦N → (1𝑜𝑦 → (𝑦N ∧ 1𝑜 <N 𝑦)))
9291imim1d 82 . . . . . . . . . . 11 (𝑦N → (((𝑦N ∧ 1𝑜 <N 𝑦) → 𝜒) → (1𝑜𝑦𝜒)))
93 ltrelpi 9663 . . . . . . . . . . . . . . 15 <N ⊆ (N × N)
9493brel 5133 . . . . . . . . . . . . . 14 (1𝑜 <N suc 𝑦 → (1𝑜N ∧ suc 𝑦N))
95 ltpiord 9661 . . . . . . . . . . . . . 14 ((1𝑜N ∧ suc 𝑦N) → (1𝑜 <N suc 𝑦 ↔ 1𝑜 ∈ suc 𝑦))
9694, 95syl 17 . . . . . . . . . . . . 13 (1𝑜 <N suc 𝑦 → (1𝑜 <N suc 𝑦 ↔ 1𝑜 ∈ suc 𝑦))
9796ibi 256 . . . . . . . . . . . 12 (1𝑜 <N suc 𝑦 → 1𝑜 ∈ suc 𝑦)
982eqvinc 3317 . . . . . . . . . . . . . . 15 (1𝑜 = 𝑦 ↔ ∃𝑥(𝑥 = 1𝑜𝑥 = 𝑦))
9998, 29, 7gencl 3224 . . . . . . . . . . . . . 14 (1𝑜 = 𝑦𝜒)
100 jao 534 . . . . . . . . . . . . . 14 ((1𝑜𝑦𝜒) → ((1𝑜 = 𝑦𝜒) → ((1𝑜𝑦 ∨ 1𝑜 = 𝑦) → 𝜒)))
10199, 100mpi 20 . . . . . . . . . . . . 13 ((1𝑜𝑦𝜒) → ((1𝑜𝑦 ∨ 1𝑜 = 𝑦) → 𝜒))
10241, 101syl5 34 . . . . . . . . . . . 12 ((1𝑜𝑦𝜒) → (1𝑜 ∈ suc 𝑦𝜒))
10397, 102syl5 34 . . . . . . . . . . 11 ((1𝑜𝑦𝜒) → (1𝑜 <N suc 𝑦𝜒))
10492, 103syl6com 37 . . . . . . . . . 10 (((𝑦N ∧ 1𝑜 <N 𝑦) → 𝜒) → (𝑦N → (1𝑜 <N suc 𝑦𝜒)))
105104impd 447 . . . . . . . . 9 (((𝑦N ∧ 1𝑜 <N 𝑦) → 𝜒) → ((𝑦N ∧ 1𝑜 <N suc 𝑦) → 𝜒))
10616sseq1i 3613 . . . . . . . . . . 11 (1𝑜𝑦 ↔ suc ∅ ⊆ 𝑦)
107 0ex 4755 . . . . . . . . . . . 12 ∅ ∈ V
108 sucssel 5783 . . . . . . . . . . . 12 (∅ ∈ V → (suc ∅ ⊆ 𝑦 → ∅ ∈ 𝑦))
109107, 108ax-mp 5 . . . . . . . . . . 11 (suc ∅ ⊆ 𝑦 → ∅ ∈ 𝑦)
110106, 109sylbi 207 . . . . . . . . . 10 (1𝑜𝑦 → ∅ ∈ 𝑦)
111 elni2 9651 . . . . . . . . . . 11 (𝑦N ↔ (𝑦 ∈ ω ∧ ∅ ∈ 𝑦))
112 indpi.6 . . . . . . . . . . 11 (𝑦N → (𝜒𝜃))
113111, 112sylbir 225 . . . . . . . . . 10 ((𝑦 ∈ ω ∧ ∅ ∈ 𝑦) → (𝜒𝜃))
114110, 113sylan2 491 . . . . . . . . 9 ((𝑦 ∈ ω ∧ 1𝑜𝑦) → (𝜒𝜃))
115105, 114syl9r 78 . . . . . . . 8 ((𝑦 ∈ ω ∧ 1𝑜𝑦) → (((𝑦N ∧ 1𝑜 <N 𝑦) → 𝜒) → ((𝑦N ∧ 1𝑜 <N suc 𝑦) → 𝜃)))
116115adantlr 750 . . . . . . 7 (((𝑦 ∈ ω ∧ 1𝑜 ∈ ω) ∧ 1𝑜𝑦) → (((𝑦N ∧ 1𝑜 <N 𝑦) → 𝜒) → ((𝑦N ∧ 1𝑜 <N suc 𝑦) → 𝜃)))
11725, 30, 82, 86, 87, 116findsg 7047 . . . . . 6 (((𝐴 ∈ ω ∧ 1𝑜 ∈ ω) ∧ 1𝑜𝐴) → ((𝐴N ∧ 1𝑜 <N 𝐴) → 𝜏))
11821, 117mpanl2 716 . . . . 5 ((𝐴 ∈ ω ∧ 1𝑜𝐴) → ((𝐴N ∧ 1𝑜 <N 𝐴) → 𝜏))
11911, 20, 118syl2anc 692 . . . 4 (𝐴N → ((𝐴N ∧ 1𝑜 <N 𝐴) → 𝜏))
120119expd 452 . . 3 (𝐴N → (𝐴N → (1𝑜 <N 𝐴𝜏)))
121120pm2.43i 52 . 2 (𝐴N → (1𝑜 <N 𝐴𝜏))
122 nlt1pi 9680 . . . 4 ¬ 𝐴 <N 1𝑜
123 ltsopi 9662 . . . . . 6 <N Or N
124 sotric 5026 . . . . . 6 (( <N Or N ∧ (𝐴N ∧ 1𝑜N)) → (𝐴 <N 1𝑜 ↔ ¬ (𝐴 = 1𝑜 ∨ 1𝑜 <N 𝐴)))
125123, 124mpan 705 . . . . 5 ((𝐴N ∧ 1𝑜N) → (𝐴 <N 1𝑜 ↔ ¬ (𝐴 = 1𝑜 ∨ 1𝑜 <N 𝐴)))
1261, 125mpan2 706 . . . 4 (𝐴N → (𝐴 <N 1𝑜 ↔ ¬ (𝐴 = 1𝑜 ∨ 1𝑜 <N 𝐴)))
127122, 126mtbii 316 . . 3 (𝐴N → ¬ ¬ (𝐴 = 1𝑜 ∨ 1𝑜 <N 𝐴))
128127notnotrd 128 . 2 (𝐴N → (𝐴 = 1𝑜 ∨ 1𝑜 <N 𝐴))
12910, 121, 128mpjaod 396 1 (𝐴N𝜏)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 383   ∧ wa 384   = wceq 1480   ∈ wcel 1987   ≠ wne 2790  Vcvv 3189   ⊆ wss 3559  ∅c0 3896   class class class wbr 4618   Or wor 4999  Ord word 5686  Oncon0 5687  suc csuc 5689  (class class class)co 6610  ωcom 7019  1𝑜c1o 7505   +𝑜 coa 7509  Ncnpi 9618   +N cpli 9619
 Copyright terms: Public domain W3C validator