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

Theorem indpi 10051
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 1pi 10027 . . . . . . 7 1oN
21elexi 3430 . . . . . 6 1o ∈ V
32eqvinc 3548 . . . . 5 (1o = 𝐴 ↔ ∃𝑥(𝑥 = 1o𝑥 = 𝐴))
4 indpi.4 . . . . 5 (𝑥 = 𝐴 → (𝜑𝜏))
5 indpi.5 . . . . . 6 𝜓
6 indpi.1 . . . . . 6 (𝑥 = 1o → (𝜑𝜓))
75, 6mpbiri 250 . . . . 5 (𝑥 = 1o𝜑)
83, 4, 7gencl 3452 . . . 4 (1o = 𝐴𝜏)
98eqcoms 2833 . . 3 (𝐴 = 1o𝜏)
109a1i 11 . 2 (𝐴N → (𝐴 = 1o𝜏))
11 pinn 10022 . . . . 5 (𝐴N𝐴 ∈ ω)
12 elni2 10021 . . . . . 6 (𝐴N ↔ (𝐴 ∈ ω ∧ ∅ ∈ 𝐴))
13 nnord 7339 . . . . . . . . 9 (𝐴 ∈ ω → Ord 𝐴)
14 ordsucss 7284 . . . . . . . . 9 (Ord 𝐴 → (∅ ∈ 𝐴 → suc ∅ ⊆ 𝐴))
1513, 14syl 17 . . . . . . . 8 (𝐴 ∈ ω → (∅ ∈ 𝐴 → suc ∅ ⊆ 𝐴))
16 df-1o 7831 . . . . . . . . 9 1o = suc ∅
1716sseq1i 3854 . . . . . . . 8 (1o𝐴 ↔ suc ∅ ⊆ 𝐴)
1815, 17syl6ibr 244 . . . . . . 7 (𝐴 ∈ ω → (∅ ∈ 𝐴 → 1o𝐴))
1918imp 397 . . . . . 6 ((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) → 1o𝐴)
2012, 19sylbi 209 . . . . 5 (𝐴N → 1o𝐴)
21 1onn 7991 . . . . . 6 1o ∈ ω
22 eleq1 2894 . . . . . . . . 9 (𝑥 = 1o → (𝑥N ↔ 1oN))
23 breq2 4879 . . . . . . . . 9 (𝑥 = 1o → (1o <N 𝑥 ↔ 1o <N 1o))
2422, 23anbi12d 624 . . . . . . . 8 (𝑥 = 1o → ((𝑥N ∧ 1o <N 𝑥) ↔ (1oN ∧ 1o <N 1o)))
2524, 6imbi12d 336 . . . . . . 7 (𝑥 = 1o → (((𝑥N ∧ 1o <N 𝑥) → 𝜑) ↔ ((1oN ∧ 1o <N 1o) → 𝜓)))
26 eleq1 2894 . . . . . . . . 9 (𝑥 = 𝑦 → (𝑥N𝑦N))
27 breq2 4879 . . . . . . . . 9 (𝑥 = 𝑦 → (1o <N 𝑥 ↔ 1o <N 𝑦))
2826, 27anbi12d 624 . . . . . . . 8 (𝑥 = 𝑦 → ((𝑥N ∧ 1o <N 𝑥) ↔ (𝑦N ∧ 1o <N 𝑦)))
29 indpi.2 . . . . . . . 8 (𝑥 = 𝑦 → (𝜑𝜒))
3028, 29imbi12d 336 . . . . . . 7 (𝑥 = 𝑦 → (((𝑥N ∧ 1o <N 𝑥) → 𝜑) ↔ ((𝑦N ∧ 1o <N 𝑦) → 𝜒)))
31 pinn 10022 . . . . . . . . . . . . . . 15 (𝑥N𝑥 ∈ ω)
32 eleq1 2894 . . . . . . . . . . . . . . . 16 (𝑥 = suc 𝑦 → (𝑥 ∈ ω ↔ suc 𝑦 ∈ ω))
33 peano2b 7347 . . . . . . . . . . . . . . . 16 (𝑦 ∈ ω ↔ suc 𝑦 ∈ ω)
3432, 33syl6bbr 281 . . . . . . . . . . . . . . 15 (𝑥 = suc 𝑦 → (𝑥 ∈ ω ↔ 𝑦 ∈ ω))
3531, 34syl5ib 236 . . . . . . . . . . . . . 14 (𝑥 = suc 𝑦 → (𝑥N𝑦 ∈ ω))
3635adantrd 487 . . . . . . . . . . . . 13 (𝑥 = suc 𝑦 → ((𝑥N ∧ 1o <N 𝑥) → 𝑦 ∈ ω))
37 ltpiord 10031 . . . . . . . . . . . . . . . 16 ((1oN𝑥N) → (1o <N 𝑥 ↔ 1o𝑥))
381, 37mpan 681 . . . . . . . . . . . . . . 15 (𝑥N → (1o <N 𝑥 ↔ 1o𝑥))
3938biimpa 470 . . . . . . . . . . . . . 14 ((𝑥N ∧ 1o <N 𝑥) → 1o𝑥)
40 eleq2 2895 . . . . . . . . . . . . . . 15 (𝑥 = suc 𝑦 → (1o𝑥 ↔ 1o ∈ suc 𝑦))
41 elsuci 6033 . . . . . . . . . . . . . . . 16 (1o ∈ suc 𝑦 → (1o𝑦 ∨ 1o = 𝑦))
42 ne0i 4152 . . . . . . . . . . . . . . . . 17 (1o𝑦𝑦 ≠ ∅)
43 0lt1o 7856 . . . . . . . . . . . . . . . . . . 19 ∅ ∈ 1o
44 eleq2 2895 . . . . . . . . . . . . . . . . . . 19 (1o = 𝑦 → (∅ ∈ 1o ↔ ∅ ∈ 𝑦))
4543, 44mpbii 225 . . . . . . . . . . . . . . . . . 18 (1o = 𝑦 → ∅ ∈ 𝑦)
4645ne0d 4153 . . . . . . . . . . . . . . . . 17 (1o = 𝑦𝑦 ≠ ∅)
4742, 46jaoi 888 . . . . . . . . . . . . . . . 16 ((1o𝑦 ∨ 1o = 𝑦) → 𝑦 ≠ ∅)
4841, 47syl 17 . . . . . . . . . . . . . . 15 (1o ∈ suc 𝑦𝑦 ≠ ∅)
4940, 48syl6bi 245 . . . . . . . . . . . . . 14 (𝑥 = suc 𝑦 → (1o𝑥𝑦 ≠ ∅))
5039, 49syl5 34 . . . . . . . . . . . . 13 (𝑥 = suc 𝑦 → ((𝑥N ∧ 1o <N 𝑥) → 𝑦 ≠ ∅))
5136, 50jcad 508 . . . . . . . . . . . 12 (𝑥 = suc 𝑦 → ((𝑥N ∧ 1o <N 𝑥) → (𝑦 ∈ ω ∧ 𝑦 ≠ ∅)))
52 elni 10020 . . . . . . . . . . . 12 (𝑦N ↔ (𝑦 ∈ ω ∧ 𝑦 ≠ ∅))
5351, 52syl6ibr 244 . . . . . . . . . . 11 (𝑥 = suc 𝑦 → ((𝑥N ∧ 1o <N 𝑥) → 𝑦N))
54 simpr 479 . . . . . . . . . . . 12 ((𝑥N ∧ 1o <N 𝑥) → 1o <N 𝑥)
55 breq2 4879 . . . . . . . . . . . 12 (𝑥 = suc 𝑦 → (1o <N 𝑥 ↔ 1o <N suc 𝑦))
5654, 55syl5ib 236 . . . . . . . . . . 11 (𝑥 = suc 𝑦 → ((𝑥N ∧ 1o <N 𝑥) → 1o <N suc 𝑦))
5753, 56jcad 508 . . . . . . . . . 10 (𝑥 = suc 𝑦 → ((𝑥N ∧ 1o <N 𝑥) → (𝑦N ∧ 1o <N suc 𝑦)))
58 addclpi 10036 . . . . . . . . . . . . . . 15 ((𝑦N ∧ 1oN) → (𝑦 +N 1o) ∈ N)
591, 58mpan2 682 . . . . . . . . . . . . . 14 (𝑦N → (𝑦 +N 1o) ∈ N)
60 addpiord 10028 . . . . . . . . . . . . . . . . . . 19 ((𝑦N ∧ 1oN) → (𝑦 +N 1o) = (𝑦 +o 1o))
611, 60mpan2 682 . . . . . . . . . . . . . . . . . 18 (𝑦N → (𝑦 +N 1o) = (𝑦 +o 1o))
62 pion 10023 . . . . . . . . . . . . . . . . . . 19 (𝑦N𝑦 ∈ On)
63 oa1suc 7883 . . . . . . . . . . . . . . . . . . 19 (𝑦 ∈ On → (𝑦 +o 1o) = suc 𝑦)
6462, 63syl 17 . . . . . . . . . . . . . . . . . 18 (𝑦N → (𝑦 +o 1o) = suc 𝑦)
6561, 64eqtrd 2861 . . . . . . . . . . . . . . . . 17 (𝑦N → (𝑦 +N 1o) = suc 𝑦)
6665eqeq2d 2835 . . . . . . . . . . . . . . . 16 (𝑦N → (𝑥 = (𝑦 +N 1o) ↔ 𝑥 = suc 𝑦))
6766biimparc 473 . . . . . . . . . . . . . . 15 ((𝑥 = suc 𝑦𝑦N) → 𝑥 = (𝑦 +N 1o))
6867eleq1d 2891 . . . . . . . . . . . . . 14 ((𝑥 = suc 𝑦𝑦N) → (𝑥N ↔ (𝑦 +N 1o) ∈ N))
6959, 68syl5ibr 238 . . . . . . . . . . . . 13 ((𝑥 = suc 𝑦𝑦N) → (𝑦N𝑥N))
7069ex 403 . . . . . . . . . . . 12 (𝑥 = suc 𝑦 → (𝑦N → (𝑦N𝑥N)))
7170pm2.43d 53 . . . . . . . . . . 11 (𝑥 = suc 𝑦 → (𝑦N𝑥N))
7255biimprd 240 . . . . . . . . . . 11 (𝑥 = suc 𝑦 → (1o <N suc 𝑦 → 1o <N 𝑥))
7371, 72anim12d 602 . . . . . . . . . 10 (𝑥 = suc 𝑦 → ((𝑦N ∧ 1o <N suc 𝑦) → (𝑥N ∧ 1o <N 𝑥)))
7457, 73impbid 204 . . . . . . . . 9 (𝑥 = suc 𝑦 → ((𝑥N ∧ 1o <N 𝑥) ↔ (𝑦N ∧ 1o <N suc 𝑦)))
7574imbi1d 333 . . . . . . . 8 (𝑥 = suc 𝑦 → (((𝑥N ∧ 1o <N 𝑥) → 𝜑) ↔ ((𝑦N ∧ 1o <N suc 𝑦) → 𝜑)))
76 indpi.3 . . . . . . . . . . . 12 (𝑥 = (𝑦 +N 1o) → (𝜑𝜃))
7766, 76syl6bir 246 . . . . . . . . . . 11 (𝑦N → (𝑥 = suc 𝑦 → (𝜑𝜃)))
7877adantr 474 . . . . . . . . . 10 ((𝑦N ∧ 1o <N suc 𝑦) → (𝑥 = suc 𝑦 → (𝜑𝜃)))
7978com12 32 . . . . . . . . 9 (𝑥 = suc 𝑦 → ((𝑦N ∧ 1o <N suc 𝑦) → (𝜑𝜃)))
8079pm5.74d 265 . . . . . . . 8 (𝑥 = suc 𝑦 → (((𝑦N ∧ 1o <N suc 𝑦) → 𝜑) ↔ ((𝑦N ∧ 1o <N suc 𝑦) → 𝜃)))
8175, 80bitrd 271 . . . . . . 7 (𝑥 = suc 𝑦 → (((𝑥N ∧ 1o <N 𝑥) → 𝜑) ↔ ((𝑦N ∧ 1o <N suc 𝑦) → 𝜃)))
82 eleq1 2894 . . . . . . . . 9 (𝑥 = 𝐴 → (𝑥N𝐴N))
83 breq2 4879 . . . . . . . . 9 (𝑥 = 𝐴 → (1o <N 𝑥 ↔ 1o <N 𝐴))
8482, 83anbi12d 624 . . . . . . . 8 (𝑥 = 𝐴 → ((𝑥N ∧ 1o <N 𝑥) ↔ (𝐴N ∧ 1o <N 𝐴)))
8584, 4imbi12d 336 . . . . . . 7 (𝑥 = 𝐴 → (((𝑥N ∧ 1o <N 𝑥) → 𝜑) ↔ ((𝐴N ∧ 1o <N 𝐴) → 𝜏)))
8652a1i 12 . . . . . . 7 (1o ∈ ω → ((1oN ∧ 1o <N 1o) → 𝜓))
87 ltpiord 10031 . . . . . . . . . . . . . . 15 ((1oN𝑦N) → (1o <N 𝑦 ↔ 1o𝑦))
881, 87mpan 681 . . . . . . . . . . . . . 14 (𝑦N → (1o <N 𝑦 ↔ 1o𝑦))
8988pm5.32i 570 . . . . . . . . . . . . 13 ((𝑦N ∧ 1o <N 𝑦) ↔ (𝑦N ∧ 1o𝑦))
9089simplbi2 496 . . . . . . . . . . . 12 (𝑦N → (1o𝑦 → (𝑦N ∧ 1o <N 𝑦)))
9190imim1d 82 . . . . . . . . . . 11 (𝑦N → (((𝑦N ∧ 1o <N 𝑦) → 𝜒) → (1o𝑦𝜒)))
92 ltrelpi 10033 . . . . . . . . . . . . . . 15 <N ⊆ (N × N)
9392brel 5405 . . . . . . . . . . . . . 14 (1o <N suc 𝑦 → (1oN ∧ suc 𝑦N))
94 ltpiord 10031 . . . . . . . . . . . . . 14 ((1oN ∧ suc 𝑦N) → (1o <N suc 𝑦 ↔ 1o ∈ suc 𝑦))
9593, 94syl 17 . . . . . . . . . . . . 13 (1o <N suc 𝑦 → (1o <N suc 𝑦 ↔ 1o ∈ suc 𝑦))
9695ibi 259 . . . . . . . . . . . 12 (1o <N suc 𝑦 → 1o ∈ suc 𝑦)
972eqvinc 3548 . . . . . . . . . . . . . . 15 (1o = 𝑦 ↔ ∃𝑥(𝑥 = 1o𝑥 = 𝑦))
9897, 29, 7gencl 3452 . . . . . . . . . . . . . 14 (1o = 𝑦𝜒)
99 jao 988 . . . . . . . . . . . . . 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 400 . . . . . . . . 9 (((𝑦N ∧ 1o <N 𝑦) → 𝜒) → ((𝑦N ∧ 1o <N suc 𝑦) → 𝜒))
10516sseq1i 3854 . . . . . . . . . . 11 (1o𝑦 ↔ suc ∅ ⊆ 𝑦)
106 0ex 5016 . . . . . . . . . . . 12 ∅ ∈ V
107 sucssel 6059 . . . . . . . . . . . 12 (∅ ∈ V → (suc ∅ ⊆ 𝑦 → ∅ ∈ 𝑦))
108106, 107ax-mp 5 . . . . . . . . . . 11 (suc ∅ ⊆ 𝑦 → ∅ ∈ 𝑦)
109105, 108sylbi 209 . . . . . . . . . 10 (1o𝑦 → ∅ ∈ 𝑦)
110 elni2 10021 . . . . . . . . . . 11 (𝑦N ↔ (𝑦 ∈ ω ∧ ∅ ∈ 𝑦))
111 indpi.6 . . . . . . . . . . 11 (𝑦N → (𝜒𝜃))
112110, 111sylbir 227 . . . . . . . . . 10 ((𝑦 ∈ ω ∧ ∅ ∈ 𝑦) → (𝜒𝜃))
113109, 112sylan2 586 . . . . . . . . 9 ((𝑦 ∈ ω ∧ 1o𝑦) → (𝜒𝜃))
114104, 113syl9r 78 . . . . . . . 8 ((𝑦 ∈ ω ∧ 1o𝑦) → (((𝑦N ∧ 1o <N 𝑦) → 𝜒) → ((𝑦N ∧ 1o <N suc 𝑦) → 𝜃)))
115114adantlr 706 . . . . . . 7 (((𝑦 ∈ ω ∧ 1o ∈ ω) ∧ 1o𝑦) → (((𝑦N ∧ 1o <N 𝑦) → 𝜒) → ((𝑦N ∧ 1o <N suc 𝑦) → 𝜃)))
11625, 30, 81, 85, 86, 115findsg 7359 . . . . . 6 (((𝐴 ∈ ω ∧ 1o ∈ ω) ∧ 1o𝐴) → ((𝐴N ∧ 1o <N 𝐴) → 𝜏))
11721, 116mpanl2 692 . . . . 5 ((𝐴 ∈ ω ∧ 1o𝐴) → ((𝐴N ∧ 1o <N 𝐴) → 𝜏))
11811, 20, 117syl2anc 579 . . . 4 (𝐴N → ((𝐴N ∧ 1o <N 𝐴) → 𝜏))
119118expd 406 . . 3 (𝐴N → (𝐴N → (1o <N 𝐴𝜏)))
120119pm2.43i 52 . 2 (𝐴N → (1o <N 𝐴𝜏))
121 nlt1pi 10050 . . . 4 ¬ 𝐴 <N 1o
122 ltsopi 10032 . . . . . 6 <N Or N
123 sotric 5292 . . . . . 6 (( <N Or N ∧ (𝐴N ∧ 1oN)) → (𝐴 <N 1o ↔ ¬ (𝐴 = 1o ∨ 1o <N 𝐴)))
124122, 123mpan 681 . . . . 5 ((𝐴N ∧ 1oN) → (𝐴 <N 1o ↔ ¬ (𝐴 = 1o ∨ 1o <N 𝐴)))
1251, 124mpan2 682 . . . 4 (𝐴N → (𝐴 <N 1o ↔ ¬ (𝐴 = 1o ∨ 1o <N 𝐴)))
126121, 125mtbii 318 . . 3 (𝐴N → ¬ ¬ (𝐴 = 1o ∨ 1o <N 𝐴))
127126notnotrd 131 . 2 (𝐴N → (𝐴 = 1o ∨ 1o <N 𝐴))
12810, 120, 127mpjaod 891 1 (𝐴N𝜏)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 386  wo 878   = wceq 1656  wcel 2164  wne 2999  Vcvv 3414  wss 3798  c0 4146   class class class wbr 4875   Or wor 5264  Ord word 5966  Oncon0 5967  suc csuc 5969  (class class class)co 6910  ωcom 7331  1oc1o 7824   +o coa 7828  Ncnpi 9988   +N cpli 9989   <N clti 9991
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-8 2166  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-13 2389  ax-ext 2803  ax-sep 5007  ax-nul 5015  ax-pow 5067  ax-pr 5129  ax-un 7214
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-3or 1112  df-3an 1113  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-ne 3000  df-ral 3122  df-rex 3123  df-reu 3124  df-rab 3126  df-v 3416  df-sbc 3663  df-csb 3758  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-pss 3814  df-nul 4147  df-if 4309  df-pw 4382  df-sn 4400  df-pr 4402  df-tp 4404  df-op 4406  df-uni 4661  df-iun 4744  df-br 4876  df-opab 4938  df-mpt 4955  df-tr 4978  df-id 5252  df-eprel 5257  df-po 5265  df-so 5266  df-fr 5305  df-we 5307  df-xp 5352  df-rel 5353  df-cnv 5354  df-co 5355  df-dm 5356  df-rn 5357  df-res 5358  df-ima 5359  df-pred 5924  df-ord 5970  df-on 5971  df-lim 5972  df-suc 5973  df-iota 6090  df-fun 6129  df-fn 6130  df-f 6131  df-f1 6132  df-fo 6133  df-f1o 6134  df-fv 6135  df-ov 6913  df-oprab 6914  df-mpt2 6915  df-om 7332  df-wrecs 7677  df-recs 7739  df-rdg 7777  df-1o 7831  df-oadd 7835  df-ni 10016  df-pli 10017  df-lti 10019
This theorem is referenced by:  prlem934  10177
  Copyright terms: Public domain W3C validator