Theorem indpi 10318

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 8093	. . . . . 6 ⊢ 1o ∈ V
2	1	eqvinc 3590	. . . . 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 3481	. . . 4 ⊢ (1o = 𝐴 → 𝜏)
8	7	eqcoms 2806	. . 3 ⊢ (𝐴 = 1o → 𝜏)
9	8	a1i 11	. 2 ⊢ (𝐴 ∈ N → (𝐴 = 1o → 𝜏))
10		pinn 10289	. . . . 5 ⊢ (𝐴 ∈ N → 𝐴 ∈ ω)
11		elni2 10288	. . . . . 6 ⊢ (𝐴 ∈ N ↔ (𝐴 ∈ ω ∧ ∅ ∈ 𝐴))
12		nnord 7568	. . . . . . . . 9 ⊢ (𝐴 ∈ ω → Ord 𝐴)
13		ordsucss 7513	. . . . . . . . 9 ⊢ (Ord 𝐴 → (∅ ∈ 𝐴 → suc ∅ ⊆ 𝐴))
14	12, 13	syl 17	. . . . . . . 8 ⊢ (𝐴 ∈ ω → (∅ ∈ 𝐴 → suc ∅ ⊆ 𝐴))
15		df-1o 8085	. . . . . . . . 9 ⊢ 1o = suc ∅
16	15	sseq1i 3943	. . . . . . . 8 ⊢ (1o ⊆ 𝐴 ↔ suc ∅ ⊆ 𝐴)
17	14, 16	syl6ibr 255	. . . . . . 7 ⊢ (𝐴 ∈ ω → (∅ ∈ 𝐴 → 1o ⊆ 𝐴))
18	17	imp 410	. . . . . 6 ⊢ ((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) → 1o ⊆ 𝐴)
19	11, 18	sylbi 220	. . . . 5 ⊢ (𝐴 ∈ N → 1o ⊆ 𝐴)
20		1onn 8248	. . . . . 6 ⊢ 1o ∈ ω
21		eleq1 2877	. . . . . . . . 9 ⊢ (𝑥 = 1o → (𝑥 ∈ N ↔ 1o ∈ N))
22		breq2 5034	. . . . . . . . 9 ⊢ (𝑥 = 1o → (1o <N 𝑥 ↔ 1o <N 1o))
23	21, 22	anbi12d 633	. . . . . . . 8 ⊢ (𝑥 = 1o → ((𝑥 ∈ N ∧ 1o <N 𝑥) ↔ (1o ∈ N ∧ 1o <N 1o)))
24	23, 5	imbi12d 348	. . . . . . 7 ⊢ (𝑥 = 1o → (((𝑥 ∈ N ∧ 1o <N 𝑥) → 𝜑) ↔ ((1o ∈ N ∧ 1o <N 1o) → 𝜓)))
25		eleq1 2877	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ N ↔ 𝑦 ∈ N))
26		breq2 5034	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (1o <N 𝑥 ↔ 1o <N 𝑦))
27	25, 26	anbi12d 633	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → ((𝑥 ∈ N ∧ 1o <N 𝑥) ↔ (𝑦 ∈ N ∧ 1o <N 𝑦)))
28		indpi.2	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝜑 ↔ 𝜒))
29	27, 28	imbi12d 348	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (((𝑥 ∈ N ∧ 1o <N 𝑥) → 𝜑) ↔ ((𝑦 ∈ N ∧ 1o <N 𝑦) → 𝜒)))
30		pinn 10289	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ N → 𝑥 ∈ ω)
31		eleq1 2877	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = suc 𝑦 → (𝑥 ∈ ω ↔ suc 𝑦 ∈ ω))
32		peano2b 7576	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ω ↔ suc 𝑦 ∈ ω)
33	31, 32	syl6bbr 292	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = suc 𝑦 → (𝑥 ∈ ω ↔ 𝑦 ∈ ω))
34	30, 33	syl5ib 247	. . . . . . . . . . . . . 14 ⊢ (𝑥 = suc 𝑦 → (𝑥 ∈ N → 𝑦 ∈ ω))
35	34	adantrd 495	. . . . . . . . . . . . 13 ⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ N ∧ 1o <N 𝑥) → 𝑦 ∈ ω))
36		1pi 10294	. . . . . . . . . . . . . . . 16 ⊢ 1o ∈ N
37		ltpiord 10298	. . . . . . . . . . . . . . . 16 ⊢ ((1o ∈ N ∧ 𝑥 ∈ N) → (1o <N 𝑥 ↔ 1o ∈ 𝑥))
38	36, 37	mpan 689	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ N → (1o <N 𝑥 ↔ 1o ∈ 𝑥))
39	38	biimpa 480	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ N ∧ 1o <N 𝑥) → 1o ∈ 𝑥)
40		eleq2 2878	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = suc 𝑦 → (1o ∈ 𝑥 ↔ 1o ∈ suc 𝑦))
41		elsuci 6225	. . . . . . . . . . . . . . . 16 ⊢ (1o ∈ suc 𝑦 → (1o ∈ 𝑦 ∨ 1o = 𝑦))
42		ne0i 4250	. . . . . . . . . . . . . . . . 17 ⊢ (1o ∈ 𝑦 → 𝑦 ≠ ∅)
43		0lt1o 8112	. . . . . . . . . . . . . . . . . . 19 ⊢ ∅ ∈ 1o
44		eleq2 2878	. . . . . . . . . . . . . . . . . . 19 ⊢ (1o = 𝑦 → (∅ ∈ 1o ↔ ∅ ∈ 𝑦))
45	43, 44	mpbii 236	. . . . . . . . . . . . . . . . . 18 ⊢ (1o = 𝑦 → ∅ ∈ 𝑦)
46	45	ne0d 4251	. . . . . . . . . . . . . . . . 17 ⊢ (1o = 𝑦 → 𝑦 ≠ ∅)
47	42, 46	jaoi 854	. . . . . . . . . . . . . . . 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 516	. . . . . . . . . . . 12 ⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ N ∧ 1o <N 𝑥) → (𝑦 ∈ ω ∧ 𝑦 ≠ ∅)))
52		elni 10287	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ N ↔ (𝑦 ∈ ω ∧ 𝑦 ≠ ∅))
53	51, 52	syl6ibr 255	. . . . . . . . . . 11 ⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ N ∧ 1o <N 𝑥) → 𝑦 ∈ N))
54		simpr 488	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ N ∧ 1o <N 𝑥) → 1o <N 𝑥)
55		breq2 5034	. . . . . . . . . . . 12 ⊢ (𝑥 = suc 𝑦 → (1o <N 𝑥 ↔ 1o <N suc 𝑦))
56	54, 55	syl5ib 247	. . . . . . . . . . 11 ⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ N ∧ 1o <N 𝑥) → 1o <N suc 𝑦))
57	53, 56	jcad 516	. . . . . . . . . 10 ⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ N ∧ 1o <N 𝑥) → (𝑦 ∈ N ∧ 1o <N suc 𝑦)))
58		addclpi 10303	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ N ∧ 1o ∈ N) → (𝑦 +N 1o) ∈ N)
59	36, 58	mpan2 690	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ N → (𝑦 +N 1o) ∈ N)
60		addpiord 10295	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ N ∧ 1o ∈ N) → (𝑦 +N 1o) = (𝑦 +o 1o))
61	36, 60	mpan2 690	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ N → (𝑦 +N 1o) = (𝑦 +o 1o))
62		pion 10290	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ N → 𝑦 ∈ On)
63		oa1suc 8139	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ On → (𝑦 +o 1o) = suc 𝑦)
64	62, 63	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ N → (𝑦 +o 1o) = suc 𝑦)
65	61, 64	eqtrd 2833	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ N → (𝑦 +N 1o) = suc 𝑦)
66	65	eqeq2d 2809	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ N → (𝑥 = (𝑦 +N 1o) ↔ 𝑥 = suc 𝑦))
67	66	biimparc 483	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = suc 𝑦 ∧ 𝑦 ∈ N) → 𝑥 = (𝑦 +N 1o))
68	67	eleq1d 2874	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = suc 𝑦 ∧ 𝑦 ∈ N) → (𝑥 ∈ N ↔ (𝑦 +N 1o) ∈ N))
69	59, 68	syl5ibr 249	. . . . . . . . . . . . 13 ⊢ ((𝑥 = suc 𝑦 ∧ 𝑦 ∈ N) → (𝑦 ∈ N → 𝑥 ∈ N))
70	69	ex 416	. . . . . . . . . . . 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 611	. . . . . . . . . 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 345	. . . . . . . 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 484	. . . . . . . . . 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 2877	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ N ↔ 𝐴 ∈ N))
83		breq2 5034	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → (1o <N 𝑥 ↔ 1o <N 𝐴))
84	82, 83	anbi12d 633	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ N ∧ 1o <N 𝑥) ↔ (𝐴 ∈ N ∧ 1o <N 𝐴)))
85	84, 3	imbi12d 348	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (((𝑥 ∈ N ∧ 1o <N 𝑥) → 𝜑) ↔ ((𝐴 ∈ N ∧ 1o <N 𝐴) → 𝜏)))
86	4	2a1i 12	. . . . . . 7 ⊢ (1o ∈ ω → ((1o ∈ N ∧ 1o <N 1o) → 𝜓))
87		ltpiord 10298	. . . . . . . . . . . . . . 15 ⊢ ((1o ∈ N ∧ 𝑦 ∈ N) → (1o <N 𝑦 ↔ 1o ∈ 𝑦))
88	36, 87	mpan 689	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ N → (1o <N 𝑦 ↔ 1o ∈ 𝑦))
89	88	pm5.32i 578	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ N ∧ 1o <N 𝑦) ↔ (𝑦 ∈ N ∧ 1o ∈ 𝑦))
90	89	simplbi2 504	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ N → (1o ∈ 𝑦 → (𝑦 ∈ N ∧ 1o <N 𝑦)))
91	90	imim1d 82	. . . . . . . . . . 11 ⊢ (𝑦 ∈ N → (((𝑦 ∈ N ∧ 1o <N 𝑦) → 𝜒) → (1o ∈ 𝑦 → 𝜒)))
92		ltrelpi 10300	. . . . . . . . . . . . . . 15 ⊢ <N ⊆ (N × N)
93	92	brel 5581	. . . . . . . . . . . . . 14 ⊢ (1o <N suc 𝑦 → (1o ∈ N ∧ suc 𝑦 ∈ N))
94		ltpiord 10298	. . . . . . . . . . . . . 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 3590	. . . . . . . . . . . . . . 15 ⊢ (1o = 𝑦 ↔ ∃𝑥(𝑥 = 1o ∧ 𝑥 = 𝑦))
98	97, 28, 6	gencl 3481	. . . . . . . . . . . . . 14 ⊢ (1o = 𝑦 → 𝜒)
99		jao 958	. . . . . . . . . . . . . 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 414	. . . . . . . . 9 ⊢ (((𝑦 ∈ N ∧ 1o <N 𝑦) → 𝜒) → ((𝑦 ∈ N ∧ 1o <N suc 𝑦) → 𝜒))
105	15	sseq1i 3943	. . . . . . . . . . 11 ⊢ (1o ⊆ 𝑦 ↔ suc ∅ ⊆ 𝑦)
106		0ex 5175	. . . . . . . . . . . 12 ⊢ ∅ ∈ V
107		sucssel 6251	. . . . . . . . . . . 12 ⊢ (∅ ∈ V → (suc ∅ ⊆ 𝑦 → ∅ ∈ 𝑦))
108	106, 107	ax-mp 5	. . . . . . . . . . 11 ⊢ (suc ∅ ⊆ 𝑦 → ∅ ∈ 𝑦)
109	105, 108	sylbi 220	. . . . . . . . . 10 ⊢ (1o ⊆ 𝑦 → ∅ ∈ 𝑦)
110		elni2 10288	. . . . . . . . . . 11 ⊢ (𝑦 ∈ N ↔ (𝑦 ∈ ω ∧ ∅ ∈ 𝑦))
111		indpi.6	. . . . . . . . . . 11 ⊢ (𝑦 ∈ N → (𝜒 → 𝜃))
112	110, 111	sylbir 238	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ω ∧ ∅ ∈ 𝑦) → (𝜒 → 𝜃))
113	109, 112	sylan2 595	. . . . . . . . 9 ⊢ ((𝑦 ∈ ω ∧ 1o ⊆ 𝑦) → (𝜒 → 𝜃))
114	104, 113	syl9r 78	. . . . . . . 8 ⊢ ((𝑦 ∈ ω ∧ 1o ⊆ 𝑦) → (((𝑦 ∈ N ∧ 1o <N 𝑦) → 𝜒) → ((𝑦 ∈ N ∧ 1o <N suc 𝑦) → 𝜃)))
115	114	adantlr 714	. . . . . . 7 ⊢ (((𝑦 ∈ ω ∧ 1o ∈ ω) ∧ 1o ⊆ 𝑦) → (((𝑦 ∈ N ∧ 1o <N 𝑦) → 𝜒) → ((𝑦 ∈ N ∧ 1o <N suc 𝑦) → 𝜃)))
116	24, 29, 81, 85, 86, 115	findsg 7590	. . . . . 6 ⊢ (((𝐴 ∈ ω ∧ 1o ∈ ω) ∧ 1o ⊆ 𝐴) → ((𝐴 ∈ N ∧ 1o <N 𝐴) → 𝜏))
117	20, 116	mpanl2 700	. . . . 5 ⊢ ((𝐴 ∈ ω ∧ 1o ⊆ 𝐴) → ((𝐴 ∈ N ∧ 1o <N 𝐴) → 𝜏))
118	10, 19, 117	syl2anc 587	. . . 4 ⊢ (𝐴 ∈ N → ((𝐴 ∈ N ∧ 1o <N 𝐴) → 𝜏))
119	118	expd 419	. . 3 ⊢ (𝐴 ∈ N → (𝐴 ∈ N → (1o <N 𝐴 → 𝜏)))
120	119	pm2.43i 52	. 2 ⊢ (𝐴 ∈ N → (1o <N 𝐴 → 𝜏))
121		nlt1pi 10317	. . . 4 ⊢ ¬ 𝐴 <N 1o
122		ltsopi 10299	. . . . . 6 ⊢ <N Or N
123		sotric 5465	. . . . . 6 ⊢ (( <N Or N ∧ (𝐴 ∈ N ∧ 1o ∈ N)) → (𝐴 <N 1o ↔ ¬ (𝐴 = 1o ∨ 1o <N 𝐴)))
124	122, 123	mpan 689	. . . . 5 ⊢ ((𝐴 ∈ N ∧ 1o ∈ N) → (𝐴 <N 1o ↔ ¬ (𝐴 = 1o ∨ 1o <N 𝐴)))
125	36, 124	mpan2 690	. . . 4 ⊢ (𝐴 ∈ N → (𝐴 <N 1o ↔ ¬ (𝐴 = 1o ∨ 1o <N 𝐴)))
126	121, 125	mtbii 329	. . 3 ⊢ (𝐴 ∈ N → ¬ ¬ (𝐴 = 1o ∨ 1o <N 𝐴))
127	126	notnotrd 135	. 2 ⊢ (𝐴 ∈ N → (𝐴 = 1o ∨ 1o <N 𝐴))
128	9, 120, 127	mpjaod 857	1 ⊢ (𝐴 ∈ N → 𝜏)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 399   ∨ wo 844   = wceq 1538   ∈ wcel 2111   ≠ wne 2987  Vcvv 3441   ⊆ wss 3881  ∅c0 4243   class class class wbr 5030   Or wor 5437  Ord word 6158  Oncon0 6159  suc csuc 6161  (class class class)co 7135  ωcom 7560  1_oc1o 8078   +_o coa 8082  Ncnpi 10255   +_N cpli 10256   <_N clti 10258

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-ov 7138  df-oprab 7139  df-mpo 7140  df-om 7561  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-1o 8085  df-oadd 8089  df-ni 10283  df-pli 10284  df-lti 10286

This theorem is referenced by:  prlem934  10444