This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem indpi

Description: Principle of Finite Induction on positive integers. (Contributed by NM, 23-Mar-1996) (New usage is discouraged.)

Ref Expression
Hypotheses indpi.1 ⊢ ( 𝑥 = 1o → ( 𝜑 ↔ 𝜓 ) )
indpi.2 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜒 ) )
indpi.3 ⊢ ( 𝑥 = ( 𝑦 +N 1o ) → ( 𝜑 ↔ 𝜃 ) )
indpi.4 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜏 ) )
indpi.5 ⊢ 𝜓
indpi.6 ⊢ ( 𝑦 ∈ N → ( 𝜒 → 𝜃 ) )
Assertion indpi ( 𝐴 ∈ N → 𝜏 )

Proof

Step Hyp Ref Expression
1 indpi.1 ⊢ ( 𝑥 = 1o → ( 𝜑 ↔ 𝜓 ) )
2 indpi.2 ⊢ ( 𝑥 = 𝑦 → ( 𝜑 ↔ 𝜒 ) )
3 indpi.3 ⊢ ( 𝑥 = ( 𝑦 +N 1o ) → ( 𝜑 ↔ 𝜃 ) )
4 indpi.4 ⊢ ( 𝑥 = 𝐴 → ( 𝜑 ↔ 𝜏 ) )
5 indpi.5 ⊢ 𝜓
6 indpi.6 ⊢ ( 𝑦 ∈ N → ( 𝜒 → 𝜃 ) )
7 1oex ⊢ 1o ∈ V
8 7 eqvinc ⊢ ( 1o = 𝐴 ↔ ∃ 𝑥 ( 𝑥 = 1o ∧ 𝑥 = 𝐴 ) )
9 5 1 mpbiri ⊢ ( 𝑥 = 1o → 𝜑 )
10 8 4 9 gencl ⊢ ( 1o = 𝐴 → 𝜏 )
11 10 eqcoms ⊢ ( 𝐴 = 1o → 𝜏 )
12 11 a1i ⊢ ( 𝐴 ∈ N → ( 𝐴 = 1o → 𝜏 ) )
13 pinn ⊢ ( 𝐴 ∈ N → 𝐴 ∈ ω )
14 elni2 ⊢ ( 𝐴 ∈ N ↔ ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) )
15 nnord ⊢ ( 𝐴 ∈ ω → Ord 𝐴 )
16 ordsucss ⊢ ( Ord 𝐴 → ( ∅ ∈ 𝐴 → suc ∅ ⊆ 𝐴 ) )
17 15 16 syl ⊢ ( 𝐴 ∈ ω → ( ∅ ∈ 𝐴 → suc ∅ ⊆ 𝐴 ) )
18 df-1o ⊢ 1o = suc ∅
19 18 sseq1i ⊢ ( 1o ⊆ 𝐴 ↔ suc ∅ ⊆ 𝐴 )
20 17 19 imbitrrdi ⊢ ( 𝐴 ∈ ω → ( ∅ ∈ 𝐴 → 1o ⊆ 𝐴 ) )
21 20 imp ⊢ ( ( 𝐴 ∈ ω ∧ ∅ ∈ 𝐴 ) → 1o ⊆ 𝐴 )
22 14 21 sylbi ⊢ ( 𝐴 ∈ N → 1o ⊆ 𝐴 )
23 1onn ⊢ 1o ∈ ω
24 eleq1 ⊢ ( 𝑥 = 1o → ( 𝑥 ∈ N ↔ 1o ∈ N ) )
25 breq2 ⊢ ( 𝑥 = 1o → ( 1o <N 𝑥 ↔ 1o <N 1o ) )
26 24 25 anbi12d ⊢ ( 𝑥 = 1o → ( ( 𝑥 ∈ N ∧ 1o <N 𝑥 ) ↔ ( 1o ∈ N ∧ 1o <N 1o ) ) )
27 26 1 imbi12d ⊢ ( 𝑥 = 1o → ( ( ( 𝑥 ∈ N ∧ 1o <N 𝑥 ) → 𝜑 ) ↔ ( ( 1o ∈ N ∧ 1o <N 1o ) → 𝜓 ) ) )
28 eleq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ N ↔ 𝑦 ∈ N ) )
29 breq2 ⊢ ( 𝑥 = 𝑦 → ( 1o <N 𝑥 ↔ 1o <N 𝑦 ) )
30 28 29 anbi12d ⊢ ( 𝑥 = 𝑦 → ( ( 𝑥 ∈ N ∧ 1o <N 𝑥 ) ↔ ( 𝑦 ∈ N ∧ 1o <N 𝑦 ) ) )
31 30 2 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝑥 ∈ N ∧ 1o <N 𝑥 ) → 𝜑 ) ↔ ( ( 𝑦 ∈ N ∧ 1o <N 𝑦 ) → 𝜒 ) ) )
32 pinn ⊢ ( 𝑥 ∈ N → 𝑥 ∈ ω )
33 eleq1 ⊢ ( 𝑥 = suc 𝑦 → ( 𝑥 ∈ ω ↔ suc 𝑦 ∈ ω ) )
34 peano2b ⊢ ( 𝑦 ∈ ω ↔ suc 𝑦 ∈ ω )
35 33 34 bitr4di ⊢ ( 𝑥 = suc 𝑦 → ( 𝑥 ∈ ω ↔ 𝑦 ∈ ω ) )
36 32 35 imbitrid ⊢ ( 𝑥 = suc 𝑦 → ( 𝑥 ∈ N → 𝑦 ∈ ω ) )
37 36 adantrd ⊢ ( 𝑥 = suc 𝑦 → ( ( 𝑥 ∈ N ∧ 1o <N 𝑥 ) → 𝑦 ∈ ω ) )
38 1pi ⊢ 1o ∈ N
39 ltpiord ⊢ ( ( 1o ∈ N ∧ 𝑥 ∈ N ) → ( 1o <N 𝑥 ↔ 1o ∈ 𝑥 ) )
40 38 39 mpan ⊢ ( 𝑥 ∈ N → ( 1o <N 𝑥 ↔ 1o ∈ 𝑥 ) )
41 40 biimpa ⊢ ( ( 𝑥 ∈ N ∧ 1o <N 𝑥 ) → 1o ∈ 𝑥 )
42 eleq2 ⊢ ( 𝑥 = suc 𝑦 → ( 1o ∈ 𝑥 ↔ 1o ∈ suc 𝑦 ) )
43 elsuci ⊢ ( 1o ∈ suc 𝑦 → ( 1o ∈ 𝑦 ∨ 1o = 𝑦 ) )
44 ne0i ⊢ ( 1o ∈ 𝑦 → 𝑦 ≠ ∅ )
45 0lt1o ⊢ ∅ ∈ 1o
46 eleq2 ⊢ ( 1o = 𝑦 → ( ∅ ∈ 1o ↔ ∅ ∈ 𝑦 ) )
47 45 46 mpbii ⊢ ( 1o = 𝑦 → ∅ ∈ 𝑦 )
48 47 ne0d ⊢ ( 1o = 𝑦 → 𝑦 ≠ ∅ )
49 44 48 jaoi ⊢ ( ( 1o ∈ 𝑦 ∨ 1o = 𝑦 ) → 𝑦 ≠ ∅ )
50 43 49 syl ⊢ ( 1o ∈ suc 𝑦 → 𝑦 ≠ ∅ )
51 42 50 biimtrdi ⊢ ( 𝑥 = suc 𝑦 → ( 1o ∈ 𝑥 → 𝑦 ≠ ∅ ) )
52 41 51 syl5 ⊢ ( 𝑥 = suc 𝑦 → ( ( 𝑥 ∈ N ∧ 1o <N 𝑥 ) → 𝑦 ≠ ∅ ) )
53 37 52 jcad ⊢ ( 𝑥 = suc 𝑦 → ( ( 𝑥 ∈ N ∧ 1o <N 𝑥 ) → ( 𝑦 ∈ ω ∧ 𝑦 ≠ ∅ ) ) )
54 elni ⊢ ( 𝑦 ∈ N ↔ ( 𝑦 ∈ ω ∧ 𝑦 ≠ ∅ ) )
55 53 54 imbitrrdi ⊢ ( 𝑥 = suc 𝑦 → ( ( 𝑥 ∈ N ∧ 1o <N 𝑥 ) → 𝑦 ∈ N ) )
56 simpr ⊢ ( ( 𝑥 ∈ N ∧ 1o <N 𝑥 ) → 1o <N 𝑥 )
57 breq2 ⊢ ( 𝑥 = suc 𝑦 → ( 1o <N 𝑥 ↔ 1o <N suc 𝑦 ) )
58 56 57 imbitrid ⊢ ( 𝑥 = suc 𝑦 → ( ( 𝑥 ∈ N ∧ 1o <N 𝑥 ) → 1o <N suc 𝑦 ) )
59 55 58 jcad ⊢ ( 𝑥 = suc 𝑦 → ( ( 𝑥 ∈ N ∧ 1o <N 𝑥 ) → ( 𝑦 ∈ N ∧ 1o <N suc 𝑦 ) ) )
60 addclpi ⊢ ( ( 𝑦 ∈ N ∧ 1o ∈ N ) → ( 𝑦 +N 1o ) ∈ N )
61 38 60 mpan2 ⊢ ( 𝑦 ∈ N → ( 𝑦 +N 1o ) ∈ N )
62 addpiord ⊢ ( ( 𝑦 ∈ N ∧ 1o ∈ N ) → ( 𝑦 +N 1o ) = ( 𝑦 +o 1o ) )
63 38 62 mpan2 ⊢ ( 𝑦 ∈ N → ( 𝑦 +N 1o ) = ( 𝑦 +o 1o ) )
64 pion ⊢ ( 𝑦 ∈ N → 𝑦 ∈ On )
65 oa1suc ⊢ ( 𝑦 ∈ On → ( 𝑦 +o 1o ) = suc 𝑦 )
66 64 65 syl ⊢ ( 𝑦 ∈ N → ( 𝑦 +o 1o ) = suc 𝑦 )
67 63 66 eqtrd ⊢ ( 𝑦 ∈ N → ( 𝑦 +N 1o ) = suc 𝑦 )
68 67 eqeq2d ⊢ ( 𝑦 ∈ N → ( 𝑥 = ( 𝑦 +N 1o ) ↔ 𝑥 = suc 𝑦 ) )
69 68 biimparc ⊢ ( ( 𝑥 = suc 𝑦 ∧ 𝑦 ∈ N ) → 𝑥 = ( 𝑦 +N 1o ) )
70 69 eleq1d ⊢ ( ( 𝑥 = suc 𝑦 ∧ 𝑦 ∈ N ) → ( 𝑥 ∈ N ↔ ( 𝑦 +N 1o ) ∈ N ) )
71 61 70 imbitrrid ⊢ ( ( 𝑥 = suc 𝑦 ∧ 𝑦 ∈ N ) → ( 𝑦 ∈ N → 𝑥 ∈ N ) )
72 71 ex ⊢ ( 𝑥 = suc 𝑦 → ( 𝑦 ∈ N → ( 𝑦 ∈ N → 𝑥 ∈ N ) ) )
73 72 pm2.43d ⊢ ( 𝑥 = suc 𝑦 → ( 𝑦 ∈ N → 𝑥 ∈ N ) )
74 57 biimprd ⊢ ( 𝑥 = suc 𝑦 → ( 1o <N suc 𝑦 → 1o <N 𝑥 ) )
75 73 74 anim12d ⊢ ( 𝑥 = suc 𝑦 → ( ( 𝑦 ∈ N ∧ 1o <N suc 𝑦 ) → ( 𝑥 ∈ N ∧ 1o <N 𝑥 ) ) )
76 59 75 impbid ⊢ ( 𝑥 = suc 𝑦 → ( ( 𝑥 ∈ N ∧ 1o <N 𝑥 ) ↔ ( 𝑦 ∈ N ∧ 1o <N suc 𝑦 ) ) )
77 76 imbi1d ⊢ ( 𝑥 = suc 𝑦 → ( ( ( 𝑥 ∈ N ∧ 1o <N 𝑥 ) → 𝜑 ) ↔ ( ( 𝑦 ∈ N ∧ 1o <N suc 𝑦 ) → 𝜑 ) ) )
78 68 3 biimtrrdi ⊢ ( 𝑦 ∈ N → ( 𝑥 = suc 𝑦 → ( 𝜑 ↔ 𝜃 ) ) )
79 78 adantr ⊢ ( ( 𝑦 ∈ N ∧ 1o <N suc 𝑦 ) → ( 𝑥 = suc 𝑦 → ( 𝜑 ↔ 𝜃 ) ) )
80 79 com12 ⊢ ( 𝑥 = suc 𝑦 → ( ( 𝑦 ∈ N ∧ 1o <N suc 𝑦 ) → ( 𝜑 ↔ 𝜃 ) ) )
81 80 pm5.74d ⊢ ( 𝑥 = suc 𝑦 → ( ( ( 𝑦 ∈ N ∧ 1o <N suc 𝑦 ) → 𝜑 ) ↔ ( ( 𝑦 ∈ N ∧ 1o <N suc 𝑦 ) → 𝜃 ) ) )
82 77 81 bitrd ⊢ ( 𝑥 = suc 𝑦 → ( ( ( 𝑥 ∈ N ∧ 1o <N 𝑥 ) → 𝜑 ) ↔ ( ( 𝑦 ∈ N ∧ 1o <N suc 𝑦 ) → 𝜃 ) ) )
83 eleq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ N ↔ 𝐴 ∈ N ) )
84 breq2 ⊢ ( 𝑥 = 𝐴 → ( 1o <N 𝑥 ↔ 1o <N 𝐴 ) )
85 83 84 anbi12d ⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 ∈ N ∧ 1o <N 𝑥 ) ↔ ( 𝐴 ∈ N ∧ 1o <N 𝐴 ) ) )
86 85 4 imbi12d ⊢ ( 𝑥 = 𝐴 → ( ( ( 𝑥 ∈ N ∧ 1o <N 𝑥 ) → 𝜑 ) ↔ ( ( 𝐴 ∈ N ∧ 1o <N 𝐴 ) → 𝜏 ) ) )
87 5 2a1i ⊢ ( 1o ∈ ω → ( ( 1o ∈ N ∧ 1o <N 1o ) → 𝜓 ) )
88 ltpiord ⊢ ( ( 1o ∈ N ∧ 𝑦 ∈ N ) → ( 1o <N 𝑦 ↔ 1o ∈ 𝑦 ) )
89 38 88 mpan ⊢ ( 𝑦 ∈ N → ( 1o <N 𝑦 ↔ 1o ∈ 𝑦 ) )
90 89 pm5.32i ⊢ ( ( 𝑦 ∈ N ∧ 1o <N 𝑦 ) ↔ ( 𝑦 ∈ N ∧ 1o ∈ 𝑦 ) )
91 90 simplbi2 ⊢ ( 𝑦 ∈ N → ( 1o ∈ 𝑦 → ( 𝑦 ∈ N ∧ 1o <N 𝑦 ) ) )
92 91 imim1d ⊢ ( 𝑦 ∈ N → ( ( ( 𝑦 ∈ N ∧ 1o <N 𝑦 ) → 𝜒 ) → ( 1o ∈ 𝑦 → 𝜒 ) ) )
93 ltrelpi ⊢ <N ⊆ ( N × N )
94 93 brel ⊢ ( 1o <N suc 𝑦 → ( 1o ∈ N ∧ suc 𝑦 ∈ N ) )
95 ltpiord ⊢ ( ( 1o ∈ N ∧ suc 𝑦 ∈ N ) → ( 1o <N suc 𝑦 ↔ 1o ∈ suc 𝑦 ) )
96 94 95 syl ⊢ ( 1o <N suc 𝑦 → ( 1o <N suc 𝑦 ↔ 1o ∈ suc 𝑦 ) )
97 96 ibi ⊢ ( 1o <N suc 𝑦 → 1o ∈ suc 𝑦 )
98 7 eqvinc ⊢ ( 1o = 𝑦 ↔ ∃ 𝑥 ( 𝑥 = 1o ∧ 𝑥 = 𝑦 ) )
99 98 2 9 gencl ⊢ ( 1o = 𝑦 → 𝜒 )
100 jao ⊢ ( ( 1o ∈ 𝑦 → 𝜒 ) → ( ( 1o = 𝑦 → 𝜒 ) → ( ( 1o ∈ 𝑦 ∨ 1o = 𝑦 ) → 𝜒 ) ) )
101 99 100 mpi ⊢ ( ( 1o ∈ 𝑦 → 𝜒 ) → ( ( 1o ∈ 𝑦 ∨ 1o = 𝑦 ) → 𝜒 ) )
102 43 101 syl5 ⊢ ( ( 1o ∈ 𝑦 → 𝜒 ) → ( 1o ∈ suc 𝑦 → 𝜒 ) )
103 97 102 syl5 ⊢ ( ( 1o ∈ 𝑦 → 𝜒 ) → ( 1o <N suc 𝑦 → 𝜒 ) )
104 92 103 syl6com ⊢ ( ( ( 𝑦 ∈ N ∧ 1o <N 𝑦 ) → 𝜒 ) → ( 𝑦 ∈ N → ( 1o <N suc 𝑦 → 𝜒 ) ) )
105 104 impd ⊢ ( ( ( 𝑦 ∈ N ∧ 1o <N 𝑦 ) → 𝜒 ) → ( ( 𝑦 ∈ N ∧ 1o <N suc 𝑦 ) → 𝜒 ) )
106 18 sseq1i ⊢ ( 1o ⊆ 𝑦 ↔ suc ∅ ⊆ 𝑦 )
107 0ex ⊢ ∅ ∈ V
108 sucssel ⊢ ( ∅ ∈ V → ( suc ∅ ⊆ 𝑦 → ∅ ∈ 𝑦 ) )
109 107 108 ax-mp ⊢ ( suc ∅ ⊆ 𝑦 → ∅ ∈ 𝑦 )
110 106 109 sylbi ⊢ ( 1o ⊆ 𝑦 → ∅ ∈ 𝑦 )
111 elni2 ⊢ ( 𝑦 ∈ N ↔ ( 𝑦 ∈ ω ∧ ∅ ∈ 𝑦 ) )
112 111 6 sylbir ⊢ ( ( 𝑦 ∈ ω ∧ ∅ ∈ 𝑦 ) → ( 𝜒 → 𝜃 ) )
113 110 112 sylan2 ⊢ ( ( 𝑦 ∈ ω ∧ 1o ⊆ 𝑦 ) → ( 𝜒 → 𝜃 ) )
114 105 113 syl9r ⊢ ( ( 𝑦 ∈ ω ∧ 1o ⊆ 𝑦 ) → ( ( ( 𝑦 ∈ N ∧ 1o <N 𝑦 ) → 𝜒 ) → ( ( 𝑦 ∈ N ∧ 1o <N suc 𝑦 ) → 𝜃 ) ) )
115 114 adantlr ⊢ ( ( ( 𝑦 ∈ ω ∧ 1o ∈ ω ) ∧ 1o ⊆ 𝑦 ) → ( ( ( 𝑦 ∈ N ∧ 1o <N 𝑦 ) → 𝜒 ) → ( ( 𝑦 ∈ N ∧ 1o <N suc 𝑦 ) → 𝜃 ) ) )
116 27 31 82 86 87 115 findsg ⊢ ( ( ( 𝐴 ∈ ω ∧ 1o ∈ ω ) ∧ 1o ⊆ 𝐴 ) → ( ( 𝐴 ∈ N ∧ 1o <N 𝐴 ) → 𝜏 ) )
117 23 116 mpanl2 ⊢ ( ( 𝐴 ∈ ω ∧ 1o ⊆ 𝐴 ) → ( ( 𝐴 ∈ N ∧ 1o <N 𝐴 ) → 𝜏 ) )
118 13 22 117 syl2anc ⊢ ( 𝐴 ∈ N → ( ( 𝐴 ∈ N ∧ 1o <N 𝐴 ) → 𝜏 ) )
119 118 expd ⊢ ( 𝐴 ∈ N → ( 𝐴 ∈ N → ( 1o <N 𝐴 → 𝜏 ) ) )
120 119 pm2.43i ⊢ ( 𝐴 ∈ N → ( 1o <N 𝐴 → 𝜏 ) )
121 nlt1pi ⊢ ¬ 𝐴 <N 1o
122 ltsopi ⊢ <N Or N
123 sotric ⊢ ( ( <N Or N ∧ ( 𝐴 ∈ N ∧ 1o ∈ N ) ) → ( 𝐴 <N 1o ↔ ¬ ( 𝐴 = 1o ∨ 1o <N 𝐴 ) ) )
124 122 123 mpan ⊢ ( ( 𝐴 ∈ N ∧ 1o ∈ N ) → ( 𝐴 <N 1o ↔ ¬ ( 𝐴 = 1o ∨ 1o <N 𝐴 ) ) )
125 38 124 mpan2 ⊢ ( 𝐴 ∈ N → ( 𝐴 <N 1o ↔ ¬ ( 𝐴 = 1o ∨ 1o <N 𝐴 ) ) )
126 121 125 mtbii ⊢ ( 𝐴 ∈ N → ¬ ¬ ( 𝐴 = 1o ∨ 1o <N 𝐴 ) )
127 126 notnotrd ⊢ ( 𝐴 ∈ N → ( 𝐴 = 1o ∨ 1o <N 𝐴 ) )
128 12 120 127 mpjaod ⊢ ( 𝐴 ∈ N → 𝜏 )