Theorem abfii4 5654

Description: Two ways to express the collection of finite intersections of a set A. Even though the expressions differ by only one symbol, the proof is not simple.

Hypothesis

Ref	Expression
abfii2.1	|- A e. _V

Assertion

Ref	Expression
abfii4	|- |^|{x | (A C_ x /\ A.y((y C_ x /\ y =/= (/) /\ y e. Fin) -> |^|y e. x))} = |^|{x | (A C_ x /\ A.y((y C_ A /\ y =/= (/) /\ y e. Fin) -> |^|y e. x))}

Distinct variable group:   x,y,A

Proof of Theorem abfii4

Step	Hyp	Ref	Expression
1		abfii2.1	. . . . . . 7 |- A e. _V
2		df-sn 3049	. . . . . . . 8 |- {|^|v} = {w | w = |^|v}
3		snex 3492	. . . . . . . 8 |- {|^|v} e. _V
4	2, 3	eqeltrri 1968	. . . . . . 7 |- {w | w = |^|v} e. _V
5	1, 4	abexssex 4848	. . . . . 6 |- {w | E.v(v C_ A /\ w = |^|v)} e. _V
6		3simpb 873	. . . . . . . 8 |- ((v C_ A /\ v e. Fin /\ w = |^|v) -> (v C_ A /\ w = |^|v))
7	6	eximi 1387	. . . . . . 7 |- (E.v(v C_ A /\ v e. Fin /\ w = |^|v) -> E.v(v C_ A /\ w = |^|v))
8	7	ss2abi 2679	. . . . . 6 |- {w | E.v(v C_ A /\ v e. Fin /\ w = |^|v)} C_ {w | E.v(v C_ A /\ w = |^|v)}
9	5, 8	ssexi 3456	. . . . 5 |- {w | E.v(v C_ A /\ v e. Fin /\ w = |^|v)} e. _V
10		sseq2 2639	. . . . . . 7 |- (x = {w | E.v(v C_ A /\ v e. Fin /\ w = |^|v)} -> (A C_ x <-> A C_ {w | E.v(v C_ A /\ v e. Fin /\ w = |^|v)}))
11		sseq2 2639	. . . . . . . . . 10 |- (x = {w | E.v(v C_ A /\ v e. Fin /\ w = |^|v)} -> (y C_ x <-> y C_ {w | E.v(v C_ A /\ v e. Fin /\ w = |^|v)}))
12	11	3anbi1d 1172	. . . . . . . . 9 |- (x = {w | E.v(v C_ A /\ v e. Fin /\ w = |^|v)} -> ((y C_ x /\ y =/= (/) /\ y e. Fin) <-> (y C_ {w | E.v(v C_ A /\ v e. Fin /\ w = |^|v)} /\ y =/= (/) /\ y e. Fin)))
13		eleq2 1958	. . . . . . . . 9 |- (x = {w | E.v(v C_ A /\ v e. Fin /\ w = |^|v)} -> (|^|y e. x <-> |^|y e. {w | E.v(v C_ A /\ v e. Fin /\ w = |^|v)}))
14	12, 13	imbi12d 688	. . . . . . . 8 |- (x = {w | E.v(v C_ A /\ v e. Fin /\ w = |^|v)} -> (((y C_ x /\ y =/= (/) /\ y e. Fin) -> |^|y e. x) <-> ((y C_ {w | E.v(v C_ A /\ v e. Fin /\ w = |^|v)} /\ y =/= (/) /\ y e. Fin) -> |^|y e. {w | E.v(v C_ A /\ v e. Fin /\ w = |^|v)})))
15	14	albidv 1656	. . . . . . 7 |- (x = {w | E.v(v C_ A /\ v e. Fin /\ w = |^|v)} -> (A.y((y C_ x /\ y =/= (/) /\ y e. Fin) -> |^|y e. x) <-> A.y((y C_ {w | E.v(v C_ A /\ v e. Fin /\ w = |^|v)} /\ y =/= (/) /\ y e. Fin) -> |^|y e. {w | E.v(v C_ A /\ v e. Fin /\ w = |^|v)})))
16	10, 15	anbi12d 690	. . . . . 6 |- (x = {w | E.v(v C_ A /\ v e. Fin /\ w = |^|v)} -> ((A C_ x /\ A.y((y C_ x /\ y =/= (/) /\ y e. Fin) -> |^|y e. x)) <-> (A C_ {w | E.v(v C_ A /\ v e. Fin /\ w = |^|v)} /\ A.y((y C_ {w | E.v(v C_ A /\ v e. Fin /\ w = |^|v)} /\ y =/= (/) /\ y e. Fin) -> |^|y e. {w | E.v(v C_ A /\ v e. Fin /\ w = |^|v)}))))
17		ssmin 3236	. . . . . . . 8 |- A C_ |^|{w | (A C_ w /\ A.v((v C_ A /\ v =/= (/) /\ v e. Fin) -> |^|v e. w))}
18	1	abfii3 5653	. . . . . . . . 9 |- |^|{w | (A C_ w /\ A.v((v C_ A /\ v =/= (/) /\ v e. Fin) -> |^|v e. w))} = |^|{w | A.v((v C_ A /\ v =/= (/) /\ v e. Fin) -> |^|v e. w)}
19	1	abfii2 5652	. . . . . . . . 9 |- {w | E.v(v C_ A /\ v e. Fin /\ w = |^|v)} = |^|{w | A.v((v C_ A /\ v =/= (/) /\ v e. Fin) -> |^|v e. w)}
20	18, 19	eqtr4i 1911	. . . . . . . 8 |- |^|{w | (A C_ w /\ A.v((v C_ A /\ v =/= (/) /\ v e. Fin) -> |^|v e. w))} = {w | E.v(v C_ A /\ v e. Fin /\ w = |^|v)}
21	17, 20	sseqtri 2649	. . . . . . 7 |- A C_ {w | E.v(v C_ A /\ v e. Fin /\ w = |^|v)}
22		eeanv 1707	. . . . . . . . . . . 12 |- (E.tE.f((t C_ A /\ t e. Fin /\ y = |^|t) /\ (f C_ A /\ f e. Fin /\ z = |^|f)) <-> (E.t(t C_ A /\ t e. Fin /\ y = |^|t) /\ E.f(f C_ A /\ f e. Fin /\ z = |^|f)))
23		an6 1177	. . . . . . . . . . . . . 14 |- (((t C_ A /\ t e. Fin /\ y = |^|t) /\ (f C_ A /\ f e. Fin /\ z = |^|f)) <-> ((t C_ A /\ f C_ A) /\ (t e. Fin /\ f e. Fin) /\ (y = |^|t /\ z = |^|f)))
24		visset 2295	. . . . . . . . . . . . . . . . 17 |- t e. _V
25		visset 2295	. . . . . . . . . . . . . . . . 17 |- f e. _V
26	24, 25	unex 3796	. . . . . . . . . . . . . . . 16 |- (t u. f) e. _V
27		sseq1 2637	. . . . . . . . . . . . . . . . 17 |- (v = (t u. f) -> (v C_ A <-> (t u. f) C_ A))
28		eleq1 1957	. . . . . . . . . . . . . . . . 17 |- (v = (t u. f) -> (v e. Fin <-> (t u. f) e. Fin))
29		inteq 3217	. . . . . . . . . . . . . . . . . 18 |- (v = (t u. f) -> |^|v = |^|(t u. f))
30	29	eqeq2d 1895	. . . . . . . . . . . . . . . . 17 |- (v = (t u. f) -> ((y i^i z) = |^|v <-> (y i^i z) = |^|(t u. f)))
31	27, 28, 30	3anbi123d 1168	. . . . . . . . . . . . . . . 16 |- (v = (t u. f) -> ((v C_ A /\ v e. Fin /\ (y i^i z) = |^|v) <-> ((t u. f) C_ A /\ (t u. f) e. Fin /\ (y i^i z) = |^|(t u. f))))
32	26, 31	cla4ev 2371	. . . . . . . . . . . . . . 15 |- (((t u. f) C_ A /\ (t u. f) e. Fin /\ (y i^i z) = |^|(t u. f)) -> E.v(v C_ A /\ v e. Fin /\ (y i^i z) = |^|v))
33		unss 2780	. . . . . . . . . . . . . . . 16 |- ((t C_ A /\ f C_ A) <-> (t u. f) C_ A)
34	33	biimpi 168	. . . . . . . . . . . . . . 15 |- ((t C_ A /\ f C_ A) -> (t u. f) C_ A)
35		unfi 5644	. . . . . . . . . . . . . . 15 |- ((t e. Fin /\ f e. Fin) -> (t u. f) e. Fin)
36		ineq12 2791	. . . . . . . . . . . . . . . 16 |- ((y = |^|t /\ z = |^|f) -> (y i^i z) = (|^|t i^i |^|f))
37		intun 3249	. . . . . . . . . . . . . . . 16 |- |^|(t u. f) = (|^|t i^i |^|f)
38	36, 37	syl6eqr 1946	. . . . . . . . . . . . . . 15 |- ((y = |^|t /\ z = |^|f) -> (y i^i z) = |^|(t u. f))
39	32, 34, 35, 38	syl3an 1139	. . . . . . . . . . . . . 14 |- (((t C_ A /\ f C_ A) /\ (t e. Fin /\ f e. Fin) /\ (y = |^|t /\ z = |^|f)) -> E.v(v C_ A /\ v e. Fin /\ (y i^i z) = |^|v))
40	23, 39	sylbi 216	. . . . . . . . . . . . 13 |- (((t C_ A /\ t e. Fin /\ y = |^|t) /\ (f C_ A /\ f e. Fin /\ z = |^|f)) -> E.v(v C_ A /\ v e. Fin /\ (y i^i z) = |^|v))
41	40	19.23aivv 1675	. . . . . . . . . . . 12 |- (E.tE.f((t C_ A /\ t e. Fin /\ y = |^|t) /\ (f C_ A /\ f e. Fin /\ z = |^|f)) -> E.v(v C_ A /\ v e. Fin /\ (y i^i z) = |^|v))
42	22, 41	sylbir 218	. . . . . . . . . . 11 |- ((E.t(t C_ A /\ t e. Fin /\ y = |^|t) /\ E.f(f C_ A /\ f e. Fin /\ z = |^|f)) -> E.v(v C_ A /\ v e. Fin /\ (y i^i z) = |^|v))
43		visset 2295	. . . . . . . . . . . . 13 |- y e. _V
44	43	inex1 3452	. . . . . . . . . . . 12 |- (y i^i z) e. _V
45		eqeq1 1890	. . . . . . . . . . . . . 14 |- (w = (y i^i z) -> (w = |^|v <-> (y i^i z) = |^|v))
46	45	3anbi3d 1174	. . . . . . . . . . . . 13 |- (w = (y i^i z) -> ((v C_ A /\ v e. Fin /\ w = |^|v) <-> (v C_ A /\ v e. Fin /\ (y i^i z) = |^|v)))
47	46	exbidv 1657	. . . . . . . . . . . 12 |- (w = (y i^i z) -> (E.v(v C_ A /\ v e. Fin /\ w = |^|v) <-> E.v(v C_ A /\ v e. Fin /\ (y i^i z) = |^|v)))
48	44, 47	elab 2403	. . . . . . . . . . 11 |- ((y i^i z) e. {w | E.v(v C_ A /\ v e. Fin /\ w = |^|v)} <-> E.v(v C_ A /\ v e. Fin /\ (y i^i z) = |^|v))
49	42, 48	sylibr 217	. . . . . . . . . 10 |- ((E.t(t C_ A /\ t e. Fin /\ y = |^|t) /\ E.f(f C_ A /\ f e. Fin /\ z = |^|f)) -> (y i^i z) e. {w | E.v(v C_ A /\ v e. Fin /\ w = |^|v)})
50		eqeq1 1890	. . . . . . . . . . . . . 14 |- (w = y -> (w = |^|v <-> y = |^|v))
51	50	3anbi3d 1174	. . . . . . . . . . . . 13 |- (w = y -> ((v C_ A /\ v e. Fin /\ w = |^|v) <-> (v C_ A /\ v e. Fin /\ y = |^|v)))
52	51	exbidv 1657	. . . . . . . . . . . 12 |- (w = y -> (E.v(v C_ A /\ v e. Fin /\ w = |^|v) <-> E.v(v C_ A /\ v e. Fin /\ y = |^|v)))
53	43, 52	elab 2403	. . . . . . . . . . 11 |- (y e. {w | E.v(v C_ A /\ v e. Fin /\ w = |^|v)} <-> E.v(v C_ A /\ v e. Fin /\ y = |^|v))
54		sseq1 2637	. . . . . . . . . . . . 13 |- (v = t -> (v C_ A <-> t C_ A))
55		eleq1 1957	. . . . . . . . . . . . 13 |- (v = t -> (v e. Fin <-> t e. Fin))
56		inteq 3217	. . . . . . . . . . . . . 14 |- (v = t -> |^|v = |^|t)
57	56	eqeq2d 1895	. . . . . . . . . . . . 13 |- (v = t -> (y = |^|v <-> y = |^|t))
58	54, 55, 57	3anbi123d 1168	. . . . . . . . . . . 12 |- (v = t -> ((v C_ A /\ v e. Fin /\ y = |^|v) <-> (t C_ A /\ t e. Fin /\ y = |^|t)))
59	58	cbvexv 1697	. . . . . . . . . . 11 |- (E.v(v C_ A /\ v e. Fin /\ y = |^|v) <-> E.t(t C_ A /\ t e. Fin /\ y = |^|t))
60	53, 59	bitri 190	. . . . . . . . . 10 |- (y e. {w | E.v(v C_ A /\ v e. Fin /\ w = |^|v)} <-> E.t(t C_ A /\ t e. Fin /\ y = |^|t))
61		visset 2295	. . . . . . . . . . . 12 |- z e. _V
62		eqeq1 1890	. . . . . . . . . . . . . 14 |- (w = z -> (w = |^|v <-> z = |^|v))
63	62	3anbi3d 1174	. . . . . . . . . . . . 13 |- (w = z -> ((v C_ A /\ v e. Fin /\ w = |^|v) <-> (v C_ A /\ v e. Fin /\ z = |^|v)))
64	63	exbidv 1657	. . . . . . . . . . . 12 |- (w = z -> (E.v(v C_ A /\ v e. Fin /\ w = |^|v) <-> E.v(v C_ A /\ v e. Fin /\ z = |^|v)))
65	61, 64	elab 2403	. . . . . . . . . . 11 |- (z e. {w | E.v(v C_ A /\ v e. Fin /\ w = |^|v)} <-> E.v(v C_ A /\ v e. Fin /\ z = |^|v))
66		sseq1 2637	. . . . . . . . . . . . 13 |- (v = f -> (v C_ A <-> f C_ A))
67		eleq1 1957	. . . . . . . . . . . . 13 |- (v = f -> (v e. Fin <-> f e. Fin))
68		inteq 3217	. . . . . . . . . . . . . 14 |- (v = f -> |^|v = |^|f)
69	68	eqeq2d 1895	. . . . . . . . . . . . 13 |- (v = f -> (z = |^|v <-> z = |^|f))
70	66, 67, 69	3anbi123d 1168	. . . . . . . . . . . 12 |- (v = f -> ((v C_ A /\ v e. Fin /\ z = |^|v) <-> (f C_ A /\ f e. Fin /\ z = |^|f)))
71	70	cbvexv 1697	. . . . . . . . . . 11 |- (E.v(v C_ A /\ v e. Fin /\ z = |^|v) <-> E.f(f C_ A /\ f e. Fin /\ z = |^|f))
72	65, 71	bitri 190	. . . . . . . . . 10 |- (z e. {w | E.v(v C_ A /\ v e. Fin /\ w = |^|v)} <-> E.f(f C_ A /\ f e. Fin /\ z = |^|f))
73	49, 60, 72	syl2anb 504	. . . . . . . . 9 |- ((y e. {w | E.v(v C_ A /\ v e. Fin /\ w = |^|v)} /\ z e. {w | E.v(v C_ A /\ v e. Fin /\ w = |^|v)}) -> (y i^i z) e. {w | E.v(v C_ A /\ v e. Fin /\ w = |^|v)})
74	73	rgen2a 2160	. . . . . . . 8 |- A.y e. {w | E.v(v C_ A /\ v e. Fin /\ w = |^|v)}A.z e. {w | E.v(v C_ A /\ v e. Fin /\ w = |^|v)} (y i^i z) e. {w | E.v(v C_ A /\ v e. Fin /\ w = |^|v)}
75		fiint 5650	. . . . . . . 8 |- (A.y e. {w | E.v(v C_ A /\ v e. Fin /\ w = |^|v)}A.z e. {w | E.v(v C_ A /\ v e. Fin /\ w = |^|v)} (y i^i z) e. {w | E.v(v C_ A /\ v e. Fin /\ w = |^|v)} <-> A.y((y C_ {w | E.v(v C_ A /\ v e. Fin /\ w = |^|v)} /\ y =/= (/) /\ y e. Fin) -> |^|y e. {w | E.v(v C_ A /\ v e. Fin /\ w = |^|v)}))
76	74, 75	mpbi 206	. . . . . . 7 |- A.y((y C_ {w | E.v(v C_ A /\ v e. Fin /\ w = |^|v)} /\ y =/= (/) /\ y e. Fin) -> |^|y e. {w | E.v(v C_ A /\ v e. Fin /\ w = |^|v)})
77	21, 76	pm3.2i 307	. . . . . 6 |- (A C_ {w | E.v(v C_ A /\ v e. Fin /\ w = |^|v)} /\ A.y((y C_ {w | E.v(v C_ A /\ v e. Fin /\ w = |^|v)} /\ y =/= (/) /\ y e. Fin) -> |^|y e. {w | E.v(v C_ A /\ v e. Fin /\ w = |^|v)}))
78	16, 77	intmin3 3245	. . . . 5 |- ({w | E.v(v C_ A /\ v e. Fin /\ w = |^|v)} e. _V -> |^|{x | (A C_ x /\ A.y((y C_ x /\ y =/= (/) /\ y e. Fin) -> |^|y e. x))} C_ {w | E.v(v C_ A /\ v e. Fin /\ w = |^|v)})
79	9, 78	ax-mp 7	. . . 4 |- |^|{x | (A C_ x /\ A.y((y C_ x /\ y =/= (/) /\ y e. Fin) -> |^|y e. x))} C_ {w | E.v(v C_ A /\ v e. Fin /\ w = |^|v)}
80		eqeq1 1890	. . . . . . . . 9 |- (w = x -> (w = |^|v <-> x = |^|v))
81	80	3anbi3d 1174	. . . . . . . 8 |- (w = x -> ((v C_ A /\ v e. Fin /\ w = |^|v) <-> (v C_ A /\ v e. Fin /\ x = |^|v)))
82	81	exbidv 1657	. . . . . . 7 |- (w = x -> (E.v(v C_ A /\ v e. Fin /\ w = |^|v) <-> E.v(v C_ A /\ v e. Fin /\ x = |^|v)))
83		sseq1 2637	. . . . . . . . 9 |- (v = y -> (v C_ A <-> y C_ A))
84		eleq1 1957	. . . . . . . . 9 |- (v = y -> (v e. Fin <-> y e. Fin))
85		inteq 3217	. . . . . . . . . 10 |- (v = y -> |^|v = |^|y)
86	85	eqeq2d 1895	. . . . . . . . 9 |- (v = y -> (x = |^|v <-> x = |^|y))
87	83, 84, 86	3anbi123d 1168	. . . . . . . 8 |- (v = y -> ((v C_ A /\ v e. Fin /\ x = |^|v) <-> (y C_ A /\ y e. Fin /\ x = |^|y)))
88	87	cbvexv 1697	. . . . . . 7 |- (E.v(v C_ A /\ v e. Fin /\ x = |^|v) <-> E.y(y C_ A /\ y e. Fin /\ x = |^|y))
89	82, 88	syl6bb 595	. . . . . 6 |- (w = x -> (E.v(v C_ A /\ v e. Fin /\ w = |^|v) <-> E.y(y C_ A /\ y e. Fin /\ x = |^|y)))
90	89	cbvabv 2420	. . . . 5 |- {w | E.v(v C_ A /\ v e. Fin /\ w = |^|v)} = {x | E.y(y C_ A /\ y e. Fin /\ x = |^|y)}
91	1	abfii2 5652	. . . . 5 |- {x | E.y(y C_ A /\ y e. Fin /\ x = |^|y)} = |^|{x | A.y((y C_ A /\ y =/= (/) /\ y e. Fin) -> |^|y e. x)}
92	90, 91	eqtri 1908	. . . 4 |- {w | E.v(v C_ A /\ v e. Fin /\ w = |^|v)} = |^|{x | A.y((y C_ A /\ y =/= (/) /\ y e. Fin) -> |^|y e. x)}
93	79, 92	sseqtri 2649	. . 3 |- |^|{x | (A C_ x /\ A.y((y C_ x /\ y =/= (/) /\ y e. Fin) -> |^|y e. x))} C_ |^|{x | A.y((y C_ A /\ y =/= (/) /\ y e. Fin) -> |^|y e. x)}
94		sstr2 2623	. . . . . . . . . 10 |- (y C_ A -> (A C_ x -> y C_ x))
95	94	com12 14	. . . . . . . . 9 |- (A C_ x -> (y C_ A -> y C_ x))
96		idd 75	. . . . . . . . 9 |- (A C_ x -> (y =/= (/) -> y =/= (/)))
97		idd 75	. . . . . . . . 9 |- (A C_ x -> (y e. Fin -> y e. Fin))
98	95, 96, 97	3anim123d 1175	. . . . . . . 8 |- (A C_ x -> ((y C_ A /\ y =/= (/) /\ y e. Fin) -> (y C_ x /\ y =/= (/) /\ y e. Fin)))
99	98	imim1d 33	. . . . . . 7 |- (A C_ x -> (((y C_ x /\ y =/= (/) /\ y e. Fin) -> |^|y e. x) -> ((y C_ A /\ y =/= (/) /\ y e. Fin) -> |^|y e. x)))
100	99	alimdv 1668	. . . . . 6 |- (A C_ x -> (A.y((y C_ x /\ y =/= (/) /\ y e. Fin) -> |^|y e. x) -> A.y((y C_ A /\ y =/= (/) /\ y e. Fin) -> |^|y e. x)))
101	100	imp 377	. . . . 5 |- ((A C_ x /\ A.y((y C_ x /\ y =/= (/) /\ y e. Fin) -> |^|y e. x)) -> A.y((y C_ A /\ y =/= (/) /\ y e. Fin) -> |^|y e. x))
102	101	ss2abi 2679	. . . 4 |- {x | (A C_ x /\ A.y((y C_ x /\ y =/= (/) /\ y e. Fin) -> |^|y e. x))} C_ {x | A.y((y C_ A /\ y =/= (/) /\ y e. Fin) -> |^|y e. x)}
103		intss 3239	. . . 4 |- ({x | (A C_ x /\ A.y((y C_ x /\ y =/= (/) /\ y e. Fin) -> |^|y e. x))} C_ {x | A.y((y C_ A /\ y =/= (/) /\ y e. Fin) -> |^|y e. x)} -> |^|{x | A.y((y C_ A /\ y =/= (/) /\ y e. Fin) -> |^|y e. x)} C_ |^|{x | (A C_ x /\ A.y((y C_ x /\ y =/= (/) /\ y e. Fin) -> |^|y e. x))})
104	102, 103	ax-mp 7	. . 3 |- |^|{x | A.y((y C_ A /\ y =/= (/) /\ y e. Fin) -> |^|y e. x)} C_ |^|{x | (A C_ x /\ A.y((y C_ x /\ y =/= (/) /\ y e. Fin) -> |^|y e. x))}
105	93, 104	eqssi 2632	. 2 |- |^|{x | (A C_ x /\ A.y((y C_ x /\ y =/= (/) /\ y e. Fin) -> |^|y e. x))} = |^|{x | A.y((y C_ A /\ y =/= (/) /\ y e. Fin) -> |^|y e. x)}
106	1	abfii3 5653	. 2 |- |^|{x | (A C_ x /\ A.y((y C_ A /\ y =/= (/) /\ y e. Fin) -> |^|y e. x))} = |^|{x | A.y((y C_ A /\ y =/= (/) /\ y e. Fin) -> |^|y e. x)}
107	105, 106	eqtr4i 1911	1 |- |^|{x | (A C_ x /\ A.y((y C_ x /\ y =/= (/) /\ y e. Fin) -> |^|y e. x))} = |^|{x | (A C_ x /\ A.y((y C_ A /\ y =/= (/) /\ y e. Fin) -> |^|y e. x))}

Syntax hints:   -> wi 3   /\ wa 240   /\ w3a 858  A.wal 1296   = wceq 1298   e. wcel 1300  E.wex 1326  {cab 1871   =/= wne 2017  A.wral 2105  _Vcvv 2292   u. cun 2591   i^i cin 2592   C_ wss 2593  (/)c0 2875  {csn 3044  |^|cint 3214  Fincfn 5426

This theorem is referenced by:  abfii5 5655

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

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-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-rdg 5140  df-1o 5177  df-oadd 5179  df-er 5318  df-en 5427  df-fin 5430

Copyright terms: Public domain