Theorem indpi 10910

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 8472	. . . . . 6 ⊢ 1o ∈ V
2	1	eqvinc 3611	. . . . 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 3499	. . . 4 ⊢ (1o = 𝐴 → 𝜏)
8	7	eqcoms 2774	. . 3 ⊢ (𝐴 = 1o → 𝜏)
9	8	a1i 11	. 2 ⊢ (𝐴 ∈ N → (𝐴 = 1o → 𝜏))
10		pinn 10881	. . . . 5 ⊢ (𝐴 ∈ N → 𝐴 ∈ ω)
11		elni2 10880	. . . . . 6 ⊢ (𝐴 ∈ N ↔ (𝐴 ∈ ω ∧ ∅ ∈ 𝐴))
12		nnord 7879	. . . . . . . . 9 ⊢ (𝐴 ∈ ω → Ord 𝐴)
13		ordsucss 7823	. . . . . . . . 9 ⊢ (Ord 𝐴 → (∅ ∈ 𝐴 → suc ∅ ⊆ 𝐴))
14	12, 13	syl 18	. . . . . . . 8 ⊢ (𝐴 ∈ ω → (∅ ∈ 𝐴 → suc ∅ ⊆ 𝐴))
15		df-1o 8462	. . . . . . . . 9 ⊢ 1o = suc ∅
16	15	sseq1i 3968	. . . . . . . 8 ⊢ (1o ⊆ 𝐴 ↔ suc ∅ ⊆ 𝐴)
17	14, 16	imbitrrdi 255	. . . . . . 7 ⊢ (𝐴 ∈ ω → (∅ ∈ 𝐴 → 1o ⊆ 𝐴))
18	17	imp 412	. . . . . 6 ⊢ ((𝐴 ∈ ω ∧ ∅ ∈ 𝐴) → 1o ⊆ 𝐴)
19	11, 18	sylbi 220	. . . . 5 ⊢ (𝐴 ∈ N → 1o ⊆ 𝐴)
20		1onn 8635	. . . . . 6 ⊢ 1o ∈ ω
21		eleq1 2854	. . . . . . . . 9 ⊢ (𝑥 = 1o → (𝑥 ∈ N ↔ 1o ∈ N))
22		breq2 5118	. . . . . . . . 9 ⊢ (𝑥 = 1o → (1o <N 𝑥 ↔ 1o <N 1o))
23	21, 22	anbi12d 644	. . . . . . . 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 2854	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (𝑥 ∈ N ↔ 𝑦 ∈ N))
26		breq2 5118	. . . . . . . . 9 ⊢ (𝑥 = 𝑦 → (1o <N 𝑥 ↔ 1o <N 𝑦))
27	25, 26	anbi12d 644	. . . . . . . 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 10881	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ N → 𝑥 ∈ ω)
31		eleq1 2854	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = suc 𝑦 → (𝑥 ∈ ω ↔ suc 𝑦 ∈ ω))
32		peano2b 7888	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ω ↔ suc 𝑦 ∈ ω)
33	31, 32	bitr4di 292	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = suc 𝑦 → (𝑥 ∈ ω ↔ 𝑦 ∈ ω))
34	30, 33	imbitrid 247	. . . . . . . . . . . . . 14 ⊢ (𝑥 = suc 𝑦 → (𝑥 ∈ N → 𝑦 ∈ ω))
35	34	adantrd 497	. . . . . . . . . . . . 13 ⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ N ∧ 1o <N 𝑥) → 𝑦 ∈ ω))
36		1pi 10886	. . . . . . . . . . . . . . . 16 ⊢ 1o ∈ N
37		ltpiord 10890	. . . . . . . . . . . . . . . 16 ⊢ ((1o ∈ N ∧ 𝑥 ∈ N) → (1o <N 𝑥 ↔ 1o ∈ 𝑥))
38	36, 37	mpan 703	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ N → (1o <N 𝑥 ↔ 1o ∈ 𝑥))
39	38	biimpa 482	. . . . . . . . . . . . . 14 ⊢ ((𝑥 ∈ N ∧ 1o <N 𝑥) → 1o ∈ 𝑥)
40		eleq2 2855	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = suc 𝑦 → (1o ∈ 𝑥 ↔ 1o ∈ suc 𝑦))
41		elsuci 6437	. . . . . . . . . . . . . . . 16 ⊢ (1o ∈ suc 𝑦 → (1o ∈ 𝑦 ∨ 1o = 𝑦))
42		ne0i 4297	. . . . . . . . . . . . . . . . 17 ⊢ (1o ∈ 𝑦 → 𝑦 ≠ ∅)
43		0lt1o 8498	. . . . . . . . . . . . . . . . . . 19 ⊢ ∅ ∈ 1o
44		eleq2 2855	. . . . . . . . . . . . . . . . . . 19 ⊢ (1o = 𝑦 → (∅ ∈ 1o ↔ ∅ ∈ 𝑦))
45	43, 44	mpbii 236	. . . . . . . . . . . . . . . . . 18 ⊢ (1o = 𝑦 → ∅ ∈ 𝑦)
46	45	ne0d 4298	. . . . . . . . . . . . . . . . 17 ⊢ (1o = 𝑦 → 𝑦 ≠ ∅)
47	42, 46	jaoi 871	. . . . . . . . . . . . . . . 16 ⊢ ((1o ∈ 𝑦 ∨ 1o = 𝑦) → 𝑦 ≠ ∅)
48	41, 47	syl 18	. . . . . . . . . . . . . . 15 ⊢ (1o ∈ suc 𝑦 → 𝑦 ≠ ∅)
49	40, 48	biimtrdi 256	. . . . . . . . . . . . . 14 ⊢ (𝑥 = suc 𝑦 → (1o ∈ 𝑥 → 𝑦 ≠ ∅))
50	39, 49	syl5 35	. . . . . . . . . . . . 13 ⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ N ∧ 1o <N 𝑥) → 𝑦 ≠ ∅))
51	35, 50	jcad 522	. . . . . . . . . . . 12 ⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ N ∧ 1o <N 𝑥) → (𝑦 ∈ ω ∧ 𝑦 ≠ ∅)))
52		elni 10879	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ N ↔ (𝑦 ∈ ω ∧ 𝑦 ≠ ∅))
53	51, 52	imbitrrdi 255	. . . . . . . . . . 11 ⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ N ∧ 1o <N 𝑥) → 𝑦 ∈ N))
54		simpr 490	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ N ∧ 1o <N 𝑥) → 1o <N 𝑥)
55		breq2 5118	. . . . . . . . . . . 12 ⊢ (𝑥 = suc 𝑦 → (1o <N 𝑥 ↔ 1o <N suc 𝑦))
56	54, 55	imbitrid 247	. . . . . . . . . . 11 ⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ N ∧ 1o <N 𝑥) → 1o <N suc 𝑦))
57	53, 56	jcad 522	. . . . . . . . . 10 ⊢ (𝑥 = suc 𝑦 → ((𝑥 ∈ N ∧ 1o <N 𝑥) → (𝑦 ∈ N ∧ 1o <N suc 𝑦)))
58		addclpi 10895	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ N ∧ 1o ∈ N) → (𝑦 +N 1o) ∈ N)
59	36, 58	mpan2 704	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ N → (𝑦 +N 1o) ∈ N)
60		addpiord 10887	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑦 ∈ N ∧ 1o ∈ N) → (𝑦 +N 1o) = (𝑦 +o 1o))
61	36, 60	mpan2 704	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ N → (𝑦 +N 1o) = (𝑦 +o 1o))
62		pion 10882	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ N → 𝑦 ∈ On)
63		oa1suc 8525	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦 ∈ On → (𝑦 +o 1o) = suc 𝑦)
64	62, 63	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦 ∈ N → (𝑦 +o 1o) = suc 𝑦)
65	61, 64	eqtrd 2801	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦 ∈ N → (𝑦 +N 1o) = suc 𝑦)
66	65	eqeq2d 2777	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ N → (𝑥 = (𝑦 +N 1o) ↔ 𝑥 = suc 𝑦))
67	66	biimparc 485	. . . . . . . . . . . . . . 15 ⊢ ((𝑥 = suc 𝑦 ∧ 𝑦 ∈ N) → 𝑥 = (𝑦 +N 1o))
68	67	eleq1d 2851	. . . . . . . . . . . . . 14 ⊢ ((𝑥 = suc 𝑦 ∧ 𝑦 ∈ N) → (𝑥 ∈ N ↔ (𝑦 +N 1o) ∈ N))
69	59, 68	imbitrrid 249	. . . . . . . . . . . . 13 ⊢ ((𝑥 = suc 𝑦 ∧ 𝑦 ∈ N) → (𝑦 ∈ N → 𝑥 ∈ N))
70	69	ex 418	. . . . . . . . . . . 12 ⊢ (𝑥 = suc 𝑦 → (𝑦 ∈ N → (𝑦 ∈ N → 𝑥 ∈ N)))
71	70	pm2.43d 54	. . . . . . . . . . 11 ⊢ (𝑥 = suc 𝑦 → (𝑦 ∈ N → 𝑥 ∈ N))
72	55	biimprd 251	. . . . . . . . . . 11 ⊢ (𝑥 = suc 𝑦 → (1o <N suc 𝑦 → 1o <N 𝑥))
73	71, 72	anim12d 621	. . . . . . . . . 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 344	. . . . . . . 8 ⊢ (𝑥 = suc 𝑦 → (((𝑥 ∈ N ∧ 1o <N 𝑥) → 𝜑) ↔ ((𝑦 ∈ N ∧ 1o <N suc 𝑦) → 𝜑)))
76		indpi.3	. . . . . . . . . . . 12 ⊢ (𝑥 = (𝑦 +N 1o) → (𝜑 ↔ 𝜃))
77	66, 76	biimtrrdi 257	. . . . . . . . . . 11 ⊢ (𝑦 ∈ N → (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃)))
78	77	adantr 486	. . . . . . . . . 10 ⊢ ((𝑦 ∈ N ∧ 1o <N suc 𝑦) → (𝑥 = suc 𝑦 → (𝜑 ↔ 𝜃)))
79	78	com12 33	. . . . . . . . 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 2854	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → (𝑥 ∈ N ↔ 𝐴 ∈ N))
83		breq2 5118	. . . . . . . . 9 ⊢ (𝑥 = 𝐴 → (1o <N 𝑥 ↔ 1o <N 𝐴))
84	82, 83	anbi12d 644	. . . . . . . 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 10890	. . . . . . . . . . . . . . 15 ⊢ ((1o ∈ N ∧ 𝑦 ∈ N) → (1o <N 𝑦 ↔ 1o ∈ 𝑦))
88	36, 87	mpan 703	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ N → (1o <N 𝑦 ↔ 1o ∈ 𝑦))
89	88	pm5.32i 585	. . . . . . . . . . . . 13 ⊢ ((𝑦 ∈ N ∧ 1o <N 𝑦) ↔ (𝑦 ∈ N ∧ 1o ∈ 𝑦))
90	89	simplbi2 506	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ N → (1o ∈ 𝑦 → (𝑦 ∈ N ∧ 1o <N 𝑦)))
91	90	imim1d 83	. . . . . . . . . . 11 ⊢ (𝑦 ∈ N → (((𝑦 ∈ N ∧ 1o <N 𝑦) → 𝜒) → (1o ∈ 𝑦 → 𝜒)))
92		ltrelpi 10892	. . . . . . . . . . . . . . 15 ⊢ <N ⊆ (N × N)
93	92	brel 5731	. . . . . . . . . . . . . 14 ⊢ (1o <N suc 𝑦 → (1o ∈ N ∧ suc 𝑦 ∈ N))
94		ltpiord 10890	. . . . . . . . . . . . . 14 ⊢ ((1o ∈ N ∧ suc 𝑦 ∈ N) → (1o <N suc 𝑦 ↔ 1o ∈ suc 𝑦))
95	93, 94	syl 18	. . . . . . . . . . . . 13 ⊢ (1o <N suc 𝑦 → (1o <N suc 𝑦 ↔ 1o ∈ suc 𝑦))
96	95	ibi 270	. . . . . . . . . . . 12 ⊢ (1o <N suc 𝑦 → 1o ∈ suc 𝑦)
97	1	eqvinc 3611	. . . . . . . . . . . . . . 15 ⊢ (1o = 𝑦 ↔ ∃𝑥(𝑥 = 1o ∧ 𝑥 = 𝑦))
98	97, 28, 6	gencl 3499	. . . . . . . . . . . . . 14 ⊢ (1o = 𝑦 → 𝜒)
99		jao 975	. . . . . . . . . . . . . 14 ⊢ ((1o ∈ 𝑦 → 𝜒) → ((1o = 𝑦 → 𝜒) → ((1o ∈ 𝑦 ∨ 1o = 𝑦) → 𝜒)))
100	98, 99	mpi 21	. . . . . . . . . . . . 13 ⊢ ((1o ∈ 𝑦 → 𝜒) → ((1o ∈ 𝑦 ∨ 1o = 𝑦) → 𝜒))
101	41, 100	syl5 35	. . . . . . . . . . . 12 ⊢ ((1o ∈ 𝑦 → 𝜒) → (1o ∈ suc 𝑦 → 𝜒))
102	96, 101	syl5 35	. . . . . . . . . . 11 ⊢ ((1o ∈ 𝑦 → 𝜒) → (1o <N suc 𝑦 → 𝜒))
103	91, 102	syl6com 38	. . . . . . . . . 10 ⊢ (((𝑦 ∈ N ∧ 1o <N 𝑦) → 𝜒) → (𝑦 ∈ N → (1o <N suc 𝑦 → 𝜒)))
104	103	impd 416	. . . . . . . . 9 ⊢ (((𝑦 ∈ N ∧ 1o <N 𝑦) → 𝜒) → ((𝑦 ∈ N ∧ 1o <N suc 𝑦) → 𝜒))
105	15	sseq1i 3968	. . . . . . . . . . 11 ⊢ (1o ⊆ 𝑦 ↔ suc ∅ ⊆ 𝑦)
106		0ex 5275	. . . . . . . . . . . 12 ⊢ ∅ ∈ V
107		sucssel 6465	. . . . . . . . . . . 12 ⊢ (∅ ∈ V → (suc ∅ ⊆ 𝑦 → ∅ ∈ 𝑦))
108	106, 107	ax-mp 5	. . . . . . . . . . 11 ⊢ (suc ∅ ⊆ 𝑦 → ∅ ∈ 𝑦)
109	105, 108	sylbi 220	. . . . . . . . . 10 ⊢ (1o ⊆ 𝑦 → ∅ ∈ 𝑦)
110		elni2 10880	. . . . . . . . . . 11 ⊢ (𝑦 ∈ N ↔ (𝑦 ∈ ω ∧ ∅ ∈ 𝑦))
111		indpi.6	. . . . . . . . . . 11 ⊢ (𝑦 ∈ N → (𝜒 → 𝜃))
112	110, 111	sylbir 238	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ω ∧ ∅ ∈ 𝑦) → (𝜒 → 𝜃))
113	109, 112	sylan2 605	. . . . . . . . 9 ⊢ ((𝑦 ∈ ω ∧ 1o ⊆ 𝑦) → (𝜒 → 𝜃))
114	104, 113	syl9r 79	. . . . . . . 8 ⊢ ((𝑦 ∈ ω ∧ 1o ⊆ 𝑦) → (((𝑦 ∈ N ∧ 1o <N 𝑦) → 𝜒) → ((𝑦 ∈ N ∧ 1o <N suc 𝑦) → 𝜃)))
115	114	adantlr 728	. . . . . . 7 ⊢ (((𝑦 ∈ ω ∧ 1o ∈ ω) ∧ 1o ⊆ 𝑦) → (((𝑦 ∈ N ∧ 1o <N 𝑦) → 𝜒) → ((𝑦 ∈ N ∧ 1o <N suc 𝑦) → 𝜃)))
116	24, 29, 81, 85, 86, 115	findsg 7903	. . . . . 6 ⊢ (((𝐴 ∈ ω ∧ 1o ∈ ω) ∧ 1o ⊆ 𝐴) → ((𝐴 ∈ N ∧ 1o <N 𝐴) → 𝜏))
117	20, 116	mpanl2 714	. . . . 5 ⊢ ((𝐴 ∈ ω ∧ 1o ⊆ 𝐴) → ((𝐴 ∈ N ∧ 1o <N 𝐴) → 𝜏))
118	10, 19, 117	syl2anc 596	. . . 4 ⊢ (𝐴 ∈ N → ((𝐴 ∈ N ∧ 1o <N 𝐴) → 𝜏))
119	118	expd 421	. . 3 ⊢ (𝐴 ∈ N → (𝐴 ∈ N → (1o <N 𝐴 → 𝜏)))
120	119	pm2.43i 53	. 2 ⊢ (𝐴 ∈ N → (1o <N 𝐴 → 𝜏))
121		nlt1pi 10909	. . . 4 ⊢ ¬ 𝐴 <N 1o
122		ltsopi 10891	. . . . . 6 ⊢ <N Or N
123		sotric 5604	. . . . . 6 ⊢ (( <N Or N ∧ (𝐴 ∈ N ∧ 1o ∈ N)) → (𝐴 <N 1o ↔ ¬ (𝐴 = 1o ∨ 1o <N 𝐴)))
124	122, 123	mpan 703	. . . . 5 ⊢ ((𝐴 ∈ N ∧ 1o ∈ N) → (𝐴 <N 1o ↔ ¬ (𝐴 = 1o ∨ 1o <N 𝐴)))
125	36, 124	mpan2 704	. . . 4 ⊢ (𝐴 ∈ N → (𝐴 <N 1o ↔ ¬ (𝐴 = 1o ∨ 1o <N 𝐴)))
126	121, 125	mtbii 329	. . 3 ⊢ (𝐴 ∈ N → ¬ ¬ (𝐴 = 1o ∨ 1o <N 𝐴))
127	126	notnotrd 134	. 2 ⊢ (𝐴 ∈ N → (𝐴 = 1o ∨ 1o <N 𝐴))
128	9, 120, 127	mpjaod 874	1 ⊢ (𝐴 ∈ N → 𝜏)

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∨ wo 861   = wceq 1570   ∈ wcel 2146   ≠ wne 2961  Vcvv 3458   ⊆ wss 3908  ∅c0 4289   class class class wbr 5114   Or wor 5573  Ord word 6366  Oncon0 6367  suc csuc 6369  (class class class)co 7423  ωcom 7871  1_oc1o 8455   +_o coa 8459  Ncnpi 10847   +_N cpli 10848   <_N clti 10850

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pr 5409  ax-un 7745

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-ral 3083  df-rex 3093  df-reu 3373  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3928  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-iun 4963  df-br 5115  df-opab 5179  df-mpt 5198  df-tr 5224  df-id 5561  df-eprel 5566  df-po 5574  df-so 5575  df-fr 5619  df-we 5621  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6309  df-ord 6370  df-on 6371  df-lim 6372  df-suc 6373  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7426  df-oprab 7427  df-mpo 7428  df-om 7872  df-2nd 7996  df-frecs 8287  df-wrecs 8318  df-recs 8367  df-rdg 8406  df-1o 8462  df-oadd 8466  df-ni 10875  df-pli 10876  df-lti 10878

This theorem is used by:  prlem934  11036