Theorem indpi 10329

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 8110	. . . . . 6 ⊢ 1o ∈ V
2	1	eqvinc 3642	. . . . 5 ⊢ (1o = 𝐴 ↔ ∃𝑥(𝑥 = 1o ∧ 𝑥 = 𝐴))
3		indpi.4	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))
4		indpi.5	. . . . . 6 ⊢ 𝜓
5		indpi.1	. . . . . 6 ⊢ (𝑥 = 1o → (𝜑 ↔ 𝜓))
6	4, 5	mpbiri 260	. . . . 5 ⊢ (𝑥 = 1o → 𝜑)
7	2, 3, 6	gencl 3534	. . . 4 ⊢ (1o = 𝐴 → 𝜏)
8	7	eqcoms 2829	. . 3 ⊢ (𝐴 = 1o → 𝜏)
9	8	a1i 11	. 2 ⊢ (𝐴 ∈ N → (𝐴 = 1o → 𝜏))
10		pinn 10300	. . . . 5 ⊢ (𝐴 ∈ N → 𝐴 ∈ ω)
11		elni2 10299	. . . . . 6 ⊢ (𝐴 ∈ N ↔ (𝐴 ∈ ω ∧ ∅ ∈ 𝐴))
12		nnord 7588	. . . . . . . . 9 ⊢ (𝐴 ∈ ω → Ord 𝐴)
13		ordsucss 7533	. . . . . . . . 9 ⊢ (Ord 𝐴 → (∅ ∈ 𝐴 → suc ∅ ⊆ 𝐴))
14	12, 13	syl 17	. . . . . . . 8 ⊢ (𝐴 ∈ ω → (∅ ∈ 𝐴 → suc ∅ ⊆ 𝐴))
15		df-1o 8102	. . . . . . . . 9 ⊢ 1o = suc ∅
16	15	sseq1i 3995	. . . . . . . 8 ⊢ (1o ⊆ 𝐴 ↔ suc ∅ ⊆ 𝐴)
17	14, 16	syl6ibr 254	. . . . . . 7 ⊢ (𝐴 ∈ ω → (∅ ∈ 𝐴 → 1o ⊆ 𝐴))
18	17	imp 409	. . . . . 6 ⊢ ((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) → 1o ⊆ 𝐴)
19	11, 18	sylbi 219	. . . . 5 ⊢ (𝐴 ∈ N → 1o ⊆ 𝐴)
20		1onn 8265	. . . . . 6 ⊢ 1o ∈ ω
21		eleq1 2900	. . . . . . . . 9 ⊢ (𝑥 = 1o → (𝑥 ∈ N ↔ 1o ∈ N))
22		breq2 5070	. . . . . . . . 9 ⊢ (𝑥 = 1o → (1o <N 𝑥 ↔ 1o <N 1o))
23	21, 22	anbi12d 632	. . . . . . . 8 ⊢ (𝑥 = 1o → ((𝑥 ∈ N ∧ 1o <N 𝑥) ↔ (1o ∈ N ∧ 1o <N 1o)))
24	23, 5	imbi12d 347	. . . . . . 7 ⊢ (𝑥 = 1o → (((𝑥 ∈ N ∧ 1o <N 𝑥) → 𝜑) ↔ ((1o ∈ N ∧ 1o <N 1o) → 𝜓)))
25		eleq1 2900	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ N ↔ 𝑦 ∈ N))
26		breq2 5070	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (1o <N 𝑥 ↔ 1o <N 𝑦))
27	25, 26	anbi12d 632	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ N ∧ 1o <N 𝑥) ↔ (𝑦 ∈ N ∧ 1o <N 𝑦)))
28		indpi.2	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))
29	27, 28	imbi12d 347	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (((𝑥 ∈ N ∧ 1o <N 𝑥) → 𝜑) ↔ ((𝑦 ∈ N ∧ 1o <N 𝑦) → 𝜒)))
30		pinn 10300	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ N → 𝑥 ∈ ω)
31		eleq1 2900	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = suc 𝑦 → (𝑥 ∈ ω ↔ suc 𝑦 ∈ ω))
32		peano2b 7596	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ω ↔ suc 𝑦 ∈ ω)
33	31, 32	syl6bbr 291	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = suc 𝑦 → (𝑥 ∈ ω ↔ 𝑦 ∈ ω))
34	30, 33	syl5ib 246	. . . . . . . . . . . . . 14 ⊢ (𝑥 = suc 𝑦 → (𝑥 ∈ N → 𝑦 ∈ ω))
35	34	adantrd 494	. . . . . . . . . . . . 13 ⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ N ∧ 1o <N 𝑥) → 𝑦 ∈ ω))
36		1pi 10305	. . . . . . . . . . . . . . . 16 ⊢ 1o ∈ N
37		ltpiord 10309	. . . . . . . . . . . . . . . 16 ⊢ ((1o ∈ N ∧ 𝑥 ∈ N) → (1o <N 𝑥 ↔ 1o ∈ 𝑥))
38	36, 37	mpan 688	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ N → (1o <N 𝑥 ↔ 1o ∈ 𝑥))
39	38	biimpa 479	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ N ∧ 1o <N 𝑥) → 1o ∈ 𝑥)
40		eleq2 2901	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = suc 𝑦 → (1o ∈ 𝑥 ↔ 1o ∈ suc 𝑦))
41		elsuci 6257	. . . . . . . . . . . . . . . 16 ⊢ (1o ∈ suc 𝑦 → (1o ∈ 𝑦 ∨ 1o = 𝑦))
42		ne0i 4300	. . . . . . . . . . . . . . . . 17 ⊢ (1o ∈ 𝑦 → 𝑦 ≠ ∅)
43		0lt1o 8129	. . . . . . . . . . . . . . . . . . 19 ⊢ ∅ ∈ 1o
44		eleq2 2901	. . . . . . . . . . . . . . . . . . 19 ⊢ (1o = 𝑦 → (∅ ∈ 1o ↔ ∅ ∈ 𝑦))
45	43, 44	mpbii 235	. . . . . . . . . . . . . . . . . 18 ⊢ (1o = 𝑦 → ∅ ∈ 𝑦)
46	45	ne0d 4301	. . . . . . . . . . . . . . . . 17 ⊢ (1o = 𝑦 → 𝑦 ≠ ∅)
47	42, 46	jaoi 853	. . . . . . . . . . . . . . . 16 ⊢ ((1o ∈ 𝑦 ∨ 1o = 𝑦) → 𝑦 ≠ ∅)
48	41, 47	syl 17	. . . . . . . . . . . . . . 15 ⊢ (1o ∈ suc 𝑦 → 𝑦 ≠ ∅)
49	40, 48	syl6bi 255	. . . . . . . . . . . . . 14 ⊢ (𝑥 = suc 𝑦 → (1o ∈ 𝑥 → 𝑦 ≠ ∅))
50	39, 49	syl5 34	. . . . . . . . . . . . 13 ⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ N ∧ 1o <N 𝑥) → 𝑦 ≠ ∅))
51	35, 50	jcad 515	. . . . . . . . . . . 12 ⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ N ∧ 1o <N 𝑥) → (𝑦 ∈ ω ∧ 𝑦 ≠ ∅)))
52		elni 10298	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ N ↔ (𝑦 ∈ ω ∧ 𝑦 ≠ ∅))
53	51, 52	syl6ibr 254	. . . . . . . . . . 11 ⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ N ∧ 1o <N 𝑥) → 𝑦 ∈ N))
54		simpr 487	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ N ∧ 1o <N 𝑥) → 1o <N 𝑥)
55		breq2 5070	. . . . . . . . . . . 12 ⊢ (𝑥 = suc 𝑦 → (1o <N 𝑥 ↔ 1o <N suc 𝑦))
56	54, 55	syl5ib 246	. . . . . . . . . . 11 ⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ N ∧ 1o <N 𝑥) → 1o <N suc 𝑦))
57	53, 56	jcad 515	. . . . . . . . . 10 ⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ N ∧ 1o <N 𝑥) → (𝑦 ∈ N ∧ 1o <N suc 𝑦)))
58		addclpi 10314	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ N ∧ 1o ∈ N) → (𝑦 +N 1o) ∈ N)
59	36, 58	mpan2 689	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ N → (𝑦 +N 1o) ∈ N)
60		addpiord 10306	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ N ∧ 1o ∈ N) → (𝑦 +N 1o) = (𝑦 +o 1o))
61	36, 60	mpan2 689	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ N → (𝑦 +N 1o) = (𝑦 +o 1o))
62		pion 10301	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ N → 𝑦 ∈ On)
63		oa1suc 8156	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ On → (𝑦 +o 1o) = suc 𝑦)
64	62, 63	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ N → (𝑦 +o 1o) = suc 𝑦)
65	61, 64	eqtrd 2856	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ N → (𝑦 +N 1o) = suc 𝑦)
66	65	eqeq2d 2832	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ N → (𝑥 = (𝑦 +N 1o) ↔ 𝑥 = suc 𝑦))
67	66	biimparc 482	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = suc 𝑦 ∧ 𝑦 ∈ N) → 𝑥 = (𝑦 +N 1o))
68	67	eleq1d 2897	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = suc 𝑦 ∧ 𝑦 ∈ N) → (𝑥 ∈ N ↔ (𝑦 +N 1o) ∈ N))
69	59, 68	syl5ibr 248	. . . . . . . . . . . . 13 ⊢ ((𝑥 = suc 𝑦 ∧ 𝑦 ∈ N) → (𝑦 ∈ N → 𝑥 ∈ N))
70	69	ex 415	. . . . . . . . . . . 12 ⊢ (𝑥 = suc 𝑦 → (𝑦 ∈ N → (𝑦 ∈ N → 𝑥 ∈ N)))
71	70	pm2.43d 53	. . . . . . . . . . 11 ⊢ (𝑥 = suc 𝑦 → (𝑦 ∈ N → 𝑥 ∈ N))
72	55	biimprd 250	. . . . . . . . . . 11 ⊢ (𝑥 = suc 𝑦 → (1o <N suc 𝑦 → 1o <N 𝑥))
73	71, 72	anim12d 610	. . . . . . . . . 10 ⊢ (𝑥 = suc 𝑦 → ((𝑦 ∈ N ∧ 1o <N suc 𝑦) → (𝑥 ∈ N ∧ 1o <N 𝑥)))
74	57, 73	impbid 214	. . . . . . . . 9 ⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ N ∧ 1o <N 𝑥) ↔ (𝑦 ∈ N ∧ 1o <N suc 𝑦)))
75	74	imbi1d 344	. . . . . . . 8 ⊢ (𝑥 = suc 𝑦 → (((𝑥 ∈ N ∧ 1o <N 𝑥) → 𝜑) ↔ ((𝑦 ∈ N ∧ 1o <N suc 𝑦) → 𝜑)))
76		indpi.3	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑦 +N 1o) → (𝜑 ↔ 𝜃))
77	66, 76	syl6bir 256	. . . . . . . . . . 11 ⊢ (𝑦 ∈ N → (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃)))
78	77	adantr 483	. . . . . . . . . 10 ⊢ ((𝑦 ∈ N ∧ 1o <N suc 𝑦) → (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃)))
79	78	com12 32	. . . . . . . . 9 ⊢ (𝑥 = suc 𝑦 → ((𝑦 ∈ N ∧ 1o <N suc 𝑦) → (𝜑 ↔ 𝜃)))
80	79	pm5.74d 275	. . . . . . . 8 ⊢ (𝑥 = suc 𝑦 → (((𝑦 ∈ N ∧ 1o <N suc 𝑦) → 𝜑) ↔ ((𝑦 ∈ N ∧ 1o <N suc 𝑦) → 𝜃)))
81	75, 80	bitrd 281	. . . . . . 7 ⊢ (𝑥 = suc 𝑦 → (((𝑥 ∈ N ∧ 1o <N 𝑥) → 𝜑) ↔ ((𝑦 ∈ N ∧ 1o <N suc 𝑦) → 𝜃)))
82		eleq1 2900	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ N ↔ 𝐴 ∈ N))
83		breq2 5070	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → (1o <N 𝑥 ↔ 1o <N 𝐴))
84	82, 83	anbi12d 632	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ N ∧ 1o <N 𝑥) ↔ (𝐴 ∈ N ∧ 1o <N 𝐴)))
85	84, 3	imbi12d 347	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (((𝑥 ∈ N ∧ 1o <N 𝑥) → 𝜑) ↔ ((𝐴 ∈ N ∧ 1o <N 𝐴) → 𝜏)))
86	4	2a1i 12	. . . . . . 7 ⊢ (1o ∈ ω → ((1o ∈ N ∧ 1o <N 1o) → 𝜓))
87		ltpiord 10309	. . . . . . . . . . . . . . 15 ⊢ ((1o ∈ N ∧ 𝑦 ∈ N) → (1o <N 𝑦 ↔ 1o ∈ 𝑦))
88	36, 87	mpan 688	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ N → (1o <N 𝑦 ↔ 1o ∈ 𝑦))
89	88	pm5.32i 577	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ N ∧ 1o <N 𝑦) ↔ (𝑦 ∈ N ∧ 1o ∈ 𝑦))
90	89	simplbi2 503	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ N → (1o ∈ 𝑦 → (𝑦 ∈ N ∧ 1o <N 𝑦)))
91	90	imim1d 82	. . . . . . . . . . 11 ⊢ (𝑦 ∈ N → (((𝑦 ∈ N ∧ 1o <N 𝑦) → 𝜒) → (1o ∈ 𝑦 → 𝜒)))
92		ltrelpi 10311	. . . . . . . . . . . . . . 15 ⊢ <N ⊆ (N × N)
93	92	brel 5617	. . . . . . . . . . . . . 14 ⊢ (1o <N suc 𝑦 → (1o ∈ N ∧ suc 𝑦 ∈ N))
94		ltpiord 10309	. . . . . . . . . . . . . 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 269	. . . . . . . . . . . 12 ⊢ (1o <N suc 𝑦 → 1o ∈ suc 𝑦)
97	1	eqvinc 3642	. . . . . . . . . . . . . . 15 ⊢ (1o = 𝑦 ↔ ∃𝑥(𝑥 = 1o ∧ 𝑥 = 𝑦))
98	97, 28, 6	gencl 3534	. . . . . . . . . . . . . 14 ⊢ (1o = 𝑦 → 𝜒)
99		jao 957	. . . . . . . . . . . . . 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 413	. . . . . . . . 9 ⊢ (((𝑦 ∈ N ∧ 1o <N 𝑦) → 𝜒) → ((𝑦 ∈ N ∧ 1o <N suc 𝑦) → 𝜒))
105	15	sseq1i 3995	. . . . . . . . . . 11 ⊢ (1o ⊆ 𝑦 ↔ suc ∅ ⊆ 𝑦)
106		0ex 5211	. . . . . . . . . . . 12 ⊢ ∅ ∈ V
107		sucssel 6283	. . . . . . . . . . . 12 ⊢ (∅ ∈ V → (suc ∅ ⊆ 𝑦 → ∅ ∈ 𝑦))
108	106, 107	ax-mp 5	. . . . . . . . . . 11 ⊢ (suc ∅ ⊆ 𝑦 → ∅ ∈ 𝑦)
109	105, 108	sylbi 219	. . . . . . . . . 10 ⊢ (1o ⊆ 𝑦 → ∅ ∈ 𝑦)
110		elni2 10299	. . . . . . . . . . 11 ⊢ (𝑦 ∈ N ↔ (𝑦 ∈ ω ∧ ∅ ∈ 𝑦))
111		indpi.6	. . . . . . . . . . 11 ⊢ (𝑦 ∈ N → (𝜒 → 𝜃))
112	110, 111	sylbir 237	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ω ∧ ∅ ∈ 𝑦) → (𝜒 → 𝜃))
113	109, 112	sylan2 594	. . . . . . . . 9 ⊢ ((𝑦 ∈ ω ∧ 1o ⊆ 𝑦) → (𝜒 → 𝜃))
114	104, 113	syl9r 78	. . . . . . . 8 ⊢ ((𝑦 ∈ ω ∧ 1o ⊆ 𝑦) → (((𝑦 ∈ N ∧ 1o <N 𝑦) → 𝜒) → ((𝑦 ∈ N ∧ 1o <N suc 𝑦) → 𝜃)))
115	114	adantlr 713	. . . . . . 7 ⊢ (((𝑦 ∈ ω ∧ 1o ∈ ω) ∧ 1o ⊆ 𝑦) → (((𝑦 ∈ N ∧ 1o <N 𝑦) → 𝜒) → ((𝑦 ∈ N ∧ 1o <N suc 𝑦) → 𝜃)))
116	24, 29, 81, 85, 86, 115	findsg 7609	. . . . . 6 ⊢ (((𝐴 ∈ ω ∧ 1o ∈ ω) ∧ 1o ⊆ 𝐴) → ((𝐴 ∈ N ∧ 1o <N 𝐴) → 𝜏))
117	20, 116	mpanl2 699	. . . . 5 ⊢ ((𝐴 ∈ ω ∧ 1o ⊆ 𝐴) → ((𝐴 ∈ N ∧ 1o <N 𝐴) → 𝜏))
118	10, 19, 117	syl2anc 586	. . . 4 ⊢ (𝐴 ∈ N → ((𝐴 ∈ N ∧ 1o <N 𝐴) → 𝜏))
119	118	expd 418	. . 3 ⊢ (𝐴 ∈ N → (𝐴 ∈ N → (1o <N 𝐴 → 𝜏)))
120	119	pm2.43i 52	. 2 ⊢ (𝐴 ∈ N → (1o <N 𝐴 → 𝜏))
121		nlt1pi 10328	. . . 4 ⊢ ¬ 𝐴 <N 1o
122		ltsopi 10310	. . . . . 6 ⊢ <N Or N
123		sotric 5501	. . . . . 6 ⊢ (( <N Or N ∧ (𝐴 ∈ N ∧ 1o ∈ N)) → (𝐴 <N 1o ↔ ¬ (𝐴 = 1o ∨ 1o <N 𝐴)))
124	122, 123	mpan 688	. . . . 5 ⊢ ((𝐴 ∈ N ∧ 1o ∈ N) → (𝐴 <N 1o ↔ ¬ (𝐴 = 1o ∨ 1o <N 𝐴)))
125	36, 124	mpan2 689	. . . 4 ⊢ (𝐴 ∈ N → (𝐴 <N 1o ↔ ¬ (𝐴 = 1o ∨ 1o <N 𝐴)))
126	121, 125	mtbii 328	. . 3 ⊢ (𝐴 ∈ N → ¬ ¬ (𝐴 = 1o ∨ 1o <N 𝐴))
127	126	notnotrd 135	. 2 ⊢ (𝐴 ∈ N → (𝐴 = 1o ∨ 1o <N 𝐴))
128	9, 120, 127	mpjaod 856	1 ⊢ (𝐴 ∈ N → 𝜏)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   ∨ wo 843   = wceq 1537   ∈ wcel 2114   ≠ wne 3016  Vcvv 3494   ⊆ wss 3936  ∅c0 4291   class class class wbr 5066   Or wor 5473  Ord word 6190  Oncon0 6191  suc csuc 6193  (class class class)co 7156  ωcom 7580  1_oc1o 8095   +_o coa 8099  Ncnpi 10266   +_N cpli 10267   <_N clti 10269

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4839  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-tr 5173  df-id 5460  df-eprel 5465  df-po 5474  df-so 5475  df-fr 5514  df-we 5516  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-pred 6148  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-ov 7159  df-oprab 7160  df-mpo 7161  df-om 7581  df-wrecs 7947  df-recs 8008  df-rdg 8046  df-1o 8102  df-oadd 8106  df-ni 10294  df-pli 10295  df-lti 10297

This theorem is referenced by:  prlem934  10455