Theorem indpi 10360

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

Step	Hyp	Ref	Expression
1		1oex 8121	. . . . . 6 ⊢ 1o ∈ V
2	1	eqvinc 3561	. . . . 5 ⊢ (1o = 𝐴 ↔ ∃𝑥(𝑥 = 1o ∧ 𝑥 = 𝐴))
3		indpi.4	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))
4		indpi.5	. . . . . 6 ⊢ 𝜓
5		indpi.1	. . . . . 6 ⊢ (𝑥 = 1o → (𝜑 ↔ 𝜓))
6	4, 5	mpbiri 261	. . . . 5 ⊢ (𝑥 = 1o → 𝜑)
7	2, 3, 6	gencl 3451	. . . 4 ⊢ (1o = 𝐴 → 𝜏)
8	7	eqcoms 2767	. . 3 ⊢ (𝐴 = 1o → 𝜏)
9	8	a1i 11	. 2 ⊢ (𝐴 ∈ N → (𝐴 = 1o → 𝜏))
10		pinn 10331	. . . . 5 ⊢ (𝐴 ∈ N → 𝐴 ∈ ω)
11		elni2 10330	. . . . . 6 ⊢ (𝐴 ∈ N ↔ (𝐴 ∈ ω ∧ ∅ ∈ 𝐴))
12		nnord 7588	. . . . . . . . 9 ⊢ (𝐴 ∈ ω → Ord 𝐴)
13		ordsucss 7533	. . . . . . . . 9 ⊢ (Ord 𝐴 → (∅ ∈ 𝐴 → suc ∅ ⊆ 𝐴))
14	12, 13	syl 17	. . . . . . . 8 ⊢ (𝐴 ∈ ω → (∅ ∈ 𝐴 → suc ∅ ⊆ 𝐴))
15		df-1o 8113	. . . . . . . . 9 ⊢ 1o = suc ∅
16	15	sseq1i 3921	. . . . . . . 8 ⊢ (1o ⊆ 𝐴 ↔ suc ∅ ⊆ 𝐴)
17	14, 16	syl6ibr 255	. . . . . . 7 ⊢ (𝐴 ∈ ω → (∅ ∈ 𝐴 → 1o ⊆ 𝐴))
18	17	imp 411	. . . . . 6 ⊢ ((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) → 1o ⊆ 𝐴)
19	11, 18	sylbi 220	. . . . 5 ⊢ (𝐴 ∈ N → 1o ⊆ 𝐴)
20		1onn 8276	. . . . . 6 ⊢ 1o ∈ ω
21		eleq1 2840	. . . . . . . . 9 ⊢ (𝑥 = 1o → (𝑥 ∈ N ↔ 1o ∈ N))
22		breq2 5037	. . . . . . . . 9 ⊢ (𝑥 = 1o → (1o <N 𝑥 ↔ 1o <N 1o))
23	21, 22	anbi12d 634	. . . . . . . 8 ⊢ (𝑥 = 1o → ((𝑥 ∈ N ∧ 1o <N 𝑥) ↔ (1o ∈ N ∧ 1o <N 1o)))
24	23, 5	imbi12d 349	. . . . . . 7 ⊢ (𝑥 = 1o → (((𝑥 ∈ N ∧ 1o <N 𝑥) → 𝜑) ↔ ((1o ∈ N ∧ 1o <N 1o) → 𝜓)))
25		eleq1 2840	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ N ↔ 𝑦 ∈ N))
26		breq2 5037	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (1o <N 𝑥 ↔ 1o <N 𝑦))
27	25, 26	anbi12d 634	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ N ∧ 1o <N 𝑥) ↔ (𝑦 ∈ N ∧ 1o <N 𝑦)))
28		indpi.2	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))
29	27, 28	imbi12d 349	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (((𝑥 ∈ N ∧ 1o <N 𝑥) → 𝜑) ↔ ((𝑦 ∈ N ∧ 1o <N 𝑦) → 𝜒)))
30		pinn 10331	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ N → 𝑥 ∈ ω)
31		eleq1 2840	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = suc 𝑦 → (𝑥 ∈ ω ↔ suc 𝑦 ∈ ω))
32		peano2b 7596	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ω ↔ suc 𝑦 ∈ ω)
33	31, 32	bitr4di 293	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = suc 𝑦 → (𝑥 ∈ ω ↔ 𝑦 ∈ ω))
34	30, 33	syl5ib 247	. . . . . . . . . . . . . 14 ⊢ (𝑥 = suc 𝑦 → (𝑥 ∈ N → 𝑦 ∈ ω))
35	34	adantrd 496	. . . . . . . . . . . . 13 ⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ N ∧ 1o <N 𝑥) → 𝑦 ∈ ω))
36		1pi 10336	. . . . . . . . . . . . . . . 16 ⊢ 1o ∈ N
37		ltpiord 10340	. . . . . . . . . . . . . . . 16 ⊢ ((1o ∈ N ∧ 𝑥 ∈ N) → (1o <N 𝑥 ↔ 1o ∈ 𝑥))
38	36, 37	mpan 690	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ N → (1o <N 𝑥 ↔ 1o ∈ 𝑥))
39	38	biimpa 481	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ N ∧ 1o <N 𝑥) → 1o ∈ 𝑥)
40		eleq2 2841	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = suc 𝑦 → (1o ∈ 𝑥 ↔ 1o ∈ suc 𝑦))
41		elsuci 6236	. . . . . . . . . . . . . . . 16 ⊢ (1o ∈ suc 𝑦 → (1o ∈ 𝑦 ∨ 1o = 𝑦))
42		ne0i 4234	. . . . . . . . . . . . . . . . 17 ⊢ (1o ∈ 𝑦 → 𝑦 ≠ ∅)
43		0lt1o 8140	. . . . . . . . . . . . . . . . . . 19 ⊢ ∅ ∈ 1o
44		eleq2 2841	. . . . . . . . . . . . . . . . . . 19 ⊢ (1o = 𝑦 → (∅ ∈ 1o ↔ ∅ ∈ 𝑦))
45	43, 44	mpbii 236	. . . . . . . . . . . . . . . . . 18 ⊢ (1o = 𝑦 → ∅ ∈ 𝑦)
46	45	ne0d 4235	. . . . . . . . . . . . . . . . 17 ⊢ (1o = 𝑦 → 𝑦 ≠ ∅)
47	42, 46	jaoi 855	. . . . . . . . . . . . . . . 16 ⊢ ((1o ∈ 𝑦 ∨ 1o = 𝑦) → 𝑦 ≠ ∅)
48	41, 47	syl 17	. . . . . . . . . . . . . . 15 ⊢ (1o ∈ suc 𝑦 → 𝑦 ≠ ∅)
49	40, 48	syl6bi 256	. . . . . . . . . . . . . 14 ⊢ (𝑥 = suc 𝑦 → (1o ∈ 𝑥 → 𝑦 ≠ ∅))
50	39, 49	syl5 34	. . . . . . . . . . . . 13 ⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ N ∧ 1o <N 𝑥) → 𝑦 ≠ ∅))
51	35, 50	jcad 517	. . . . . . . . . . . 12 ⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ N ∧ 1o <N 𝑥) → (𝑦 ∈ ω ∧ 𝑦 ≠ ∅)))
52		elni 10329	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ N ↔ (𝑦 ∈ ω ∧ 𝑦 ≠ ∅))
53	51, 52	syl6ibr 255	. . . . . . . . . . 11 ⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ N ∧ 1o <N 𝑥) → 𝑦 ∈ N))
54		simpr 489	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ N ∧ 1o <N 𝑥) → 1o <N 𝑥)
55		breq2 5037	. . . . . . . . . . . 12 ⊢ (𝑥 = suc 𝑦 → (1o <N 𝑥 ↔ 1o <N suc 𝑦))
56	54, 55	syl5ib 247	. . . . . . . . . . 11 ⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ N ∧ 1o <N 𝑥) → 1o <N suc 𝑦))
57	53, 56	jcad 517	. . . . . . . . . 10 ⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ N ∧ 1o <N 𝑥) → (𝑦 ∈ N ∧ 1o <N suc 𝑦)))
58		addclpi 10345	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ N ∧ 1o ∈ N) → (𝑦 +N 1o) ∈ N)
59	36, 58	mpan2 691	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ N → (𝑦 +N 1o) ∈ N)
60		addpiord 10337	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ N ∧ 1o ∈ N) → (𝑦 +N 1o) = (𝑦 +o 1o))
61	36, 60	mpan2 691	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ N → (𝑦 +N 1o) = (𝑦 +o 1o))
62		pion 10332	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ N → 𝑦 ∈ On)
63		oa1suc 8167	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ On → (𝑦 +o 1o) = suc 𝑦)
64	62, 63	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ N → (𝑦 +o 1o) = suc 𝑦)
65	61, 64	eqtrd 2794	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ N → (𝑦 +N 1o) = suc 𝑦)
66	65	eqeq2d 2770	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ N → (𝑥 = (𝑦 +N 1o) ↔ 𝑥 = suc 𝑦))
67	66	biimparc 484	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = suc 𝑦 ∧ 𝑦 ∈ N) → 𝑥 = (𝑦 +N 1o))
68	67	eleq1d 2837	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = suc 𝑦 ∧ 𝑦 ∈ N) → (𝑥 ∈ N ↔ (𝑦 +N 1o) ∈ N))
69	59, 68	syl5ibr 249	. . . . . . . . . . . . 13 ⊢ ((𝑥 = suc 𝑦 ∧ 𝑦 ∈ N) → (𝑦 ∈ N → 𝑥 ∈ N))
70	69	ex 417	. . . . . . . . . . . 12 ⊢ (𝑥 = suc 𝑦 → (𝑦 ∈ N → (𝑦 ∈ N → 𝑥 ∈ N)))
71	70	pm2.43d 53	. . . . . . . . . . 11 ⊢ (𝑥 = suc 𝑦 → (𝑦 ∈ N → 𝑥 ∈ N))
72	55	biimprd 251	. . . . . . . . . . 11 ⊢ (𝑥 = suc 𝑦 → (1o <N suc 𝑦 → 1o <N 𝑥))
73	71, 72	anim12d 612	. . . . . . . . . 10 ⊢ (𝑥 = suc 𝑦 → ((𝑦 ∈ N ∧ 1o <N suc 𝑦) → (𝑥 ∈ N ∧ 1o <N 𝑥)))
74	57, 73	impbid 215	. . . . . . . . 9 ⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ N ∧ 1o <N 𝑥) ↔ (𝑦 ∈ N ∧ 1o <N suc 𝑦)))
75	74	imbi1d 346	. . . . . . . 8 ⊢ (𝑥 = suc 𝑦 → (((𝑥 ∈ N ∧ 1o <N 𝑥) → 𝜑) ↔ ((𝑦 ∈ N ∧ 1o <N suc 𝑦) → 𝜑)))
76		indpi.3	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑦 +N 1o) → (𝜑 ↔ 𝜃))
77	66, 76	syl6bir 257	. . . . . . . . . . 11 ⊢ (𝑦 ∈ N → (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃)))
78	77	adantr 485	. . . . . . . . . 10 ⊢ ((𝑦 ∈ N ∧ 1o <N suc 𝑦) → (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃)))
79	78	com12 32	. . . . . . . . 9 ⊢ (𝑥 = suc 𝑦 → ((𝑦 ∈ N ∧ 1o <N suc 𝑦) → (𝜑 ↔ 𝜃)))
80	79	pm5.74d 276	. . . . . . . 8 ⊢ (𝑥 = suc 𝑦 → (((𝑦 ∈ N ∧ 1o <N suc 𝑦) → 𝜑) ↔ ((𝑦 ∈ N ∧ 1o <N suc 𝑦) → 𝜃)))
81	75, 80	bitrd 282	. . . . . . 7 ⊢ (𝑥 = suc 𝑦 → (((𝑥 ∈ N ∧ 1o <N 𝑥) → 𝜑) ↔ ((𝑦 ∈ N ∧ 1o <N suc 𝑦) → 𝜃)))
82		eleq1 2840	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ N ↔ 𝐴 ∈ N))
83		breq2 5037	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → (1o <N 𝑥 ↔ 1o <N 𝐴))
84	82, 83	anbi12d 634	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ N ∧ 1o <N 𝑥) ↔ (𝐴 ∈ N ∧ 1o <N 𝐴)))
85	84, 3	imbi12d 349	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (((𝑥 ∈ N ∧ 1o <N 𝑥) → 𝜑) ↔ ((𝐴 ∈ N ∧ 1o <N 𝐴) → 𝜏)))
86	4	2a1i 12	. . . . . . 7 ⊢ (1o ∈ ω → ((1o ∈ N ∧ 1o <N 1o) → 𝜓))
87		ltpiord 10340	. . . . . . . . . . . . . . 15 ⊢ ((1o ∈ N ∧ 𝑦 ∈ N) → (1o <N 𝑦 ↔ 1o ∈ 𝑦))
88	36, 87	mpan 690	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ N → (1o <N 𝑦 ↔ 1o ∈ 𝑦))
89	88	pm5.32i 579	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ N ∧ 1o <N 𝑦) ↔ (𝑦 ∈ N ∧ 1o ∈ 𝑦))
90	89	simplbi2 505	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ N → (1o ∈ 𝑦 → (𝑦 ∈ N ∧ 1o <N 𝑦)))
91	90	imim1d 82	. . . . . . . . . . 11 ⊢ (𝑦 ∈ N → (((𝑦 ∈ N ∧ 1o <N 𝑦) → 𝜒) → (1o ∈ 𝑦 → 𝜒)))
92		ltrelpi 10342	. . . . . . . . . . . . . . 15 ⊢ <N ⊆ (N × N)
93	92	brel 5587	. . . . . . . . . . . . . 14 ⊢ (1o <N suc 𝑦 → (1o ∈ N ∧ suc 𝑦 ∈ N))
94		ltpiord 10340	. . . . . . . . . . . . . 14 ⊢ ((1o ∈ N ∧ suc 𝑦 ∈ N) → (1o <N suc 𝑦 ↔ 1o ∈ suc 𝑦))
95	93, 94	syl 17	. . . . . . . . . . . . 13 ⊢ (1o <N suc 𝑦 → (1o <N suc 𝑦 ↔ 1o ∈ suc 𝑦))
96	95	ibi 270	. . . . . . . . . . . 12 ⊢ (1o <N suc 𝑦 → 1o ∈ suc 𝑦)
97	1	eqvinc 3561	. . . . . . . . . . . . . . 15 ⊢ (1o = 𝑦 ↔ ∃𝑥(𝑥 = 1o ∧ 𝑥 = 𝑦))
98	97, 28, 6	gencl 3451	. . . . . . . . . . . . . 14 ⊢ (1o = 𝑦 → 𝜒)
99		jao 959	. . . . . . . . . . . . . 14 ⊢ ((1o ∈ 𝑦 → 𝜒) → ((1o = 𝑦 → 𝜒) → ((1o ∈ 𝑦 ∨ 1o = 𝑦) → 𝜒)))
100	98, 99	mpi 20	. . . . . . . . . . . . 13 ⊢ ((1o ∈ 𝑦 → 𝜒) → ((1o ∈ 𝑦 ∨ 1o = 𝑦) → 𝜒))
101	41, 100	syl5 34	. . . . . . . . . . . 12 ⊢ ((1o ∈ 𝑦 → 𝜒) → (1o ∈ suc 𝑦 → 𝜒))
102	96, 101	syl5 34	. . . . . . . . . . 11 ⊢ ((1o ∈ 𝑦 → 𝜒) → (1o <N suc 𝑦 → 𝜒))
103	91, 102	syl6com 37	. . . . . . . . . 10 ⊢ (((𝑦 ∈ N ∧ 1o <N 𝑦) → 𝜒) → (𝑦 ∈ N → (1o <N suc 𝑦 → 𝜒)))
104	103	impd 415	. . . . . . . . 9 ⊢ (((𝑦 ∈ N ∧ 1o <N 𝑦) → 𝜒) → ((𝑦 ∈ N ∧ 1o <N suc 𝑦) → 𝜒))
105	15	sseq1i 3921	. . . . . . . . . . 11 ⊢ (1o ⊆ 𝑦 ↔ suc ∅ ⊆ 𝑦)
106		0ex 5178	. . . . . . . . . . . 12 ⊢ ∅ ∈ V
107		sucssel 6262	. . . . . . . . . . . 12 ⊢ (∅ ∈ V → (suc ∅ ⊆ 𝑦 → ∅ ∈ 𝑦))
108	106, 107	ax-mp 5	. . . . . . . . . . 11 ⊢ (suc ∅ ⊆ 𝑦 → ∅ ∈ 𝑦)
109	105, 108	sylbi 220	. . . . . . . . . 10 ⊢ (1o ⊆ 𝑦 → ∅ ∈ 𝑦)
110		elni2 10330	. . . . . . . . . . 11 ⊢ (𝑦 ∈ N ↔ (𝑦 ∈ ω ∧ ∅ ∈ 𝑦))
111		indpi.6	. . . . . . . . . . 11 ⊢ (𝑦 ∈ N → (𝜒 → 𝜃))
112	110, 111	sylbir 238	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ω ∧ ∅ ∈ 𝑦) → (𝜒 → 𝜃))
113	109, 112	sylan2 596	. . . . . . . . 9 ⊢ ((𝑦 ∈ ω ∧ 1o ⊆ 𝑦) → (𝜒 → 𝜃))
114	104, 113	syl9r 78	. . . . . . . 8 ⊢ ((𝑦 ∈ ω ∧ 1o ⊆ 𝑦) → (((𝑦 ∈ N ∧ 1o <N 𝑦) → 𝜒) → ((𝑦 ∈ N ∧ 1o <N suc 𝑦) → 𝜃)))
115	114	adantlr 715	. . . . . . 7 ⊢ (((𝑦 ∈ ω ∧ 1o ∈ ω) ∧ 1o ⊆ 𝑦) → (((𝑦 ∈ N ∧ 1o <N 𝑦) → 𝜒) → ((𝑦 ∈ N ∧ 1o <N suc 𝑦) → 𝜃)))
116	24, 29, 81, 85, 86, 115	findsg 7610	. . . . . 6 ⊢ (((𝐴 ∈ ω ∧ 1o ∈ ω) ∧ 1o ⊆ 𝐴) → ((𝐴 ∈ N ∧ 1o <N 𝐴) → 𝜏))
117	20, 116	mpanl2 701	. . . . 5 ⊢ ((𝐴 ∈ ω ∧ 1o ⊆ 𝐴) → ((𝐴 ∈ N ∧ 1o <N 𝐴) → 𝜏))
118	10, 19, 117	syl2anc 588	. . . 4 ⊢ (𝐴 ∈ N → ((𝐴 ∈ N ∧ 1o <N 𝐴) → 𝜏))
119	118	expd 420	. . 3 ⊢ (𝐴 ∈ N → (𝐴 ∈ N → (1o <N 𝐴 → 𝜏)))
120	119	pm2.43i 52	. 2 ⊢ (𝐴 ∈ N → (1o <N 𝐴 → 𝜏))
121		nlt1pi 10359	. . . 4 ⊢ ¬ 𝐴 <N 1o
122		ltsopi 10341	. . . . . 6 ⊢ <N Or N
123		sotric 5471	. . . . . 6 ⊢ (( <N Or N ∧ (𝐴 ∈ N ∧ 1o ∈ N)) → (𝐴 <N 1o ↔ ¬ (𝐴 = 1o ∨ 1o <N 𝐴)))
124	122, 123	mpan 690	. . . . 5 ⊢ ((𝐴 ∈ N ∧ 1o ∈ N) → (𝐴 <N 1o ↔ ¬ (𝐴 = 1o ∨ 1o <N 𝐴)))
125	36, 124	mpan2 691	. . . 4 ⊢ (𝐴 ∈ N → (𝐴 <N 1o ↔ ¬ (𝐴 = 1o ∨ 1o <N 𝐴)))
126	121, 125	mtbii 330	. . 3 ⊢ (𝐴 ∈ N → ¬ ¬ (𝐴 = 1o ∨ 1o <N 𝐴))
127	126	notnotrd 135	. 2 ⊢ (𝐴 ∈ N → (𝐴 = 1o ∨ 1o <N 𝐴))
128	9, 120, 127	mpjaod 858	1 ⊢ (𝐴 ∈ N → 𝜏)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 400   ∨ wo 845   = wceq 1539   ∈ wcel 2112   ≠ wne 2952  Vcvv 3410   ⊆ wss 3859  ∅c0 4226   class class class wbr 5033   Or wor 5443  Ord word 6169  Oncon0 6170  suc csuc 6172  (class class class)co 7151  ωcom 7580  1_oc1o 8106   +_o coa 8110  Ncnpi 10297   +_N cpli 10298   <_N clti 10300

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-sep 5170  ax-nul 5177  ax-pr 5299  ax-un 7460

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-ral 3076  df-rex 3077  df-reu 3078  df-rab 3080  df-v 3412  df-sbc 3698  df-csb 3807  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-pss 3878  df-nul 4227  df-if 4422  df-pw 4497  df-sn 4524  df-pr 4526  df-tp 4528  df-op 4530  df-uni 4800  df-iun 4886  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5431  df-eprel 5436  df-po 5444  df-so 5445  df-fr 5484  df-we 5486  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-pred 6127  df-ord 6173  df-on 6174  df-lim 6175  df-suc 6176  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341  df-fo 6342  df-f1o 6343  df-fv 6344  df-ov 7154  df-oprab 7155  df-mpo 7156  df-om 7581  df-wrecs 7958  df-recs 8019  df-rdg 8057  df-1o 8113  df-oadd 8117  df-ni 10325  df-pli 10326  df-lti 10328

This theorem is referenced by:  prlem934  10486