Theorem ufileu 15573

Description: If the ultrafilter containing a given filter is unique, the filter is an ultrafilter.

Hypothesis

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

Assertion

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

Distinct variable groups:   f,F   f,X

Proof of Theorem ufileu

Step	Hyp	Ref	Expression
1		ufileu.1	. . . . . . . . . 10 |- X = U.F
2		eqid 1884	. . . . . . . . . 10 |- U.f = U.f
3	1, 2	ufilmax 15568	. . . . . . . . 9 |- (((F e. UFil /\ f e. Fil) /\ (X = U.f /\ F C_ f)) -> F = f)
4	3	eqcomd 1889	. . . . . . . 8 |- (((F e. UFil /\ f e. Fil) /\ (X = U.f /\ F C_ f)) -> f = F)
5	4	ex 402	. . . . . . 7 |- ((F e. UFil /\ f e. Fil) -> ((X = U.f /\ F C_ f) -> f = F))
6		ufilfil 15566	. . . . . . 7 |- (f e. UFil -> f e. Fil)
7	5, 6	sylan2 500	. . . . . 6 |- ((F e. UFil /\ f e. UFil) -> ((X = U.f /\ F C_ f) -> f = F))
8		eqid 1884	. . . . . . . 8 |- X = X
9		ssid 2634	. . . . . . . 8 |- F C_ F
10	8, 9	pm3.2i 307	. . . . . . 7 |- (X = X /\ F C_ F)
11		unieq 3185	. . . . . . . . . 10 |- (f = F -> U.f = U.F)
12	11, 1	syl6eqr 1946	. . . . . . . . 9 |- (f = F -> U.f = X)
13	12	eqeq2d 1895	. . . . . . . 8 |- (f = F -> (X = U.f <-> X = X))
14		sseq2 2639	. . . . . . . 8 |- (f = F -> (F C_ f <-> F C_ F))
15	13, 14	anbi12d 690	. . . . . . 7 |- (f = F -> ((X = U.f /\ F C_ f) <-> (X = X /\ F C_ F)))
16	10, 15	mpbiri 211	. . . . . 6 |- (f = F -> (X = U.f /\ F C_ f))
17	7, 16	impbid1 575	. . . . 5 |- ((F e. UFil /\ f e. UFil) -> ((X = U.f /\ F C_ f) <-> f = F))
18	17	r19.21aiva 2176	. . . 4 |- (F e. UFil -> A.f e. UFil ((X = U.f /\ F C_ f) <-> f = F))
19		eqeq2 1893	. . . . . . 7 |- (g = F -> (f = g <-> f = F))
20	19	bibi2d 680	. . . . . 6 |- (g = F -> (((X = U.f /\ F C_ f) <-> f = g) <-> ((X = U.f /\ F C_ f) <-> f = F)))
21	20	ralbidv 2123	. . . . 5 |- (g = F -> (A.f e. UFil ((X = U.f /\ F C_ f) <-> f = g) <-> A.f e. UFil ((X = U.f /\ F C_ f) <-> f = F)))
22	21	rcla4ev 2381	. . . 4 |- ((F e. UFil /\ A.f e. UFil ((X = U.f /\ F C_ f) <-> f = F)) -> E.g e. UFil A.f e. UFil ((X = U.f /\ F C_ f) <-> f = g))
23	18, 22	mpdan 768	. . 3 |- (F e. UFil -> E.g e. UFil A.f e. UFil ((X = U.f /\ F C_ f) <-> f = g))
24		reu6 2443	. . 3 |- (E!f e. UFil (X = U.f /\ F C_ f) <-> E.g e. UFil A.f e. UFil ((X = U.f /\ F C_ f) <-> f = g))
25	23, 24	sylibr 217	. 2 |- (F e. UFil -> E!f e. UFil (X = U.f /\ F C_ f))
26	1	ufileulem 15572	. . . . . . . . . . . 12 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> ( fi ` (F u. {s})) e. fBas)
27		fgfil 10290	. . . . . . . . . . . 12 |- (( fi ` (F u. {s})) e. fBas -> (filGen` ( fi ` (F u. {s}))) e. Fil)
28		eqid 1884	. . . . . . . . . . . . 13 |- U.(filGen` ( fi ` (F u. {s}))) = U.(filGen` ( fi ` (F u. {s})))
29	28	filssufil 15571	. . . . . . . . . . . 12 |- ((filGen` ( fi ` (F u. {s}))) e. Fil -> E.u e. UFil (U.(filGen` ( fi ` (F u. {s}))) = U.u /\ (filGen` ( fi ` (F u. {s}))) C_ u))
30	26, 27, 29	3syl 24	. . . . . . . . . . 11 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> E.u e. UFil (U.(filGen` ( fi ` (F u. {s}))) = U.u /\ (filGen` ( fi ` (F u. {s}))) C_ u))
31		snex 3492	. . . . . . . . . . . . . . . 16 |- {(X \ s)} e. _V
32		unexg 3798	. . . . . . . . . . . . . . . 16 |- ((F e. Fil /\ {(X \ s)} e. _V) -> (F u. {(X \ s)}) e. _V)
33	31, 32	mpan2 760	. . . . . . . . . . . . . . 15 |- (F e. Fil -> (F u. {(X \ s)}) e. _V)
34		fsubbas 10281	. . . . . . . . . . . . . . 15 |- ((F u. {(X \ s)}) e. _V -> (( fi ` (F u. {(X \ s)})) e. fBas <-> ((F u. {(X \ s)}) =/= (/) /\ (/) e/ ( fi ` (F u. {(X \ s)})))))
35	33, 34	syl 12	. . . . . . . . . . . . . 14 |- (F e. Fil -> (( fi ` (F u. {(X \ s)})) e. fBas <-> ((F u. {(X \ s)}) =/= (/) /\ (/) e/ ( fi ` (F u. {(X \ s)})))))
36	35	ad2antrr 440	. . . . . . . . . . . . 13 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> (( fi ` (F u. {(X \ s)})) e. fBas <-> ((F u. {(X \ s)}) =/= (/) /\ (/) e/ ( fi ` (F u. {(X \ s)})))))
37	1	filusb 10267	. . . . . . . . . . . . . . 15 |- (F e. Fil -> X e. F)
38		ne0i 2881	. . . . . . . . . . . . . . 15 |- (X e. F -> F =/= (/))
39		ssun1 2767	. . . . . . . . . . . . . . . 16 |- F C_ (F u. {(X \ s)})
40		ssn0 2905	. . . . . . . . . . . . . . . 16 |- ((F C_ (F u. {(X \ s)}) /\ F =/= (/)) -> (F u. {(X \ s)}) =/= (/))
41	39, 40	mpan 759	. . . . . . . . . . . . . . 15 |- (F =/= (/) -> (F u. {(X \ s)}) =/= (/))
42	37, 38, 41	3syl 24	. . . . . . . . . . . . . 14 |- (F e. Fil -> (F u. {(X \ s)}) =/= (/))
43	42	ad2antrr 440	. . . . . . . . . . . . 13 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> (F u. {(X \ s)}) =/= (/))
44		ineq2 2790	. . . . . . . . . . . . . . . . . . . . 21 |- (y = (X \ s) -> (x i^i y) = (x i^i (X \ s)))
45	44	neeq1d 2028	. . . . . . . . . . . . . . . . . . . 20 |- (y = (X \ s) -> ((x i^i y) =/= (/) <-> (x i^i (X \ s)) =/= (/)))
46	45	imbi2d 674	. . . . . . . . . . . . . . . . . . 19 |- (y = (X \ s) -> ((x e. F -> (x i^i y) =/= (/)) <-> (x e. F -> (x i^i (X \ s)) =/= (/))))
47		elssuni 3206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (x e. F -> x C_ U.F)
48	47, 1	syl6ssr 2664	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (x e. F -> x C_ X)
49		reldisj 2916	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (x C_ X -> ((x i^i (X \ s)) = (/) <-> x C_ (X \ (X \ s))))
50	48, 49	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (x e. F -> ((x i^i (X \ s)) = (/) <-> x C_ (X \ (X \ s))))
51	50	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((F e. Fil /\ s C_ X) /\ x e. F) -> ((x i^i (X \ s)) = (/) <-> x C_ (X \ (X \ s))))
52		dfss4 2827	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (s C_ X <-> (X \ (X \ s)) = s)
53	52	biimpi 168	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (s C_ X -> (X \ (X \ s)) = s)
54	53	sseq2d 2645	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (s C_ X -> (x C_ (X \ (X \ s)) <-> x C_ s))
55	54	ad2antlr 441	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((F e. Fil /\ s C_ X) /\ x e. F) -> (x C_ (X \ (X \ s)) <-> x C_ s))
56	51, 55	bitrd 587	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((F e. Fil /\ s C_ X) /\ x e. F) -> ((x i^i (X \ s)) = (/) <-> x C_ s))
57	1	fillsb 10270	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (F e. Fil -> ((x e. F /\ s C_ X /\ x C_ s) -> s e. F))
58	57	3expd 1085	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (F e. Fil -> (x e. F -> (s C_ X -> (x C_ s -> s e. F))))
59	58	com23 36	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (F e. Fil -> (s C_ X -> (x e. F -> (x C_ s -> s e. F))))
60	59	imp31 389	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((F e. Fil /\ s C_ X) /\ x e. F) -> (x C_ s -> s e. F))
61	56, 60	sylbid 220	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((F e. Fil /\ s C_ X) /\ x e. F) -> ((x i^i (X \ s)) = (/) -> s e. F))
62	61	necon3bd 2039	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((F e. Fil /\ s C_ X) /\ x e. F) -> (-. s e. F -> (x i^i (X \ s)) =/= (/)))
63	62	ex 402	. . . . . . . . . . . . . . . . . . . . . 22 |- ((F e. Fil /\ s C_ X) -> (x e. F -> (-. s e. F -> (x i^i (X \ s)) =/= (/))))
64	63	com23 36	. . . . . . . . . . . . . . . . . . . . 21 |- ((F e. Fil /\ s C_ X) -> (-. s e. F -> (x e. F -> (x i^i (X \ s)) =/= (/))))
65	64	imp 377	. . . . . . . . . . . . . . . . . . . 20 |- (((F e. Fil /\ s C_ X) /\ -. s e. F) -> (x e. F -> (x i^i (X \ s)) =/= (/)))
66	65	adantrr 431	. . . . . . . . . . . . . . . . . . 19 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> (x e. F -> (x i^i (X \ s)) =/= (/)))
67	46, 66	syl5cbir 228	. . . . . . . . . . . . . . . . . 18 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> (y = (X \ s) -> (x e. F -> (x i^i y) =/= (/))))
68		elsn 3058	. . . . . . . . . . . . . . . . . 18 |- (y e. {(X \ s)} <-> y = (X \ s))
69	67, 68	syl5ib 223	. . . . . . . . . . . . . . . . 17 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> (y e. {(X \ s)} -> (x e. F -> (x i^i y) =/= (/))))
70	69	com23 36	. . . . . . . . . . . . . . . 16 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> (x e. F -> (y e. {(X \ s)} -> (x i^i y) =/= (/))))
71	70	imp3a 388	. . . . . . . . . . . . . . 15 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> ((x e. F /\ y e. {(X \ s)}) -> (x i^i y) =/= (/)))
72	71	r19.21aivv 2183	. . . . . . . . . . . . . 14 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> A.x e. F A.y e. {(X \ s)} (x i^i y) =/= (/))
73		filfbas 10276	. . . . . . . . . . . . . . . 16 |- (F e. Fil -> F e. fBas)
74	73	ad2antrr 440	. . . . . . . . . . . . . . 15 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> F e. fBas)
75		uniexg 3795	. . . . . . . . . . . . . . . . . . . 20 |- (F e. Fil -> U.F e. _V)
76	75, 1	syl5eqel 1975	. . . . . . . . . . . . . . . . . . 19 |- (F e. Fil -> X e. _V)
77		difexg 3458	. . . . . . . . . . . . . . . . . . 19 |- (X e. _V -> (X \ s) e. _V)
78	76, 77	syl 12	. . . . . . . . . . . . . . . . . 18 |- (F e. Fil -> (X \ s) e. _V)
79	78	ad2antrr 440	. . . . . . . . . . . . . . . . 17 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> (X \ s) e. _V)
80	53	eqcomd 1889	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (s C_ X -> s = (X \ (X \ s)))
81	80	adantl 424	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((F e. Fil /\ s C_ X) -> s = (X \ (X \ s)))
82		difeq2 2719	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((X \ s) = (/) -> (X \ (X \ s)) = (X \ (/)))
83	81, 82	sylan9eq 1948	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((F e. Fil /\ s C_ X) /\ (X \ s) = (/)) -> s = (X \ (/)))
84		dif0 2943	. . . . . . . . . . . . . . . . . . . . . . 23 |- (X \ (/)) = X
85	83, 84	syl6eq 1944	. . . . . . . . . . . . . . . . . . . . . 22 |- (((F e. Fil /\ s C_ X) /\ (X \ s) = (/)) -> s = X)
86	37	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . 22 |- (((F e. Fil /\ s C_ X) /\ (X \ s) = (/)) -> X e. F)
87	85, 86	eqeltrd 1971	. . . . . . . . . . . . . . . . . . . . 21 |- (((F e. Fil /\ s C_ X) /\ (X \ s) = (/)) -> s e. F)
88	87	ex 402	. . . . . . . . . . . . . . . . . . . 20 |- ((F e. Fil /\ s C_ X) -> ((X \ s) = (/) -> s e. F))
89	88	necon3bd 2039	. . . . . . . . . . . . . . . . . . 19 |- ((F e. Fil /\ s C_ X) -> (-. s e. F -> (X \ s) =/= (/)))
90	89	imp 377	. . . . . . . . . . . . . . . . . 18 |- (((F e. Fil /\ s C_ X) /\ -. s e. F) -> (X \ s) =/= (/))
91	90	adantrr 431	. . . . . . . . . . . . . . . . 17 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> (X \ s) =/= (/))
92		oefil2 10275	. . . . . . . . . . . . . . . . 17 |- (((X \ s) e. _V /\ (X \ s) =/= (/)) -> {(X \ s)} e. Fil)
93	79, 91, 92	syl11anc 524	. . . . . . . . . . . . . . . 16 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> {(X \ s)} e. Fil)
94		filfbas 10276	. . . . . . . . . . . . . . . 16 |- ({(X \ s)} e. Fil -> {(X \ s)} e. fBas)
95	93, 94	syl 12	. . . . . . . . . . . . . . 15 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> {(X \ s)} e. fBas)
96		fbunfip 10282	. . . . . . . . . . . . . . 15 |- ((F e. fBas /\ {(X \ s)} e. fBas) -> ((/) e/ ( fi ` (F u. {(X \ s)})) <-> A.x e. F A.y e. {(X \ s)} (x i^i y) =/= (/)))
97	74, 95, 96	syl11anc 524	. . . . . . . . . . . . . 14 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> ((/) e/ ( fi ` (F u. {(X \ s)})) <-> A.x e. F A.y e. {(X \ s)} (x i^i y) =/= (/)))
98	72, 97	mpbird 213	. . . . . . . . . . . . 13 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> (/) e/ ( fi ` (F u. {(X \ s)})))
99	36, 43, 98	mpbir2and 802	. . . . . . . . . . . 12 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> ( fi ` (F u. {(X \ s)})) e. fBas)
100		fgfil 10290	. . . . . . . . . . . 12 |- (( fi ` (F u. {(X \ s)})) e. fBas -> (filGen` ( fi ` (F u. {(X \ s)}))) e. Fil)
101		eqid 1884	. . . . . . . . . . . . 13 |- U.(filGen` ( fi ` (F u. {(X \ s)}))) = U.(filGen` ( fi ` (F u. {(X \ s)})))
102	101	filssufil 15571	. . . . . . . . . . . 12 |- ((filGen` ( fi ` (F u. {(X \ s)}))) e. Fil -> E.v e. UFil (U.(filGen` ( fi ` (F u. {(X \ s)}))) = U.v /\ (filGen` ( fi ` (F u. {(X \ s)}))) C_ v))
103	99, 100, 102	3syl 24	. . . . . . . . . . 11 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> E.v e. UFil (U.(filGen` ( fi ` (F u. {(X \ s)}))) = U.v /\ (filGen` ( fi ` (F u. {(X \ s)}))) C_ v))
104		simplrl 454	. . . . . . . . . . . . . . . 16 |- (((((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) /\ (u e. UFil /\ v e. UFil)) /\ ((U.(filGen` ( fi ` (F u. {s}))) = U.u /\ (filGen` ( fi ` (F u. {s}))) C_ u) /\ (U.(filGen` ( fi ` (F u. {(X \ s)}))) = U.v /\ (filGen` ( fi ` (F u. {(X \ s)}))) C_ v))) -> u e. UFil)
105		simplr 449	. . . . . . . . . . . . . . . . . . . . . 22 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> s C_ X)
106		ssequn2 2779	. . . . . . . . . . . . . . . . . . . . . 22 |- (s C_ X <-> (X u. s) = X)
107	105, 106	sylib 215	. . . . . . . . . . . . . . . . . . . . 21 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> (X u. s) = X)
108		visset 2295	. . . . . . . . . . . . . . . . . . . . . . . 24 |- s e. _V
109	108	unisn 3193	. . . . . . . . . . . . . . . . . . . . . . 23 |- U.{s} = s
110	109	eqcomi 1888	. . . . . . . . . . . . . . . . . . . . . 22 |- s = U.{s}
111	1, 110	uneq12i 2753	. . . . . . . . . . . . . . . . . . . . 21 |- (X u. s) = (U.F u. U.{s})
112	107, 111	syl5reqr 1943	. . . . . . . . . . . . . . . . . . . 20 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> X = (U.F u. U.{s}))
113		uniun 3196	. . . . . . . . . . . . . . . . . . . 20 |- U.(F u. {s}) = (U.F u. U.{s})
114	112, 113	syl6eqr 1946	. . . . . . . . . . . . . . . . . . 19 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> X = U.(F u. {s}))
115		snex 3492	. . . . . . . . . . . . . . . . . . . . . 22 |- {s} e. _V
116		unexg 3798	. . . . . . . . . . . . . . . . . . . . . 22 |- ((F e. Fil /\ {s} e. _V) -> (F u. {s}) e. _V)
117	115, 116	mpan2 760	. . . . . . . . . . . . . . . . . . . . 21 |- (F e. Fil -> (F u. {s}) e. _V)
118	117	ad2antrr 440	. . . . . . . . . . . . . . . . . . . 20 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> (F u. {s}) e. _V)
119		fiuni 10219	. . . . . . . . . . . . . . . . . . . 20 |- ((F u. {s}) e. _V -> U.(F u. {s}) = U.( fi ` (F u. {s})))
120	118, 119	syl 12	. . . . . . . . . . . . . . . . . . 19 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> U.(F u. {s}) = U.( fi ` (F u. {s})))
121		eqid 1884	. . . . . . . . . . . . . . . . . . . . 21 |- U.( fi ` (F u. {s})) = U.( fi ` (F u. {s}))
122	121	fgbas 10286	. . . . . . . . . . . . . . . . . . . 20 |- (( fi ` (F u. {s})) e. fBas -> U.( fi ` (F u. {s})) = U.(filGen` ( fi ` (F u. {s}))))
123	26, 122	syl 12	. . . . . . . . . . . . . . . . . . 19 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> U.( fi ` (F u. {s})) = U.(filGen` ( fi ` (F u. {s}))))
124	114, 120, 123	3eqtrd 1929	. . . . . . . . . . . . . . . . . 18 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> X = U.(filGen` ( fi ` (F u. {s}))))
125	124	ad2antrr 440	. . . . . . . . . . . . . . . . 17 |- (((((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) /\ (u e. UFil /\ v e. UFil)) /\ ((U.(filGen` ( fi ` (F u. {s}))) = U.u /\ (filGen` ( fi ` (F u. {s}))) C_ u) /\ (U.(filGen` ( fi ` (F u. {(X \ s)}))) = U.v /\ (filGen` ( fi ` (F u. {(X \ s)}))) C_ v))) -> X = U.(filGen` ( fi ` (F u. {s}))))
126		simprll 456	. . . . . . . . . . . . . . . . 17 |- (((((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) /\ (u e. UFil /\ v e. UFil)) /\ ((U.(filGen` ( fi ` (F u. {s}))) = U.u /\ (filGen` ( fi ` (F u. {s}))) C_ u) /\ (U.(filGen` ( fi ` (F u. {(X \ s)}))) = U.v /\ (filGen` ( fi ` (F u. {(X \ s)}))) C_ v))) -> U.(filGen` ( fi ` (F u. {s}))) = U.u)
127	125, 126	eqtrd 1925	. . . . . . . . . . . . . . . 16 |- (((((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) /\ (u e. UFil /\ v e. UFil)) /\ ((U.(filGen` ( fi ` (F u. {s}))) = U.u /\ (filGen` ( fi ` (F u. {s}))) C_ u) /\ (U.(filGen` ( fi ` (F u. {(X \ s)}))) = U.v /\ (filGen` ( fi ` (F u. {(X \ s)}))) C_ v))) -> X = U.u)
128		ssun1 2767	. . . . . . . . . . . . . . . . . . . . 21 |- F C_ (F u. {s})
129	128	a1i 8	. . . . . . . . . . . . . . . . . . . 20 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> F C_ (F u. {s}))
130		abfi2 10216	. . . . . . . . . . . . . . . . . . . . . 22 |- ((F u. {s}) e. _V -> (F u. {s}) C_ ( fi ` (F u. {s})))
131	117, 130	syl 12	. . . . . . . . . . . . . . . . . . . . 21 |- (F e. Fil -> (F u. {s}) C_ ( fi ` (F u. {s})))
132	131	ad2antrr 440	. . . . . . . . . . . . . . . . . . . 20 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> (F u. {s}) C_ ( fi ` (F u. {s})))
133	129, 132	sstrd 2627	. . . . . . . . . . . . . . . . . . 19 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> F C_ ( fi ` (F u. {s})))
134		fbssfg 10285	. . . . . . . . . . . . . . . . . . . 20 |- (( fi ` (F u. {s})) e. fBas -> ( fi ` (F u. {s})) C_ (filGen` ( fi ` (F u. {s}))))
135	26, 134	syl 12	. . . . . . . . . . . . . . . . . . 19 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> ( fi ` (F u. {s})) C_ (filGen` ( fi ` (F u. {s}))))
136	133, 135	sstrd 2627	. . . . . . . . . . . . . . . . . 18 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> F C_ (filGen` ( fi ` (F u. {s}))))
137	136	ad2antrr 440	. . . . . . . . . . . . . . . . 17 |- (((((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) /\ (u e. UFil /\ v e. UFil)) /\ ((U.(filGen` ( fi ` (F u. {s}))) = U.u /\ (filGen` ( fi ` (F u. {s}))) C_ u) /\ (U.(filGen` ( fi ` (F u. {(X \ s)}))) = U.v /\ (filGen` ( fi ` (F u. {(X \ s)}))) C_ v))) -> F C_ (filGen` ( fi ` (F u. {s}))))
138		simprlr 457	. . . . . . . . . . . . . . . . 17 |- (((((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) /\ (u e. UFil /\ v e. UFil)) /\ ((U.(filGen` ( fi ` (F u. {s}))) = U.u /\ (filGen` ( fi ` (F u. {s}))) C_ u) /\ (U.(filGen` ( fi ` (F u. {(X \ s)}))) = U.v /\ (filGen` ( fi ` (F u. {(X \ s)}))) C_ v))) -> (filGen` ( fi ` (F u. {s}))) C_ u)
139	137, 138	sstrd 2627	. . . . . . . . . . . . . . . 16 |- (((((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) /\ (u e. UFil /\ v e. UFil)) /\ ((U.(filGen` ( fi ` (F u. {s}))) = U.u /\ (filGen` ( fi ` (F u. {s}))) C_ u) /\ (U.(filGen` ( fi ` (F u. {(X \ s)}))) = U.v /\ (filGen` ( fi ` (F u. {(X \ s)}))) C_ v))) -> F C_ u)
140	104, 127, 139	jca32 312	. . . . . . . . . . . . . . 15 |- (((((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) /\ (u e. UFil /\ v e. UFil)) /\ ((U.(filGen` ( fi ` (F u. {s}))) = U.u /\ (filGen` ( fi ` (F u. {s}))) C_ u) /\ (U.(filGen` ( fi ` (F u. {(X \ s)}))) = U.v /\ (filGen` ( fi ` (F u. {(X \ s)}))) C_ v))) -> (u e. UFil /\ (X = U.u /\ F C_ u)))
141		simplrr 455	. . . . . . . . . . . . . . . 16 |- (((((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) /\ (u e. UFil /\ v e. UFil)) /\ ((U.(filGen` ( fi ` (F u. {s}))) = U.u /\ (filGen` ( fi ` (F u. {s}))) C_ u) /\ (U.(filGen` ( fi ` (F u. {(X \ s)}))) = U.v /\ (filGen` ( fi ` (F u. {(X \ s)}))) C_ v))) -> v e. UFil)
142	1	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (F e. Fil -> X = U.F)
143		unisng 3194	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((X \ s) e. _V -> U.{(X \ s)} = (X \ s))
144	76, 77, 143	3syl 24	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (F e. Fil -> U.{(X \ s)} = (X \ s))
145	144	eqcomd 1889	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (F e. Fil -> (X \ s) = U.{(X \ s)})
146	142, 145	uneq12d 2756	. . . . . . . . . . . . . . . . . . . . . . 23 |- (F e. Fil -> (X u. (X \ s)) = (U.F u. U.{(X \ s)}))
147		difss 2735	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (X \ s) C_ X
148		ssequn2 2779	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((X \ s) C_ X <-> (X u. (X \ s)) = X)
149	147, 148	mpbi 206	. . . . . . . . . . . . . . . . . . . . . . 23 |- (X u. (X \ s)) = X
150	146, 149	syl5eqr 1942	. . . . . . . . . . . . . . . . . . . . . 22 |- (F e. Fil -> X = (U.F u. U.{(X \ s)}))
151		uniun 3196	. . . . . . . . . . . . . . . . . . . . . 22 |- U.(F u. {(X \ s)}) = (U.F u. U.{(X \ s)})
152	150, 151	syl6eqr 1946	. . . . . . . . . . . . . . . . . . . . 21 |- (F e. Fil -> X = U.(F u. {(X \ s)}))
153		fiuni 10219	. . . . . . . . . . . . . . . . . . . . . 22 |- ((F u. {(X \ s)}) e. _V -> U.(F u. {(X \ s)}) = U.( fi ` (F u. {(X \ s)})))
154	33, 153	syl 12	. . . . . . . . . . . . . . . . . . . . 21 |- (F e. Fil -> U.(F u. {(X \ s)}) = U.( fi ` (F u. {(X \ s)})))
155	152, 154	eqtrd 1925	. . . . . . . . . . . . . . . . . . . 20 |- (F e. Fil -> X = U.( fi ` (F u. {(X \ s)})))
156	155	ad2antrr 440	. . . . . . . . . . . . . . . . . . 19 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> X = U.( fi ` (F u. {(X \ s)})))
157		eqid 1884	. . . . . . . . . . . . . . . . . . . . 21 |- U.( fi ` (F u. {(X \ s)})) = U.( fi ` (F u. {(X \ s)}))
158	157	fgbas 10286	. . . . . . . . . . . . . . . . . . . 20 |- (( fi ` (F u. {(X \ s)})) e. fBas -> U.( fi ` (F u. {(X \ s)})) = U.(filGen` ( fi ` (F u. {(X \ s)}))))
159	99, 158	syl 12	. . . . . . . . . . . . . . . . . . 19 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> U.( fi ` (F u. {(X \ s)})) = U.(filGen` ( fi ` (F u. {(X \ s)}))))
160	156, 159	eqtrd 1925	. . . . . . . . . . . . . . . . . 18 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> X = U.(filGen` ( fi ` (F u. {(X \ s)}))))
161	160	ad2antrr 440	. . . . . . . . . . . . . . . . 17 |- (((((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) /\ (u e. UFil /\ v e. UFil)) /\ ((U.(filGen` ( fi ` (F u. {s}))) = U.u /\ (filGen` ( fi ` (F u. {s}))) C_ u) /\ (U.(filGen` ( fi ` (F u. {(X \ s)}))) = U.v /\ (filGen` ( fi ` (F u. {(X \ s)}))) C_ v))) -> X = U.(filGen` ( fi ` (F u. {(X \ s)}))))
162		simprrl 458	. . . . . . . . . . . . . . . . 17 |- (((((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) /\ (u e. UFil /\ v e. UFil)) /\ ((U.(filGen` ( fi ` (F u. {s}))) = U.u /\ (filGen` ( fi ` (F u. {s}))) C_ u) /\ (U.(filGen` ( fi ` (F u. {(X \ s)}))) = U.v /\ (filGen` ( fi ` (F u. {(X \ s)}))) C_ v))) -> U.(filGen` ( fi ` (F u. {(X \ s)}))) = U.v)
163	161, 162	eqtrd 1925	. . . . . . . . . . . . . . . 16 |- (((((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) /\ (u e. UFil /\ v e. UFil)) /\ ((U.(filGen` ( fi ` (F u. {s}))) = U.u /\ (filGen` ( fi ` (F u. {s}))) C_ u) /\ (U.(filGen` ( fi ` (F u. {(X \ s)}))) = U.v /\ (filGen` ( fi ` (F u. {(X \ s)}))) C_ v))) -> X = U.v)
164	39	a1i 8	. . . . . . . . . . . . . . . . . . . 20 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> F C_ (F u. {(X \ s)}))
165		abfi2 10216	. . . . . . . . . . . . . . . . . . . . . 22 |- ((F u. {(X \ s)}) e. _V -> (F u. {(X \ s)}) C_ ( fi ` (F u. {(X \ s)})))
166	33, 165	syl 12	. . . . . . . . . . . . . . . . . . . . 21 |- (F e. Fil -> (F u. {(X \ s)}) C_ ( fi ` (F u. {(X \ s)})))
167	166	ad2antrr 440	. . . . . . . . . . . . . . . . . . . 20 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> (F u. {(X \ s)}) C_ ( fi ` (F u. {(X \ s)})))
168	164, 167	sstrd 2627	. . . . . . . . . . . . . . . . . . 19 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> F C_ ( fi ` (F u. {(X \ s)})))
169		fbssfg 10285	. . . . . . . . . . . . . . . . . . . 20 |- (( fi ` (F u. {(X \ s)})) e. fBas -> ( fi ` (F u. {(X \ s)})) C_ (filGen` ( fi ` (F u. {(X \ s)}))))
170	99, 169	syl 12	. . . . . . . . . . . . . . . . . . 19 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> ( fi ` (F u. {(X \ s)})) C_ (filGen` ( fi ` (F u. {(X \ s)}))))
171	168, 170	sstrd 2627	. . . . . . . . . . . . . . . . . 18 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> F C_ (filGen` ( fi ` (F u. {(X \ s)}))))
172	171	ad2antrr 440	. . . . . . . . . . . . . . . . 17 |- (((((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) /\ (u e. UFil /\ v e. UFil)) /\ ((U.(filGen` ( fi ` (F u. {s}))) = U.u /\ (filGen` ( fi ` (F u. {s}))) C_ u) /\ (U.(filGen` ( fi ` (F u. {(X \ s)}))) = U.v /\ (filGen` ( fi ` (F u. {(X \ s)}))) C_ v))) -> F C_ (filGen` ( fi ` (F u. {(X \ s)}))))
173		simprrr 459	. . . . . . . . . . . . . . . . 17 |- (((((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) /\ (u e. UFil /\ v e. UFil)) /\ ((U.(filGen` ( fi ` (F u. {s}))) = U.u /\ (filGen` ( fi ` (F u. {s}))) C_ u) /\ (U.(filGen` ( fi ` (F u. {(X \ s)}))) = U.v /\ (filGen` ( fi ` (F u. {(X \ s)}))) C_ v))) -> (filGen` ( fi ` (F u. {(X \ s)}))) C_ v)
174	172, 173	sstrd 2627	. . . . . . . . . . . . . . . 16 |- (((((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) /\ (u e. UFil /\ v e. UFil)) /\ ((U.(filGen` ( fi ` (F u. {s}))) = U.u /\ (filGen` ( fi ` (F u. {s}))) C_ u) /\ (U.(filGen` ( fi ` (F u. {(X \ s)}))) = U.v /\ (filGen` ( fi ` (F u. {(X \ s)}))) C_ v))) -> F C_ v)
175	141, 163, 174	jca32 312	. . . . . . . . . . . . . . 15 |- (((((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) /\ (u e. UFil /\ v e. UFil)) /\ ((U.(filGen` ( fi ` (F u. {s}))) = U.u /\ (filGen` ( fi ` (F u. {s}))) C_ u) /\ (U.(filGen` ( fi ` (F u. {(X \ s)}))) = U.v /\ (filGen` ( fi ` (F u. {(X \ s)}))) C_ v))) -> (v e. UFil /\ (X = U.v /\ F C_ v)))
176		ufilfil 15566	. . . . . . . . . . . . . . . . . . 19 |- (u e. UFil -> u e. Fil)
177		filesn 10268	. . . . . . . . . . . . . . . . . . 19 |- (u e. Fil -> -. (/) e. u)
178	176, 177	syl 12	. . . . . . . . . . . . . . . . . 18 |- (u e. UFil -> -. (/) e. u)
179	178	adantr 425	. . . . . . . . . . . . . . . . 17 |- ((u e. UFil /\ v e. UFil) -> -. (/) e. u)
180	179	ad2antlr 441	. . . . . . . . . . . . . . . 16 |- (((((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) /\ (u e. UFil /\ v e. UFil)) /\ ((U.(filGen` ( fi ` (F u. {s}))) = U.u /\ (filGen` ( fi ` (F u. {s}))) C_ u) /\ (U.(filGen` ( fi ` (F u. {(X \ s)}))) = U.v /\ (filGen` ( fi ` (F u. {(X \ s)}))) C_ v))) -> -. (/) e. u)
181	176	ad2antrl 442	. . . . . . . . . . . . . . . . . . 19 |- ((((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) /\ (u e. UFil /\ v e. UFil)) -> u e. Fil)
182	181	ad2antrr 440	. . . . . . . . . . . . . . . . . 18 |- ((((((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) /\ (u e. UFil /\ v e. UFil)) /\ ((U.(filGen` ( fi ` (F u. {s}))) = U.u /\ (filGen` ( fi ` (F u. {s}))) C_ u) /\ (U.(filGen` ( fi ` (F u. {(X \ s)}))) = U.v /\ (filGen` ( fi ` (F u. {(X \ s)}))) C_ v))) /\ u = v) -> u e. Fil)
183		ssun2 2768	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- {s} C_ (F u. {s})
184	183	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> {s} C_ (F u. {s}))
185	184, 132	sstrd 2627	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> {s} C_ ( fi ` (F u. {s})))
186	185, 135	sstrd 2627	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> {s} C_ (filGen` ( fi ` (F u. {s}))))
187	186	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) /\ u e. UFil) /\ (U.(filGen` ( fi ` (F u. {s}))) = U.u /\ (filGen` ( fi ` (F u. {s}))) C_ u)) -> {s} C_ (filGen` ( fi ` (F u. {s}))))
188		simprr 451	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) /\ u e. UFil) /\ (U.(filGen` ( fi ` (F u. {s}))) = U.u /\ (filGen` ( fi ` (F u. {s}))) C_ u)) -> (filGen` ( fi ` (F u. {s}))) C_ u)
189	187, 188	sstrd 2627	. . . . . . . . . . . . . . . . . . . . . 22 |- (((((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) /\ u e. UFil) /\ (U.(filGen` ( fi ` (F u. {s}))) = U.u /\ (filGen` ( fi ` (F u. {s}))) C_ u)) -> {s} C_ u)
190	108	snid 3069	. . . . . . . . . . . . . . . . . . . . . . 23 |- s e. {s}
191	190	a1i 8	. . . . . . . . . . . . . . . . . . . . . 22 |- (((((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) /\ u e. UFil) /\ (U.(filGen` ( fi ` (F u. {s}))) = U.u /\ (filGen` ( fi ` (F u. {s}))) C_ u)) -> s e. {s})
192	189, 191	sseldd 2620	. . . . . . . . . . . . . . . . . . . . 21 |- (((((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) /\ u e. UFil) /\ (U.(filGen` ( fi ` (F u. {s}))) = U.u /\ (filGen` ( fi ` (F u. {s}))) C_ u)) -> s e. u)
193	192	adantlrr 435	. . . . . . . . . . . . . . . . . . . 20 |- (((((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) /\ (u e. UFil /\ v e. UFil)) /\ (U.(filGen` ( fi ` (F u. {s}))) = U.u /\ (filGen` ( fi ` (F u. {s}))) C_ u)) -> s e. u)
194	193	adantrr 431	. . . . . . . . . . . . . . . . . . 19 |- (((((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) /\ (u e. UFil /\ v e. UFil)) /\ ((U.(filGen` ( fi ` (F u. {s}))) = U.u /\ (filGen` ( fi ` (F u. {s}))) C_ u) /\ (U.(filGen` ( fi ` (F u. {(X \ s)}))) = U.v /\ (filGen` ( fi ` (F u. {(X \ s)}))) C_ v))) -> s e. u)
195	194	adantr 425	. . . . . . . . . . . . . . . . . 18 |- ((((((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) /\ (u e. UFil /\ v e. UFil)) /\ ((U.(filGen` ( fi ` (F u. {s}))) = U.u /\ (filGen` ( fi ` (F u. {s}))) C_ u) /\ (U.(filGen` ( fi ` (F u. {(X \ s)}))) = U.v /\ (filGen` ( fi ` (F u. {(X \ s)}))) C_ v))) /\ u = v) -> s e. u)
196		simprr 451	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) /\ v e. UFil) /\ (U.(filGen` ( fi ` (F u. {(X \ s)}))) = U.v /\ (filGen` ( fi ` (F u. {(X \ s)}))) C_ v)) -> (filGen` ( fi ` (F u. {(X \ s)}))) C_ v)
197		ssun2 2768	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- {(X \ s)} C_ (F u. {(X \ s)})
198	197	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> {(X \ s)} C_ (F u. {(X \ s)}))
199	198, 167	sstrd 2627	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> {(X \ s)} C_ ( fi ` (F u. {(X \ s)})))
200	199, 170	sstrd 2627	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> {(X \ s)} C_ (filGen` ( fi ` (F u. {(X \ s)}))))
201		snidg 3067	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((X \ s) e. _V -> (X \ s) e. {(X \ s)})
202	76, 77, 201	3syl 24	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (F e. Fil -> (X \ s) e. {(X \ s)})
203	202	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> (X \ s) e. {(X \ s)})
204	200, 203	sseldd 2620	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> (X \ s) e. (filGen` ( fi ` (F u. {(X \ s)}))))
205	204	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) /\ v e. UFil) /\ (U.(filGen` ( fi ` (F u. {(X \ s)}))) = U.v /\ (filGen` ( fi ` (F u. {(X \ s)}))) C_ v)) -> (X \ s) e. (filGen` ( fi ` (F u. {(X \ s)}))))
206	196, 205	sseldd 2620	. . . . . . . . . . . . . . . . . . . . . 22 |- (((((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) /\ v e. UFil) /\ (U.(filGen` ( fi ` (F u. {(X \ s)}))) = U.v /\ (filGen` ( fi ` (F u. {(X \ s)}))) C_ v)) -> (X \ s) e. v)
207	206	adantlrl 434	. . . . . . . . . . . . . . . . . . . . 21 |- (((((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) /\ (u e. UFil /\ v e. UFil)) /\ (U.(filGen` ( fi ` (F u. {(X \ s)}))) = U.v /\ (filGen` ( fi ` (F u. {(X \ s)}))) C_ v)) -> (X \ s) e. v)
208	207	adantrl 430	. . . . . . . . . . . . . . . . . . . 20 |- (((((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) /\ (u e. UFil /\ v e. UFil)) /\ ((U.(filGen` ( fi ` (F u. {s}))) = U.u /\ (filGen` ( fi ` (F u. {s}))) C_ u) /\ (U.(filGen` ( fi ` (F u. {(X \ s)}))) = U.v /\ (filGen` ( fi ` (F u. {(X \ s)}))) C_ v))) -> (X \ s) e. v)
209	208	adantr 425	. . . . . . . . . . . . . . . . . . 19 |- ((((((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) /\ (u e. UFil /\ v e. UFil)) /\ ((U.(filGen` ( fi ` (F u. {s}))) = U.u /\ (filGen` ( fi ` (F u. {s}))) C_ u) /\ (U.(filGen` ( fi ` (F u. {(X \ s)}))) = U.v /\ (filGen` ( fi ` (F u. {(X \ s)}))) C_ v))) /\ u = v) -> (X \ s) e. v)
210		simpr 350	. . . . . . . . . . . . . . . . . . 19 |- ((((((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) /\ (u e. UFil /\ v e. UFil)) /\ ((U.(filGen` ( fi ` (F u. {s}))) = U.u /\ (filGen` ( fi ` (F u. {s}))) C_ u) /\ (U.(filGen` ( fi ` (F u. {(X \ s)}))) = U.v /\ (filGen` ( fi ` (F u. {(X \ s)}))) C_ v))) /\ u = v) -> u = v)
211	209, 210	eleqtrrd 1974	. . . . . . . . . . . . . . . . . 18 |- ((((((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) /\ (u e. UFil /\ v e. UFil)) /\ ((U.(filGen` ( fi ` (F u. {s}))) = U.u /\ (filGen` ( fi ` (F u. {s}))) C_ u) /\ (U.(filGen` ( fi ` (F u. {(X \ s)}))) = U.v /\ (filGen` ( fi ` (F u. {(X \ s)}))) C_ v))) /\ u = v) -> (X \ s) e. u)
212		filint 10269	. . . . . . . . . . . . . . . . . 18 |- ((u e. Fil /\ s e. u /\ (X \ s) e. u) -> (s i^i (X \ s)) e. u)
213	182, 195, 211, 212	syl111anc 1100	. . . . . . . . . . . . . . . . 17 |- ((((((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) /\ (u e. UFil /\ v e. UFil)) /\ ((U.(filGen` ( fi ` (F u. {s}))) = U.u /\ (filGen` ( fi ` (F u. {s}))) C_ u) /\ (U.(filGen` ( fi ` (F u. {(X \ s)}))) = U.v /\ (filGen` ( fi ` (F u. {(X \ s)}))) C_ v))) /\ u = v) -> (s i^i (X \ s)) e. u)
214		difdisj 2945	. . . . . . . . . . . . . . . . 17 |- (s i^i (X \ s)) = (/)
215	213, 214	syl5eqelr 1976	. . . . . . . . . . . . . . . 16 |- ((((((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) /\ (u e. UFil /\ v e. UFil)) /\ ((U.(filGen` ( fi ` (F u. {s}))) = U.u /\ (filGen` ( fi ` (F u. {s}))) C_ u) /\ (U.(filGen` ( fi ` (F u. {(X \ s)}))) = U.v /\ (filGen` ( fi ` (F u. {(X \ s)}))) C_ v))) /\ u = v) -> (/) e. u)
216	180, 215	mtand 520	. . . . . . . . . . . . . . 15 |- (((((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) /\ (u e. UFil /\ v e. UFil)) /\ ((U.(filGen` ( fi ` (F u. {s}))) = U.u /\ (filGen` ( fi ` (F u. {s}))) C_ u) /\ (U.(filGen` ( fi ` (F u. {(X \ s)}))) = U.v /\ (filGen` ( fi ` (F u. {(X \ s)}))) C_ v))) -> -. u = v)
217		visset 2295	. . . . . . . . . . . . . . . 16 |- u e. _V
218		visset 2295	. . . . . . . . . . . . . . . 16 |- v e. _V
219		eleq1 1957	. . . . . . . . . . . . . . . . . . . 20 |- (f = u -> (f e. UFil <-> u e. UFil))
220		unieq 3185	. . . . . . . . . . . . . . . . . . . . . 22 |- (f = u -> U.f = U.u)
221	220	eqeq2d 1895	. . . . . . . . . . . . . . . . . . . . 21 |- (f = u -> (X = U.f <-> X = U.u))
222		sseq2 2639	. . . . . . . . . . . . . . . . . . . . 21 |- (f = u -> (F C_ f <-> F C_ u))
223	221, 222	anbi12d 690	. . . . . . . . . . . . . . . . . . . 20 |- (f = u -> ((X = U.f /\ F C_ f) <-> (X = U.u /\ F C_ u)))
224	219, 223	anbi12d 690	. . . . . . . . . . . . . . . . . . 19 |- (f = u -> ((f e. UFil /\ (X = U.f /\ F C_ f)) <-> (u e. UFil /\ (X = U.u /\ F C_ u))))
225	224	anbi1d 679	. . . . . . . . . . . . . . . . . 18 |- (f = u -> (((f e. UFil /\ (X = U.f /\ F C_ f)) /\ (g e. UFil /\ (X = U.g /\ F C_ g))) <-> ((u e. UFil /\ (X = U.u /\ F C_ u)) /\ (g e. UFil /\ (X = U.g /\ F C_ g)))))
226		eqeq1 1890	. . . . . . . . . . . . . . . . . . 19 |- (f = u -> (f = g <-> u = g))
227	226	notbid 673	. . . . . . . . . . . . . . . . . 18 |- (f = u -> (-. f = g <-> -. u = g))
228	225, 227	anbi12d 690	. . . . . . . . . . . . . . . . 17 |- (f = u -> ((((f e. UFil /\ (X = U.f /\ F C_ f)) /\ (g e. UFil /\ (X = U.g /\ F C_ g))) /\ -. f = g) <-> (((u e. UFil /\ (X = U.u /\ F C_ u)) /\ (g e. UFil /\ (X = U.g /\ F C_ g))) /\ -. u = g)))
229		eleq1 1957	. . . . . . . . . . . . . . . . . . . 20 |- (g = v -> (g e. UFil <-> v e. UFil))
230		unieq 3185	. . . . . . . . . . . . . . . . . . . . . 22 |- (g = v -> U.g = U.v)
231	230	eqeq2d 1895	. . . . . . . . . . . . . . . . . . . . 21 |- (g = v -> (X = U.g <-> X = U.v))
232		sseq2 2639	. . . . . . . . . . . . . . . . . . . . 21 |- (g = v -> (F C_ g <-> F C_ v))
233	231, 232	anbi12d 690	. . . . . . . . . . . . . . . . . . . 20 |- (g = v -> ((X = U.g /\ F C_ g) <-> (X = U.v /\ F C_ v)))
234	229, 233	anbi12d 690	. . . . . . . . . . . . . . . . . . 19 |- (g = v -> ((g e. UFil /\ (X = U.g /\ F C_ g)) <-> (v e. UFil /\ (X = U.v /\ F C_ v))))
235	234	anbi2d 678	. . . . . . . . . . . . . . . . . 18 |- (g = v -> (((u e. UFil /\ (X = U.u /\ F C_ u)) /\ (g e. UFil /\ (X = U.g /\ F C_ g))) <-> ((u e. UFil /\ (X = U.u /\ F C_ u)) /\ (v e. UFil /\ (X = U.v /\ F C_ v)))))
236		eqeq2 1893	. . . . . . . . . . . . . . . . . . 19 |- (g = v -> (u = g <-> u = v))
237	236	notbid 673	. . . . . . . . . . . . . . . . . 18 |- (g = v -> (-. u = g <-> -. u = v))
238	235, 237	anbi12d 690	. . . . . . . . . . . . . . . . 17 |- (g = v -> ((((u e. UFil /\ (X = U.u /\ F C_ u)) /\ (g e. UFil /\ (X = U.g /\ F C_ g))) /\ -. u = g) <-> (((u e. UFil /\ (X = U.u /\ F C_ u)) /\ (v e. UFil /\ (X = U.v /\ F C_ v))) /\ -. u = v)))
239	228, 238	sylan9bb 599	. . . . . . . . . . . . . . . 16 |- ((f = u /\ g = v) -> ((((f e. UFil /\ (X = U.f /\ F C_ f)) /\ (g e. UFil /\ (X = U.g /\ F C_ g))) /\ -. f = g) <-> (((u e. UFil /\ (X = U.u /\ F C_ u)) /\ (v e. UFil /\ (X = U.v /\ F C_ v))) /\ -. u = v)))
240	217, 218, 239	cla42ev 2372	. . . . . . . . . . . . . . 15 |- ((((u e. UFil /\ (X = U.u /\ F C_ u)) /\ (v e. UFil /\ (X = U.v /\ F C_ v))) /\ -. u = v) -> E.fE.g(((f e. UFil /\ (X = U.f /\ F C_ f)) /\ (g e. UFil /\ (X = U.g /\ F C_ g))) /\ -. f = g))
241	140, 175, 216, 240	syl21anc 1099	. . . . . . . . . . . . . 14 |- (((((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) /\ (u e. UFil /\ v e. UFil)) /\ ((U.(filGen` ( fi ` (F u. {s}))) = U.u /\ (filGen` ( fi ` (F u. {s}))) C_ u) /\ (U.(filGen` ( fi ` (F u. {(X \ s)}))) = U.v /\ (filGen` ( fi ` (F u. {(X \ s)}))) C_ v))) -> E.fE.g(((f e. UFil /\ (X = U.f /\ F C_ f)) /\ (g e. UFil /\ (X = U.g /\ F C_ g))) /\ -. f = g))
242	241	exp31 407	. . . . . . . . . . . . 13 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> ((u e. UFil /\ v e. UFil) -> (((U.(filGen` ( fi ` (F u. {s}))) = U.u /\ (filGen` ( fi ` (F u. {s}))) C_ u) /\ (U.(filGen` ( fi ` (F u. {(X \ s)}))) = U.v /\ (filGen` ( fi ` (F u. {(X \ s)}))) C_ v)) -> E.fE.g(((f e. UFil /\ (X = U.f /\ F C_ f)) /\ (g e. UFil /\ (X = U.g /\ F C_ g))) /\ -. f = g))))
243	242	r19.23advv 2218	. . . . . . . . . . . 12 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> (E.u e. UFil E.v e. UFil ((U.(filGen` ( fi ` (F u. {s}))) = U.u /\ (filGen` ( fi ` (F u. {s}))) C_ u) /\ (U.(filGen` ( fi ` (F u. {(X \ s)}))) = U.v /\ (filGen` ( fi ` (F u. {(X \ s)}))) C_ v)) -> E.fE.g(((f e. UFil /\ (X = U.f /\ F C_ f)) /\ (g e. UFil /\ (X = U.g /\ F C_ g))) /\ -. f = g)))
244		reeanv 2249	. . . . . . . . . . . 12 |- (E.u e. UFil E.v e. UFil ((U.(filGen` ( fi ` (F u. {s}))) = U.u /\ (filGen` ( fi ` (F u. {s}))) C_ u) /\ (U.(filGen` ( fi ` (F u. {(X \ s)}))) = U.v /\ (filGen` ( fi ` (F u. {(X \ s)}))) C_ v)) <-> (E.u e. UFil (U.(filGen` ( fi ` (F u. {s}))) = U.u /\ (filGen` ( fi ` (F u. {s}))) C_ u) /\ E.v e. UFil (U.(filGen` ( fi ` (F u. {(X \ s)}))) = U.v /\ (filGen` ( fi ` (F u. {(X \ s)}))) C_ v)))
245	243, 244	syl5ibr 224	. . . . . . . . . . 11 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> ((E.u e. UFil (U.(filGen` ( fi ` (F u. {s}))) = U.u /\ (filGen` ( fi ` (F u. {s}))) C_ u) /\ E.v e. UFil (U.(filGen` ( fi ` (F u. {(X \ s)}))) = U.v /\ (filGen` ( fi ` (F u. {(X \ s)}))) C_ v)) -> E.fE.g(((f e. UFil /\ (X = U.f /\ F C_ f)) /\ (g e. UFil /\ (X = U.g /\ F C_ g))) /\ -. f = g)))
246	30, 103, 245	mp2and 767	. . . . . . . . . 10 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> E.fE.g(((f e. UFil /\ (X = U.f /\ F C_ f)) /\ (g e. UFil /\ (X = U.g /\ F C_ g))) /\ -. f = g))
247	246	exp31 407	. . . . . . . . 9 |- (F e. Fil -> (s C_ X -> ((-. s e. F /\ -. (X \ s) e. F) -> E.fE.g(((f e. UFil /\ (X = U.f /\ F C_ f)) /\ (g e. UFil /\ (X = U.g /\ F C_ g))) /\ -. f = g))))
248	108	elpw 3037	. . . . . . . . 9 |- (s e. ~PX <-> s C_ X)
249	247, 248	syl5ib 223	. . . . . . . 8 |- (F e. Fil -> (s e. ~PX -> ((-. s e. F /\ -. (X \ s) e. F) -> E.fE.g(((f e. UFil /\ (X = U.f /\ F C_ f)) /\ (g e. UFil /\ (X = U.g /\ F C_ g))) /\ -. f = g))))
250	249	r19.23adv 2215	. . . . . . 7 |- (F e. Fil -> (E.s e. ~P X(-. s e. F /\ -. (X \ s) e. F) -> E.fE.g(((f e. UFil /\ (X = U.f /\ F C_ f)) /\ (g e. UFil /\ (X = U.g /\ F C_ g))) /\ -. f = g)))
251		rexnal 2114	. . . . . . . 8 |- (E.s e. ~P X -. (s e. F \/ (X \ s) e. F) <-> -. A.s e. ~P X(s e. F \/ (X \ s) e. F))
252		ioran 331	. . . . . . . . 9 |- (-. (s e. F \/ (X \ s) e. F) <-> (-. s e. F /\ -. (X \ s) e. F))
253	252	rexbii 2128	. . . . . . . 8 |- (E.s e. ~P X -. (s e. F \/ (X \ s) e. F) <-> E.s e. ~P X(-. s e. F /\ -. (X \ s) e. F))
254	251, 253	bitr3i 192	. . . . . . 7 |- (-. A.s e. ~P X(s e. F \/ (X \ s) e. F) <-> E.s e. ~P X(-. s e. F /\ -. (X \ s) e. F))
255		eleq1 1957	. . . . . . . . . . 11 |- (f = g -> (f e. UFil <-> g e. UFil))
256		unieq 3185	. . . . . . . . . . . . 13 |- (f = g -> U.f = U.g)
257	256	eqeq2d 1895	. . . . . . . . . . . 12 |- (f = g -> (X = U.f <-> X = U.g))
258		sseq2 2639	. . . . . . . . . . . 12 |- (f = g -> (F C_ f <-> F C_ g))
259	257, 258	anbi12d 690	. . . . . . . . . . 11 |- (f = g -> ((X = U.f /\ F C_ f) <-> (X = U.g /\ F C_ g)))
260	255, 259	anbi12d 690	. . . . . . . . . 10 |- (f = g -> ((f e. UFil /\ (X = U.f /\ F C_ f)) <-> (g e. UFil /\ (X = U.g /\ F C_ g))))
261	260	mo4 1799	. . . . . . . . 9 |- (E*f(f e. UFil /\ (X = U.f /\ F C_ f)) <-> A.fA.g(((f e. UFil /\ (X = U.f /\ F C_ f)) /\ (g e. UFil /\ (X = U.g /\ F C_ g))) -> f = g))
262	261	notbii 204	. . . . . . . 8 |- (-. E*f(f e. UFil /\ (X = U.f /\ F C_ f)) <-> -. A.fA.g(((f e. UFil /\ (X = U.f /\ F C_ f)) /\ (g e. UFil /\ (X = U.g /\ F C_ g))) -> f = g))
263		exnal 1385	. . . . . . . 8 |- (E.f -. A.g(((f e. UFil /\ (X = U.f /\ F C_ f)) /\ (g e. UFil /\ (X = U.g /\ F C_ g))) -> f = g) <-> -. A.fA.g(((f e. UFil /\ (X = U.f /\ F C_ f)) /\ (g e. UFil /\ (X = U.g /\ F C_ g))) -> f = g))
264		annim 257	. . . . . . . . . . 11 |- ((((f e. UFil /\ (X = U.f /\ F C_ f)) /\ (g e. UFil /\ (X = U.g /\ F C_ g))) /\ -. f = g) <-> -. (((f e. UFil /\ (X = U.f /\ F C_ f)) /\ (g e. UFil /\ (X = U.g /\ F C_ g))) -> f = g))
265	264	exbii 1398	. . . . . . . . . 10 |- (E.g(((f e. UFil /\ (X = U.f /\ F C_ f)) /\ (g e. UFil /\ (X = U.g /\ F C_ g))) /\ -. f = g) <-> E.g -. (((f e. UFil /\ (X = U.f /\ F C_ f)) /\ (g e. UFil /\ (X = U.g /\ F C_ g))) -> f = g))
266		exnal 1385	. . . . . . . . . 10 |- (E.g -. (((f e. UFil /\ (X = U.f /\ F C_ f)) /\ (g e. UFil /\ (X = U.g /\ F C_ g))) -> f = g) <-> -. A.g(((f e. UFil /\ (X = U.f /\ F C_ f)) /\ (g e. UFil /\ (X = U.g /\ F C_ g))) -> f = g))
267	265, 266	bitr2i 191	. . . . . . . . 9 |- (-. A.g(((f e. UFil /\ (X = U.f /\ F C_ f)) /\ (g e. UFil /\ (X = U.g /\ F C_ g))) -> f = g) <-> E.g(((f e. UFil /\ (X = U.f /\ F C_ f)) /\ (g e. UFil /\ (X = U.g /\ F C_ g))) /\ -. f = g))
268	267	exbii 1398	. . . . . . . 8 |- (E.f -. A.g(((f e. UFil /\ (X = U.f /\ F C_ f)) /\ (g e. UFil /\ (X = U.g /\ F C_ g))) -> f = g) <-> E.fE.g(((f e. UFil /\ (X = U.f /\ F C_ f)) /\ (g e. UFil /\ (X = U.g /\ F C_ g))) /\ -. f = g))
269	262, 263, 268	3bitr2i 196	. . . . . . 7 |- (-. E*f(f e. UFil /\ (X = U.f /\ F C_ f)) <-> E.fE.g(((f e. UFil /\ (X = U.f /\ F C_ f)) /\ (g e. UFil /\ (X = U.g /\ F C_ g))) /\ -. f = g))
270	250, 254, 269	3imtr4g 612	. . . . . 6 |- (F e. Fil -> (-. A.s e. ~P X(s e. F \/ (X \ s) e. F) -> -. E*f(f e. UFil /\ (X = U.f /\ F C_ f))))
271		eumo 1807	. . . . . . 7 |- (E!f(f e. UFil /\ (X = U.f /\ F C_ f)) -> E*f(f e. UFil /\ (X = U.f /\ F C_ f)))
272	271	a1i 8	. . . . . 6 |- (F e. Fil -> (E!f(f e. UFil /\ (X = U.f /\ F C_ f)) -> E*f(f e. UFil /\ (X = U.f /\ F C_ f))))
273	270, 272	nsyld 132	. . . . 5 |- (F e. Fil -> (-. A.s e. ~P X(s e. F \/ (X \ s) e. F) -> -. E!f(f e. UFil /\ (X = U.f /\ F C_ f))))
274	273	con4d 91	. . . 4 |- (F e. Fil -> (E!f(f e. UFil /\ (X = U.f /\ F C_ f)) -> A.s e. ~P X(s e. F \/ (X \ s) e. F)))
275		df-reu 2111	. . . 4 |- (E!f e. UFil (X = U.f /\ F C_ f) <-> E!f(f e. UFil /\ (X = U.f /\ F C_ f)))
276	274, 275	syl5ib 223	. . 3 |- (F e. Fil -> (E!f e. UFil (X = U.f /\ F C_ f) -> A.s e. ~P X(s e. F \/ (X \ s) e. F)))
277	1	isufil 15564	. . . 4 |- (F e. UFil <-> (F e. Fil /\ A.s e. ~P X(s e. F \/ (X \ s) e. F)))
278	277	baibr 750	. . 3 |- (F e. Fil -> (A.s e. ~P X(s e. F \/ (X \ s) e. F) <-> F e. UFil))
279	276, 278	sylibd 219	. 2 |- (F e. Fil -> (E!f e. UFil (X = U.f /\ F C_ f) -> F e. UFil))
280	25, 279	impbid2 576	1 |- (F e. Fil -> (F e. UFil <-> E!f e. UFil (X = U.f /\ F C_ f)))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   \/ wo 239   /\ wa 240  A.wal 1296   = wceq 1298   e. wcel 1300  E.wex 1326  E!weu 1771  E*wmo 1772   =/= wne 2017   e/ wnel 2018  A.wral 2105  E.wrex 2106  E!wreu 2107  _Vcvv 2292   \ cdif 2590   u. cun 2591   i^i cin 2592   C_ wss 2593  (/)c0 2875  ~Pcpw 3032  {csn 3044  U.cuni 3177  ` cfv 3998   fi cfi 10210  fBascfbas 10257  filGencfg 10258  Filcfil 10264  UFilcufil 15562

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