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

Theorem indpi 10906
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 8480 . . . . . 6 1o ∈ V
21eqvinc 3638 . . . . 5 (1o = 𝐴 ↔ ∃𝑥(𝑥 = 1o𝑥 = 𝐴))
3 indpi.4 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜏))
4 indpi.5 . . . . . 6 𝜓
5 indpi.1 . . . . . 6 (𝑥 = 1o → (𝜑𝜓))
64, 5mpbiri 257 . . . . 5 (𝑥 = 1o𝜑)
72, 3, 6gencl 3514 . . . 4 (1o = 𝐴𝜏)
87eqcoms 2738 . . 3 (𝐴 = 1o𝜏)
98a1i 11 . 2 (𝐴N → (𝐴 = 1o𝜏))
10 pinn 10877 . . . . 5 (𝐴N𝐴 ∈ ω)
11 elni2 10876 . . . . . 6 (𝐴N ↔ (𝐴 ∈ ω ∧ ∅ ∈ 𝐴))
12 nnord 7867 . . . . . . . . 9 (𝐴 ∈ ω → Ord 𝐴)
13 ordsucss 7810 . . . . . . . . 9 (Ord 𝐴 → (∅ ∈ 𝐴 → suc ∅ ⊆ 𝐴))
1412, 13syl 17 . . . . . . . 8 (𝐴 ∈ ω → (∅ ∈ 𝐴 → suc ∅ ⊆ 𝐴))
15 df-1o 8470 . . . . . . . . 9 1o = suc ∅
1615sseq1i 4011 . . . . . . . 8 (1o𝐴 ↔ suc ∅ ⊆ 𝐴)
1714, 16imbitrrdi 251 . . . . . . 7 (𝐴 ∈ ω → (∅ ∈ 𝐴 → 1o𝐴))
1817imp 405 . . . . . 6 ((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) → 1o𝐴)
1911, 18sylbi 216 . . . . 5 (𝐴N → 1o𝐴)
20 1onn 8643 . . . . . 6 1o ∈ ω
21 eleq1 2819 . . . . . . . . 9 (𝑥 = 1o → (𝑥N ↔ 1oN))
22 breq2 5153 . . . . . . . . 9 (𝑥 = 1o → (1o <N 𝑥 ↔ 1o <N 1o))
2321, 22anbi12d 629 . . . . . . . 8 (𝑥 = 1o → ((𝑥N ∧ 1o <N 𝑥) ↔ (1oN ∧ 1o <N 1o)))
2423, 5imbi12d 343 . . . . . . 7 (𝑥 = 1o → (((𝑥N ∧ 1o <N 𝑥) → 𝜑) ↔ ((1oN ∧ 1o <N 1o) → 𝜓)))
25 eleq1 2819 . . . . . . . . 9 (𝑥 = 𝑦 → (𝑥N𝑦N))
26 breq2 5153 . . . . . . . . 9 (𝑥 = 𝑦 → (1o <N 𝑥 ↔ 1o <N 𝑦))
2725, 26anbi12d 629 . . . . . . . 8 (𝑥 = 𝑦 → ((𝑥N ∧ 1o <N 𝑥) ↔ (𝑦N ∧ 1o <N 𝑦)))
28 indpi.2 . . . . . . . 8 (𝑥 = 𝑦 → (𝜑𝜒))
2927, 28imbi12d 343 . . . . . . 7 (𝑥 = 𝑦 → (((𝑥N ∧ 1o <N 𝑥) → 𝜑) ↔ ((𝑦N ∧ 1o <N 𝑦) → 𝜒)))
30 pinn 10877 . . . . . . . . . . . . . . 15 (𝑥N𝑥 ∈ ω)
31 eleq1 2819 . . . . . . . . . . . . . . . 16 (𝑥 = suc 𝑦 → (𝑥 ∈ ω ↔ suc 𝑦 ∈ ω))
32 peano2b 7876 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ω ↔ suc 𝑦 ∈ ω)
3331, 32bitr4di 288 . . . . . . . . . . . . . . 15 (𝑥 = suc 𝑦 → (𝑥 ∈ ω ↔ 𝑦 ∈ ω))
3430, 33imbitrid 243 . . . . . . . . . . . . . 14 (𝑥 = suc 𝑦 → (𝑥N𝑦 ∈ ω))
3534adantrd 490 . . . . . . . . . . . . 13 (𝑥 = suc 𝑦 → ((𝑥N ∧ 1o <N 𝑥) → 𝑦 ∈ ω))
36 1pi 10882 . . . . . . . . . . . . . . . 16 1oN
37 ltpiord 10886 . . . . . . . . . . . . . . . 16 ((1oN𝑥N) → (1o <N 𝑥 ↔ 1o𝑥))
3836, 37mpan 686 . . . . . . . . . . . . . . 15 (𝑥N → (1o <N 𝑥 ↔ 1o𝑥))
3938biimpa 475 . . . . . . . . . . . . . 14 ((𝑥N ∧ 1o <N 𝑥) → 1o𝑥)
40 eleq2 2820 . . . . . . . . . . . . . . 15 (𝑥 = suc 𝑦 → (1o𝑥 ↔ 1o ∈ suc 𝑦))
41 elsuci 6432 . . . . . . . . . . . . . . . 16 (1o ∈ suc 𝑦 → (1o𝑦 ∨ 1o = 𝑦))
42 ne0i 4335 . . . . . . . . . . . . . . . . 17 (1o𝑦𝑦 ≠ ∅)
43 0lt1o 8508 . . . . . . . . . . . . . . . . . . 19 ∅ ∈ 1o
44 eleq2 2820 . . . . . . . . . . . . . . . . . . 19 (1o = 𝑦 → (∅ ∈ 1o ↔ ∅ ∈ 𝑦))
4543, 44mpbii 232 . . . . . . . . . . . . . . . . . 18 (1o = 𝑦 → ∅ ∈ 𝑦)
4645ne0d 4336 . . . . . . . . . . . . . . . . 17 (1o = 𝑦𝑦 ≠ ∅)
4742, 46jaoi 853 . . . . . . . . . . . . . . . 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 511 . . . . . . . . . . . 12 (𝑥 = suc 𝑦 → ((𝑥N ∧ 1o <N 𝑥) → (𝑦 ∈ ω ∧ 𝑦 ≠ ∅)))
52 elni 10875 . . . . . . . . . . . 12 (𝑦N ↔ (𝑦 ∈ ω ∧ 𝑦 ≠ ∅))
5351, 52imbitrrdi 251 . . . . . . . . . . 11 (𝑥 = suc 𝑦 → ((𝑥N ∧ 1o <N 𝑥) → 𝑦N))
54 simpr 483 . . . . . . . . . . . 12 ((𝑥N ∧ 1o <N 𝑥) → 1o <N 𝑥)
55 breq2 5153 . . . . . . . . . . . 12 (𝑥 = suc 𝑦 → (1o <N 𝑥 ↔ 1o <N suc 𝑦))
5654, 55imbitrid 243 . . . . . . . . . . 11 (𝑥 = suc 𝑦 → ((𝑥N ∧ 1o <N 𝑥) → 1o <N suc 𝑦))
5753, 56jcad 511 . . . . . . . . . 10 (𝑥 = suc 𝑦 → ((𝑥N ∧ 1o <N 𝑥) → (𝑦N ∧ 1o <N suc 𝑦)))
58 addclpi 10891 . . . . . . . . . . . . . . 15 ((𝑦N ∧ 1oN) → (𝑦 +N 1o) ∈ N)
5936, 58mpan2 687 . . . . . . . . . . . . . 14 (𝑦N → (𝑦 +N 1o) ∈ N)
60 addpiord 10883 . . . . . . . . . . . . . . . . . . 19 ((𝑦N ∧ 1oN) → (𝑦 +N 1o) = (𝑦 +o 1o))
6136, 60mpan2 687 . . . . . . . . . . . . . . . . . 18 (𝑦N → (𝑦 +N 1o) = (𝑦 +o 1o))
62 pion 10878 . . . . . . . . . . . . . . . . . . 19 (𝑦N𝑦 ∈ On)
63 oa1suc 8535 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ On → (𝑦 +o 1o) = suc 𝑦)
6462, 63syl 17 . . . . . . . . . . . . . . . . . 18 (𝑦N → (𝑦 +o 1o) = suc 𝑦)
6561, 64eqtrd 2770 . . . . . . . . . . . . . . . . 17 (𝑦N → (𝑦 +N 1o) = suc 𝑦)
6665eqeq2d 2741 . . . . . . . . . . . . . . . 16 (𝑦N → (𝑥 = (𝑦 +N 1o) ↔ 𝑥 = suc 𝑦))
6766biimparc 478 . . . . . . . . . . . . . . 15 ((𝑥 = suc 𝑦𝑦N) → 𝑥 = (𝑦 +N 1o))
6867eleq1d 2816 . . . . . . . . . . . . . 14 ((𝑥 = suc 𝑦𝑦N) → (𝑥N ↔ (𝑦 +N 1o) ∈ N))
6959, 68imbitrrid 245 . . . . . . . . . . . . 13 ((𝑥 = suc 𝑦𝑦N) → (𝑦N𝑥N))
7069ex 411 . . . . . . . . . . . 12 (𝑥 = suc 𝑦 → (𝑦N → (𝑦N𝑥N)))
7170pm2.43d 53 . . . . . . . . . . 11 (𝑥 = suc 𝑦 → (𝑦N𝑥N))
7255biimprd 247 . . . . . . . . . . 11 (𝑥 = suc 𝑦 → (1o <N suc 𝑦 → 1o <N 𝑥))
7371, 72anim12d 607 . . . . . . . . . 10 (𝑥 = suc 𝑦 → ((𝑦N ∧ 1o <N suc 𝑦) → (𝑥N ∧ 1o <N 𝑥)))
7457, 73impbid 211 . . . . . . . . 9 (𝑥 = suc 𝑦 → ((𝑥N ∧ 1o <N 𝑥) ↔ (𝑦N ∧ 1o <N suc 𝑦)))
7574imbi1d 340 . . . . . . . 8 (𝑥 = suc 𝑦 → (((𝑥N ∧ 1o <N 𝑥) → 𝜑) ↔ ((𝑦N ∧ 1o <N suc 𝑦) → 𝜑)))
76 indpi.3 . . . . . . . . . . . 12 (𝑥 = (𝑦 +N 1o) → (𝜑𝜃))
7766, 76syl6bir 253 . . . . . . . . . . 11 (𝑦N → (𝑥 = suc 𝑦 → (𝜑𝜃)))
7877adantr 479 . . . . . . . . . 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 2819 . . . . . . . . 9 (𝑥 = 𝐴 → (𝑥N𝐴N))
83 breq2 5153 . . . . . . . . 9 (𝑥 = 𝐴 → (1o <N 𝑥 ↔ 1o <N 𝐴))
8482, 83anbi12d 629 . . . . . . . 8 (𝑥 = 𝐴 → ((𝑥N ∧ 1o <N 𝑥) ↔ (𝐴N ∧ 1o <N 𝐴)))
8584, 3imbi12d 343 . . . . . . 7 (𝑥 = 𝐴 → (((𝑥N ∧ 1o <N 𝑥) → 𝜑) ↔ ((𝐴N ∧ 1o <N 𝐴) → 𝜏)))
8642a1i 12 . . . . . . 7 (1o ∈ ω → ((1oN ∧ 1o <N 1o) → 𝜓))
87 ltpiord 10886 . . . . . . . . . . . . . . 15 ((1oN𝑦N) → (1o <N 𝑦 ↔ 1o𝑦))
8836, 87mpan 686 . . . . . . . . . . . . . 14 (𝑦N → (1o <N 𝑦 ↔ 1o𝑦))
8988pm5.32i 573 . . . . . . . . . . . . 13 ((𝑦N ∧ 1o <N 𝑦) ↔ (𝑦N ∧ 1o𝑦))
9089simplbi2 499 . . . . . . . . . . . 12 (𝑦N → (1o𝑦 → (𝑦N ∧ 1o <N 𝑦)))
9190imim1d 82 . . . . . . . . . . 11 (𝑦N → (((𝑦N ∧ 1o <N 𝑦) → 𝜒) → (1o𝑦𝜒)))
92 ltrelpi 10888 . . . . . . . . . . . . . . 15 <N ⊆ (N × N)
9392brel 5742 . . . . . . . . . . . . . 14 (1o <N suc 𝑦 → (1oN ∧ suc 𝑦N))
94 ltpiord 10886 . . . . . . . . . . . . . 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 3638 . . . . . . . . . . . . . . 15 (1o = 𝑦 ↔ ∃𝑥(𝑥 = 1o𝑥 = 𝑦))
9897, 28, 6gencl 3514 . . . . . . . . . . . . . 14 (1o = 𝑦𝜒)
99 jao 957 . . . . . . . . . . . . . 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 409 . . . . . . . . 9 (((𝑦N ∧ 1o <N 𝑦) → 𝜒) → ((𝑦N ∧ 1o <N suc 𝑦) → 𝜒))
10515sseq1i 4011 . . . . . . . . . . 11 (1o𝑦 ↔ suc ∅ ⊆ 𝑦)
106 0ex 5308 . . . . . . . . . . . 12 ∅ ∈ V
107 sucssel 6460 . . . . . . . . . . . 12 (∅ ∈ V → (suc ∅ ⊆ 𝑦 → ∅ ∈ 𝑦))
108106, 107ax-mp 5 . . . . . . . . . . 11 (suc ∅ ⊆ 𝑦 → ∅ ∈ 𝑦)
109105, 108sylbi 216 . . . . . . . . . 10 (1o𝑦 → ∅ ∈ 𝑦)
110 elni2 10876 . . . . . . . . . . 11 (𝑦N ↔ (𝑦 ∈ ω ∧ ∅ ∈ 𝑦))
111 indpi.6 . . . . . . . . . . 11 (𝑦N → (𝜒𝜃))
112110, 111sylbir 234 . . . . . . . . . 10 ((𝑦 ∈ ω ∧ ∅ ∈ 𝑦) → (𝜒𝜃))
113109, 112sylan2 591 . . . . . . . . 9 ((𝑦 ∈ ω ∧ 1o𝑦) → (𝜒𝜃))
114104, 113syl9r 78 . . . . . . . 8 ((𝑦 ∈ ω ∧ 1o𝑦) → (((𝑦N ∧ 1o <N 𝑦) → 𝜒) → ((𝑦N ∧ 1o <N suc 𝑦) → 𝜃)))
115114adantlr 711 . . . . . . 7 (((𝑦 ∈ ω ∧ 1o ∈ ω) ∧ 1o𝑦) → (((𝑦N ∧ 1o <N 𝑦) → 𝜒) → ((𝑦N ∧ 1o <N suc 𝑦) → 𝜃)))
11624, 29, 81, 85, 86, 115findsg 7894 . . . . . 6 (((𝐴 ∈ ω ∧ 1o ∈ ω) ∧ 1o𝐴) → ((𝐴N ∧ 1o <N 𝐴) → 𝜏))
11720, 116mpanl2 697 . . . . 5 ((𝐴 ∈ ω ∧ 1o𝐴) → ((𝐴N ∧ 1o <N 𝐴) → 𝜏))
11810, 19, 117syl2anc 582 . . . 4 (𝐴N → ((𝐴N ∧ 1o <N 𝐴) → 𝜏))
119118expd 414 . . 3 (𝐴N → (𝐴N → (1o <N 𝐴𝜏)))
120119pm2.43i 52 . 2 (𝐴N → (1o <N 𝐴𝜏))
121 nlt1pi 10905 . . . 4 ¬ 𝐴 <N 1o
122 ltsopi 10887 . . . . . 6 <N Or N
123 sotric 5617 . . . . . 6 (( <N Or N ∧ (𝐴N ∧ 1oN)) → (𝐴 <N 1o ↔ ¬ (𝐴 = 1o ∨ 1o <N 𝐴)))
124122, 123mpan 686 . . . . 5 ((𝐴N ∧ 1oN) → (𝐴 <N 1o ↔ ¬ (𝐴 = 1o ∨ 1o <N 𝐴)))
12536, 124mpan2 687 . . . 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 856 1 (𝐴N𝜏)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394  wo 843   = wceq 1539  wcel 2104  wne 2938  Vcvv 3472  wss 3949  c0 4323   class class class wbr 5149   Or wor 5588  Ord word 6364  Oncon0 6365  suc csuc 6367  (class class class)co 7413  ωcom 7859  1oc1o 8463   +o coa 8467  Ncnpi 10843   +N cpli 10844   <N clti 10846
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7729
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-pss 3968  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5575  df-eprel 5581  df-po 5589  df-so 5590  df-fr 5632  df-we 5634  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-pred 6301  df-ord 6368  df-on 6369  df-lim 6370  df-suc 6371  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-ov 7416  df-oprab 7417  df-mpo 7418  df-om 7860  df-2nd 7980  df-frecs 8270  df-wrecs 8301  df-recs 8375  df-rdg 8414  df-1o 8470  df-oadd 8474  df-ni 10871  df-pli 10872  df-lti 10874
This theorem is referenced by:  prlem934  11032
  Copyright terms: Public domain W3C validator