Theorem acdc3lem 8754

Description: Lemma for acdc3 8755. Build a sequence G starting at value c, as follows. Given a previous value x of G, we construct, for the next value of G, the v such that A.u e. (F` x)-. urv, which is unique when r is a well-ordering on A.

Hypotheses

Ref	Expression
acdc3lem.1	|- A e. _V
acdc3lem.2	|- S = {<.<.x, y>., z>. | ((x e. A /\ y e. A) /\ z = U.{v e. (F` x) | A.u e. (F` x) -. urv})}
acdc3lem.3	|- G = (S seq1 (NN X. {c}))

Assertion

Ref	Expression
acdc3lem	|- ((r We A /\ (c e. A /\ F:A-->(~PA \ {(/)}))) -> (G:NN-->A /\ (G` 1) = c /\ A.k e. NN (G` (k + 1)) e. (F` (G` k))))

Distinct variable groups:   u,k,v,x,y,z,A   k,F,u,v,x,y,z   u,G,v,x,y,z   k,c,x,y,z   k,r,u,v,x,y,z

Proof of Theorem acdc3lem

Step	Hyp	Ref	Expression
1		fss 4571	. . . . . 6 |- (((NN X. {c}):NN-->{c} /\ {c} C_ A) -> (NN X. {c}):NN-->A)
2		visset 2295	. . . . . . 7 |- c e. _V
3	2	fconst 4602	. . . . . 6 |- (NN X. {c}):NN-->{c}
4		snssi 3129	. . . . . 6 |- (c e. A -> {c} C_ A)
5	1, 3, 4	sylancr 526	. . . . 5 |- (c e. A -> (NN X. {c}):NN-->A)
6	5	ad2antrl 442	. . . 4 |- ((r We A /\ (c e. A /\ F:A-->(~PA \ {(/)}))) -> (NN X. {c}):NN-->A)
7		fvex 4689	. . . . . . . . . . . . 13 |- (F` s) e. _V
8	7	rabex 3461	. . . . . . . . . . . 12 |- {v e. (F` s) | A.u e. (F` s) -. urv} e. _V
9	8	uniex 3794	. . . . . . . . . . 11 |- U.{v e. (F` s) | A.u e. (F` s) -. urv} e. _V
10		fveq2 4681	. . . . . . . . . . . . 13 |- (x = s -> (F` x) = (F` s))
11		rabeq 2289	. . . . . . . . . . . . . 14 |- ((F` x) = (F` s) -> {v e. (F` x) | A.u e. (F` x) -. urv} = {v e. (F` s) | A.u e. (F` x) -. urv})
12		raleq 2266	. . . . . . . . . . . . . . 15 |- ((F` x) = (F` s) -> (A.u e. (F` x) -. urv <-> A.u e. (F` s) -. urv))
13	12	rabbidv 2287	. . . . . . . . . . . . . 14 |- ((F` x) = (F` s) -> {v e. (F` s) | A.u e. (F` x) -. urv} = {v e. (F` s) | A.u e. (F` s) -. urv})
14	11, 13	eqtrd 1925	. . . . . . . . . . . . 13 |- ((F` x) = (F` s) -> {v e. (F` x) | A.u e. (F` x) -. urv} = {v e. (F` s) | A.u e. (F` s) -. urv})
15	10, 14	syl 12	. . . . . . . . . . . 12 |- (x = s -> {v e. (F` x) | A.u e. (F` x) -. urv} = {v e. (F` s) | A.u e. (F` s) -. urv})
16	15	unieqd 3188	. . . . . . . . . . 11 |- (x = s -> U.{v e. (F` x) | A.u e. (F` x) -. urv} = U.{v e. (F` s) | A.u e. (F` s) -. urv})
17		eqidd 1885	. . . . . . . . . . 11 |- (y = t -> U.{v e. (F` s) | A.u e. (F` s) -. urv} = U.{v e. (F` s) | A.u e. (F` s) -. urv})
18		acdc3lem.2	. . . . . . . . . . 11 |- S = {<.<.x, y>., z>. | ((x e. A /\ y e. A) /\ z = U.{v e. (F` x) | A.u e. (F` x) -. urv})}
19	9, 16, 17, 18	oprabval2 4957	. . . . . . . . . 10 |- ((s e. A /\ t e. A) -> (sSt) = U.{v e. (F` s) | A.u e. (F` s) -. urv})
20	19	adantl 424	. . . . . . . . 9 |- (((r We A /\ (c e. A /\ F:A-->(~PA \ {(/)}))) /\ (s e. A /\ t e. A)) -> (sSt) = U.{v e. (F` s) | A.u e. (F` s) -. urv})
21		ffvelrn 4787	. . . . . . . . . . . . . . 15 |- ((F:A-->(~PA \ {(/)}) /\ s e. A) -> (F` s) e. (~PA \ {(/)}))
22		eldifi 2730	. . . . . . . . . . . . . . 15 |- ((F` s) e. (~PA \ {(/)}) -> (F` s) e. ~PA)
23	21, 22	syl 12	. . . . . . . . . . . . . 14 |- ((F:A-->(~PA \ {(/)}) /\ s e. A) -> (F` s) e. ~PA)
24	23	adantll 428	. . . . . . . . . . . . 13 |- (((r We A /\ F:A-->(~PA \ {(/)})) /\ s e. A) -> (F` s) e. ~PA)
25		elpwi 3039	. . . . . . . . . . . . 13 |- ((F` s) e. ~PA -> (F` s) C_ A)
26	24, 25	syl 12	. . . . . . . . . . . 12 |- (((r We A /\ F:A-->(~PA \ {(/)})) /\ s e. A) -> (F` s) C_ A)
27		simpll 448	. . . . . . . . . . . . 13 |- (((r We A /\ F:A-->(~PA \ {(/)})) /\ s e. A) -> r We A)
28		eldifn 2731	. . . . . . . . . . . . . . . 16 |- ((F` s) e. (~PA \ {(/)}) -> -. (F` s) e. {(/)})
29		id 73	. . . . . . . . . . . . . . . . . 18 |- ((F` s) = (/) -> (F` s) = (/))
30		0ex 3446	. . . . . . . . . . . . . . . . . . 19 |- (/) e. _V
31	30	snid 3069	. . . . . . . . . . . . . . . . . 18 |- (/) e. {(/)}
32	29, 31	syl6eqel 1979	. . . . . . . . . . . . . . . . 17 |- ((F` s) = (/) -> (F` s) e. {(/)})
33	32	necon3bi 2045	. . . . . . . . . . . . . . . 16 |- (-. (F` s) e. {(/)} -> (F` s) =/= (/))
34	28, 33	syl 12	. . . . . . . . . . . . . . 15 |- ((F` s) e. (~PA \ {(/)}) -> (F` s) =/= (/))
35	21, 34	syl 12	. . . . . . . . . . . . . 14 |- ((F:A-->(~PA \ {(/)}) /\ s e. A) -> (F` s) =/= (/))
36	35	adantll 428	. . . . . . . . . . . . 13 |- (((r We A /\ F:A-->(~PA \ {(/)})) /\ s e. A) -> (F` s) =/= (/))
37	7	wereucl 3655	. . . . . . . . . . . . 13 |- ((r We A /\ (F` s) C_ A /\ (F` s) =/= (/)) -> U.{v e. (F` s) | A.u e. (F` s) -. urv} e. (F` s))
38	27, 26, 36, 37	syl111anc 1100	. . . . . . . . . . . 12 |- (((r We A /\ F:A-->(~PA \ {(/)})) /\ s e. A) -> U.{v e. (F` s) | A.u e. (F` s) -. urv} e. (F` s))
39	26, 38	sseldd 2620	. . . . . . . . . . 11 |- (((r We A /\ F:A-->(~PA \ {(/)})) /\ s e. A) -> U.{v e. (F` s) | A.u e. (F` s) -. urv} e. A)
40	39	adantlrl 434	. . . . . . . . . 10 |- (((r We A /\ (c e. A /\ F:A-->(~PA \ {(/)}))) /\ s e. A) -> U.{v e. (F` s) | A.u e. (F` s) -. urv} e. A)
41	40	adantrr 431	. . . . . . . . 9 |- (((r We A /\ (c e. A /\ F:A-->(~PA \ {(/)}))) /\ (s e. A /\ t e. A)) -> U.{v e. (F` s) | A.u e. (F` s) -. urv} e. A)
42	20, 41	eqeltrd 1971	. . . . . . . 8 |- (((r We A /\ (c e. A /\ F:A-->(~PA \ {(/)}))) /\ (s e. A /\ t e. A)) -> (sSt) e. A)
43	42	ex 402	. . . . . . 7 |- ((r We A /\ (c e. A /\ F:A-->(~PA \ {(/)}))) -> ((s e. A /\ t e. A) -> (sSt) e. A))
44	43	r19.21aivv 2183	. . . . . 6 |- ((r We A /\ (c e. A /\ F:A-->(~PA \ {(/)}))) -> A.s e. A A.t e. A (sSt) e. A)
45		fvex 4689	. . . . . . . . 9 |- (F` x) e. _V
46	45	rabex 3461	. . . . . . . 8 |- {v e. (F` x) | A.u e. (F` x) -. urv} e. _V
47	46	uniex 3794	. . . . . . 7 |- U.{v e. (F` x) | A.u e. (F` x) -. urv} e. _V
48	47, 18	fnoprab2 5064	. . . . . 6 |- S Fn (A X. A)
49	44, 48	jctil 316	. . . . 5 |- ((r We A /\ (c e. A /\ F:A-->(~PA \ {(/)}))) -> (S Fn (A X. A) /\ A.s e. A A.t e. A (sSt) e. A))
50		ffnoprv 4943	. . . . 5 |- (S:(A X. A)-->A <-> (S Fn (A X. A) /\ A.s e. A A.t e. A (sSt) e. A))
51	49, 50	sylibr 217	. . . 4 |- ((r We A /\ (c e. A /\ F:A-->(~PA \ {(/)}))) -> S:(A X. A)-->A)
52		acdc3lem.1	. . . . . 6 |- A e. _V
53	52, 52, 18	oprabex2 4950	. . . . 5 |- S e. _V
54		nnex 7116	. . . . . 6 |- NN e. _V
55		snex 3492	. . . . . 6 |- {c} e. _V
56	54, 55	xpex 4096	. . . . 5 |- (NN X. {c}) e. _V
57	53, 56	seq1f 7736	. . . 4 |- (((NN X. {c}):NN-->A /\ S:(A X. A)-->A) -> (S seq1 (NN X. {c})):NN-->A)
58	6, 51, 57	syl11anc 524	. . 3 |- ((r We A /\ (c e. A /\ F:A-->(~PA \ {(/)}))) -> (S seq1 (NN X. {c})):NN-->A)
59		acdc3lem.3	. . . 4 |- G = (S seq1 (NN X. {c}))
60	59	feq1i 4558	. . 3 |- (G:NN-->A <-> (S seq1 (NN X. {c})):NN-->A)
61	58, 60	sylibr 217	. 2 |- ((r We A /\ (c e. A /\ F:A-->(~PA \ {(/)}))) -> G:NN-->A)
62	59	fveq1i 4682	. . . 4 |- (G` 1) = ((S seq1 (NN X. {c}))` 1)
63	53, 56	seq11 7730	. . . . 5 |- ((S seq1 (NN X. {c}))` 1) = ((NN X. {c})` 1)
64		1nn 7117	. . . . . 6 |- 1 e. NN
65	2	fvconst2 4822	. . . . . 6 |- (1 e. NN -> ((NN X. {c})` 1) = c)
66	64, 65	ax-mp 7	. . . . 5 |- ((NN X. {c})` 1) = c
67	63, 66	eqtri 1908	. . . 4 |- ((S seq1 (NN X. {c}))` 1) = c
68	62, 67	eqtri 1908	. . 3 |- (G` 1) = c
69	68	a1i 8	. 2 |- ((r We A /\ (c e. A /\ F:A-->(~PA \ {(/)}))) -> (G` 1) = c)
70	53, 56	seq1p1 7731	. . . . . . 7 |- (k e. NN -> ((S seq1 (NN X. {c}))` (k + 1)) = (((S seq1 (NN X. {c}))` k)S((NN X. {c})` (k + 1))))
71	70	adantl 424	. . . . . 6 |- (((r We A /\ (c e. A /\ F:A-->(~PA \ {(/)}))) /\ k e. NN) -> ((S seq1 (NN X. {c}))` (k + 1)) = (((S seq1 (NN X. {c}))` k)S((NN X. {c})` (k + 1))))
72		peano2nn 7118	. . . . . . . . . . 11 |- (k e. NN -> (k + 1) e. NN)
73	2	fvconst2 4822	. . . . . . . . . . 11 |- ((k + 1) e. NN -> ((NN X. {c})` (k + 1)) = c)
74	72, 73	syl 12	. . . . . . . . . 10 |- (k e. NN -> ((NN X. {c})` (k + 1)) = c)
75	74	opreq2d 4898	. . . . . . . . 9 |- (k e. NN -> ((G` k)S((NN X. {c})` (k + 1))) = ((G` k)Sc))
76	75	adantl 424	. . . . . . . 8 |- (((r We A /\ (c e. A /\ F:A-->(~PA \ {(/)}))) /\ k e. NN) -> ((G` k)S((NN X. {c})` (k + 1))) = ((G` k)Sc))
77		simpr 350	. . . . . . . . . . 11 |- (((r We A /\ (c e. A /\ F:A-->(~PA \ {(/)}))) /\ k e. NN) -> k e. NN)
78	5	adantr 425	. . . . . . . . . . . 12 |- ((c e. A /\ F:A-->(~PA \ {(/)})) -> (NN X. {c}):NN-->A)
79	78	ad2antlr 441	. . . . . . . . . . 11 |- (((r We A /\ (c e. A /\ F:A-->(~PA \ {(/)}))) /\ k e. NN) -> (NN X. {c}):NN-->A)
80	51	adantr 425	. . . . . . . . . . 11 |- (((r We A /\ (c e. A /\ F:A-->(~PA \ {(/)}))) /\ k e. NN) -> S:(A X. A)-->A)
81	53, 56	seq1cl 7738	. . . . . . . . . . 11 |- ((k e. NN /\ (NN X. {c}):NN-->A /\ S:(A X. A)-->A) -> ((S seq1 (NN X. {c}))` k) e. A)
82	77, 79, 80, 81	syl111anc 1100	. . . . . . . . . 10 |- (((r We A /\ (c e. A /\ F:A-->(~PA \ {(/)}))) /\ k e. NN) -> ((S seq1 (NN X. {c}))` k) e. A)
83	59	fveq1i 4682	. . . . . . . . . 10 |- (G` k) = ((S seq1 (NN X. {c}))` k)
84	82, 83	syl5eqel 1975	. . . . . . . . 9 |- (((r We A /\ (c e. A /\ F:A-->(~PA \ {(/)}))) /\ k e. NN) -> (G` k) e. A)
85		simplrl 454	. . . . . . . . 9 |- (((r We A /\ (c e. A /\ F:A-->(~PA \ {(/)}))) /\ k e. NN) -> c e. A)
86		fvex 4689	. . . . . . . . . . . 12 |- (F` (G` k)) e. _V
87	86	rabex 3461	. . . . . . . . . . 11 |- {v e. (F` (G` k)) | A.u e. (F` (G` k)) -. urv} e. _V
88	87	uniex 3794	. . . . . . . . . 10 |- U.{v e. (F` (G` k)) | A.u e. (F` (G` k)) -. urv} e. _V
89		fveq2 4681	. . . . . . . . . . . 12 |- (x = (G` k) -> (F` x) = (F` (G` k)))
90		rabeq 2289	. . . . . . . . . . . . 13 |- ((F` x) = (F` (G` k)) -> {v e. (F` x) | A.u e. (F` x) -. urv} = {v e. (F` (G` k)) | A.u e. (F` x) -. urv})
91		raleq 2266	. . . . . . . . . . . . . 14 |- ((F` x) = (F` (G` k)) -> (A.u e. (F` x) -. urv <-> A.u e. (F` (G` k)) -. urv))
92	91	rabbidv 2287	. . . . . . . . . . . . 13 |- ((F` x) = (F` (G` k)) -> {v e. (F` (G` k)) | A.u e. (F` x) -. urv} = {v e. (F` (G` k)) | A.u e. (F` (G` k)) -. urv})
93	90, 92	eqtrd 1925	. . . . . . . . . . . 12 |- ((F` x) = (F` (G` k)) -> {v e. (F` x) | A.u e. (F` x) -. urv} = {v e. (F` (G` k)) | A.u e. (F` (G` k)) -. urv})
94	89, 93	syl 12	. . . . . . . . . . 11 |- (x = (G` k) -> {v e. (F` x) | A.u e. (F` x) -. urv} = {v e. (F` (G` k)) | A.u e. (F` (G` k)) -. urv})
95	94	unieqd 3188	. . . . . . . . . 10 |- (x = (G` k) -> U.{v e. (F` x) | A.u e. (F` x) -. urv} = U.{v e. (F` (G` k)) | A.u e. (F` (G` k)) -. urv})
96		eqidd 1885	. . . . . . . . . 10 |- (y = c -> U.{v e. (F` (G` k)) | A.u e. (F` (G` k)) -. urv} = U.{v e. (F` (G` k)) | A.u e. (F` (G` k)) -. urv})
97	88, 95, 96, 18	oprabval2 4957	. . . . . . . . 9 |- (((G` k) e. A /\ c e. A) -> ((G` k)Sc) = U.{v e. (F` (G` k)) | A.u e. (F` (G` k)) -. urv})
98	84, 85, 97	syl11anc 524	. . . . . . . 8 |- (((r We A /\ (c e. A /\ F:A-->(~PA \ {(/)}))) /\ k e. NN) -> ((G` k)Sc) = U.{v e. (F` (G` k)) | A.u e. (F` (G` k)) -. urv})
99	76, 98	eqtrd 1925	. . . . . . 7 |- (((r We A /\ (c e. A /\ F:A-->(~PA \ {(/)}))) /\ k e. NN) -> ((G` k)S((NN X. {c})` (k + 1))) = U.{v e. (F` (G` k)) | A.u e. (F` (G` k)) -. urv})
100	83	opreq1i 4892	. . . . . . 7 |- ((G` k)S((NN X. {c})` (k + 1))) = (((S seq1 (NN X. {c}))` k)S((NN X. {c})` (k + 1)))
101	99, 100	syl5eqr 1942	. . . . . 6 |- (((r We A /\ (c e. A /\ F:A-->(~PA \ {(/)}))) /\ k e. NN) -> (((S seq1 (NN X. {c}))` k)S((NN X. {c})` (k + 1))) = U.{v e. (F` (G` k)) | A.u e. (F` (G` k)) -. urv})
102	71, 101	eqtrd 1925	. . . . 5 |- (((r We A /\ (c e. A /\ F:A-->(~PA \ {(/)}))) /\ k e. NN) -> ((S seq1 (NN X. {c}))` (k + 1)) = U.{v e. (F` (G` k)) | A.u e. (F` (G` k)) -. urv})
103	59	fveq1i 4682	. . . . 5 |- (G` (k + 1)) = ((S seq1 (NN X. {c}))` (k + 1))
104	102, 103	syl5eq 1940	. . . 4 |- (((r We A /\ (c e. A /\ F:A-->(~PA \ {(/)}))) /\ k e. NN) -> (G` (k + 1)) = U.{v e. (F` (G` k)) | A.u e. (F` (G` k)) -. urv})
105		simpll 448	. . . . 5 |- (((r We A /\ (c e. A /\ F:A-->(~PA \ {(/)}))) /\ k e. NN) -> r We A)
106		simplrr 455	. . . . . . . 8 |- (((r We A /\ (c e. A /\ F:A-->(~PA \ {(/)}))) /\ k e. NN) -> F:A-->(~PA \ {(/)}))
107		ffvelrn 4787	. . . . . . . 8 |- ((F:A-->(~PA \ {(/)}) /\ (G` k) e. A) -> (F` (G` k)) e. (~PA \ {(/)}))
108	106, 84, 107	syl11anc 524	. . . . . . 7 |- (((r We A /\ (c e. A /\ F:A-->(~PA \ {(/)}))) /\ k e. NN) -> (F` (G` k)) e. (~PA \ {(/)}))
109		eldifi 2730	. . . . . . 7 |- ((F` (G` k)) e. (~PA \ {(/)}) -> (F` (G` k)) e. ~PA)
110	108, 109	syl 12	. . . . . 6 |- (((r We A /\ (c e. A /\ F:A-->(~PA \ {(/)}))) /\ k e. NN) -> (F` (G` k)) e. ~PA)
111		elpwi 3039	. . . . . 6 |- ((F` (G` k)) e. ~PA -> (F` (G` k)) C_ A)
112	110, 111	syl 12	. . . . 5 |- (((r We A /\ (c e. A /\ F:A-->(~PA \ {(/)}))) /\ k e. NN) -> (F` (G` k)) C_ A)
113		eldifn 2731	. . . . . . 7 |- ((F` (G` k)) e. (~PA \ {(/)}) -> -. (F` (G` k)) e. {(/)})
114		id 73	. . . . . . . . 9 |- ((F` (G` k)) = (/) -> (F` (G` k)) = (/))
115	114, 31	syl6eqel 1979	. . . . . . . 8 |- ((F` (G` k)) = (/) -> (F` (G` k)) e. {(/)})
116	115	necon3bi 2045	. . . . . . 7 |- (-. (F` (G` k)) e. {(/)} -> (F` (G` k)) =/= (/))
117	113, 116	syl 12	. . . . . 6 |- ((F` (G` k)) e. (~PA \ {(/)}) -> (F` (G` k)) =/= (/))
118	108, 117	syl 12	. . . . 5 |- (((r We A /\ (c e. A /\ F:A-->(~PA \ {(/)}))) /\ k e. NN) -> (F` (G` k)) =/= (/))
119	86	wereucl 3655	. . . . 5 |- ((r We A /\ (F` (G` k)) C_ A /\ (F` (G` k)) =/= (/)) -> U.{v e. (F` (G` k)) | A.u e. (F` (G` k)) -. urv} e. (F` (G` k)))
120	105, 112, 118, 119	syl111anc 1100	. . . 4 |- (((r We A /\ (c e. A /\ F:A-->(~PA \ {(/)}))) /\ k e. NN) -> U.{v e. (F` (G` k)) | A.u e. (F` (G` k)) -. urv} e. (F` (G` k)))
121	104, 120	eqeltrd 1971	. . 3 |- (((r We A /\ (c e. A /\ F:A-->(~PA \ {(/)}))) /\ k e. NN) -> (G` (k + 1)) e. (F` (G` k)))
122	121	r19.21aiva 2176	. 2 |- ((r We A /\ (c e. A /\ F:A-->(~PA \ {(/)}))) -> A.k e. NN (G` (k + 1)) e. (F` (G` k)))
123	61, 69, 122	3jca 1050	1 |- ((r We A /\ (c e. A /\ F:A-->(~PA \ {(/)}))) -> (G:NN-->A /\ (G` 1) = c /\ A.k e. NN (G` (k + 1)) e. (F` (G` k))))

Syntax hints:  -. wn 2   -> wi 3   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300   =/= wne 2017  A.wral 2105  {crab 2108  _Vcvv 2292   \ cdif 2590   C_ wss 2593  (/)c0 2875  ~Pcpw 3032  {csn 3044  U.cuni 3177   class class class wbr 3338   We wwe 3624   X. cxp 3984   Fn wfn 3993  -->wf 3994  ` cfv 3998  (class class class)co 4884  {copab2 4885  1c1 6387   + caddc 6389  NNcn 6449   seq1 cseq1 7720

This theorem is referenced by:  acdc3 8755

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790  ax-inf2 5731

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-nel 2020  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-f1 4011  df-fo 4012  df-f1o 4013  df-fv 4014  df-opr 4886  df-oprab 4887  df-mpt 5006  df-1st 5020  df-2nd 5021  df-iota 5089  df-rdg 5140  df-1o 5177  df-oadd 5179  df-omul 5180  df-er 5318  df-ec 5320  df-qs 5323  df-en 5427  df-dom 5428  df-sdom 5429  df-undef 5556  df-riota 5560  df-ni 6152  df-pli 6153  df-mi 6154  df-lti 6155  df-plpq 6187  df-mpq 6188  df-enq 6189  df-nq 6190  df-plq 6191  df-mq 6192  df-rq 6193  df-ltq 6194  df-1q 6195  df-np 6238  df-1p 6239  df-plp 6240  df-mp 6241  df-ltp 6242  df-plpr 6316  df-mpr 6317  df-enr 6318  df-nr 6319  df-plr 6320  df-mr 6321  df-ltr 6322  df-0r 6323  df-1r 6324  df-m1r 6325  df-c 6392  df-0 6393  df-1 6394  df-i 6395  df-r 6396  df-plus 6397  df-mul 6398  df-lt 6399  df-sub 6511  df-neg 6513  df-pnf 6654  df-mnf 6655  df-xr 6656  df-ltxr 6657  df-le 6658  df-n 7108  df-n0 7309  df-z 7345  df-seq1 7721

Copyright terms: Public domain