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

Theorem indpi 10843
Description: Principle of Finite Induction on positive integers. (Contributed by NM, 23-Mar-1996.) (New usage is discouraged.)
Hypotheses
Ref Expression
indpi.1 (𝑥 = 1o → (𝜑𝜓))
indpi.2 (𝑥 = 𝑦 → (𝜑𝜒))
indpi.3 (𝑥 = (𝑦 +N 1o) → (𝜑𝜃))
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 1oex 8422 . . . . . 6 1o ∈ V
21eqvinc 3599 . . . . 5 (1o = 𝐴 ↔ ∃𝑥(𝑥 = 1o𝑥 = 𝐴))
3 indpi.4 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜏))
4 indpi.5 . . . . . 6 𝜓
5 indpi.1 . . . . . 6 (𝑥 = 1o → (𝜑𝜓))
64, 5mpbiri 257 . . . . 5 (𝑥 = 1o𝜑)
72, 3, 6gencl 3485 . . . 4 (1o = 𝐴𝜏)
87eqcoms 2744 . . 3 (𝐴 = 1o𝜏)
98a1i 11 . 2 (𝐴N → (𝐴 = 1o𝜏))
10 pinn 10814 . . . . 5 (𝐴N𝐴 ∈ ω)
11 elni2 10813 . . . . . 6 (𝐴N ↔ (𝐴 ∈ ω ∧ ∅ ∈ 𝐴))
12 nnord 7810 . . . . . . . . 9 (𝐴 ∈ ω → Ord 𝐴)
13 ordsucss 7753 . . . . . . . . 9 (Ord 𝐴 → (∅ ∈ 𝐴 → suc ∅ ⊆ 𝐴))
1412, 13syl 17 . . . . . . . 8 (𝐴 ∈ ω → (∅ ∈ 𝐴 → suc ∅ ⊆ 𝐴))
15 df-1o 8412 . . . . . . . . 9 1o = suc ∅
1615sseq1i 3972 . . . . . . . 8 (1o𝐴 ↔ suc ∅ ⊆ 𝐴)
1714, 16syl6ibr 251 . . . . . . 7 (𝐴 ∈ ω → (∅ ∈ 𝐴 → 1o𝐴))
1817imp 407 . . . . . 6 ((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) → 1o𝐴)
1911, 18sylbi 216 . . . . 5 (𝐴N → 1o𝐴)
20 1onn 8586 . . . . . 6 1o ∈ ω
21 eleq1 2825 . . . . . . . . 9 (𝑥 = 1o → (𝑥N ↔ 1oN))
22 breq2 5109 . . . . . . . . 9 (𝑥 = 1o → (1o <N 𝑥 ↔ 1o <N 1o))
2321, 22anbi12d 631 . . . . . . . 8 (𝑥 = 1o → ((𝑥N ∧ 1o <N 𝑥) ↔ (1oN ∧ 1o <N 1o)))
2423, 5imbi12d 344 . . . . . . 7 (𝑥 = 1o → (((𝑥N ∧ 1o <N 𝑥) → 𝜑) ↔ ((1oN ∧ 1o <N 1o) → 𝜓)))
25 eleq1 2825 . . . . . . . . 9 (𝑥 = 𝑦 → (𝑥N𝑦N))
26 breq2 5109 . . . . . . . . 9 (𝑥 = 𝑦 → (1o <N 𝑥 ↔ 1o <N 𝑦))
2725, 26anbi12d 631 . . . . . . . 8 (𝑥 = 𝑦 → ((𝑥N ∧ 1o <N 𝑥) ↔ (𝑦N ∧ 1o <N 𝑦)))
28 indpi.2 . . . . . . . 8 (𝑥 = 𝑦 → (𝜑𝜒))
2927, 28imbi12d 344 . . . . . . 7 (𝑥 = 𝑦 → (((𝑥N ∧ 1o <N 𝑥) → 𝜑) ↔ ((𝑦N ∧ 1o <N 𝑦) → 𝜒)))
30 pinn 10814 . . . . . . . . . . . . . . 15 (𝑥N𝑥 ∈ ω)
31 eleq1 2825 . . . . . . . . . . . . . . . 16 (𝑥 = suc 𝑦 → (𝑥 ∈ ω ↔ suc 𝑦 ∈ ω))
32 peano2b 7819 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ω ↔ suc 𝑦 ∈ ω)
3331, 32bitr4di 288 . . . . . . . . . . . . . . 15 (𝑥 = suc 𝑦 → (𝑥 ∈ ω ↔ 𝑦 ∈ ω))
3430, 33imbitrid 243 . . . . . . . . . . . . . 14 (𝑥 = suc 𝑦 → (𝑥N𝑦 ∈ ω))
3534adantrd 492 . . . . . . . . . . . . 13 (𝑥 = suc 𝑦 → ((𝑥N ∧ 1o <N 𝑥) → 𝑦 ∈ ω))
36 1pi 10819 . . . . . . . . . . . . . . . 16 1oN
37 ltpiord 10823 . . . . . . . . . . . . . . . 16 ((1oN𝑥N) → (1o <N 𝑥 ↔ 1o𝑥))
3836, 37mpan 688 . . . . . . . . . . . . . . 15 (𝑥N → (1o <N 𝑥 ↔ 1o𝑥))
3938biimpa 477 . . . . . . . . . . . . . 14 ((𝑥N ∧ 1o <N 𝑥) → 1o𝑥)
40 eleq2 2826 . . . . . . . . . . . . . . 15 (𝑥 = suc 𝑦 → (1o𝑥 ↔ 1o ∈ suc 𝑦))
41 elsuci 6384 . . . . . . . . . . . . . . . 16 (1o ∈ suc 𝑦 → (1o𝑦 ∨ 1o = 𝑦))
42 ne0i 4294 . . . . . . . . . . . . . . . . 17 (1o𝑦𝑦 ≠ ∅)
43 0lt1o 8450 . . . . . . . . . . . . . . . . . . 19 ∅ ∈ 1o
44 eleq2 2826 . . . . . . . . . . . . . . . . . . 19 (1o = 𝑦 → (∅ ∈ 1o ↔ ∅ ∈ 𝑦))
4543, 44mpbii 232 . . . . . . . . . . . . . . . . . 18 (1o = 𝑦 → ∅ ∈ 𝑦)
4645ne0d 4295 . . . . . . . . . . . . . . . . 17 (1o = 𝑦𝑦 ≠ ∅)
4742, 46jaoi 855 . . . . . . . . . . . . . . . 16 ((1o𝑦 ∨ 1o = 𝑦) → 𝑦 ≠ ∅)
4841, 47syl 17 . . . . . . . . . . . . . . 15 (1o ∈ suc 𝑦𝑦 ≠ ∅)
4940, 48syl6bi 252 . . . . . . . . . . . . . 14 (𝑥 = suc 𝑦 → (1o𝑥𝑦 ≠ ∅))
5039, 49syl5 34 . . . . . . . . . . . . 13 (𝑥 = suc 𝑦 → ((𝑥N ∧ 1o <N 𝑥) → 𝑦 ≠ ∅))
5135, 50jcad 513 . . . . . . . . . . . 12 (𝑥 = suc 𝑦 → ((𝑥N ∧ 1o <N 𝑥) → (𝑦 ∈ ω ∧ 𝑦 ≠ ∅)))
52 elni 10812 . . . . . . . . . . . 12 (𝑦N ↔ (𝑦 ∈ ω ∧ 𝑦 ≠ ∅))
5351, 52syl6ibr 251 . . . . . . . . . . 11 (𝑥 = suc 𝑦 → ((𝑥N ∧ 1o <N 𝑥) → 𝑦N))
54 simpr 485 . . . . . . . . . . . 12 ((𝑥N ∧ 1o <N 𝑥) → 1o <N 𝑥)
55 breq2 5109 . . . . . . . . . . . 12 (𝑥 = suc 𝑦 → (1o <N 𝑥 ↔ 1o <N suc 𝑦))
5654, 55imbitrid 243 . . . . . . . . . . 11 (𝑥 = suc 𝑦 → ((𝑥N ∧ 1o <N 𝑥) → 1o <N suc 𝑦))
5753, 56jcad 513 . . . . . . . . . 10 (𝑥 = suc 𝑦 → ((𝑥N ∧ 1o <N 𝑥) → (𝑦N ∧ 1o <N suc 𝑦)))
58 addclpi 10828 . . . . . . . . . . . . . . 15 ((𝑦N ∧ 1oN) → (𝑦 +N 1o) ∈ N)
5936, 58mpan2 689 . . . . . . . . . . . . . 14 (𝑦N → (𝑦 +N 1o) ∈ N)
60 addpiord 10820 . . . . . . . . . . . . . . . . . . 19 ((𝑦N ∧ 1oN) → (𝑦 +N 1o) = (𝑦 +o 1o))
6136, 60mpan2 689 . . . . . . . . . . . . . . . . . 18 (𝑦N → (𝑦 +N 1o) = (𝑦 +o 1o))
62 pion 10815 . . . . . . . . . . . . . . . . . . 19 (𝑦N𝑦 ∈ On)
63 oa1suc 8477 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ On → (𝑦 +o 1o) = suc 𝑦)
6462, 63syl 17 . . . . . . . . . . . . . . . . . 18 (𝑦N → (𝑦 +o 1o) = suc 𝑦)
6561, 64eqtrd 2776 . . . . . . . . . . . . . . . . 17 (𝑦N → (𝑦 +N 1o) = suc 𝑦)
6665eqeq2d 2747 . . . . . . . . . . . . . . . 16 (𝑦N → (𝑥 = (𝑦 +N 1o) ↔ 𝑥 = suc 𝑦))
6766biimparc 480 . . . . . . . . . . . . . . 15 ((𝑥 = suc 𝑦𝑦N) → 𝑥 = (𝑦 +N 1o))
6867eleq1d 2822 . . . . . . . . . . . . . 14 ((𝑥 = suc 𝑦𝑦N) → (𝑥N ↔ (𝑦 +N 1o) ∈ N))
6959, 68syl5ibr 245 . . . . . . . . . . . . 13 ((𝑥 = suc 𝑦𝑦N) → (𝑦N𝑥N))
7069ex 413 . . . . . . . . . . . 12 (𝑥 = suc 𝑦 → (𝑦N → (𝑦N𝑥N)))
7170pm2.43d 53 . . . . . . . . . . 11 (𝑥 = suc 𝑦 → (𝑦N𝑥N))
7255biimprd 247 . . . . . . . . . . 11 (𝑥 = suc 𝑦 → (1o <N suc 𝑦 → 1o <N 𝑥))
7371, 72anim12d 609 . . . . . . . . . 10 (𝑥 = suc 𝑦 → ((𝑦N ∧ 1o <N suc 𝑦) → (𝑥N ∧ 1o <N 𝑥)))
7457, 73impbid 211 . . . . . . . . 9 (𝑥 = suc 𝑦 → ((𝑥N ∧ 1o <N 𝑥) ↔ (𝑦N ∧ 1o <N suc 𝑦)))
7574imbi1d 341 . . . . . . . 8 (𝑥 = suc 𝑦 → (((𝑥N ∧ 1o <N 𝑥) → 𝜑) ↔ ((𝑦N ∧ 1o <N suc 𝑦) → 𝜑)))
76 indpi.3 . . . . . . . . . . . 12 (𝑥 = (𝑦 +N 1o) → (𝜑𝜃))
7766, 76syl6bir 253 . . . . . . . . . . 11 (𝑦N → (𝑥 = suc 𝑦 → (𝜑𝜃)))
7877adantr 481 . . . . . . . . . 10 ((𝑦N ∧ 1o <N suc 𝑦) → (𝑥 = suc 𝑦 → (𝜑𝜃)))
7978com12 32 . . . . . . . . 9 (𝑥 = suc 𝑦 → ((𝑦N ∧ 1o <N suc 𝑦) → (𝜑𝜃)))
8079pm5.74d 272 . . . . . . . 8 (𝑥 = suc 𝑦 → (((𝑦N ∧ 1o <N suc 𝑦) → 𝜑) ↔ ((𝑦N ∧ 1o <N suc 𝑦) → 𝜃)))
8175, 80bitrd 278 . . . . . . 7 (𝑥 = suc 𝑦 → (((𝑥N ∧ 1o <N 𝑥) → 𝜑) ↔ ((𝑦N ∧ 1o <N suc 𝑦) → 𝜃)))
82 eleq1 2825 . . . . . . . . 9 (𝑥 = 𝐴 → (𝑥N𝐴N))
83 breq2 5109 . . . . . . . . 9 (𝑥 = 𝐴 → (1o <N 𝑥 ↔ 1o <N 𝐴))
8482, 83anbi12d 631 . . . . . . . 8 (𝑥 = 𝐴 → ((𝑥N ∧ 1o <N 𝑥) ↔ (𝐴N ∧ 1o <N 𝐴)))
8584, 3imbi12d 344 . . . . . . 7 (𝑥 = 𝐴 → (((𝑥N ∧ 1o <N 𝑥) → 𝜑) ↔ ((𝐴N ∧ 1o <N 𝐴) → 𝜏)))
8642a1i 12 . . . . . . 7 (1o ∈ ω → ((1oN ∧ 1o <N 1o) → 𝜓))
87 ltpiord 10823 . . . . . . . . . . . . . . 15 ((1oN𝑦N) → (1o <N 𝑦 ↔ 1o𝑦))
8836, 87mpan 688 . . . . . . . . . . . . . 14 (𝑦N → (1o <N 𝑦 ↔ 1o𝑦))
8988pm5.32i 575 . . . . . . . . . . . . 13 ((𝑦N ∧ 1o <N 𝑦) ↔ (𝑦N ∧ 1o𝑦))
9089simplbi2 501 . . . . . . . . . . . 12 (𝑦N → (1o𝑦 → (𝑦N ∧ 1o <N 𝑦)))
9190imim1d 82 . . . . . . . . . . 11 (𝑦N → (((𝑦N ∧ 1o <N 𝑦) → 𝜒) → (1o𝑦𝜒)))
92 ltrelpi 10825 . . . . . . . . . . . . . . 15 <N ⊆ (N × N)
9392brel 5697 . . . . . . . . . . . . . 14 (1o <N suc 𝑦 → (1oN ∧ suc 𝑦N))
94 ltpiord 10823 . . . . . . . . . . . . . 14 ((1oN ∧ suc 𝑦N) → (1o <N suc 𝑦 ↔ 1o ∈ suc 𝑦))
9593, 94syl 17 . . . . . . . . . . . . 13 (1o <N suc 𝑦 → (1o <N suc 𝑦 ↔ 1o ∈ suc 𝑦))
9695ibi 266 . . . . . . . . . . . 12 (1o <N suc 𝑦 → 1o ∈ suc 𝑦)
971eqvinc 3599 . . . . . . . . . . . . . . 15 (1o = 𝑦 ↔ ∃𝑥(𝑥 = 1o𝑥 = 𝑦))
9897, 28, 6gencl 3485 . . . . . . . . . . . . . 14 (1o = 𝑦𝜒)
99 jao 959 . . . . . . . . . . . . . 14 ((1o𝑦𝜒) → ((1o = 𝑦𝜒) → ((1o𝑦 ∨ 1o = 𝑦) → 𝜒)))
10098, 99mpi 20 . . . . . . . . . . . . 13 ((1o𝑦𝜒) → ((1o𝑦 ∨ 1o = 𝑦) → 𝜒))
10141, 100syl5 34 . . . . . . . . . . . 12 ((1o𝑦𝜒) → (1o ∈ suc 𝑦𝜒))
10296, 101syl5 34 . . . . . . . . . . 11 ((1o𝑦𝜒) → (1o <N suc 𝑦𝜒))
10391, 102syl6com 37 . . . . . . . . . 10 (((𝑦N ∧ 1o <N 𝑦) → 𝜒) → (𝑦N → (1o <N suc 𝑦𝜒)))
104103impd 411 . . . . . . . . 9 (((𝑦N ∧ 1o <N 𝑦) → 𝜒) → ((𝑦N ∧ 1o <N suc 𝑦) → 𝜒))
10515sseq1i 3972 . . . . . . . . . . 11 (1o𝑦 ↔ suc ∅ ⊆ 𝑦)
106 0ex 5264 . . . . . . . . . . . 12 ∅ ∈ V
107 sucssel 6412 . . . . . . . . . . . 12 (∅ ∈ V → (suc ∅ ⊆ 𝑦 → ∅ ∈ 𝑦))
108106, 107ax-mp 5 . . . . . . . . . . 11 (suc ∅ ⊆ 𝑦 → ∅ ∈ 𝑦)
109105, 108sylbi 216 . . . . . . . . . 10 (1o𝑦 → ∅ ∈ 𝑦)
110 elni2 10813 . . . . . . . . . . 11 (𝑦N ↔ (𝑦 ∈ ω ∧ ∅ ∈ 𝑦))
111 indpi.6 . . . . . . . . . . 11 (𝑦N → (𝜒𝜃))
112110, 111sylbir 234 . . . . . . . . . 10 ((𝑦 ∈ ω ∧ ∅ ∈ 𝑦) → (𝜒𝜃))
113109, 112sylan2 593 . . . . . . . . 9 ((𝑦 ∈ ω ∧ 1o𝑦) → (𝜒𝜃))
114104, 113syl9r 78 . . . . . . . 8 ((𝑦 ∈ ω ∧ 1o𝑦) → (((𝑦N ∧ 1o <N 𝑦) → 𝜒) → ((𝑦N ∧ 1o <N suc 𝑦) → 𝜃)))
115114adantlr 713 . . . . . . 7 (((𝑦 ∈ ω ∧ 1o ∈ ω) ∧ 1o𝑦) → (((𝑦N ∧ 1o <N 𝑦) → 𝜒) → ((𝑦N ∧ 1o <N suc 𝑦) → 𝜃)))
11624, 29, 81, 85, 86, 115findsg 7836 . . . . . 6 (((𝐴 ∈ ω ∧ 1o ∈ ω) ∧ 1o𝐴) → ((𝐴N ∧ 1o <N 𝐴) → 𝜏))
11720, 116mpanl2 699 . . . . 5 ((𝐴 ∈ ω ∧ 1o𝐴) → ((𝐴N ∧ 1o <N 𝐴) → 𝜏))
11810, 19, 117syl2anc 584 . . . 4 (𝐴N → ((𝐴N ∧ 1o <N 𝐴) → 𝜏))
119118expd 416 . . 3 (𝐴N → (𝐴N → (1o <N 𝐴𝜏)))
120119pm2.43i 52 . 2 (𝐴N → (1o <N 𝐴𝜏))
121 nlt1pi 10842 . . . 4 ¬ 𝐴 <N 1o
122 ltsopi 10824 . . . . . 6 <N Or N
123 sotric 5573 . . . . . 6 (( <N Or N ∧ (𝐴N ∧ 1oN)) → (𝐴 <N 1o ↔ ¬ (𝐴 = 1o ∨ 1o <N 𝐴)))
124122, 123mpan 688 . . . . 5 ((𝐴N ∧ 1oN) → (𝐴 <N 1o ↔ ¬ (𝐴 = 1o ∨ 1o <N 𝐴)))
12536, 124mpan2 689 . . . 4 (𝐴N → (𝐴 <N 1o ↔ ¬ (𝐴 = 1o ∨ 1o <N 𝐴)))
126121, 125mtbii 325 . . 3 (𝐴N → ¬ ¬ (𝐴 = 1o ∨ 1o <N 𝐴))
127126notnotrd 133 . 2 (𝐴N → (𝐴 = 1o ∨ 1o <N 𝐴))
1289, 120, 127mpjaod 858 1 (𝐴N𝜏)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 396  wo 845   = wceq 1541  wcel 2106  wne 2943  Vcvv 3445  wss 3910  c0 4282   class class class wbr 5105   Or wor 5544  Ord word 6316  Oncon0 6317  suc csuc 6319  (class class class)co 7357  ωcom 7802  1oc1o 8405   +o coa 8409  Ncnpi 10780   +N cpli 10781   <N clti 10783
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pr 5384  ax-un 7672
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-oadd 8416  df-ni 10808  df-pli 10809  df-lti 10811
This theorem is referenced by:  prlem934  10969
  Copyright terms: Public domain W3C validator