Theorem indpi 10921

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 8490	. . . . . 6 ⊢ 1o ∈ V
2	1	eqvinc 3628	. . . . 5 ⊢ (1o = 𝐴 ↔ ∃𝑥(𝑥 = 1o ∧ 𝑥 = 𝐴))
3		indpi.4	. . . . 5 ⊢ (𝑥 = 𝐴 → (𝜑 ↔ 𝜏))
4		indpi.5	. . . . . 6 ⊢ 𝜓
5		indpi.1	. . . . . 6 ⊢ (𝑥 = 1o → (𝜑 ↔ 𝜓))
6	4, 5	mpbiri 258	. . . . 5 ⊢ (𝑥 = 1o → 𝜑)
7	2, 3, 6	gencl 3502	. . . 4 ⊢ (1o = 𝐴 → 𝜏)
8	7	eqcoms 2743	. . 3 ⊢ (𝐴 = 1o → 𝜏)
9	8	a1i 11	. 2 ⊢ (𝐴 ∈ N → (𝐴 = 1o → 𝜏))
10		pinn 10892	. . . . 5 ⊢ (𝐴 ∈ N → 𝐴 ∈ ω)
11		elni2 10891	. . . . . 6 ⊢ (𝐴 ∈ N ↔ (𝐴 ∈ ω ∧ ∅ ∈ 𝐴))
12		nnord 7869	. . . . . . . . 9 ⊢ (𝐴 ∈ ω → Ord 𝐴)
13		ordsucss 7812	. . . . . . . . 9 ⊢ (Ord 𝐴 → (∅ ∈ 𝐴 → suc ∅ ⊆ 𝐴))
14	12, 13	syl 17	. . . . . . . 8 ⊢ (𝐴 ∈ ω → (∅ ∈ 𝐴 → suc ∅ ⊆ 𝐴))
15		df-1o 8480	. . . . . . . . 9 ⊢ 1o = suc ∅
16	15	sseq1i 3987	. . . . . . . 8 ⊢ (1o ⊆ 𝐴 ↔ suc ∅ ⊆ 𝐴)
17	14, 16	imbitrrdi 252	. . . . . . 7 ⊢ (𝐴 ∈ ω → (∅ ∈ 𝐴 → 1o ⊆ 𝐴))
18	17	imp 406	. . . . . 6 ⊢ ((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) → 1o ⊆ 𝐴)
19	11, 18	sylbi 217	. . . . 5 ⊢ (𝐴 ∈ N → 1o ⊆ 𝐴)
20		1onn 8652	. . . . . 6 ⊢ 1o ∈ ω
21		eleq1 2822	. . . . . . . . 9 ⊢ (𝑥 = 1o → (𝑥 ∈ N ↔ 1o ∈ N))
22		breq2 5123	. . . . . . . . 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 344	. . . . . . 7 ⊢ (𝑥 = 1o → (((𝑥 ∈ N ∧ 1o <N 𝑥) → 𝜑) ↔ ((1o ∈ N ∧ 1o <N 1o) → 𝜓)))
25		eleq1 2822	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ N ↔ 𝑦 ∈ N))
26		breq2 5123	. . . . . . . . 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 344	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (((𝑥 ∈ N ∧ 1o <N 𝑥) → 𝜑) ↔ ((𝑦 ∈ N ∧ 1o <N 𝑦) → 𝜒)))
30		pinn 10892	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ N → 𝑥 ∈ ω)
31		eleq1 2822	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = suc 𝑦 → (𝑥 ∈ ω ↔ suc 𝑦 ∈ ω))
32		peano2b 7878	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ω ↔ suc 𝑦 ∈ ω)
33	31, 32	bitr4di 289	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = suc 𝑦 → (𝑥 ∈ ω ↔ 𝑦 ∈ ω))
34	30, 33	imbitrid 244	. . . . . . . . . . . . . 14 ⊢ (𝑥 = suc 𝑦 → (𝑥 ∈ N → 𝑦 ∈ ω))
35	34	adantrd 491	. . . . . . . . . . . . 13 ⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ N ∧ 1o <N 𝑥) → 𝑦 ∈ ω))
36		1pi 10897	. . . . . . . . . . . . . . . 16 ⊢ 1o ∈ N
37		ltpiord 10901	. . . . . . . . . . . . . . . 16 ⊢ ((1o ∈ N ∧ 𝑥 ∈ N) → (1o <N 𝑥 ↔ 1o ∈ 𝑥))
38	36, 37	mpan 690	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ N → (1o <N 𝑥 ↔ 1o ∈ 𝑥))
39	38	biimpa 476	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ N ∧ 1o <N 𝑥) → 1o ∈ 𝑥)
40		eleq2 2823	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = suc 𝑦 → (1o ∈ 𝑥 ↔ 1o ∈ suc 𝑦))
41		elsuci 6421	. . . . . . . . . . . . . . . 16 ⊢ (1o ∈ suc 𝑦 → (1o ∈ 𝑦 ∨ 1o = 𝑦))
42		ne0i 4316	. . . . . . . . . . . . . . . . 17 ⊢ (1o ∈ 𝑦 → 𝑦 ≠ ∅)
43		0lt1o 8516	. . . . . . . . . . . . . . . . . . 19 ⊢ ∅ ∈ 1o
44		eleq2 2823	. . . . . . . . . . . . . . . . . . 19 ⊢ (1o = 𝑦 → (∅ ∈ 1o ↔ ∅ ∈ 𝑦))
45	43, 44	mpbii 233	. . . . . . . . . . . . . . . . . 18 ⊢ (1o = 𝑦 → ∅ ∈ 𝑦)
46	45	ne0d 4317	. . . . . . . . . . . . . . . . 17 ⊢ (1o = 𝑦 → 𝑦 ≠ ∅)
47	42, 46	jaoi 857	. . . . . . . . . . . . . . . 16 ⊢ ((1o ∈ 𝑦 ∨ 1o = 𝑦) → 𝑦 ≠ ∅)
48	41, 47	syl 17	. . . . . . . . . . . . . . 15 ⊢ (1o ∈ suc 𝑦 → 𝑦 ≠ ∅)
49	40, 48	biimtrdi 253	. . . . . . . . . . . . . 14 ⊢ (𝑥 = suc 𝑦 → (1o ∈ 𝑥 → 𝑦 ≠ ∅))
50	39, 49	syl5 34	. . . . . . . . . . . . 13 ⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ N ∧ 1o <N 𝑥) → 𝑦 ≠ ∅))
51	35, 50	jcad 512	. . . . . . . . . . . 12 ⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ N ∧ 1o <N 𝑥) → (𝑦 ∈ ω ∧ 𝑦 ≠ ∅)))
52		elni 10890	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ N ↔ (𝑦 ∈ ω ∧ 𝑦 ≠ ∅))
53	51, 52	imbitrrdi 252	. . . . . . . . . . 11 ⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ N ∧ 1o <N 𝑥) → 𝑦 ∈ N))
54		simpr 484	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ N ∧ 1o <N 𝑥) → 1o <N 𝑥)
55		breq2 5123	. . . . . . . . . . . 12 ⊢ (𝑥 = suc 𝑦 → (1o <N 𝑥 ↔ 1o <N suc 𝑦))
56	54, 55	imbitrid 244	. . . . . . . . . . 11 ⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ N ∧ 1o <N 𝑥) → 1o <N suc 𝑦))
57	53, 56	jcad 512	. . . . . . . . . 10 ⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ N ∧ 1o <N 𝑥) → (𝑦 ∈ N ∧ 1o <N suc 𝑦)))
58		addclpi 10906	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ N ∧ 1o ∈ N) → (𝑦 +N 1o) ∈ N)
59	36, 58	mpan2 691	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ N → (𝑦 +N 1o) ∈ N)
60		addpiord 10898	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ N ∧ 1o ∈ N) → (𝑦 +N 1o) = (𝑦 +o 1o))
61	36, 60	mpan2 691	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ N → (𝑦 +N 1o) = (𝑦 +o 1o))
62		pion 10893	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ N → 𝑦 ∈ On)
63		oa1suc 8543	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ On → (𝑦 +o 1o) = suc 𝑦)
64	62, 63	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ N → (𝑦 +o 1o) = suc 𝑦)
65	61, 64	eqtrd 2770	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ N → (𝑦 +N 1o) = suc 𝑦)
66	65	eqeq2d 2746	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ N → (𝑥 = (𝑦 +N 1o) ↔ 𝑥 = suc 𝑦))
67	66	biimparc 479	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = suc 𝑦 ∧ 𝑦 ∈ N) → 𝑥 = (𝑦 +N 1o))
68	67	eleq1d 2819	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = suc 𝑦 ∧ 𝑦 ∈ N) → (𝑥 ∈ N ↔ (𝑦 +N 1o) ∈ N))
69	59, 68	imbitrrid 246	. . . . . . . . . . . . 13 ⊢ ((𝑥 = suc 𝑦 ∧ 𝑦 ∈ N) → (𝑦 ∈ N → 𝑥 ∈ N))
70	69	ex 412	. . . . . . . . . . . 12 ⊢ (𝑥 = suc 𝑦 → (𝑦 ∈ N → (𝑦 ∈ N → 𝑥 ∈ N)))
71	70	pm2.43d 53	. . . . . . . . . . 11 ⊢ (𝑥 = suc 𝑦 → (𝑦 ∈ N → 𝑥 ∈ N))
72	55	biimprd 248	. . . . . . . . . . 11 ⊢ (𝑥 = suc 𝑦 → (1o <N suc 𝑦 → 1o <N 𝑥))
73	71, 72	anim12d 609	. . . . . . . . . 10 ⊢ (𝑥 = suc 𝑦 → ((𝑦 ∈ N ∧ 1o <N suc 𝑦) → (𝑥 ∈ N ∧ 1o <N 𝑥)))
74	57, 73	impbid 212	. . . . . . . . 9 ⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ N ∧ 1o <N 𝑥) ↔ (𝑦 ∈ N ∧ 1o <N suc 𝑦)))
75	74	imbi1d 341	. . . . . . . 8 ⊢ (𝑥 = suc 𝑦 → (((𝑥 ∈ N ∧ 1o <N 𝑥) → 𝜑) ↔ ((𝑦 ∈ N ∧ 1o <N suc 𝑦) → 𝜑)))
76		indpi.3	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑦 +N 1o) → (𝜑 ↔ 𝜃))
77	66, 76	biimtrrdi 254	. . . . . . . . . . 11 ⊢ (𝑦 ∈ N → (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃)))
78	77	adantr 480	. . . . . . . . . 10 ⊢ ((𝑦 ∈ N ∧ 1o <N suc 𝑦) → (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃)))
79	78	com12 32	. . . . . . . . 9 ⊢ (𝑥 = suc 𝑦 → ((𝑦 ∈ N ∧ 1o <N suc 𝑦) → (𝜑 ↔ 𝜃)))
80	79	pm5.74d 273	. . . . . . . 8 ⊢ (𝑥 = suc 𝑦 → (((𝑦 ∈ N ∧ 1o <N suc 𝑦) → 𝜑) ↔ ((𝑦 ∈ N ∧ 1o <N suc 𝑦) → 𝜃)))
81	75, 80	bitrd 279	. . . . . . 7 ⊢ (𝑥 = suc 𝑦 → (((𝑥 ∈ N ∧ 1o <N 𝑥) → 𝜑) ↔ ((𝑦 ∈ N ∧ 1o <N suc 𝑦) → 𝜃)))
82		eleq1 2822	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ N ↔ 𝐴 ∈ N))
83		breq2 5123	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → (1o <N 𝑥 ↔ 1o <N 𝐴))
84	82, 83	anbi12d 632	. . . . . . . 8 ⊢ (𝑥 = 𝐴 → ((𝑥 ∈ N ∧ 1o <N 𝑥) ↔ (𝐴 ∈ N ∧ 1o <N 𝐴)))
85	84, 3	imbi12d 344	. . . . . . 7 ⊢ (𝑥 = 𝐴 → (((𝑥 ∈ N ∧ 1o <N 𝑥) → 𝜑) ↔ ((𝐴 ∈ N ∧ 1o <N 𝐴) → 𝜏)))
86	4	2a1i 12	. . . . . . 7 ⊢ (1o ∈ ω → ((1o ∈ N ∧ 1o <N 1o) → 𝜓))
87		ltpiord 10901	. . . . . . . . . . . . . . 15 ⊢ ((1o ∈ N ∧ 𝑦 ∈ N) → (1o <N 𝑦 ↔ 1o ∈ 𝑦))
88	36, 87	mpan 690	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ N → (1o <N 𝑦 ↔ 1o ∈ 𝑦))
89	88	pm5.32i 574	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ N ∧ 1o <N 𝑦) ↔ (𝑦 ∈ N ∧ 1o ∈ 𝑦))
90	89	simplbi2 500	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ N → (1o ∈ 𝑦 → (𝑦 ∈ N ∧ 1o <N 𝑦)))
91	90	imim1d 82	. . . . . . . . . . 11 ⊢ (𝑦 ∈ N → (((𝑦 ∈ N ∧ 1o <N 𝑦) → 𝜒) → (1o ∈ 𝑦 → 𝜒)))
92		ltrelpi 10903	. . . . . . . . . . . . . . 15 ⊢ <N ⊆ (N × N)
93	92	brel 5719	. . . . . . . . . . . . . 14 ⊢ (1o <N suc 𝑦 → (1o ∈ N ∧ suc 𝑦 ∈ N))
94		ltpiord 10901	. . . . . . . . . . . . . 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 267	. . . . . . . . . . . 12 ⊢ (1o <N suc 𝑦 → 1o ∈ suc 𝑦)
97	1	eqvinc 3628	. . . . . . . . . . . . . . 15 ⊢ (1o = 𝑦 ↔ ∃𝑥(𝑥 = 1o ∧ 𝑥 = 𝑦))
98	97, 28, 6	gencl 3502	. . . . . . . . . . . . . 14 ⊢ (1o = 𝑦 → 𝜒)
99		jao 962	. . . . . . . . . . . . . 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 410	. . . . . . . . 9 ⊢ (((𝑦 ∈ N ∧ 1o <N 𝑦) → 𝜒) → ((𝑦 ∈ N ∧ 1o <N suc 𝑦) → 𝜒))
105	15	sseq1i 3987	. . . . . . . . . . 11 ⊢ (1o ⊆ 𝑦 ↔ suc ∅ ⊆ 𝑦)
106		0ex 5277	. . . . . . . . . . . 12 ⊢ ∅ ∈ V
107		sucssel 6449	. . . . . . . . . . . 12 ⊢ (∅ ∈ V → (suc ∅ ⊆ 𝑦 → ∅ ∈ 𝑦))
108	106, 107	ax-mp 5	. . . . . . . . . . 11 ⊢ (suc ∅ ⊆ 𝑦 → ∅ ∈ 𝑦)
109	105, 108	sylbi 217	. . . . . . . . . 10 ⊢ (1o ⊆ 𝑦 → ∅ ∈ 𝑦)
110		elni2 10891	. . . . . . . . . . 11 ⊢ (𝑦 ∈ N ↔ (𝑦 ∈ ω ∧ ∅ ∈ 𝑦))
111		indpi.6	. . . . . . . . . . 11 ⊢ (𝑦 ∈ N → (𝜒 → 𝜃))
112	110, 111	sylbir 235	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ω ∧ ∅ ∈ 𝑦) → (𝜒 → 𝜃))
113	109, 112	sylan2 593	. . . . . . . . 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 7893	. . . . . 6 ⊢ (((𝐴 ∈ ω ∧ 1o ∈ ω) ∧ 1o ⊆ 𝐴) → ((𝐴 ∈ N ∧ 1o <N 𝐴) → 𝜏))
117	20, 116	mpanl2 701	. . . . 5 ⊢ ((𝐴 ∈ ω ∧ 1o ⊆ 𝐴) → ((𝐴 ∈ N ∧ 1o <N 𝐴) → 𝜏))
118	10, 19, 117	syl2anc 584	. . . 4 ⊢ (𝐴 ∈ N → ((𝐴 ∈ N ∧ 1o <N 𝐴) → 𝜏))
119	118	expd 415	. . 3 ⊢ (𝐴 ∈ N → (𝐴 ∈ N → (1o <N 𝐴 → 𝜏)))
120	119	pm2.43i 52	. 2 ⊢ (𝐴 ∈ N → (1o <N 𝐴 → 𝜏))
121		nlt1pi 10920	. . . 4 ⊢ ¬ 𝐴 <N 1o
122		ltsopi 10902	. . . . . 6 ⊢ <N Or N
123		sotric 5591	. . . . . 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 326	. . 3 ⊢ (𝐴 ∈ N → ¬ ¬ (𝐴 = 1o ∨ 1o <N 𝐴))
127	126	notnotrd 133	. 2 ⊢ (𝐴 ∈ N → (𝐴 = 1o ∨ 1o <N 𝐴))
128	9, 120, 127	mpjaod 860	1 ⊢ (𝐴 ∈ N → 𝜏)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   = wceq 1540   ∈ wcel 2108   ≠ wne 2932  Vcvv 3459   ⊆ wss 3926  ∅c0 4308   class class class wbr 5119   Or wor 5560  Ord word 6351  Oncon0 6352  suc csuc 6354  (class class class)co 7405  ωcom 7861  1_oc1o 8473   +_o coa 8477  Ncnpi 10858   +_N cpli 10859   <_N clti 10861

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402  ax-un 7729

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-reu 3360  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-pss 3946  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-tr 5230  df-id 5548  df-eprel 5553  df-po 5561  df-so 5562  df-fr 5606  df-we 5608  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-pred 6290  df-ord 6355  df-on 6356  df-lim 6357  df-suc 6358  df-iota 6484  df-fun 6533  df-fn 6534  df-f 6535  df-f1 6536  df-fo 6537  df-f1o 6538  df-fv 6539  df-ov 7408  df-oprab 7409  df-mpo 7410  df-om 7862  df-2nd 7989  df-frecs 8280  df-wrecs 8311  df-recs 8385  df-rdg 8424  df-1o 8480  df-oadd 8484  df-ni 10886  df-pli 10887  df-lti 10889

This theorem is referenced by:  prlem934  11047