Theorem cnfilca 10562

Description: Condition to have a filter finer than a given filter and containing a set A. Bourbaki T.G. I.37 cor. 1

Assertion

Ref	Expression
cnfilca	|- ((F e. Fil /\ A (_ U.F /\ A =/= (/)) -> (E.g e. Fil (A e. g /\ F (_ g) <-> A.x e. F (x i^i A) =/= (/)))

Distinct variable groups:   A,g   x,A   g,F   x,F

Proof of Theorem cnfilca

Step	Hyp	Ref	Expression
1		ssexg 2726	. . . . . . 7 |- ((A (_ U.F /\ U.F e. V) -> A e. V)
2		uniexg 2877	. . . . . . 7 |- (F e. Fil -> U.F e. V)
3	1, 2	sylan2 453	. . . . . 6 |- ((A (_ U.F /\ F e. Fil) -> A e. V)
4	3	ancoms 438	. . . . 5 |- ((F e. Fil /\ A (_ U.F) -> A e. V)
5	4	3adant3 801	. . . 4 |- ((F e. Fil /\ A (_ U.F /\ A =/= (/)) -> A e. V)
6		snssg 2467	. . . . . 6 |- (A e. V -> (A e. g <-> {A} (_ g))
7	6	anbi1d 619	. . . . 5 |- (A e. V -> ((A e. g /\ F (_ g) <-> ({A} (_ g /\ F (_ g)))
8		unss 2207	. . . . 5 |- (({A} (_ g /\ F (_ g) <-> ({A} u. F) (_ g)
9	7, 8	syl6bb 538	. . . 4 |- (A e. V -> ((A e. g /\ F (_ g) <-> ({A} u. F) (_ g))
10	5, 9	syl 10	. . 3 |- ((F e. Fil /\ A (_ U.F /\ A =/= (/)) -> ((A e. g /\ F (_ g) <-> ({A} u. F) (_ g))
11	10	rexbidv 1667	. 2 |- ((F e. Fil /\ A (_ U.F /\ A =/= (/)) -> (E.g e. Fil (A e. g /\ F (_ g) <-> E.g e. Fil ({A} u. F) (_ g))
12		efilcp2 10561	. . 3 |- ((({A} u. F) (_ P~U.F /\ U.F e. V /\ ({A} u. F) =/= (/)) -> (-. (/) e. (fi` ({A} u. F)) <-> E.g e. Fil ({A} u. F) (_ g))
13	1	ex 373	. . . . . . 7 |- (A (_ U.F -> (U.F e. V -> A e. V))
14		elpwg 2409	. . . . . . . . 9 |- (A e. V -> (A e. P~U.F <-> A (_ U.F))
15		snssg 2467	. . . . . . . . 9 |- (A e. V -> (A e. P~U.F <-> {A} (_ P~U.F))
16	14, 15	bitr3d 532	. . . . . . . 8 |- (A e. V -> (A (_ U.F <-> {A} (_ P~U.F))
17		pwuni 2763	. . . . . . . . 9 |- F (_ P~U.F
18		unss 2207	. . . . . . . . . 10 |- (({A} (_ P~U.F /\ F (_ P~U.F) <-> ({A} u. F) (_ P~U.F)
19	18	biimp 151	. . . . . . . . 9 |- (({A} (_ P~U.F /\ F (_ P~U.F) -> ({A} u. F) (_ P~U.F)
20	17, 19	mpan2 698	. . . . . . . 8 |- ({A} (_ P~U.F -> ({A} u. F) (_ P~U.F)
21	16, 20	syl6bi 214	. . . . . . 7 |- (A e. V -> (A (_ U.F -> ({A} u. F) (_ P~U.F))
22	13, 21	syl6 22	. . . . . 6 |- (A (_ U.F -> (U.F e. V -> (A (_ U.F -> ({A} u. F) (_ P~U.F)))
23	22	pm2.43a 66	. . . . 5 |- (A (_ U.F -> (U.F e. V -> ({A} u. F) (_ P~U.F))
24	2, 23	mpan9 472	. . . 4 |- ((F e. Fil /\ A (_ U.F) -> ({A} u. F) (_ P~U.F)
25	24	3adant3 801	. . 3 |- ((F e. Fil /\ A (_ U.F /\ A =/= (/)) -> ({A} u. F) (_ P~U.F)
26	2	3ad2ant1 802	. . 3 |- ((F e. Fil /\ A (_ U.F /\ A =/= (/)) -> U.F e. V)
27		emnfil 10551	. . . . 5 |- -. (/) e. Fil
28		nelneq 1564	. . . . . 6 |- ((F e. Fil /\ -. (/) e. Fil) -> -. F = (/))
29		pm3.27 323	. . . . . . . 8 |- (({A} = (/) /\ F = (/)) -> F = (/))
30	29	con3i 98	. . . . . . 7 |- (-. F = (/) -> -. ({A} = (/) /\ F = (/)))
31		un00 2310	. . . . . . . 8 |- (({A} = (/) /\ F = (/)) <-> ({A} u. F) = (/))
32	31	necon3bbii 1600	. . . . . . 7 |- (-. ({A} = (/) /\ F = (/)) <-> ({A} u. F) =/= (/))
33	30, 32	sylib 198	. . . . . 6 |- (-. F = (/) -> ({A} u. F) =/= (/))
34	28, 33	syl 10	. . . . 5 |- ((F e. Fil /\ -. (/) e. Fil) -> ({A} u. F) =/= (/))
35	27, 34	mpan2 698	. . . 4 |- (F e. Fil -> ({A} u. F) =/= (/))
36	35	3ad2ant1 802	. . 3 |- ((F e. Fil /\ A (_ U.F /\ A =/= (/)) -> ({A} u. F) =/= (/))
37	12, 25, 26, 36	syl3anc 860	. 2 |- ((F e. Fil /\ A (_ U.F /\ A =/= (/)) -> (-. (/) e. (fi` ({A} u. F)) <-> E.g e. Fil ({A} u. F) (_ g))
38		elisset 1820	. . . . . . . 8 |- (F e. Fil -> F e. V)
39	38	3ad2ant1 802	. . . . . . 7 |- ((F e. Fil /\ A (_ U.F /\ A =/= (/)) -> F e. V)
40		snex 2756	. . . . . . 7 |- {A} e. V
41	39, 40	jctil 292	. . . . . 6 |- ((F e. Fil /\ A (_ U.F /\ A =/= (/)) -> ({A} e. V /\ F e. V))
42		unexb 2879	. . . . . 6 |- (({A} e. V /\ F e. V) <-> ({A} u. F) e. V)
43	41, 42	sylib 198	. . . . 5 |- ((F e. Fil /\ A (_ U.F /\ A =/= (/)) -> ({A} u. F) e. V)
44		0ex 2716	. . . . 5 |- (/) e. V
45	43, 44	jctil 292	. . . 4 |- ((F e. Fil /\ A (_ U.F /\ A =/= (/)) -> ((/) e. V /\ ({A} u. F) e. V))
46		sppfi 10472	. . . . 5 |- (((/) e. V /\ ({A} u. F) e. V) -> ((/) e. (fi` ({A} u. F)) <-> E.y(y (_ ({A} u. F) /\ y e. Fin /\ (/) = |^|y)))
47	46	negbid 613	. . . 4 |- (((/) e. V /\ ({A} u. F) e. V) -> (-. (/) e. (fi` ({A} u. F)) <-> -. E.y(y (_ ({A} u. F) /\ y e. Fin /\ (/) = |^|y)))
48	45, 47	syl 10	. . 3 |- ((F e. Fil /\ A (_ U.F /\ A =/= (/)) -> (-. (/) e. (fi` ({A} u. F)) <-> -. E.y(y (_ ({A} u. F) /\ y e. Fin /\ (/) = |^|y)))
49		ax-17 973	. . . . . 6 |- (((F e. Fil /\ A (_ U.F /\ A =/= (/)) /\ A.y((y (_ ({A} u. F) /\ y e. Fin) -> -. (/) = |^|y)) -> A.x((F e. Fil /\ A (_ U.F /\ A =/= (/)) /\ A.y((y (_ ({A} u. F) /\ y e. Fin) -> -. (/) = |^|y)))
50		elun2 2201	. . . . . . . . . . . . . . . . . 18 |- (x e. F -> x e. ({A} u. F))
51	50	adantl 390	. . . . . . . . . . . . . . . . 17 |- (((F e. Fil /\ A (_ U.F /\ A =/= (/)) /\ x e. F) -> x e. ({A} u. F))
52		snidg 2437	. . . . . . . . . . . . . . . . . . . 20 |- (A e. V -> A e. {A})
53		elun1 2200	. . . . . . . . . . . . . . . . . . . 20 |- (A e. {A} -> A e. ({A} u. F))
54	52, 53	syl 10	. . . . . . . . . . . . . . . . . . 19 |- (A e. V -> A e. ({A} u. F))
55	5, 54	syl 10	. . . . . . . . . . . . . . . . . 18 |- ((F e. Fil /\ A (_ U.F /\ A =/= (/)) -> A e. ({A} u. F))
56	55	adantr 391	. . . . . . . . . . . . . . . . 17 |- (((F e. Fil /\ A (_ U.F /\ A =/= (/)) /\ x e. F) -> A e. ({A} u. F))
57	51, 56	jca 288	. . . . . . . . . . . . . . . 16 |- (((F e. Fil /\ A (_ U.F /\ A =/= (/)) /\ x e. F) -> (x e. ({A} u. F) /\ A e. ({A} u. F)))
58		prssg 2476	. . . . . . . . . . . . . . . . . 18 |- ((x e. F /\ A e. P~U.F) -> ((x e. ({A} u. F) /\ A e. ({A} u. F)) <-> {x, A} (_ ({A} u. F)))
59	58	bicomd 523	. . . . . . . . . . . . . . . . 17 |- ((x e. F /\ A e. P~U.F) -> ({x, A} (_ ({A} u. F) <-> (x e. ({A} u. F) /\ A e. ({A} u. F))))
60		pm3.27 323	. . . . . . . . . . . . . . . . 17 |- (((F e. Fil /\ A (_ U.F /\ A =/= (/)) /\ x e. F) -> x e. F)
61		3simp2 791	. . . . . . . . . . . . . . . . . . 19 |- ((F e. Fil /\ A (_ U.F /\ A =/= (/)) -> A (_ U.F)
62	5, 14	syl 10	. . . . . . . . . . . . . . . . . . 19 |- ((F e. Fil /\ A (_ U.F /\ A =/= (/)) -> (A e. P~U.F <-> A (_ U.F))
63	61, 62	mpbird 196	. . . . . . . . . . . . . . . . . 18 |- ((F e. Fil /\ A (_ U.F /\ A =/= (/)) -> A e. P~U.F)
64	63	adantr 391	. . . . . . . . . . . . . . . . 17 |- (((F e. Fil /\ A (_ U.F /\ A =/= (/)) /\ x e. F) -> A e. P~U.F)
65	59, 60, 64	sylanc 473	. . . . . . . . . . . . . . . 16 |- (((F e. Fil /\ A (_ U.F /\ A =/= (/)) /\ x e. F) -> ({x, A} (_ ({A} u. F) <-> (x e. ({A} u. F) /\ A e. ({A} u. F))))
66	57, 65	mpbird 196	. . . . . . . . . . . . . . 15 |- (((F e. Fil /\ A (_ U.F /\ A =/= (/)) /\ x e. F) -> {x, A} (_ ({A} u. F))
67		prfi 4568	. . . . . . . . . . . . . . 15 |- {x, A} e. Fin
68	66, 67	jctir 293	. . . . . . . . . . . . . 14 |- (((F e. Fil /\ A (_ U.F /\ A =/= (/)) /\ x e. F) -> ({x, A} (_ ({A} u. F) /\ {x, A} e. Fin))
69		prex 2787	. . . . . . . . . . . . . . . 16 |-