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 → 𝜏 )