Theorem indpi 9729

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

Hypotheses

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

Assertion

Ref	Expression
indpi	⊢ (𝐴 ∈ N → 𝜏)

Distinct variable groups:   𝑥,𝑦   𝑥,𝐴   𝜓,𝑥   𝜒,𝑥   𝜃,𝑥   𝜏,𝑥   𝜑,𝑦

Allowed substitution hints:   𝜑(𝑥)   𝜓(𝑦)   𝜒(𝑦)   𝜃(𝑦)   𝜏(𝑦)   𝐴(𝑦)

Proof of Theorem indpi

Step	Hyp	Ref	Expression
1		1pi 9705	. . . . . . 7 ⊢ 1𝑜 ∈ N
2	1	elexi 3213	. . . . . 6 ⊢ 1𝑜 ∈ V
3	2	eqvinc 3330	. . . . 5 ⊢ (1𝑜 = 𝐴 ↔ ∃𝑥(𝑥 = 1𝑜 ∧ 𝑥 = 𝐴))
4		indpi.4	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))
5		indpi.5	. . . . . 6 ⊢ 𝜓
6		indpi.1	. . . . . 6 ⊢ (𝑥 = 1𝑜 → (𝜑 ↔ 𝜓))
7	5, 6	mpbiri 248	. . . . 5 ⊢ (𝑥 = 1𝑜 → 𝜑)
8	3, 4, 7	gencl 3235	. . . 4 ⊢ (1𝑜 = 𝐴 → 𝜏)
9	8	eqcoms 2630	. . 3 ⊢ (𝐴 = 1𝑜 → 𝜏)
10	9	a1i 11	. 2 ⊢ (𝐴 ∈ N → (𝐴 = 1𝑜 → 𝜏))
11		pinn 9700	. . . . 5 ⊢ (𝐴 ∈ N → 𝐴 ∈ ω)
12		elni2 9699	. . . . . 6 ⊢ (𝐴 ∈ N ↔ (𝐴 ∈ ω ∧ ∅ ∈ 𝐴))
13		nnord 7073	. . . . . . . . 9 ⊢ (𝐴 ∈ ω → Ord 𝐴)
14		ordsucss 7018	. . . . . . . . 9 ⊢ (Ord 𝐴 → (∅ ∈ 𝐴 → suc ∅ ⊆ 𝐴))
15	13, 14	syl 17	. . . . . . . 8 ⊢ (𝐴 ∈ ω → (∅ ∈ 𝐴 → suc ∅ ⊆ 𝐴))
16		df-1o 7560	. . . . . . . . 9 ⊢ 1𝑜 = suc ∅
17	16	sseq1i 3629	. . . . . . . 8 ⊢ (1𝑜 ⊆ 𝐴 ↔ suc ∅ ⊆ 𝐴)
18	15, 17	syl6ibr 242	. . . . . . 7 ⊢ (𝐴 ∈ ω → (∅ ∈ 𝐴 → 1𝑜 ⊆ 𝐴))
19	18	imp 445	. . . . . 6 ⊢ ((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) → 1𝑜 ⊆ 𝐴)
20	12, 19	sylbi 207	. . . . 5 ⊢ (𝐴 ∈ N → 1𝑜 ⊆ 𝐴)
21		1onn 7719	. . . . . 6 ⊢ 1𝑜 ∈ ω
22		eleq1 2689	. . . . . . . . 9 ⊢ (𝑥 = 1𝑜 → (𝑥 ∈ N ↔ 1𝑜 ∈ N))
23		breq2 4657	. . . . . . . . 9 ⊢ (𝑥 = 1𝑜 → (1𝑜 <N 𝑥 ↔ 1𝑜 <N 1𝑜))
24	22, 23	anbi12d 747	. . . . . . . 8 ⊢ (𝑥 = 1𝑜 → ((𝑥 ∈ N ∧ 1𝑜 <N 𝑥) ↔ (1𝑜 ∈ N ∧ 1𝑜 <N 1𝑜)))
25	24, 6	imbi12d 334	. . . . . . 7 ⊢ (𝑥 = 1𝑜 → (((𝑥 ∈ N ∧ 1𝑜 <N 𝑥) → 𝜑) ↔ ((1𝑜 ∈ N ∧ 1𝑜 <N 1𝑜) → 𝜓)))
26		eleq1 2689	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ N ↔ 𝑦 ∈ N))
27		breq2 4657	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (1𝑜 <N 𝑥 ↔ 1𝑜 <N 𝑦))
28	26, 27	anbi12d 747	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ N ∧ 1𝑜 <N 𝑥) ↔ (𝑦 ∈ N ∧ 1𝑜 <N 𝑦)))
29		indpi.2	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))
30	28, 29	imbi12d 334	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (((𝑥 ∈ N ∧ 1𝑜 <N 𝑥) → 𝜑) ↔ ((𝑦 ∈ N ∧ 1𝑜 <N 𝑦) → 𝜒)))
31		pinn 9700	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ N → 𝑥 ∈ ω)
32		eleq1 2689	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = suc 𝑦 → (𝑥 ∈ ω ↔ suc 𝑦 ∈ ω))
33		peano2b 7081	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ω ↔ suc 𝑦 ∈ ω)
34	32, 33	syl6bbr 278	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = suc 𝑦 → (𝑥 ∈ ω ↔ 𝑦 ∈ ω))
35	31, 34	syl5ib 234	. . . . . . . . . . . . . 14 ⊢ (𝑥 = suc 𝑦 → (𝑥 ∈ N → 𝑦 ∈ ω))
36	35	adantrd 484	. . . . . . . . . . . . 13 ⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ N ∧ 1𝑜 <N 𝑥) → 𝑦 ∈ ω))
37		ltpiord 9709	. . . . . . . . . . . . . . . 16 ⊢ ((1𝑜 ∈ N ∧ 𝑥 ∈ N) → (1𝑜 <N 𝑥 ↔ 1𝑜 ∈ 𝑥))
38	1, 37	mpan 706	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ N → (1𝑜 <N 𝑥 ↔ 1𝑜 ∈ 𝑥))
39	38	biimpa 501	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ N ∧ 1𝑜 <N 𝑥) → 1𝑜 ∈ 𝑥)
40		eleq2 2690	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = suc 𝑦 → (1𝑜 ∈ 𝑥 ↔ 1𝑜 ∈ suc 𝑦))
41		elsuci 5791	. . . . . . . . . . . . . . . 16 ⊢ (1𝑜 ∈ suc 𝑦 → (1𝑜 ∈ 𝑦 ∨ 1𝑜 = 𝑦))
42		ne0i 3921	. . . . . . . . . . . . . . . . 17 ⊢ (1𝑜 ∈ 𝑦 → 𝑦 ≠ ∅)
43		0lt1o 7584	. . . . . . . . . . . . . . . . . . 19 ⊢ ∅ ∈ 1𝑜
44		eleq2 2690	. . . . . . . . . . . . . . . . . . 19 ⊢ (1𝑜 = 𝑦 → (∅ ∈ 1𝑜 ↔ ∅ ∈ 𝑦))
45	43, 44	mpbii 223	. . . . . . . . . . . . . . . . . 18 ⊢ (1𝑜 = 𝑦 → ∅ ∈ 𝑦)
46		ne0i 3921	. . . . . . . . . . . . . . . . . 18 ⊢ (∅ ∈ 𝑦 → 𝑦 ≠ ∅)
47	45, 46	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (1𝑜 = 𝑦 → 𝑦 ≠ ∅)
48	42, 47	jaoi 394	. . . . . . . . . . . . . . . 16 ⊢ ((1𝑜 ∈ 𝑦 ∨ 1𝑜 = 𝑦) → 𝑦 ≠ ∅)
49	41, 48	syl 17	. . . . . . . . . . . . . . 15 ⊢ (1𝑜 ∈ suc 𝑦 → 𝑦 ≠ ∅)
50	40, 49	syl6bi 243	. . . . . . . . . . . . . 14 ⊢ (𝑥 = suc 𝑦 → (1𝑜 ∈ 𝑥 → 𝑦 ≠ ∅))
51	39, 50	syl5 34	. . . . . . . . . . . . 13 ⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ N ∧ 1𝑜 <N 𝑥) → 𝑦 ≠ ∅))
52	36, 51	jcad 555	. . . . . . . . . . . 12 ⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ N ∧ 1𝑜 <N 𝑥) → (𝑦 ∈ ω ∧ 𝑦 ≠ ∅)))
53		elni 9698	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ N ↔ (𝑦 ∈ ω ∧ 𝑦 ≠ ∅))
54	52, 53	syl6ibr 242	. . . . . . . . . . 11 ⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ N ∧ 1𝑜 <N 𝑥) → 𝑦 ∈ N))
55		simpr 477	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ N ∧ 1𝑜 <N 𝑥) → 1𝑜 <N 𝑥)
56		breq2 4657	. . . . . . . . . . . 12 ⊢ (𝑥 = suc 𝑦 → (1𝑜 <N 𝑥 ↔ 1𝑜 <N suc 𝑦))
57	55, 56	syl5ib 234	. . . . . . . . . . 11 ⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ N ∧ 1𝑜 <N 𝑥) → 1𝑜 <N suc 𝑦))
58	54, 57	jcad 555	. . . . . . . . . 10 ⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ N ∧ 1𝑜 <N 𝑥) → (𝑦 ∈ N ∧ 1𝑜 <N suc 𝑦)))
59		addclpi 9714	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ N ∧ 1𝑜 ∈ N) → (𝑦 +N 1𝑜) ∈ N)
60	1, 59	mpan2 707	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ N → (𝑦 +N 1𝑜) ∈ N)
61		addpiord 9706	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ N ∧ 1𝑜 ∈ N) → (𝑦 +N 1𝑜) = (𝑦 +𝑜 1𝑜))
62	1, 61	mpan2 707	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ N → (𝑦 +N 1𝑜) = (𝑦 +𝑜 1𝑜))
63		pion 9701	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ N → 𝑦 ∈ On)
64		oa1suc 7611	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ On → (𝑦 +𝑜 1𝑜) = suc 𝑦)
65	63, 64	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ N → (𝑦 +𝑜 1𝑜) = suc 𝑦)
66	62, 65	eqtrd 2656	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ N → (𝑦 +N 1𝑜) = suc 𝑦)
67	66	eqeq2d 2632	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ N → (𝑥 = (𝑦 +N 1𝑜) ↔ 𝑥 = suc 𝑦))
68	67	biimparc 504	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = suc 𝑦 ∧ 𝑦 ∈ N) → 𝑥 = (𝑦 +N 1𝑜))
69	68	eleq1d 2686	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = suc 𝑦 ∧ 𝑦 ∈ N) → (𝑥 ∈ N ↔ (𝑦 +N 1𝑜) ∈ N))
70	60, 69	syl5ibr 236	. . . . . . . . . . . . 13 ⊢ ((𝑥 = suc 𝑦 ∧ 𝑦 ∈ N) → (𝑦 ∈ N → 𝑥 ∈ N))
71	70	ex 450	. . . . . . . . . . . 12 ⊢ (𝑥 = suc 𝑦 → (𝑦 ∈ N → (𝑦 ∈ N → 𝑥 ∈ N)))
72	71	pm2.43d 53	. . . . . . . . . . 11 ⊢ (𝑥 = suc 𝑦 → (𝑦 ∈ N → 𝑥 ∈ N))
73	56	biimprd 238	. . . . . . . . . . 11 ⊢ (𝑥 = suc 𝑦 → (1𝑜 <N suc 𝑦 → 1𝑜 <N 𝑥))
74	72, 73	anim12d 586	. . . . . . . . . 10 ⊢ (𝑥 = suc 𝑦 → ((𝑦 ∈ N ∧ 1𝑜 <N suc 𝑦) → (𝑥 ∈ N ∧ 1𝑜 <N 𝑥)))
75	58, 74	impbid 202	. . . . . . . . 9 ⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ N ∧ 1𝑜 <N 𝑥) ↔ (𝑦 ∈ N ∧ 1𝑜 <N suc 𝑦)))
76	75	imbi1d 331	. . . . . . . 8 ⊢ (𝑥 = suc 𝑦 → (((𝑥 ∈ N ∧ 1𝑜 <N 𝑥) → 𝜑) ↔ ((𝑦 ∈ N ∧ 1𝑜 <N suc 𝑦) → 𝜑)))
77		indpi.3	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑦 +N 1𝑜) → (𝜑 ↔ 𝜃))
78	67, 77	syl6bir 244	. . . . . . . . . . 11 ⊢ (𝑦 ∈ N → (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃)))
79	78	adantr 481	. . . . . . . . . 10 ⊢ ((𝑦 ∈ N ∧ 1𝑜 <N suc 𝑦) → (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃)))
80	79	com12 32	. . . . . . . . 9 ⊢ (𝑥 = suc 𝑦 → ((𝑦 ∈ N ∧ 1𝑜 <N suc 𝑦) → (𝜑 ↔ 𝜃)))
81	80	pm5.74d 262	. . . . . . . 8 ⊢ (𝑥 = suc 𝑦 → (((𝑦 ∈ N ∧ 1𝑜 <N suc 𝑦) → 𝜑) ↔ ((𝑦 ∈ N ∧ 1𝑜 <N suc 𝑦) → 𝜃)))
82	76, 81	bitrd 268	. . . . . . 7 ⊢ (𝑥 = suc 𝑦 → (((𝑥 ∈ N ∧ 1𝑜 <N 𝑥) → 𝜑) ↔ ((𝑦 ∈ N ∧ 1𝑜 <N suc 𝑦) → 𝜃)))
83		eleq1 2689	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ N ↔ 𝐴 ∈ N))
84		breq2 4657	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → (1𝑜 <N 𝑥 ↔ 1𝑜 <N 𝐴))
85	83, 84	anbi12d 747	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ N ∧ 1𝑜 <N 𝑥) ↔ (𝐴 ∈ N ∧ 1𝑜 <N 𝐴)))
86	85, 4	imbi12d 334	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (((𝑥 ∈ N ∧ 1𝑜 <N 𝑥) → 𝜑) ↔ ((𝐴 ∈ N ∧ 1𝑜 <N 𝐴) → 𝜏)))
87	5	2a1i 12	. . . . . . 7 ⊢ (1𝑜 ∈ ω → ((1𝑜 ∈ N ∧ 1𝑜 <N 1𝑜) → 𝜓))
88		ltpiord 9709	. . . . . . . . . . . . . . 15 ⊢ ((1𝑜 ∈ N ∧ 𝑦 ∈ N) → (1𝑜 <N 𝑦 ↔ 1𝑜 ∈ 𝑦))
89	1, 88	mpan 706	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ N → (1𝑜 <N 𝑦 ↔ 1𝑜 ∈ 𝑦))
90	89	pm5.32i 669	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ N ∧ 1𝑜 <N 𝑦) ↔ (𝑦 ∈ N ∧ 1𝑜 ∈ 𝑦))
91	90	simplbi2 655	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ N → (1𝑜 ∈ 𝑦 → (𝑦 ∈ N ∧ 1𝑜 <N 𝑦)))
92	91	imim1d 82	. . . . . . . . . . 11 ⊢ (𝑦 ∈ N → (((𝑦 ∈ N ∧ 1𝑜 <N 𝑦) → 𝜒) → (1𝑜 ∈ 𝑦 → 𝜒)))
93		ltrelpi 9711	. . . . . . . . . . . . . . 15 ⊢ <N ⊆ (N × N)
94	93	brel 5168	. . . . . . . . . . . . . 14 ⊢ (1𝑜 <N suc 𝑦 → (1𝑜 ∈ N ∧ suc 𝑦 ∈ N))
95		ltpiord 9709	. . . . . . . . . . . . . 14 ⊢ ((1𝑜 ∈ N ∧ suc 𝑦 ∈ N) → (1𝑜 <N suc 𝑦 ↔ 1𝑜 ∈ suc 𝑦))
96	94, 95	syl 17	. . . . . . . . . . . . 13 ⊢ (1𝑜 <N suc 𝑦 → (1𝑜 <N suc 𝑦 ↔ 1𝑜 ∈ suc 𝑦))
97	96	ibi 256	. . . . . . . . . . . 12 ⊢ (1𝑜 <N suc 𝑦 → 1𝑜 ∈ suc 𝑦)
98	2	eqvinc 3330	. . . . . . . . . . . . . . 15 ⊢ (1𝑜 = 𝑦 ↔ ∃𝑥(𝑥 = 1𝑜 ∧ 𝑥 = 𝑦))
99	98, 29, 7	gencl 3235	. . . . . . . . . . . . . 14 ⊢ (1𝑜 = 𝑦 → 𝜒)
100		jao 534	. . . . . . . . . . . . . 14 ⊢ ((1𝑜 ∈ 𝑦 → 𝜒) → ((1𝑜 = 𝑦 → 𝜒) → ((1𝑜 ∈ 𝑦 ∨ 1𝑜 = 𝑦) → 𝜒)))
101	99, 100	mpi 20	. . . . . . . . . . . . 13 ⊢ ((1𝑜 ∈ 𝑦 → 𝜒) → ((1𝑜 ∈ 𝑦 ∨ 1𝑜 = 𝑦) → 𝜒))
102	41, 101	syl5 34	. . . . . . . . . . . 12 ⊢ ((1𝑜 ∈ 𝑦 → 𝜒) → (1𝑜 ∈ suc 𝑦 → 𝜒))
103	97, 102	syl5 34	. . . . . . . . . . 11 ⊢ ((1𝑜 ∈ 𝑦 → 𝜒) → (1𝑜 <N suc 𝑦 → 𝜒))
104	92, 103	syl6com 37	. . . . . . . . . 10 ⊢ (((𝑦 ∈ N ∧ 1𝑜 <N 𝑦) → 𝜒) → (𝑦 ∈ N → (1𝑜 <N suc 𝑦 → 𝜒)))
105	104	impd 447	. . . . . . . . 9 ⊢ (((𝑦 ∈ N ∧ 1𝑜 <N 𝑦) → 𝜒) → ((𝑦 ∈ N ∧ 1𝑜 <N suc 𝑦) → 𝜒))
106	16	sseq1i 3629	. . . . . . . . . . 11 ⊢ (1𝑜 ⊆ 𝑦 ↔ suc ∅ ⊆ 𝑦)
107		0ex 4790	. . . . . . . . . . . 12 ⊢ ∅ ∈ V
108		sucssel 5819	. . . . . . . . . . . 12 ⊢ (∅ ∈ V → (suc ∅ ⊆ 𝑦 → ∅ ∈ 𝑦))
109	107, 108	ax-mp 5	. . . . . . . . . . 11 ⊢ (suc ∅ ⊆ 𝑦 → ∅ ∈ 𝑦)
110	106, 109	sylbi 207	. . . . . . . . . 10 ⊢ (1𝑜 ⊆ 𝑦 → ∅ ∈ 𝑦)
111		elni2 9699	. . . . . . . . . . 11 ⊢ (𝑦 ∈ N ↔ (𝑦 ∈ ω ∧ ∅ ∈ 𝑦))
112		indpi.6	. . . . . . . . . . 11 ⊢ (𝑦 ∈ N → (𝜒 → 𝜃))
113	111, 112	sylbir 225	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ω ∧ ∅ ∈ 𝑦) → (𝜒 → 𝜃))
114	110, 113	sylan2 491	. . . . . . . . 9 ⊢ ((𝑦 ∈ ω ∧ 1𝑜 ⊆ 𝑦) → (𝜒 → 𝜃))
115	105, 114	syl9r 78	. . . . . . . 8 ⊢ ((𝑦 ∈ ω ∧ 1𝑜 ⊆ 𝑦) → (((𝑦 ∈ N ∧ 1𝑜 <N 𝑦) → 𝜒) → ((𝑦 ∈ N ∧ 1𝑜 <N suc 𝑦) → 𝜃)))
116	115	adantlr 751	. . . . . . 7 ⊢ (((𝑦 ∈ ω ∧ 1𝑜 ∈ ω) ∧ 1𝑜 ⊆ 𝑦) → (((𝑦 ∈ N ∧ 1𝑜 <N 𝑦) → 𝜒) → ((𝑦 ∈ N ∧ 1𝑜 <N suc 𝑦) → 𝜃)))
117	25, 30, 82, 86, 87, 116	findsg 7093	. . . . . 6 ⊢ (((𝐴 ∈ ω ∧ 1𝑜 ∈ ω) ∧ 1𝑜 ⊆ 𝐴) → ((𝐴 ∈ N ∧ 1𝑜 <N 𝐴) → 𝜏))
118	21, 117	mpanl2 717	. . . . 5 ⊢ ((𝐴 ∈ ω ∧ 1𝑜 ⊆ 𝐴) → ((𝐴 ∈ N ∧ 1𝑜 <N 𝐴) → 𝜏))
119	11, 20, 118	syl2anc 693	. . . 4 ⊢ (𝐴 ∈ N → ((𝐴 ∈ N ∧ 1𝑜 <N 𝐴) → 𝜏))
120	119	expd 452	. . 3 ⊢ (𝐴 ∈ N → (𝐴 ∈ N → (1𝑜 <N 𝐴 → 𝜏)))
121	120	pm2.43i 52	. 2 ⊢ (𝐴 ∈ N → (1𝑜 <N 𝐴 → 𝜏))
122		nlt1pi 9728	. . . 4 ⊢ ¬ 𝐴 <N 1𝑜
123		ltsopi 9710	. . . . . 6 ⊢ <N Or N
124		sotric 5061	. . . . . 6 ⊢ (( <N Or N ∧ (𝐴 ∈ N ∧ 1𝑜 ∈ N)) → (𝐴 <N 1𝑜 ↔ ¬ (𝐴 = 1𝑜 ∨ 1𝑜 <N 𝐴)))
125	123, 124	mpan 706	. . . . 5 ⊢ ((𝐴 ∈ N ∧ 1𝑜 ∈ N) → (𝐴 <N 1𝑜 ↔ ¬ (𝐴 = 1𝑜 ∨ 1𝑜 <N 𝐴)))
126	1, 125	mpan2 707	. . . 4 ⊢ (𝐴 ∈ N → (𝐴 <N 1𝑜 ↔ ¬ (𝐴 = 1𝑜 ∨ 1𝑜 <N 𝐴)))
127	122, 126	mtbii 316	. . 3 ⊢ (𝐴 ∈ N → ¬ ¬ (𝐴 = 1𝑜 ∨ 1𝑜 <N 𝐴))
128	127	notnotrd 128	. 2 ⊢ (𝐴 ∈ N → (𝐴 = 1𝑜 ∨ 1𝑜 <N 𝐴))
129	10, 121, 128	mpjaod 396	1 ⊢ (𝐴 ∈ N → 𝜏)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∨ wo 383   ∧ wa 384   = wceq 1483   ∈ wcel 1990   ≠ wne 2794  Vcvv 3200   ⊆ wss 3574  ∅c0 3915   class class class wbr 4653   Or wor 5034  Ord word 5722  Oncon0 5723  suc csuc 5725  (class class class)co 6650  ωcom 7065  1_𝑜c1o 7553   +_𝑜 coa 7557  Ncnpi 9666   +_N cpli 9667   <_N clti 9669

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-reu 2919  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-iun 4522  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-om 7066  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-ni 9694  df-pli 9695  df-lti 9697

This theorem is referenced by:  prlem934  9855