Theorem filssufil 15571

Description: A filter is contained in some ultrafilter. (Requires the Axiom of Choice.)

Hypothesis

Ref	Expression
filssufil.1	|- X = U.F

Assertion

Ref	Expression
filssufil	|- (F e. Fil -> E.f e. UFil (X = U.f /\ F C_ f))

Distinct variable groups:   f,F   f,X

Proof of Theorem filssufil

Step	Hyp	Ref	Expression
1		unieq 3185	. . . . . . . . 9 |- (k = F -> U.k = U.F)
2		filssufil.1	. . . . . . . . 9 |- X = U.F
3	1, 2	syl6eqr 1946	. . . . . . . 8 |- (k = F -> U.k = X)
4	3	eqeq1d 1892	. . . . . . 7 |- (k = F -> (U.k = U.g <-> X = U.g))
5		sseq1 2637	. . . . . . 7 |- (k = F -> (k C_ g <-> F C_ g))
6	4, 5	anbi12d 690	. . . . . 6 |- (k = F -> ((U.k = U.g /\ k C_ g) <-> (X = U.g /\ F C_ g)))
7	6	rabbidv 2287	. . . . 5 |- (k = F -> {g e. Fil | (U.k = U.g /\ k C_ g)} = {g e. Fil | (X = U.g /\ F C_ g)})
8	7	uneq2d 2755	. . . 4 |- (k = F -> ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) = ({(/)} u. {g e. Fil | (X = U.g /\ F C_ g)}))
9	8	raleqdv 2269	. . . 4 |- (k = F -> (A.h e. ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) -. f C. h <-> A.h e. ({(/)} u. {g e. Fil | (X = U.g /\ F C_ g)}) -. f C. h))
10	8, 9	rexeqbidv 2275	. . 3 |- (k = F -> (E.f e. ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)})A.h e. ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) -. f C. h <-> E.f e. ({(/)} u. {g e. Fil | (X = U.g /\ F C_ g)})A.h e. ({(/)} u. {g e. Fil | (X = U.g /\ F C_ g)}) -. f C. h))
11	2	filssufillem 15570	. . . 4 |- (k e. Fil -> A.x((x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f)) -> U.x e. ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)})))
12		p0ex 3495	. . . . . 6 |- {(/)} e. _V
13		visset 2295	. . . . . . . . . 10 |- k e. _V
14	13	uniex 3794	. . . . . . . . 9 |- U.k e. _V
15	14	pwex 3487	. . . . . . . 8 |- ~PU.k e. _V
16	15	pwex 3487	. . . . . . 7 |- ~P~PU.k e. _V
17		rabss 2684	. . . . . . . 8 |- ({g e. Fil | (U.k = U.g /\ k C_ g)} C_ ~P~PU.k <-> A.g e. Fil ((U.k = U.g /\ k C_ g) -> g e. ~P~PU.k))
18		eqimss2 2667	. . . . . . . . . . 11 |- (U.k = U.g -> U.g C_ U.k)
19		pwuni 3505	. . . . . . . . . . . . 13 |- g C_ ~PU.g
20		sstr 2625	. . . . . . . . . . . . 13 |- ((g C_ ~PU.g /\ ~PU.g C_ ~PU.k) -> g C_ ~PU.k)
21	19, 20	mpan 759	. . . . . . . . . . . 12 |- (~PU.g C_ ~PU.k -> g C_ ~PU.k)
22		sspwb 3503	. . . . . . . . . . . 12 |- (U.g C_ U.k <-> ~PU.g C_ ~PU.k)
23		visset 2295	. . . . . . . . . . . . 13 |- g e. _V
24	23	elpw 3037	. . . . . . . . . . . 12 |- (g e. ~P~PU.k <-> g C_ ~PU.k)
25	21, 22, 24	3imtr4i 236	. . . . . . . . . . 11 |- (U.g C_ U.k -> g e. ~P~PU.k)
26	18, 25	syl 12	. . . . . . . . . 10 |- (U.k = U.g -> g e. ~P~PU.k)
27	26	adantr 425	. . . . . . . . 9 |- ((U.k = U.g /\ k C_ g) -> g e. ~P~PU.k)
28	27	a1i 8	. . . . . . . 8 |- (g e. Fil -> ((U.k = U.g /\ k C_ g) -> g e. ~P~PU.k))
29	17, 28	mprgbir 2163	. . . . . . 7 |- {g e. Fil | (U.k = U.g /\ k C_ g)} C_ ~P~PU.k
30	16, 29	ssexi 3456	. . . . . 6 |- {g e. Fil | (U.k = U.g /\ k C_ g)} e. _V
31	12, 30	unex 3796	. . . . 5 |- ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) e. _V
32	31	zorn 5959	. . . 4 |- (A.x((x C_ ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) /\ A.f e. x A.h e. x (f C_ h \/ h C_ f)) -> U.x e. ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)})) -> E.f e. ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)})A.h e. ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) -. f C. h)
33	11, 32	syl 12	. . 3 |- (k e. Fil -> E.f e. ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)})A.h e. ({(/)} u. {g e. Fil | (U.k = U.g /\ k C_ g)}) -. f C. h)
34	10, 33	vtoclga 2352	. 2 |- (F e. Fil -> E.f e. ({(/)} u. {g e. Fil | (X = U.g /\ F C_ g)})A.h e. ({(/)} u. {g e. Fil | (X = U.g /\ F C_ g)}) -. f C. h)
35		ssun2 2768	. . . . . . . . . . . . . . 15 |- {g e. Fil | (X = U.g /\ F C_ g)} C_ ({(/)} u. {g e. Fil | (X = U.g /\ F C_ g)})
36	35	a1i 8	. . . . . . . . . . . . . 14 |- (F e. Fil -> {g e. Fil | (X = U.g /\ F C_ g)} C_ ({(/)} u. {g e. Fil | (X = U.g /\ F C_ g)}))
37		eqid 1884	. . . . . . . . . . . . . . . . 17 |- X = X
38		ssid 2634	. . . . . . . . . . . . . . . . 17 |- F C_ F
39	37, 38	pm3.2i 307	. . . . . . . . . . . . . . . 16 |- (X = X /\ F C_ F)
40	39	jctr 315	. . . . . . . . . . . . . . 15 |- (F e. Fil -> (F e. Fil /\ (X = X /\ F C_ F)))
41		unieq 3185	. . . . . . . . . . . . . . . . . . 19 |- (g = F -> U.g = U.F)
42	41, 2	syl6eqr 1946	. . . . . . . . . . . . . . . . . 18 |- (g = F -> U.g = X)
43	42	eqeq2d 1895	. . . . . . . . . . . . . . . . 17 |- (g = F -> (X = U.g <-> X = X))
44		sseq2 2639	. . . . . . . . . . . . . . . . 17 |- (g = F -> (F C_ g <-> F C_ F))
45	43, 44	anbi12d 690	. . . . . . . . . . . . . . . 16 |- (g = F -> ((X = U.g /\ F C_ g) <-> (X = X /\ F C_ F)))
46	45	elrab 2414	. . . . . . . . . . . . . . 15 |- (F e. {g e. Fil | (X = U.g /\ F C_ g)} <-> (F e. Fil /\ (X = X /\ F C_ F)))
47	40, 46	sylibr 217	. . . . . . . . . . . . . 14 |- (F e. Fil -> F e. {g e. Fil | (X = U.g /\ F C_ g)})
48	36, 47	sseldd 2620	. . . . . . . . . . . . 13 |- (F e. Fil -> F e. ({(/)} u. {g e. Fil | (X = U.g /\ F C_ g)}))
49		psseq2 2698	. . . . . . . . . . . . . . 15 |- (h = F -> (f C. h <-> f C. F))
50	49	notbid 673	. . . . . . . . . . . . . 14 |- (h = F -> (-. f C. h <-> -. f C. F))
51	50	rcla4v 2376	. . . . . . . . . . . . 13 |- (F e. ({(/)} u. {g e. Fil | (X = U.g /\ F C_ g)}) -> (A.h e. ({(/)} u. {g e. Fil | (X = U.g /\ F C_ g)}) -. f C. h -> -. f C. F))
52	48, 51	syl 12	. . . . . . . . . . . 12 |- (F e. Fil -> (A.h e. ({(/)} u. {g e. Fil | (X = U.g /\ F C_ g)}) -. f C. h -> -. f C. F))
53		psseq1 2697	. . . . . . . . . . . . 13 |- (f = (/) -> (f C. F <-> (/) C. F))
54	2	filusb 10267	. . . . . . . . . . . . . . 15 |- (F e. Fil -> X e. F)
55		ne0i 2881	. . . . . . . . . . . . . . 15 |- (X e. F -> F =/= (/))
56	54, 55	syl 12	. . . . . . . . . . . . . 14 |- (F e. Fil -> F =/= (/))
57		0pss 2910	. . . . . . . . . . . . . 14 |- ((/) C. F <-> F =/= (/))
58	56, 57	sylibr 217	. . . . . . . . . . . . 13 |- (F e. Fil -> (/) C. F)
59	53, 58	syl5cbir 228	. . . . . . . . . . . 12 |- (F e. Fil -> (f = (/) -> f C. F))
60	52, 59	nsyld 132	. . . . . . . . . . 11 |- (F e. Fil -> (A.h e. ({(/)} u. {g e. Fil | (X = U.g /\ F C_ g)}) -. f C. h -> -. f = (/)))
61	60	con2d 107	. . . . . . . . . 10 |- (F e. Fil -> (f = (/) -> -. A.h e. ({(/)} u. {g e. Fil | (X = U.g /\ F C_ g)}) -. f C. h))
62	61	imp 377	. . . . . . . . 9 |- ((F e. Fil /\ f = (/)) -> -. A.h e. ({(/)} u. {g e. Fil | (X = U.g /\ F C_ g)}) -. f C. h)
63	62	pm2.21d 94	. . . . . . . 8 |- ((F e. Fil /\ f = (/)) -> (A.h e. ({(/)} u. {g e. Fil | (X = U.g /\ F C_ g)}) -. f C. h -> (f e. UFil /\ (X = U.f /\ F C_ f))))
64	63	ex 402	. . . . . . 7 |- (F e. Fil -> (f = (/) -> (A.h e. ({(/)} u. {g e. Fil | (X = U.g /\ F C_ g)}) -. f C. h -> (f e. UFil /\ (X = U.f /\ F C_ f)))))
65		elsn 3058	. . . . . . 7 |- (f e. {(/)} <-> f = (/))
66	64, 65	syl5ib 223	. . . . . 6 |- (F e. Fil -> (f e. {(/)} -> (A.h e. ({(/)} u. {g e. Fil | (X = U.g /\ F C_ g)}) -. f C. h -> (f e. UFil /\ (X = U.f /\ F C_ f)))))
67		eqid 1884	. . . . . . . . . . 11 |- U.f = U.f
68	67	isufil2 15565	. . . . . . . . . 10 |- (f e. UFil <-> (f e. Fil /\ A.h e. Fil ((U.f = U.h /\ f C_ h) -> f = h)))
69		simplrl 454	. . . . . . . . . 10 |- (((F e. Fil /\ (f e. Fil /\ (X = U.f /\ F C_ f))) /\ A.h e. ({(/)} u. {g e. Fil | (X = U.g /\ F C_ g)}) -. f C. h) -> f e. Fil)
70	35	a1i 8	. . . . . . . . . . . . . . . . . 18 |- (((F e. Fil /\ (f e. Fil /\ (X = U.f /\ F C_ f))) /\ (h e. Fil /\ (U.f = U.h /\ f C_ h))) -> {g e. Fil | (X = U.g /\ F C_ g)} C_ ({(/)} u. {g e. Fil | (X = U.g /\ F C_ g)}))
71		simprl 450	. . . . . . . . . . . . . . . . . . . 20 |- (((F e. Fil /\ (f e. Fil /\ (X = U.f /\ F C_ f))) /\ (h e. Fil /\ (U.f = U.h /\ f C_ h))) -> h e. Fil)
72		eqtr 1904	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((X = U.f /\ U.f = U.h) -> X = U.h)
73	72	adantlr 429	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((X = U.f /\ F C_ f) /\ U.f = U.h) -> X = U.h)
74	73	adantll 428	. . . . . . . . . . . . . . . . . . . . . 22 |- (((f e. Fil /\ (X = U.f /\ F C_ f)) /\ U.f = U.h) -> X = U.h)
75	74	ad2ant2l 444	. . . . . . . . . . . . . . . . . . . . 21 |- (((F e. Fil /\ (f e. Fil /\ (X = U.f /\ F C_ f))) /\ (h e. Fil /\ U.f = U.h)) -> X = U.h)
76	75	adantrrr 439	. . . . . . . . . . . . . . . . . . . 20 |- (((F e. Fil /\ (f e. Fil /\ (X = U.f /\ F C_ f))) /\ (h e. Fil /\ (U.f = U.h /\ f C_ h))) -> X = U.h)
77		sstr 2625	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((F C_ f /\ f C_ h) -> F C_ h)
78	77	adantll 428	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((X = U.f /\ F C_ f) /\ f C_ h) -> F C_ h)
79	78	adantll 428	. . . . . . . . . . . . . . . . . . . . . 22 |- (((f e. Fil /\ (X = U.f /\ F C_ f)) /\ f C_ h) -> F C_ h)
80	79	ad2ant2l 444	. . . . . . . . . . . . . . . . . . . . 21 |- (((F e. Fil /\ (f e. Fil /\ (X = U.f /\ F C_ f))) /\ (U.f = U.h /\ f C_ h)) -> F C_ h)
81	80	adantrl 430	. . . . . . . . . . . . . . . . . . . 20 |- (((F e. Fil /\ (f e. Fil /\ (X = U.f /\ F C_ f))) /\ (h e. Fil /\ (U.f = U.h /\ f C_ h))) -> F C_ h)
82	71, 76, 81	jca32 312	. . . . . . . . . . . . . . . . . . 19 |- (((F e. Fil /\ (f e. Fil /\ (X = U.f /\ F C_ f))) /\ (h e. Fil /\ (U.f = U.h /\ f C_ h))) -> (h e. Fil /\ (X = U.h /\ F C_ h)))
83		unieq 3185	. . . . . . . . . . . . . . . . . . . . . 22 |- (g = h -> U.g = U.h)
84	83	eqeq2d 1895	. . . . . . . . . . . . . . . . . . . . 21 |- (g = h -> (X = U.g <-> X = U.h))
85		sseq2 2639	. . . . . . . . . . . . . . . . . . . . 21 |- (g = h -> (F C_ g <-> F C_ h))
86	84, 85	anbi12d 690	. . . . . . . . . . . . . . . . . . . 20 |- (g = h -> ((X = U.g /\ F C_ g) <-> (X = U.h /\ F C_ h)))
87	86	elrab 2414	. . . . . . . . . . . . . . . . . . 19 |- (h e. {g e. Fil | (X = U.g /\ F C_ g)} <-> (h e. Fil /\ (X = U.h /\ F C_ h)))
88	82, 87	sylibr 217	. . . . . . . . . . . . . . . . . 18 |- (((F e. Fil /\ (f e. Fil /\ (X = U.f /\ F C_ f))) /\ (h e. Fil /\ (U.f = U.h /\ f C_ h))) -> h e. {g e. Fil | (X = U.g /\ F C_ g)})
89	70, 88	sseldd 2620	. . . . . . . . . . . . . . . . 17 |- (((F e. Fil /\ (f e. Fil /\ (X = U.f /\ F C_ f))) /\ (h e. Fil /\ (U.f = U.h /\ f C_ h))) -> h e. ({(/)} u. {g e. Fil | (X = U.g /\ F C_ g)}))
90		df-pss 2607	. . . . . . . . . . . . . . . . . . . . . 22 |- (f C. h <-> (f C_ h /\ f =/= h))
91	90	simplbi2 466	. . . . . . . . . . . . . . . . . . . . 21 |- (f C_ h -> (f =/= h -> f C. h))
92	91	necon1bd 2080	. . . . . . . . . . . . . . . . . . . 20 |- (f C_ h -> (-. f C. h -> f = h))
93	92	adantl 424	. . . . . . . . . . . . . . . . . . 19 |- ((U.f = U.h /\ f C_ h) -> (-. f C. h -> f = h))
94	93	ad2antll 443	. . . . . . . . . . . . . . . . . 18 |- (((F e. Fil /\ (f e. Fil /\ (X = U.f /\ F C_ f))) /\ (h e. Fil /\ (U.f = U.h /\ f C_ h))) -> (-. f C. h -> f = h))
95	94	imim2d 28	. . . . . . . . . . . . . . . . 17 |- (((F e. Fil /\ (f e. Fil /\ (X = U.f /\ F C_ f))) /\ (h e. Fil /\ (U.f = U.h /\ f C_ h))) -> ((h e. ({(/)} u. {g e. Fil | (X = U.g /\ F C_ g)}) -> -. f C. h) -> (h e. ({(/)} u. {g e. Fil | (X = U.g /\ F C_ g)}) -> f = h)))
96	89, 95	mpid 58	. . . . . . . . . . . . . . . 16 |- (((F e. Fil /\ (f e. Fil /\ (X = U.f /\ F C_ f))) /\ (h e. Fil /\ (U.f = U.h /\ f C_ h))) -> ((h e. ({(/)} u. {g e. Fil | (X = U.g /\ F C_ g)}) -> -. f C. h) -> f = h))
97	96	expr 418	. . . . . . . . . . . . . . 15 |- (((F e. Fil /\ (f e. Fil /\ (X = U.f /\ F C_ f))) /\ h e. Fil) -> ((U.f = U.h /\ f C_ h) -> ((h e. ({(/)} u. {g e. Fil | (X = U.g /\ F C_ g)}) -> -. f C. h) -> f = h)))
98	97	com23 36	. . . . . . . . . . . . . 14 |- (((F e. Fil /\ (f e. Fil /\ (X = U.f /\ F C_ f))) /\ h e. Fil) -> ((h e. ({(/)} u. {g e. Fil | (X = U.g /\ F C_ g)}) -> -. f C. h) -> ((U.f = U.h /\ f C_ h) -> f = h)))
99	98	ex 402	. . . . . . . . . . . . 13 |- ((F e. Fil /\ (f e. Fil /\ (X = U.f /\ F C_ f))) -> (h e. Fil -> ((h e. ({(/)} u. {g e. Fil | (X = U.g /\ F C_ g)}) -> -. f C. h) -> ((U.f = U.h /\ f C_ h) -> f = h))))
100	99	com23 36	. . . . . . . . . . . 12 |- ((F e. Fil /\ (f e. Fil /\ (X = U.f /\ F C_ f))) -> ((h e. ({(/)} u. {g e. Fil | (X = U.g /\ F C_ g)}) -> -. f C. h) -> (h e. Fil -> ((U.f = U.h /\ f C_ h) -> f = h))))
101	100	ralimdv2 2173	. . . . . . . . . . 11 |- ((F e. Fil /\ (f e. Fil /\ (X = U.f /\ F C_ f))) -> (A.h e. ({(/)} u. {g e. Fil | (X = U.g /\ F C_ g)}) -. f C. h -> A.h e. Fil ((U.f = U.h /\ f C_ h) -> f = h)))
102	101	imp 377	. . . . . . . . . 10 |- (((F e. Fil /\ (f e. Fil /\ (X = U.f /\ F C_ f))) /\ A.h e. ({(/)} u. {g e. Fil | (X = U.g /\ F C_ g)}) -. f C. h) -> A.h e. Fil ((U.f = U.h /\ f C_ h) -> f = h))
103	68, 69, 102	sylanbrc 527	. . . . . . . . 9 |- (((F e. Fil /\ (f e. Fil /\ (X = U.f /\ F C_ f))) /\ A.h e. ({(/)} u. {g e. Fil | (X = U.g /\ F C_ g)}) -. f C. h) -> f e. UFil)
104		simplrr 455	. . . . . . . . 9 |- (((F e. Fil /\ (f e. Fil /\ (X = U.f /\ F C_ f))) /\ A.h e. ({(/)} u. {g e. Fil | (X = U.g /\ F C_ g)}) -. f C. h) -> (X = U.f /\ F C_ f))
105	103, 104	jca 310	. . . . . . . 8 |- (((F e. Fil /\ (f e. Fil /\ (X = U.f /\ F C_ f))) /\ A.h e. ({(/)} u. {g e. Fil | (X = U.g /\ F C_ g)}) -. f C. h) -> (f e. UFil /\ (X = U.f /\ F C_ f)))
106	105	exp31 407	. . . . . . 7 |- (F e. Fil -> ((f e. Fil /\ (X = U.f /\ F C_ f)) -> (A.h e. ({(/)} u. {g e. Fil | (X = U.g /\ F C_ g)}) -. f C. h -> (f e. UFil /\ (X = U.f /\ F C_ f)))))
107		unieq 3185	. . . . . . . . . 10 |- (g = f -> U.g = U.f)
108	107	eqeq2d 1895	. . . . . . . . 9 |- (g = f -> (X = U.g <-> X = U.f))
109		sseq2 2639	. . . . . . . . 9 |- (g = f -> (F C_ g <-> F C_ f))
110	108, 109	anbi12d 690	. . . . . . . 8 |- (g = f -> ((X = U.g /\ F C_ g) <-> (X = U.f /\ F C_ f)))
111	110	elrab 2414	. . . . . . 7 |- (f e. {g e. Fil | (X = U.g /\ F C_ g)} <-> (f e. Fil /\ (X = U.f /\ F C_ f)))
112	106, 111	syl5ib 223	. . . . . 6 |- (F e. Fil -> (f e. {g e. Fil | (X = U.g /\ F C_ g)} -> (A.h e. ({(/)} u. {g e. Fil | (X = U.g /\ F C_ g)}) -. f C. h -> (f e. UFil /\ (X = U.f /\ F C_ f)))))
113	66, 112	jaod 469	. . . . 5 |- (F e. Fil -> ((f e. {(/)} \/ f e. {g e. Fil | (X = U.g /\ F C_ g)}) -> (A.h e. ({(/)} u. {g e. Fil | (X = U.g /\ F C_ g)}) -. f C. h -> (f e. UFil /\ (X = U.f /\ F C_ f)))))
114		elun 2741	. . . . 5 |- (f e. ({(/)} u. {g e. Fil | (X = U.g /\ F C_ g)}) <-> (f e. {(/)} \/ f e. {g e. Fil | (X = U.g /\ F C_ g)}))
115	113, 114	syl5ib 223	. . . 4 |- (F e. Fil -> (f e. ({(/)} u. {g e. Fil | (X = U.g /\ F C_ g)}) -> (A.h e. ({(/)} u. {g e. Fil | (X = U.g /\ F C_ g)}) -. f C. h -> (f e. UFil /\ (X = U.f /\ F C_ f)))))
116	115	imp3a 388	. . 3 |- (F e. Fil -> ((f e. ({(/)} u. {g e. Fil | (X = U.g /\ F C_ g)}) /\ A.h e. ({(/)} u. {g e. Fil | (X = U.g /\ F C_ g)}) -. f C. h) -> (f e. UFil /\ (X = U.f /\ F C_ f))))
117	116	reximdv2 2200	. 2 |- (F e. Fil -> (E.f e. ({(/)} u. {g e. Fil | (X = U.g /\ F C_ g)})A.h e. ({(/)} u. {g e. Fil | (X = U.g /\ F C_ g)}) -. f C. h -> E.f e. UFil (X = U.f /\ F C_ f)))
118	34, 117	mpd 29	1 |- (F e. Fil -> E.f e. UFil (X = U.f /\ F C_ f))

Syntax hints:  -. wn 2   -> wi 3   \/ wo 239   /\ wa 240  A.wal 1296   = wceq 1298   e. wcel 1300   =/= wne 2017  A.wral 2105  E.wrex 2106  {crab 2108   u. cun 2591   C_ wss 2593   C. wpss 2594  (/)c0 2875  ~Pcpw 3032  {csn 3044  U.cuni 3177  Filcfil 10264  UFilcufil 15562

This theorem is referenced by:  ufileu 15573  filufint 15574  ufinffr 15578  ufilen 15579  ufcomp 15622

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-ac 5906

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-iso 4015  df-opr 4886  df-oprab 4887  df-rdg 5140  df-1o 5177  df-oadd 5179  df-er 5318  df-en 5427  df-fin 5430  df-fi 10211  df-fbas 10259  df-fg 10260  df-fil 10265  df-ufil 15563

Copyright terms: Public domain