Theorem ufileu 16658

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		ufilfil 16651	. . . . . . 7 |- (f e. UFil -> f e. Fil)
2		ufileu.1	. . . . . . . . . 10 |- X = U.F
3		eqid 2170	. . . . . . . . . 10 |- U.f = U.f
4	2, 3	ufilmax 16653	. . . . . . . . 9 |- (((F e. UFil /\ f e. Fil) /\ (X = U.f /\ F C_ f)) -> F = f)
5	4	eqcomd 2175	. . . . . . . 8 |- (((F e. UFil /\ f e. Fil) /\ (X = U.f /\ F C_ f)) -> f = F)
6	5	ex 494	. . . . . . 7 |- ((F e. UFil /\ f e. Fil) -> ((X = U.f /\ F C_ f) -> f = F))
7	1, 6	sylan2 696	. . . . . 6 |- ((F e. UFil /\ f e. UFil) -> ((X = U.f /\ F C_ f) -> f = F))
8		eqid 2170	. . . . . . . 8 |- X = X
9		ssid 2895	. . . . . . . 8 |- F C_ F
10	8, 9	pm3.2i 514	. . . . . . 7 |- (X = X /\ F C_ F)
11		unieq 3407	. . . . . . . . . 10 |- (f = F -> U.f = U.F)
12	11, 2	syl6eqr 2224	. . . . . . . . 9 |- (f = F -> U.f = X)
13	12	eqeq2d 2181	. . . . . . . 8 |- (f = F -> (X = U.f <-> X = X))
14		sseq2 2898	. . . . . . . 8 |- (f = F -> (F C_ f <-> F C_ F))
15	13, 14	anbi12d 821	. . . . . . 7 |- (f = F -> ((X = U.f /\ F C_ f) <-> (X = X /\ F C_ F)))
16	10, 15	mpbiri 260	. . . . . 6 |- (f = F -> (X = U.f /\ F C_ f))
17	7, 16	impbid1 251	. . . . 5 |- ((F e. UFil /\ f e. UFil) -> ((X = U.f /\ F C_ f) <-> f = F))
18	17	r19.21aiva 2456	. . . 4 |- (F e. UFil -> A.f e. UFil ((X = U.f /\ F C_ f) <-> f = F))
19		eqeq2 2179	. . . . . . 7 |- (g = F -> (f = g <-> f = F))
20	19	bibi2d 382	. . . . . 6 |- (g = F -> (((X = U.f /\ F C_ f) <-> f = g) <-> ((X = U.f /\ F C_ f) <-> f = F)))
21	20	ralbidv 2403	. . . . 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 2651	. . . 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 769	. . 3 |- (F e. UFil -> E.g e. UFil A.f e. UFil ((X = U.f /\ F C_ f) <-> f = g))
24		reu6 2720	. . 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 264	. 2 |- (F e. UFil -> E!f e. UFil (X = U.f /\ F C_ f))
26		df-reu 2391	. . . 4 |- (E!f e. UFil (X = U.f /\ F C_ f) <-> E!f(f e. UFil /\ (X = U.f /\ F C_ f)))
27		visset 2572	. . . . . . . . . 10 |- s e. _V
28	27	elpw 3263	. . . . . . . . 9 |- (s e. ~PX <-> s C_ X)
29	2	ufileulem 16657	. . . . . . . . . . . 12 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> ( fi ` (F u. {s})) e. fBas)
30		fgfil 11286	. . . . . . . . . . . 12 |- (( fi ` (F u. {s})) e. fBas -> (filGen` ( fi ` (F u. {s}))) e. Fil)
31		eqid 2170	. . . . . . . . . . . . 13 |- U.(filGen` ( fi ` (F u. {s}))) = U.(filGen` ( fi ` (F u. {s})))
32	31	filssufil 16656	. . . . . . . . . . . 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))
33	29, 30, 32	3syl 38	. . . . . . . . . . 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))
34		snex 3689	. . . . . . . . . . . . . . . 16 |- {(X \ s)} e. _V
35		unexg 3969	. . . . . . . . . . . . . . . 16 |- ((F e. Fil /\ {(X \ s)} e. _V) -> (F u. {(X \ s)}) e. _V)
36	34, 35	mpan2 775	. . . . . . . . . . . . . . 15 |- (F e. Fil -> (F u. {(X \ s)}) e. _V)
37		fsubbas 11277	. . . . . . . . . . . . . . 15 |- ((F u. {(X \ s)}) e. _V -> (( fi ` (F u. {(X \ s)})) e. fBas <-> ((F u. {(X \ s)}) =/= (/) /\ (/) e/ ( fi ` (F u. {(X \ s)})))))
38	36, 37	syl 13	. . . . . . . . . . . . . 14 |- (F e. Fil -> (( fi ` (F u. {(X \ s)})) e. fBas <-> ((F u. {(X \ s)}) =/= (/) /\ (/) e/ ( fi ` (F u. {(X \ s)})))))
39	38	ad2antrr 856	. . . . . . . . . . . . 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)})))))
40	2	filusb 11263	. . . . . . . . . . . . . . 15 |- (F e. Fil -> X e. F)
41		ne0i 3120	. . . . . . . . . . . . . . 15 |- (X e. F -> F =/= (/))
42		ssun1 3014	. . . . . . . . . . . . . . . 16 |- F C_ (F u. {(X \ s)})
43		ssn0 3143	. . . . . . . . . . . . . . . 16 |- ((F C_ (F u. {(X \ s)}) /\ F =/= (/)) -> (F u. {(X \ s)}) =/= (/))
44	42, 43	mpan 773	. . . . . . . . . . . . . . 15 |- (F =/= (/) -> (F u. {(X \ s)}) =/= (/))
45	40, 41, 44	3syl 38	. . . . . . . . . . . . . 14 |- (F e. Fil -> (F u. {(X \ s)}) =/= (/))
46	45	ad2antrr 856	. . . . . . . . . . . . 13 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> (F u. {(X \ s)}) =/= (/))
47		elsn 3283	. . . . . . . . . . . . . . . . . 18 |- (y e. {(X \ s)} <-> y = (X \ s))
48		elssuni 3424	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (x e. F -> x C_ U.F)
49	48, 2	syl6sseqr 2925	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (x e. F -> x C_ X)
50		reldisj 3153	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (x C_ X -> ((x i^i (X \ s)) = (/) <-> x C_ (X \ (X \ s))))
51	49, 50	syl 13	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (x e. F -> ((x i^i (X \ s)) = (/) <-> x C_ (X \ (X \ s))))
52	51	adantl 544	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((F e. Fil /\ s C_ X) /\ x e. F) -> ((x i^i (X \ s)) = (/) <-> x C_ (X \ (X \ s))))
53		dfss4 3070	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (s C_ X <-> (X \ (X \ s)) = s)
54	53	biimpi 236	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (s C_ X -> (X \ (X \ s)) = s)
55	54	sseq2d 2904	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (s C_ X -> (x C_ (X \ (X \ s)) <-> x C_ s))
56	55	ad2antlr 859	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((F e. Fil /\ s C_ X) /\ x e. F) -> (x C_ (X \ (X \ s)) <-> x C_ s))
57	52, 56	bitrd 311	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((F e. Fil /\ s C_ X) /\ x e. F) -> ((x i^i (X \ s)) = (/) <-> x C_ s))
58	2	fillsb 11266	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (F e. Fil -> ((x e. F /\ s C_ X /\ x C_ s) -> s e. F))
59	58	3expd 1362	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (F e. Fil -> (x e. F -> (s C_ X -> (x C_ s -> s e. F))))
60	59	com23 68	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (F e. Fil -> (s C_ X -> (x e. F -> (x C_ s -> s e. F))))
61	60	imp31 492	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((F e. Fil /\ s C_ X) /\ x e. F) -> (x C_ s -> s e. F))
62	57, 61	sylbid 267	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((F e. Fil /\ s C_ X) /\ x e. F) -> ((x i^i (X \ s)) = (/) -> s e. F))
63	62	necon3bd 2331	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((F e. Fil /\ s C_ X) /\ x e. F) -> (-. s e. F -> (x i^i (X \ s)) =/= (/)))
64	63	ex 494	. . . . . . . . . . . . . . . . . . . . . 22 |- ((F e. Fil /\ s C_ X) -> (x e. F -> (-. s e. F -> (x i^i (X \ s)) =/= (/))))
65	64	com23 68	. . . . . . . . . . . . . . . . . . . . 21 |- ((F e. Fil /\ s C_ X) -> (-. s e. F -> (x e. F -> (x i^i (X \ s)) =/= (/))))
66	65	imp 489	. . . . . . . . . . . . . . . . . . . 20 |- (((F e. Fil /\ s C_ X) /\ -. s e. F) -> (x e. F -> (x i^i (X \ s)) =/= (/)))
67	66	adantrr 838	. . . . . . . . . . . . . . . . . . 19 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> (x e. F -> (x i^i (X \ s)) =/= (/)))
68		ineq2 3035	. . . . . . . . . . . . . . . . . . . . 21 |- (y = (X \ s) -> (x i^i y) = (x i^i (X \ s)))
69	68	neeq1d 2307	. . . . . . . . . . . . . . . . . . . 20 |- (y = (X \ s) -> ((x i^i y) =/= (/) <-> (x i^i (X \ s)) =/= (/)))
70	69	imbi2d 380	. . . . . . . . . . . . . . . . . . 19 |- (y = (X \ s) -> ((x e. F -> (x i^i y) =/= (/)) <-> (x e. F -> (x i^i (X \ s)) =/= (/))))
71	67, 70	syl5ibrcom 279	. . . . . . . . . . . . . . . . . 18 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> (y = (X \ s) -> (x e. F -> (x i^i y) =/= (/))))
72	47, 71	syl5bi 270	. . . . . . . . . . . . . . . . 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) =/= (/))))
73	72	com23 68	. . . . . . . . . . . . . . . 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) =/= (/))))
74	73	imp3a 491	. . . . . . . . . . . . . . 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) =/= (/)))
75	74	r19.21aivv 2463	. . . . . . . . . . . . . 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) =/= (/))
76		filfbas 11272	. . . . . . . . . . . . . . . 16 |- (F e. Fil -> F e. fBas)
77	76	ad2antrr 856	. . . . . . . . . . . . . . 15 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> F e. fBas)
78		uniexg 3966	. . . . . . . . . . . . . . . . . . . 20 |- (F e. Fil -> U.F e. _V)
79	2, 78	syl5eqel 2251	. . . . . . . . . . . . . . . . . . 19 |- (F e. Fil -> X e. _V)
80		difexg 3657	. . . . . . . . . . . . . . . . . . 19 |- (X e. _V -> (X \ s) e. _V)
81	79, 80	syl 13	. . . . . . . . . . . . . . . . . 18 |- (F e. Fil -> (X \ s) e. _V)
82	81	ad2antrr 856	. . . . . . . . . . . . . . . . 17 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> (X \ s) e. _V)
83	54	eqcomd 2175	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (s C_ X -> s = (X \ (X \ s)))
84	83	adantl 544	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((F e. Fil /\ s C_ X) -> s = (X \ (X \ s)))
85		difeq2 2972	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((X \ s) = (/) -> (X \ (X \ s)) = (X \ (/)))
86	84, 85	sylan9eq 2226	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((F e. Fil /\ s C_ X) /\ (X \ s) = (/)) -> s = (X \ (/)))
87		dif0 3176	. . . . . . . . . . . . . . . . . . . . . . 23 |- (X \ (/)) = X
88	86, 87	syl6eq 2222	. . . . . . . . . . . . . . . . . . . . . 22 |- (((F e. Fil /\ s C_ X) /\ (X \ s) = (/)) -> s = X)
89	40	ad2antrr 856	. . . . . . . . . . . . . . . . . . . . . 22 |- (((F e. Fil /\ s C_ X) /\ (X \ s) = (/)) -> X e. F)
90	88, 89	eqeltrd 2247	. . . . . . . . . . . . . . . . . . . . 21 |- (((F e. Fil /\ s C_ X) /\ (X \ s) = (/)) -> s e. F)
91	90	ex 494	. . . . . . . . . . . . . . . . . . . 20 |- ((F e. Fil /\ s C_ X) -> ((X \ s) = (/) -> s e. F))
92	91	necon3bd 2331	. . . . . . . . . . . . . . . . . . 19 |- ((F e. Fil /\ s C_ X) -> (-. s e. F -> (X \ s) =/= (/)))
93	92	imp 489	. . . . . . . . . . . . . . . . . 18 |- (((F e. Fil /\ s C_ X) /\ -. s e. F) -> (X \ s) =/= (/))
94	93	adantrr 838	. . . . . . . . . . . . . . . . 17 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> (X \ s) =/= (/))
95		oefil2 11271	. . . . . . . . . . . . . . . . 17 |- (((X \ s) e. _V /\ (X \ s) =/= (/)) -> {(X \ s)} e. Fil)
96	82, 94, 95	syl11anc 755	. . . . . . . . . . . . . . . 16 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> {(X \ s)} e. Fil)
97		filfbas 11272	. . . . . . . . . . . . . . . 16 |- ({(X \ s)} e. Fil -> {(X \ s)} e. fBas)
98	96, 97	syl 13	. . . . . . . . . . . . . . 15 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> {(X \ s)} e. fBas)
99		fbunfip 11278	. . . . . . . . . . . . . . 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) =/= (/)))
100	77, 98, 99	syl11anc 755	. . . . . . . . . . . . . 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) =/= (/)))
101	75, 100	mpbird 257	. . . . . . . . . . . . 13 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> (/) e/ ( fi ` (F u. {(X \ s)})))
102	39, 46, 101	mpbir2and 1065	. . . . . . . . . . . 12 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> ( fi ` (F u. {(X \ s)})) e. fBas)
103		fgfil 11286	. . . . . . . . . . . 12 |- (( fi ` (F u. {(X \ s)})) e. fBas -> (filGen` ( fi ` (F u. {(X \ s)}))) e. Fil)
104		eqid 2170	. . . . . . . . . . . . 13 |- U.(filGen` ( fi ` (F u. {(X \ s)}))) = U.(filGen` ( fi ` (F u. {(X \ s)})))
105	104	filssufil 16656	. . . . . . . . . . . 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))
106	102, 103, 105	3syl 38	. . . . . . . . . . 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))
107		reeanv 2524	. . . . . . . . . . . 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)))
108		simplrl 873	. . . . . . . . . . . . . . . 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)
109	27	unisn 3414	. . . . . . . . . . . . . . . . . . . . . . 23 |- U.{s} = s
110	109	eqcomi 2174	. . . . . . . . . . . . . . . . . . . . . 22 |- s = U.{s}
111	2, 110	uneq12i 3003	. . . . . . . . . . . . . . . . . . . . 21 |- (X u. s) = (U.F u. U.{s})
112		simplr 868	. . . . . . . . . . . . . . . . . . . . . 22 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> s C_ X)
113		ssequn2 3024	. . . . . . . . . . . . . . . . . . . . . 22 |- (s C_ X <-> (X u. s) = X)
114	112, 113	sylib 263	. . . . . . . . . . . . . . . . . . . . 21 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> (X u. s) = X)
115	111, 114	syl5reqr 2220	. . . . . . . . . . . . . . . . . . . 20 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> X = (U.F u. U.{s}))
116		uniun 3417	. . . . . . . . . . . . . . . . . . . 20 |- U.(F u. {s}) = (U.F u. U.{s})
117	115, 116	syl6eqr 2224	. . . . . . . . . . . . . . . . . . 19 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> X = U.(F u. {s}))
118		snex 3689	. . . . . . . . . . . . . . . . . . . . . 22 |- {s} e. _V
119		unexg 3969	. . . . . . . . . . . . . . . . . . . . . 22 |- ((F e. Fil /\ {s} e. _V) -> (F u. {s}) e. _V)
120	118, 119	mpan2 775	. . . . . . . . . . . . . . . . . . . . 21 |- (F e. Fil -> (F u. {s}) e. _V)
121	120	ad2antrr 856	. . . . . . . . . . . . . . . . . . . 20 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> (F u. {s}) e. _V)
122		fiuni 11212	. . . . . . . . . . . . . . . . . . . 20 |- ((F u. {s}) e. _V -> U.(F u. {s}) = U.( fi ` (F u. {s})))
123	121, 122	syl 13	. . . . . . . . . . . . . . . . . . 19 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> U.(F u. {s}) = U.( fi ` (F u. {s})))
124		eqid 2170	. . . . . . . . . . . . . . . . . . . . 21 |- U.( fi ` (F u. {s})) = U.( fi ` (F u. {s}))
125	124	fgbas 11282	. . . . . . . . . . . . . . . . . . . 20 |- (( fi ` (F u. {s})) e. fBas -> U.( fi ` (F u. {s})) = U.(filGen` ( fi ` (F u. {s}))))
126	29, 125	syl 13	. . . . . . . . . . . . . . . . . . 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}))))
127	117, 123, 126	3eqtrd 2206	. . . . . . . . . . . . . . . . . 18 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> X = U.(filGen` ( fi ` (F u. {s}))))
128	127	ad2antrr 856	. . . . . . . . . . . . . . . . 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}))))
129		simprll 875	. . . . . . . . . . . . . . . . 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)
130	128, 129	eqtrd 2202	. . . . . . . . . . . . . . . 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)
131		ssun1 3014	. . . . . . . . . . . . . . . . . . . . 21 |- F C_ (F u. {s})
132	131	a1i 8	. . . . . . . . . . . . . . . . . . . 20 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> F C_ (F u. {s}))
133		abfi2 11209	. . . . . . . . . . . . . . . . . . . . . 22 |- ((F u. {s}) e. _V -> (F u. {s}) C_ ( fi ` (F u. {s})))
134	120, 133	syl 13	. . . . . . . . . . . . . . . . . . . . 21 |- (F e. Fil -> (F u. {s}) C_ ( fi ` (F u. {s})))
135	134	ad2antrr 856	. . . . . . . . . . . . . . . . . . . 20 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> (F u. {s}) C_ ( fi ` (F u. {s})))
136	132, 135	sstrd 2889	. . . . . . . . . . . . . . . . . . 19 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> F C_ ( fi ` (F u. {s})))
137		fbssfg 11281	. . . . . . . . . . . . . . . . . . . 20 |- (( fi ` (F u. {s})) e. fBas -> ( fi ` (F u. {s})) C_ (filGen` ( fi ` (F u. {s}))))
138	29, 137	syl 13	. . . . . . . . . . . . . . . . . . 19 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> ( fi ` (F u. {s})) C_ (filGen` ( fi ` (F u. {s}))))
139	136, 138	sstrd 2889	. . . . . . . . . . . . . . . . . 18 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> F C_ (filGen` ( fi ` (F u. {s}))))
140	139	ad2antrr 856	. . . . . . . . . . . . . . . . 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}))))
141		simprlr 876	. . . . . . . . . . . . . . . . 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)
142	140, 141	sstrd 2889	. . . . . . . . . . . . . . . 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)
143	108, 130, 142	jca32 595	. . . . . . . . . . . . . . 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)))
144		simplrr 874	. . . . . . . . . . . . . . . 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)
145		difss 2986	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (X \ s) C_ X
146		ssequn2 3024	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((X \ s) C_ X <-> (X u. (X \ s)) = X)
147	145, 146	mpbi 254	. . . . . . . . . . . . . . . . . . . . . . 23 |- (X u. (X \ s)) = X
148	2	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (F e. Fil -> X = U.F)
149		unisng 3415	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((X \ s) e. _V -> U.{(X \ s)} = (X \ s))
150	79, 80, 149	3syl 38	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (F e. Fil -> U.{(X \ s)} = (X \ s))
151	150	eqcomd 2175	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (F e. Fil -> (X \ s) = U.{(X \ s)})
152	148, 151	uneq12d 3006	. . . . . . . . . . . . . . . . . . . . . . 23 |- (F e. Fil -> (X u. (X \ s)) = (U.F u. U.{(X \ s)}))
153	147, 152	syl5eqr 2218	. . . . . . . . . . . . . . . . . . . . . 22 |- (F e. Fil -> X = (U.F u. U.{(X \ s)}))
154		uniun 3417	. . . . . . . . . . . . . . . . . . . . . 22 |- U.(F u. {(X \ s)}) = (U.F u. U.{(X \ s)})
155	153, 154	syl6eqr 2224	. . . . . . . . . . . . . . . . . . . . 21 |- (F e. Fil -> X = U.(F u. {(X \ s)}))
156		fiuni 11212	. . . . . . . . . . . . . . . . . . . . . 22 |- ((F u. {(X \ s)}) e. _V -> U.(F u. {(X \ s)}) = U.( fi ` (F u. {(X \ s)})))
157	36, 156	syl 13	. . . . . . . . . . . . . . . . . . . . 21 |- (F e. Fil -> U.(F u. {(X \ s)}) = U.( fi ` (F u. {(X \ s)})))
158	155, 157	eqtrd 2202	. . . . . . . . . . . . . . . . . . . 20 |- (F e. Fil -> X = U.( fi ` (F u. {(X \ s)})))
159	158	ad2antrr 856	. . . . . . . . . . . . . . . . . . 19 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> X = U.( fi ` (F u. {(X \ s)})))
160		eqid 2170	. . . . . . . . . . . . . . . . . . . . 21 |- U.( fi ` (F u. {(X \ s)})) = U.( fi ` (F u. {(X \ s)}))
161	160	fgbas 11282	. . . . . . . . . . . . . . . . . . . 20 |- (( fi ` (F u. {(X \ s)})) e. fBas -> U.( fi ` (F u. {(X \ s)})) = U.(filGen` ( fi ` (F u. {(X \ s)}))))
162	102, 161	syl 13	. . . . . . . . . . . . . . . . . . 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)}))))
163	159, 162	eqtrd 2202	. . . . . . . . . . . . . . . . . 18 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> X = U.(filGen` ( fi ` (F u. {(X \ s)}))))
164	163	ad2antrr 856	. . . . . . . . . . . . . . . . 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)}))))
165		simprrl 877	. . . . . . . . . . . . . . . . 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)
166	164, 165	eqtrd 2202	. . . . . . . . . . . . . . . 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)
167	42	a1i 8	. . . . . . . . . . . . . . . . . . . 20 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> F C_ (F u. {(X \ s)}))
168		abfi2 11209	. . . . . . . . . . . . . . . . . . . . . 22 |- ((F u. {(X \ s)}) e. _V -> (F u. {(X \ s)}) C_ ( fi ` (F u. {(X \ s)})))
169	36, 168	syl 13	. . . . . . . . . . . . . . . . . . . . 21 |- (F e. Fil -> (F u. {(X \ s)}) C_ ( fi ` (F u. {(X \ s)})))
170	169	ad2antrr 856	. . . . . . . . . . . . . . . . . . . 20 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> (F u. {(X \ s)}) C_ ( fi ` (F u. {(X \ s)})))
171	167, 170	sstrd 2889	. . . . . . . . . . . . . . . . . . 19 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> F C_ ( fi ` (F u. {(X \ s)})))
172		fbssfg 11281	. . . . . . . . . . . . . . . . . . . 20 |- (( fi ` (F u. {(X \ s)})) e. fBas -> ( fi ` (F u. {(X \ s)})) C_ (filGen` ( fi ` (F u. {(X \ s)}))))
173	102, 172	syl 13	. . . . . . . . . . . . . . . . . . 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)}))))
174	171, 173	sstrd 2889	. . . . . . . . . . . . . . . . . 18 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> F C_ (filGen` ( fi ` (F u. {(X \ s)}))))
175	174	ad2antrr 856	. . . . . . . . . . . . . . . . 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)}))))
176		simprrr 878	. . . . . . . . . . . . . . . . 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)
177	175, 176	sstrd 2889	. . . . . . . . . . . . . . . 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)
178	144, 166, 177	jca32 595	. . . . . . . . . . . . . . 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)))
179		ufilfil 16651	. . . . . . . . . . . . . . . . . . 19 |- (u e. UFil -> u e. Fil)
180		filesn 11264	. . . . . . . . . . . . . . . . . . 19 |- (u e. Fil -> -. (/) e. u)
181	179, 180	syl 13	. . . . . . . . . . . . . . . . . 18 |- (u e. UFil -> -. (/) e. u)
182	181	adantr 543	. . . . . . . . . . . . . . . . 17 |- ((u e. UFil /\ v e. UFil) -> -. (/) e. u)
183	182	ad2antlr 859	. . . . . . . . . . . . . . . 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)
184		difdisj 3178	. . . . . . . . . . . . . . . . 17 |- (s i^i (X \ s)) = (/)
185	179	ad2antrl 861	. . . . . . . . . . . . . . . . . . 19 |- ((((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) /\ (u e. UFil /\ v e. UFil)) -> u e. Fil)
186	185	ad2antrr 856	. . . . . . . . . . . . . . . . . 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)
187		ssun2 3015	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- {s} C_ (F u. {s})
188	187	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> {s} C_ (F u. {s}))
189	188, 135	sstrd 2889	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> {s} C_ ( fi ` (F u. {s})))
190	189, 138	sstrd 2889	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> {s} C_ (filGen` ( fi ` (F u. {s}))))
191	190	ad2antrr 856	. . . . . . . . . . . . . . . . . . . . . . 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}))))
192		simprr 870	. . . . . . . . . . . . . . . . . . . . . . 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)
193	191, 192	sstrd 2889	. . . . . . . . . . . . . . . . . . . . . 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)
194	27	snid 3294	. . . . . . . . . . . . . . . . . . . . . . 23 |- s e. {s}
195	194	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})
196	193, 195	sseldd 2883	. . . . . . . . . . . . . . . . . . . . 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)
197	196	adantlrr 846	. . . . . . . . . . . . . . . . . . . 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)
198	197	adantrr 838	. . . . . . . . . . . . . . . . . . 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)
199	198	adantr 543	. . . . . . . . . . . . . . . . . 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)
200		simprr 870	. . . . . . . . . . . . . . . . . . . . . . 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)
201		ssun2 3015	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- {(X \ s)} C_ (F u. {(X \ s)})
202	201	a1i 8	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> {(X \ s)} C_ (F u. {(X \ s)}))
203	202, 170	sstrd 2889	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> {(X \ s)} C_ ( fi ` (F u. {(X \ s)})))
204	203, 173	sstrd 2889	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> {(X \ s)} C_ (filGen` ( fi ` (F u. {(X \ s)}))))
205		snidg 3292	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((X \ s) e. _V -> (X \ s) e. {(X \ s)})
206	79, 80, 205	3syl 38	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (F e. Fil -> (X \ s) e. {(X \ s)})
207	206	ad2antrr 856	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> (X \ s) e. {(X \ s)})
208	204, 207	sseldd 2883	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((F e. Fil /\ s C_ X) /\ (-. s e. F /\ -. (X \ s) e. F)) -> (X \ s) e. (filGen` ( fi ` (F u. {(X \ s)}))))
209	208	ad2antrr 856	. . . . . . . . . . . . . . . . . . . . . . 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)}))))
210	200, 209	sseldd 2883	. . . . . . . . . . . . . . . . . . . . . 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)
211	210	adantlrl 844	. . . . . . . . . . . . . . . . . . . . 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)
212	211	adantrl 836	. . . . . . . . . . . . . . . . . . . 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)
213	212	adantr 543	. . . . . . . . . . . . . . . . . . 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)
214		simpr 538	. . . . . . . . . . . . . . . . . . 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)
215	213, 214	eleqtrrd 2250	. . . . . . . . . . . . . . . . . 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)
216		filint 11265	. . . . . . . . . . . . . . . . . 18 |- ((u e. Fil /\ s e. u /\ (X \ s) e. u) -> (s i^i (X \ s)) e. u)
217	186, 199, 215, 216	syl111anc 1377	. . . . . . . . . . . . . . . . 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)
218	184, 217	syl5eqelr 2253	. . . . . . . . . . . . . . . 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)
219	183, 218	mtand 753	. . . . . . . . . . . . . . 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)
220		visset 2572	. . . . . . . . . . . . . . . 16 |- u e. _V
221		visset 2572	. . . . . . . . . . . . . . . 16 |- v e. _V
222		eleq1 2233	. . . . . . . . . . . . . . . . . . . 20 |- (f = u -> (f e. UFil <-> u e. UFil))
223		unieq 3407	. . . . . . . . . . . . . . . . . . . . . 22 |- (f = u -> U.f = U.u)
224	223	eqeq2d 2181	. . . . . . . . . . . . . . . . . . . . 21 |- (f = u -> (X = U.f <-> X = U.u))
225		sseq2 2898	. . . . . . . . . . . . . . . . . . . . 21 |- (f = u -> (F C_ f <-> F C_ u))
226	224, 225	anbi12d 821	. . . . . . . . . . . . . . . . . . . 20 |- (f = u -> ((X = U.f /\ F C_ f) <-> (X = U.u /\ F C_ u)))
227	222, 226	anbi12d 821	. . . . . . . . . . . . . . . . . . 19 |- (f = u -> ((f e. UFil /\ (X = U.f /\ F C_ f)) <-> (u e. UFil /\ (X = U.u /\ F C_ u))))
228	227	anbi1d 815	. . . . . . . . . . . . . . . . . 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)))))
229		eqeq1 2176	. . . . . . . . . . . . . . . . . . 19 |- (f = u -> (f = g <-> u = g))
230	229	notbid 356	. . . . . . . . . . . . . . . . . 18 |- (f = u -> (-. f = g <-> -. u = g))
231	228, 230	anbi12d 821	. . . . . . . . . . . . . . . . 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)))
232		eleq1 2233	. . . . . . . . . . . . . . . . . . . 20 |- (g = v -> (g e. UFil <-> v e. UFil))
233		unieq 3407	. . . . . . . . . . . . . . . . . . . . . 22 |- (g = v -> U.g = U.v)
234	233	eqeq2d 2181	. . . . . . . . . . . . . . . . . . . . 21 |- (g = v -> (X = U.g <-> X = U.v))
235		sseq2 2898	. . . . . . . . . . . . . . . . . . . . 21 |- (g = v -> (F C_ g <-> F C_ v))
236	234, 235	anbi12d 821	. . . . . . . . . . . . . . . . . . . 20 |- (g = v -> ((X = U.g /\ F C_ g) <-> (X = U.v /\ F C_ v)))
237	232, 236	anbi12d 821	. . . . . . . . . . . . . . . . . . 19 |- (g = v -> ((g e. UFil /\ (X = U.g /\ F C_ g)) <-> (v e. UFil /\ (X = U.v /\ F C_ v))))
238	237	anbi2d 814	. . . . . . . . . . . . . . . . . 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)))))
239		eqeq2 2179	. . . . . . . . . . . . . . . . . . 19 |- (g = v -> (u = g <-> u = v))
240	239	notbid 356	. . . . . . . . . . . . . . . . . 18 |- (g = v -> (-. u = g <-> -. u = v))
241	238, 240	anbi12d 821	. . . . . . . . . . . . . . . . 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)))
242	231, 241	sylan9bb 809	. . . . . . . . . . . . . . . 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)))
243	220, 221, 242	cla42ev 2643	. . . . . . . . . . . . . . 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))
244	143, 178, 219, 243	syl21anc 1376	. . . . . . . . . . . . . 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))
245	244	exp31 673	. . . . . . . . . . . . 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))))
246	245	r19.23advv 2496	. . . . . . . . . . . 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)))
247	107, 246	syl5bir 272	. . . . . . . . . . 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)))
248	33, 106, 247	mp2and 787	. . . . . . . . . 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))
249	248	exp31 673	. . . . . . . . 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))))
250	28, 249	syl5bi 270	. . . . . . . 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))))
251	250	r19.23adv 2493	. . . . . . 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)))
252		rexnal 2394	. . . . . . . 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))
253		ioran 520	. . . . . . . . 9 |- (-. (s e. F \/ (X \ s) e. F) <-> (-. s e. F /\ -. (X \ s) e. F))
254	253	rexbii 2408	. . . . . . . 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))
255	252, 254	bitr3i 309	. . . . . . 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))
256		eleq1 2233	. . . . . . . . . . 11 |- (f = g -> (f e. UFil <-> g e. UFil))
257		unieq 3407	. . . . . . . . . . . . 13 |- (f = g -> U.f = U.g)
258	257	eqeq2d 2181	. . . . . . . . . . . 12 |- (f = g -> (X = U.f <-> X = U.g))
259		sseq2 2898	. . . . . . . . . . . 12 |- (f = g -> (F C_ f <-> F C_ g))
260	258, 259	anbi12d 821	. . . . . . . . . . 11 |- (f = g -> ((X = U.f /\ F C_ f) <-> (X = U.g /\ F C_ g)))
261	256, 260	anbi12d 821	. . . . . . . . . 10 |- (f = g -> ((f e. UFil /\ (X = U.f /\ F C_ f)) <-> (g e. UFil /\ (X = U.g /\ F C_ g))))
262	261	mo4 2093	. . . . . . . . 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))
263	262	notbii 362	. . . . . . . 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))
264		exnal 1703	. . . . . . . 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))
265		annim 461	. . . . . . . . . . 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))
266	265	exbii 1716	. . . . . . . . . 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))
267		exnal 1703	. . . . . . . . . 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))
268	266, 267	bitr2i 308	. . . . . . . . 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))
269	268	exbii 1716	. . . . . . . 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))
270	263, 264, 269	3bitr2i 336	. . . . . . 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))
271	251, 255, 270	3imtr4g 333	. . . . . 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))))
272		eumo 2101	. . . . . . 7 |- (E!f(f e. UFil /\ (X = U.f /\ F C_ f)) -> E*f(f e. UFil /\ (X = U.f /\ F C_ f)))
273	272	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))))
274	271, 273	nsyld 176	. . . . 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))))
275	274	con4d 126	. . . 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)))
276	26, 275	syl5bi 270	. . 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	2	isufil 16649	. . . 4 |- (F e. UFil <-> (F e. Fil /\ A.s e. ~P X(s e. F \/ (X \ s) e. F)))
278	277	baibr 1052	. . 3 |- (F e. Fil -> (A.s e. ~P X(s e. F \/ (X \ s) e. F) <-> F e. UFil))
279	276, 278	sylibd 266	. 2 |- (F e. Fil -> (E!f e. UFil (X = U.f /\ F C_ f) -> F e. UFil))
280	25, 279	impbid2 252	1 |- (F e. Fil -> (F e. UFil <-> E!f e. UFil (X = U.f /\ F C_ f)))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 231   \/ wo 432   /\ wa 433  A.wal 1613   = wceq 1615   e. wcel 1617  E.wex 1644  E!weu 2066  E*wmo 2067   =/= wne 2295   e/ wnel 2296  A.wral 2385  E.wrex 2386  E!wreu 2387  _Vcvv 2569   \ cdif 2856   u. cun 2857   i^i cin 2858   C_ wss 2859  (/)c0 3114  ~Pcpw 3259  {csn 3270  U.cuni 3398  ` cfv 4163   fi cfi 11200  fBascfbas 11253  filGencfg 11254  Filcfil 11260  UFilcufil 16647

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1621  ax-gen 1622  ax-8 1623  ax-9 1624  ax-10 1625  ax-11 1626  ax-12 1627  ax-13 1628  ax-14 1629  ax-17 1634  ax-4 1637  ax-5o 1639  ax-6o 1642  ax-9o 1792  ax-10o 1810  ax-16 1883  ax-11o 1893  ax-ext 2152  ax-rep 3628  ax-sep 3638  ax-nul 3645  ax-pow 3681  ax-pr 3719  ax-un 3961  ax-ac 6385

This theorem depends on definitions:  df-bi 232  df-or 434  df-an 435  df-3or 1131  df-3an 1132  df-ex 1645  df-sb 1845  df-eu 2070  df-mo 2071  df-clab 2158  df-cleq 2163  df-clel 2166  df-ne 2297  df-nel 2298  df-ral 2389  df-rex 2390  df-reu 2391  df-rab 2392  df-v 2571  df-sbc 2731  df-csb 2806  df-dif 2862  df-un 2864  df-in 2866  df-ss 2868  df-pss 2870  df-nul 3115  df-if 3213  df-pw 3261  df-sn 3274  df-pr 3275  df-tp 3277  df-op 3278  df-uni 3399  df-int 3433  df-iun 3470  df-br 3540  df-opab 3598  df-tr 3612  df-eprel 3776  df-id 3779  df-po 3784  df-so 3796  df-fr 3814  df-we 3830  df-ord 3846  df-on 3847  df-lim 3848  df-suc 3849  df-om 4118  df-xp 4165  df-rel 4166  df-cnv 4167  df-co 4168  df-dm 4169  df-rn 4170  df-res 4171  df-ima 4172  df-fun 4173  df-fn 4174  df-f 4175  df-f1 4176  df-fo 4177  df-f1o 4178  df-fv 4179  df-iso 4180  df-opr 5022  df-oprab 5023  df-rdg 5344  df-1o 5384  df-oadd 5386  df-er 5519  df-en 5631  df-fin 5634  df-fi 11201  df-fbas 11255  df-fg 11256  df-fil 11261  df-ufil 16648

Copyright terms: Public domain