Theorem indpi 9608

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 9584	. . . . . . 7 ⊢ 1𝑜 ∈ N
2	1	elexi 3186	. . . . . 6 ⊢ 1𝑜 ∈ V
3	2	eqvinc 3300	. . . . 5 ⊢ (1𝑜 = 𝐴 ↔ ∃𝑥(𝑥 = 1𝑜 ∧ 𝑥 = 𝐴))
4		indpi.4	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))
5		indpi.5	. . . . . 6 ⊢ 𝜓
6		indpi.1	. . . . . 6 ⊢ (𝑥 = 1𝑜 → (𝜑 ↔ 𝜓))
7	5, 6	mpbiri 247	. . . . 5 ⊢ (𝑥 = 1𝑜 → 𝜑)
8	3, 4, 7	gencl 3208	. . . 4 ⊢ (1𝑜 = 𝐴 → 𝜏)
9	8	eqcoms 2618	. . 3 ⊢ (𝐴 = 1𝑜 → 𝜏)
10	9	a1i 11	. 2 ⊢ (𝐴 ∈ N → (𝐴 = 1𝑜 → 𝜏))
11		pinn 9579	. . . . 5 ⊢ (𝐴 ∈ N → 𝐴 ∈ ω)
12		elni2 9578	. . . . . 6 ⊢ (𝐴 ∈ N ↔ (𝐴 ∈ ω ∧ ∅ ∈ 𝐴))
13		nnord 6965	. . . . . . . . 9 ⊢ (𝐴 ∈ ω → Ord 𝐴)
14		ordsucss 6910	. . . . . . . . 9 ⊢ (Ord 𝐴 → (∅ ∈ 𝐴 → suc ∅ ⊆ 𝐴))
15	13, 14	syl 17	. . . . . . . 8 ⊢ (𝐴 ∈ ω → (∅ ∈ 𝐴 → suc ∅ ⊆ 𝐴))
16		df-1o 7447	. . . . . . . . 9 ⊢ 1𝑜 = suc ∅
17	16	sseq1i 3592	. . . . . . . 8 ⊢ (1𝑜 ⊆ 𝐴 ↔ suc ∅ ⊆ 𝐴)
18	15, 17	syl6ibr 241	. . . . . . 7 ⊢ (𝐴 ∈ ω → (∅ ∈ 𝐴 → 1𝑜 ⊆ 𝐴))
19	18	imp 444	. . . . . 6 ⊢ ((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) → 1𝑜 ⊆ 𝐴)
20	12, 19	sylbi 206	. . . . 5 ⊢ (𝐴 ∈ N → 1𝑜 ⊆ 𝐴)
21		1onn 7606	. . . . . 6 ⊢ 1𝑜 ∈ ω
22		eleq1 2676	. . . . . . . . 9 ⊢ (𝑥 = 1𝑜 → (𝑥 ∈ N ↔ 1𝑜 ∈ N))
23		breq2 4587	. . . . . . . . 9 ⊢ (𝑥 = 1𝑜 → (1𝑜 <N 𝑥 ↔ 1𝑜 <N 1𝑜))
24	22, 23	anbi12d 743	. . . . . . . 8 ⊢ (𝑥 = 1𝑜 → ((𝑥 ∈ N ∧ 1𝑜 <N 𝑥) ↔ (1𝑜 ∈ N ∧ 1𝑜 <N 1𝑜)))
25	24, 6	imbi12d 333	. . . . . . 7 ⊢ (𝑥 = 1𝑜 → (((𝑥 ∈ N ∧ 1𝑜 <N 𝑥) → 𝜑) ↔ ((1𝑜 ∈ N ∧ 1𝑜 <N 1𝑜) → 𝜓)))
26		eleq1 2676	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ N ↔ 𝑦 ∈ N))
27		breq2 4587	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (1𝑜 <N 𝑥 ↔ 1𝑜 <N 𝑦))
28	26, 27	anbi12d 743	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ N ∧ 1𝑜 <N 𝑥) ↔ (𝑦 ∈ N ∧ 1𝑜 <N 𝑦)))
29		indpi.2	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))
30	28, 29	imbi12d 333	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (((𝑥 ∈ N ∧ 1𝑜 <N 𝑥) → 𝜑) ↔ ((𝑦 ∈ N ∧ 1𝑜 <N 𝑦) → 𝜒)))
31		pinn 9579	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ N → 𝑥 ∈ ω)
32		eleq1 2676	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = suc 𝑦 → (𝑥 ∈ ω ↔ suc 𝑦 ∈ ω))
33		peano2b 6973	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ω ↔ suc 𝑦 ∈ ω)
34	32, 33	syl6bbr 277	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = suc 𝑦 → (𝑥 ∈ ω ↔ 𝑦 ∈ ω))
35	31, 34	syl5ib 233	. . . . . . . . . . . . . 14 ⊢ (𝑥 = suc 𝑦 → (𝑥 ∈ N → 𝑦 ∈ ω))
36	35	adantrd 483	. . . . . . . . . . . . 13 ⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ N ∧ 1𝑜 <N 𝑥) → 𝑦 ∈ ω))
37		ltpiord 9588	. . . . . . . . . . . . . . . 16 ⊢ ((1𝑜 ∈ N ∧ 𝑥 ∈ N) → (1𝑜 <N 𝑥 ↔ 1𝑜 ∈ 𝑥))
38	1, 37	mpan 702	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ N → (1𝑜 <N 𝑥 ↔ 1𝑜 ∈ 𝑥))
39	38	biimpa 500	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ N ∧ 1𝑜 <N 𝑥) → 1𝑜 ∈ 𝑥)
40		eleq2 2677	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = suc 𝑦 → (1𝑜 ∈ 𝑥 ↔ 1𝑜 ∈ suc 𝑦))
41		elsuci 5708	. . . . . . . . . . . . . . . 16 ⊢ (1𝑜 ∈ suc 𝑦 → (1𝑜 ∈ 𝑦 ∨ 1𝑜 = 𝑦))
42		ne0i 3880	. . . . . . . . . . . . . . . . 17 ⊢ (1𝑜 ∈ 𝑦 → 𝑦 ≠ ∅)
43		0lt1o 7471	. . . . . . . . . . . . . . . . . . 19 ⊢ ∅ ∈ 1𝑜
44		eleq2 2677	. . . . . . . . . . . . . . . . . . 19 ⊢ (1𝑜 = 𝑦 → (∅ ∈ 1𝑜 ↔ ∅ ∈ 𝑦))
45	43, 44	mpbii 222	. . . . . . . . . . . . . . . . . 18 ⊢ (1𝑜 = 𝑦 → ∅ ∈ 𝑦)
46		ne0i 3880	. . . . . . . . . . . . . . . . . 18 ⊢ (∅ ∈ 𝑦 → 𝑦 ≠ ∅)
47	45, 46	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (1𝑜 = 𝑦 → 𝑦 ≠ ∅)
48	42, 47	jaoi 393	. . . . . . . . . . . . . . . 16 ⊢ ((1𝑜 ∈ 𝑦 ∨ 1𝑜 = 𝑦) → 𝑦 ≠ ∅)
49	41, 48	syl 17	. . . . . . . . . . . . . . 15 ⊢ (1𝑜 ∈ suc 𝑦 → 𝑦 ≠ ∅)
50	40, 49	syl6bi 242	. . . . . . . . . . . . . 14 ⊢ (𝑥 = suc 𝑦 → (1𝑜 ∈ 𝑥 → 𝑦 ≠ ∅))
51	39, 50	syl5 33	. . . . . . . . . . . . 13 ⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ N ∧ 1𝑜 <N 𝑥) → 𝑦 ≠ ∅))
52	36, 51	jcad 554	. . . . . . . . . . . 12 ⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ N ∧ 1𝑜 <N 𝑥) → (𝑦 ∈ ω ∧ 𝑦 ≠ ∅)))
53		elni 9577	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ N ↔ (𝑦 ∈ ω ∧ 𝑦 ≠ ∅))
54	52, 53	syl6ibr 241	. . . . . . . . . . 11 ⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ N ∧ 1𝑜 <N 𝑥) → 𝑦 ∈ N))
55		simpr 476	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ N ∧ 1𝑜 <N 𝑥) → 1𝑜 <N 𝑥)
56		breq2 4587	. . . . . . . . . . . 12 ⊢ (𝑥 = suc 𝑦 → (1𝑜 <N 𝑥 ↔ 1𝑜 <N suc 𝑦))
57	55, 56	syl5ib 233	. . . . . . . . . . 11 ⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ N ∧ 1𝑜 <N 𝑥) → 1𝑜 <N suc 𝑦))
58	54, 57	jcad 554	. . . . . . . . . 10 ⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ N ∧ 1𝑜 <N 𝑥) → (𝑦 ∈ N ∧ 1𝑜 <N suc 𝑦)))
59		addclpi 9593	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ N ∧ 1𝑜 ∈ N) → (𝑦 +N 1𝑜) ∈ N)
60	1, 59	mpan2 703	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ N → (𝑦 +N 1𝑜) ∈ N)
61		addpiord 9585	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ N ∧ 1𝑜 ∈ N) → (𝑦 +N 1𝑜) = (𝑦 +𝑜 1𝑜))
62	1, 61	mpan2 703	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ N → (𝑦 +N 1𝑜) = (𝑦 +𝑜 1𝑜))
63		pion 9580	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ N → 𝑦 ∈ On)
64		oa1suc 7498	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ On → (𝑦 +𝑜 1𝑜) = suc 𝑦)
65	63, 64	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ N → (𝑦 +𝑜 1𝑜) = suc 𝑦)
66	62, 65	eqtrd 2644	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ N → (𝑦 +N 1𝑜) = suc 𝑦)
67	66	eqeq2d 2620	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ N → (𝑥 = (𝑦 +N 1𝑜) ↔ 𝑥 = suc 𝑦))
68	67	biimparc 503	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = suc 𝑦 ∧ 𝑦 ∈ N) → 𝑥 = (𝑦 +N 1𝑜))
69	68	eleq1d 2672	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = suc 𝑦 ∧ 𝑦 ∈ N) → (𝑥 ∈ N ↔ (𝑦 +N 1𝑜) ∈ N))
70	60, 69	syl5ibr 235	. . . . . . . . . . . . 13 ⊢ ((𝑥 = suc 𝑦 ∧ 𝑦 ∈ N) → (𝑦 ∈ N → 𝑥 ∈ N))
71	70	ex 449	. . . . . . . . . . . 12 ⊢ (𝑥 = suc 𝑦 → (𝑦 ∈ N → (𝑦 ∈ N → 𝑥 ∈ N)))
72	71	pm2.43d 51	. . . . . . . . . . 11 ⊢ (𝑥 = suc 𝑦 → (𝑦 ∈ N → 𝑥 ∈ N))
73	56	biimprd 237	. . . . . . . . . . 11 ⊢ (𝑥 = suc 𝑦 → (1𝑜 <N suc 𝑦 → 1𝑜 <N 𝑥))
74	72, 73	anim12d 584	. . . . . . . . . 10 ⊢ (𝑥 = suc 𝑦 → ((𝑦 ∈ N ∧ 1𝑜 <N suc 𝑦) → (𝑥 ∈ N ∧ 1𝑜 <N 𝑥)))
75	58, 74	impbid 201	. . . . . . . . 9 ⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ N ∧ 1𝑜 <N 𝑥) ↔ (𝑦 ∈ N ∧ 1𝑜 <N suc 𝑦)))
76	75	imbi1d 330	. . . . . . . 8 ⊢ (𝑥 = suc 𝑦 → (((𝑥 ∈ N ∧ 1𝑜 <N 𝑥) → 𝜑) ↔ ((𝑦 ∈ N ∧ 1𝑜 <N suc 𝑦) → 𝜑)))
77		indpi.3	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑦 +N 1𝑜) → (𝜑 ↔ 𝜃))
78	67, 77	syl6bir 243	. . . . . . . . . . 11 ⊢ (𝑦 ∈ N → (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃)))
79	78	adantr 480	. . . . . . . . . 10 ⊢ ((𝑦 ∈ N ∧ 1𝑜 <N suc 𝑦) → (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃)))
80	79	com12 32	. . . . . . . . 9 ⊢ (𝑥 = suc 𝑦 → ((𝑦 ∈ N ∧ 1𝑜 <N suc 𝑦) → (𝜑 ↔ 𝜃)))
81	80	pm5.74d 261	. . . . . . . 8 ⊢ (𝑥 = suc 𝑦 → (((𝑦 ∈ N ∧ 1𝑜 <N suc 𝑦) → 𝜑) ↔ ((𝑦 ∈ N ∧ 1𝑜 <N suc 𝑦) → 𝜃)))
82	76, 81	bitrd 267	. . . . . . 7 ⊢ (𝑥 = suc 𝑦 → (((𝑥 ∈ N ∧ 1𝑜 <N 𝑥) → 𝜑) ↔ ((𝑦 ∈ N ∧ 1𝑜 <N suc 𝑦) → 𝜃)))
83		eleq1 2676	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ N ↔ 𝐴 ∈ N))
84		breq2 4587	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → (1𝑜 <N 𝑥 ↔ 1𝑜 <N 𝐴))
85	83, 84	anbi12d 743	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ N ∧ 1𝑜 <N 𝑥) ↔ (𝐴 ∈ N ∧ 1𝑜 <N 𝐴)))
86	85, 4	imbi12d 333	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (((𝑥 ∈ N ∧ 1𝑜 <N 𝑥) → 𝜑) ↔ ((𝐴 ∈ N ∧ 1𝑜 <N 𝐴) → 𝜏)))
87	5	2a1i 12	. . . . . . 7 ⊢ (1𝑜 ∈ ω → ((1𝑜 ∈ N ∧ 1𝑜 <N 1𝑜) → 𝜓))
88		ltpiord 9588	. . . . . . . . . . . . . . 15 ⊢ ((1𝑜 ∈ N ∧ 𝑦 ∈ N) → (1𝑜 <N 𝑦 ↔ 1𝑜 ∈ 𝑦))
89	1, 88	mpan 702	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ N → (1𝑜 <N 𝑦 ↔ 1𝑜 ∈ 𝑦))
90	89	pm5.32i 667	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ N ∧ 1𝑜 <N 𝑦) ↔ (𝑦 ∈ N ∧ 1𝑜 ∈ 𝑦))
91	90	simplbi2 653	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ N → (1𝑜 ∈ 𝑦 → (𝑦 ∈ N ∧ 1𝑜 <N 𝑦)))
92	91	imim1d 80	. . . . . . . . . . 11 ⊢ (𝑦 ∈ N → (((𝑦 ∈ N ∧ 1𝑜 <N 𝑦) → 𝜒) → (1𝑜 ∈ 𝑦 → 𝜒)))
93		ltrelpi 9590	. . . . . . . . . . . . . . 15 ⊢ <N ⊆ (N × N)
94	93	brel 5090	. . . . . . . . . . . . . 14 ⊢ (1𝑜 <N suc 𝑦 → (1𝑜 ∈ N ∧ suc 𝑦 ∈ N))
95		ltpiord 9588	. . . . . . . . . . . . . 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 255	. . . . . . . . . . . 12 ⊢ (1𝑜 <N suc 𝑦 → 1𝑜 ∈ suc 𝑦)
98	2	eqvinc 3300	. . . . . . . . . . . . . . 15 ⊢ (1𝑜 = 𝑦 ↔ ∃𝑥(𝑥 = 1𝑜 ∧ 𝑥 = 𝑦))
99	98, 29, 7	gencl 3208	. . . . . . . . . . . . . 14 ⊢ (1𝑜 = 𝑦 → 𝜒)
100		jao 533	. . . . . . . . . . . . . 14 ⊢ ((1𝑜 ∈ 𝑦 → 𝜒) → ((1𝑜 = 𝑦 → 𝜒) → ((1𝑜 ∈ 𝑦 ∨ 1𝑜 = 𝑦) → 𝜒)))
101	99, 100	mpi 20	. . . . . . . . . . . . 13 ⊢ ((1𝑜 ∈ 𝑦 → 𝜒) → ((1𝑜 ∈ 𝑦 ∨ 1𝑜 = 𝑦) → 𝜒))
102	41, 101	syl5 33	. . . . . . . . . . . 12 ⊢ ((1𝑜 ∈ 𝑦 → 𝜒) → (1𝑜 ∈ suc 𝑦 → 𝜒))
103	97, 102	syl5 33	. . . . . . . . . . 11 ⊢ ((1𝑜 ∈ 𝑦 → 𝜒) → (1𝑜 <N suc 𝑦 → 𝜒))
104	92, 103	syl6com 36	. . . . . . . . . 10 ⊢ (((𝑦 ∈ N ∧ 1𝑜 <N 𝑦) → 𝜒) → (𝑦 ∈ N → (1𝑜 <N suc 𝑦 → 𝜒)))
105	104	impd 446	. . . . . . . . 9 ⊢ (((𝑦 ∈ N ∧ 1𝑜 <N 𝑦) → 𝜒) → ((𝑦 ∈ N ∧ 1𝑜 <N suc 𝑦) → 𝜒))
106	16	sseq1i 3592	. . . . . . . . . . 11 ⊢ (1𝑜 ⊆ 𝑦 ↔ suc ∅ ⊆ 𝑦)
107		0ex 4718	. . . . . . . . . . . 12 ⊢ ∅ ∈ V
108		sucssel 5736	. . . . . . . . . . . 12 ⊢ (∅ ∈ V → (suc ∅ ⊆ 𝑦 → ∅ ∈ 𝑦))
109	107, 108	ax-mp 5	. . . . . . . . . . 11 ⊢ (suc ∅ ⊆ 𝑦 → ∅ ∈ 𝑦)
110	106, 109	sylbi 206	. . . . . . . . . 10 ⊢ (1𝑜 ⊆ 𝑦 → ∅ ∈ 𝑦)
111		elni2 9578	. . . . . . . . . . 11 ⊢ (𝑦 ∈ N ↔ (𝑦 ∈ ω ∧ ∅ ∈ 𝑦))
112		indpi.6	. . . . . . . . . . 11 ⊢ (𝑦 ∈ N → (𝜒 → 𝜃))
113	111, 112	sylbir 224	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ω ∧ ∅ ∈ 𝑦) → (𝜒 → 𝜃))
114	110, 113	sylan2 490	. . . . . . . . 9 ⊢ ((𝑦 ∈ ω ∧ 1𝑜 ⊆ 𝑦) → (𝜒 → 𝜃))
115	105, 114	syl9r 76	. . . . . . . 8 ⊢ ((𝑦 ∈ ω ∧ 1𝑜 ⊆ 𝑦) → (((𝑦 ∈ N ∧ 1𝑜 <N 𝑦) → 𝜒) → ((𝑦 ∈ N ∧ 1𝑜 <N suc 𝑦) → 𝜃)))
116	115	adantlr 747	. . . . . . 7 ⊢ (((𝑦 ∈ ω ∧ 1𝑜 ∈ ω) ∧ 1𝑜 ⊆ 𝑦) → (((𝑦 ∈ N ∧ 1𝑜 <N 𝑦) → 𝜒) → ((𝑦 ∈ N ∧ 1𝑜 <N suc 𝑦) → 𝜃)))
117	25, 30, 82, 86, 87, 116	findsg 6985	. . . . . 6 ⊢ (((𝐴 ∈ ω ∧ 1𝑜 ∈ ω) ∧ 1𝑜 ⊆ 𝐴) → ((𝐴 ∈ N ∧ 1𝑜 <N 𝐴) → 𝜏))
118	21, 117	mpanl2 713	. . . . 5 ⊢ ((𝐴 ∈ ω ∧ 1𝑜 ⊆ 𝐴) → ((𝐴 ∈ N ∧ 1𝑜 <N 𝐴) → 𝜏))
119	11, 20, 118	syl2anc 691	. . . 4 ⊢ (𝐴 ∈ N → ((𝐴 ∈ N ∧ 1𝑜 <N 𝐴) → 𝜏))
120	119	expd 451	. . 3 ⊢ (𝐴 ∈ N → (𝐴 ∈ N → (1𝑜 <N 𝐴 → 𝜏)))
121	120	pm2.43i 50	. 2 ⊢ (𝐴 ∈ N → (1𝑜 <N 𝐴 → 𝜏))
122		nlt1pi 9607	. . . 4 ⊢ ¬ 𝐴 <N 1𝑜
123		ltsopi 9589	. . . . . 6 ⊢ <N Or N
124		sotric 4985	. . . . . 6 ⊢ (( <N Or N ∧ (𝐴 ∈ N ∧ 1𝑜 ∈ N)) → (𝐴 <N 1𝑜 ↔ ¬ (𝐴 = 1𝑜 ∨ 1𝑜 <N 𝐴)))
125	123, 124	mpan 702	. . . . 5 ⊢ ((𝐴 ∈ N ∧ 1𝑜 ∈ N) → (𝐴 <N 1𝑜 ↔ ¬ (𝐴 = 1𝑜 ∨ 1𝑜 <N 𝐴)))
126	1, 125	mpan2 703	. . . 4 ⊢ (𝐴 ∈ N → (𝐴 <N 1𝑜 ↔ ¬ (𝐴 = 1𝑜 ∨ 1𝑜 <N 𝐴)))
127	122, 126	mtbii 315	. . 3 ⊢ (𝐴 ∈ N → ¬ ¬ (𝐴 = 1𝑜 ∨ 1𝑜 <N 𝐴))
128	127	notnotrd 127	. 2 ⊢ (𝐴 ∈ N → (𝐴 = 1𝑜 ∨ 1𝑜 <N 𝐴))
129	10, 121, 128	mpjaod 395	1 ⊢ (𝐴 ∈ N → 𝜏)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∨ wo 382   ∧ wa 383   = wceq 1475   ∈ wcel 1977   ≠ wne 2780  Vcvv 3173   ⊆ wss 3540  ∅c0 3874   class class class wbr 4583   Or wor 4958  Ord word 5639  Oncon0 5640  suc csuc 5642  (class class class)co 6549  ωcom 6957  1_𝑜c1o 7440   +_𝑜 coa 7444  Ncnpi 9545   +_N cpli 9546   <_N clti 9548

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-reu 2903  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-ni 9573  df-pli 9574  df-lti 9576

This theorem is referenced by:  prlem934  9734