Theorem efilcp2 10486

Description: A filter containing a set A exists iff A has the finite intersection property (i.e. no finite intersection of elements of A is empty). Bourbaki TG I.37 prop. 1.

Assertion

Ref	Expression
efilcp2	|- ((A (_ P~X /\ X e. V /\ A =/= (/)) -> (-. (/) e. (fi` A) <-> E.x e. Fil A (_ x))

Distinct variable groups:   x,A   x,X

Proof of Theorem efilcp2

Step	Hyp	Ref	Expression
1		sseq2 2079	. . . . 5 |- (x = {z e. P~X | E.y e. (fi` A)y (_ z} -> (A (_ x <-> A (_ {z e. P~X | E.y e. (fi` A)y (_ z}))
2	1	rcla4ev 1873	. . . 4 |- (({z e. P~X | E.y e. (fi` A)y (_ z} e. Fil /\ A (_ {z e. P~X | E.y e. (fi` A)y (_ z}) -> E.x e. Fil A (_ x)
3		fgsb2 10485	. . . . 5 |- ((A (_ P~X /\ X e. V /\ A =/= (/)) -> (-. (/) e. (fi` A) -> {z e. P~X | E.y e. (fi` A)y (_ z} e. Fil))
4	3	imp 350	. . . 4 |- (((A (_ P~X /\ X e. V /\ A =/= (/)) /\ -. (/) e. (fi` A)) -> {z e. P~X | E.y e. (fi` A)y (_ z} e. Fil)
5		3simp1 787	. . . . . . 7 |- ((A (_ P~X /\ X e. V /\ A =/= (/)) -> A (_ P~X)
6	5	adantr 389	. . . . . 6 |- (((A (_ P~X /\ X e. V /\ A =/= (/)) /\ -. (/) e. (fi` A)) -> A (_ P~X)
7		pwexg 2741	. . . . . . . . . . . 12 |- (X e. V -> P~X e. V)
8		elpw2g 2722	. . . . . . . . . . . 12 |- (P~X e. V -> (A e. P~P~X <-> A (_ P~X))
9	7, 8	syl 10	. . . . . . . . . . 11 |- (X e. V -> (A e. P~P~X <-> A (_ P~X))
10	9	biimprd 154	. . . . . . . . . 10 |- (X e. V -> (A (_ P~X -> A e. P~P~X))
11		elisset 1813	. . . . . . . . . . 11 |- (A e. P~P~X -> A e. V)
12	11	a1d 12	. . . . . . . . . 10 |- (A e. P~P~X -> (A =/= (/) -> A e. V))
13	10, 12	syl6com 53	. . . . . . . . 9 |- (A (_ P~X -> (X e. V -> (A =/= (/) -> A e. V)))
14	13	3imp 826	. . . . . . . 8 |- ((A (_ P~X /\ X e. V /\ A =/= (/)) -> A e. V)
15	14	adantr 389	. . . . . . 7 |- (((A (_ P~X /\ X e. V /\ A =/= (/)) /\ -. (/) e. (fi` A)) -> A e. V)
16		abfi2 10414	. . . . . . . 8 |- (A e. V -> A (_ (fi` A))
17		ssel2 2060	. . . . . . . . . 10 |- ((A (_ (fi` A) /\ z e. A) -> z e. (fi` A))
18		ssid 2076	. . . . . . . . . . 11 |- z (_ z
19		sseq1 2078	. . . . . . . . . . . 12 |- (y = z -> (y (_ z <-> z (_ z))
20	19	rcla4ev 1873	. . . . . . . . . . 11 |- ((z e. (fi` A) /\ z (_ z) -> E.y e. (fi` A)y (_ z)
21	18, 20	mpan2 695	. . . . . . . . . 10 |- (z e. (fi` A) -> E.y e. (fi` A)y (_ z)
22	17, 21	syl 10	. . . . . . . . 9 |- ((A (_ (fi` A) /\ z e. A) -> E.y e. (fi` A)y (_ z)
23	22	r19.21aiva 1711	. . . . . . . 8 |- (A (_ (fi` A) -> A.z e. A E.y e. (fi` A)y (_ z)
24	16, 23	syl 10	. . . . . . 7 |- (A e. V -> A.z e. A E.y e. (fi` A)y (_ z)
25	15, 24	syl 10	. . . . . 6 |- (((A (_ P~X /\ X e. V /\ A =/= (/)) /\ -. (/) e. (fi` A)) -> A.z e. A E.y e. (fi` A)y (_ z)
26	6, 25	jca 288	. . . . 5 |- (((A (_ P~X /\ X e. V /\ A =/= (/)) /\ -. (/) e. (fi` A)) -> (A (_ P~X /\ A.z e. A E.y e. (fi` A)y (_ z))
27		ssrab 2121	. . . . 5 |- (A (_ {z e. P~X | E.y e. (fi` A)y (_ z} <-> (A (_ P~X /\ A.z e. A E.y e. (fi` A)y (_ z))
28	26, 27	sylibr 200	. . . 4 |- (((A (_ P~X /\ X e. V /\ A =/= (/)) /\ -. (/) e. (fi` A)) -> A (_ {z e. P~X | E.y e. (fi` A)y (_ z})
29	2, 4, 28	sylanc 471	. . 3 |- (((A (_ P~X /\ X e. V /\ A =/= (/)) /\ -. (/) e. (fi` A)) -> E.x e. Fil A (_ x)
30	29	ex 373	. 2 |- ((A (_ P~X /\ X e. V /\ A =/= (/)) -> (-. (/) e. (fi` A) -> E.x e. Fil A (_ x))
31		0ex 2706	. . . . . . . . . . 11 |- (/) e. V
32		sppfi 10412	. . . . . . . . . . 11 |- (((/) e. V /\ A e. V) -> ((/) e. (fi` A) <-> E.y(y (_ A /\ E.u e. om y ~~ u /\ (/) = |^|y)))
33	31, 32	mpan 694	. . . . . . . . . 10 |- (A e. V -> ((/) e. (fi` A) <-> E.y(y (_ A /\ E.u e. om y ~~ u /\ (/) = |^|y)))
34	33	negbid 610	. . . . . . . . 9 |- (A e. V -> (-. (/) e. (fi` A) <-> -. E.y(y (_ A /\ E.u e. om y ~~ u /\ (/) = |^|y)))
35		sstr 2068	. . . . . . . . . . . . . . . . . . . . . 22 |- ((y (_ A /\ A (_ x) -> y (_ x)
36		df-ne 1584	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (y =/= (/) <-> -. y = (/))
37		fipfil2 10475	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (x e. Fil -> ((y (_ x /\ y =/= (/) /\ E.u e. om y ~~ u) -> |^|y =/= (/)))
38		pm2.27 62	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ((y (_ x /\ y =/= (/) /\ E.u e. om y ~~ u) -> (((y (_ x /\ y =/= (/) /\ E.u e. om y ~~ u) -> |^|y =/= (/)) -> |^|y =/= (/)))
39		necom 1633	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((/) =/= |^|y <-> |^|y =/= (/))
40		df-ne 1584	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ((/) =/= |^|y <-> -. (/) = |^|y)
41	40	biimp 151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ((/) =/= |^|y -> -. (/) = |^|y)
42	39, 41	sylbir 201	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- (|^|y =/= (/) -> -. (/) = |^|y)
43	38, 42	syl6 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((y (_ x /\ y =/= (/) /\ E.u e. om y ~~ u) -> (((y (_ x /\ y =/= (/) /\ E.u e. om y ~~ u) -> |^|y =/= (/)) -> -. (/) = |^|y))
44	43	3exp 831	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (y (_ x -> (y =/= (/) -> (E.u e. om y ~~ u -> (((y (_ x /\ y =/= (/) /\ E.u e. om y ~~ u) -> |^|y =/= (/)) -> -. (/) = |^|y))))
45	44	com34 36	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (y (_ x -> (y =/= (/) -> (((y (_ x /\ y =/= (/) /\ E.u e. om y ~~ u) -> |^|y =/= (/)) -> (E.u e. om y ~~ u -> -. (/) = |^|y))))
46	45	com4t 40	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((y (_ x /\ y =/= (/) /\ E.u e. om y ~~ u) -> |^|y =/= (/)) -> (E.u e. om y ~~ u -> (y (_ x -> (y =/= (/) -> -. (/) = |^|y))))
47	37, 46	syl 10	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (x e. Fil -> (E.u e. om y ~~ u -> (y (_ x -> (y =/= (/) -> -. (/) = |^|y))))
48	47	adantr 389	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((x e. Fil /\ (A (_ P~X /\ X e. V /\ A =/= (/))) -> (E.u e. om y ~~ u -> (y (_ x -> (y =/= (/) -> -. (/) = |^|y))))
49	48	com14 38	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (y =/= (/) -> (E.u e. om y ~~ u -> (y (_ x -> ((x e. Fil /\ (A (_ P~X /\ X e. V /\ A =/= (/))) -> -. (/) = |^|y))))
50	36, 49	sylbir 201	. . . . . . . . . . . . . . . . . . . . . . 23 |- (-. y = (/) -> (E.u e. om y ~~ u -> (y (_ x -> ((x e. Fil /\ (A (_ P~X /\ X e. V /\ A =/= (/))) -> -. (/) = |^|y))))
51	50	com13 33	. . . . . . . . . . . . . . . . . . . . . 22 |- (y (_ x -> (E.u e. om y ~~ u -> (-. y = (/) -> ((x e. Fil /\ (A (_ P~X /\ X e. V /\ A =/= (/))) -> -. (/) = |^|y))))
52	35, 51	syl 10	. . . . . . . . . . . . . . . . . . . . 21 |- ((y (_ A /\ A (_ x) -> (E.u e. om y ~~ u -> (-. y = (/) -> ((x e. Fil /\ (A (_ P~X /\ X e. V /\ A =/= (/))) -> -. (/) = |^|y))))
53	52	ex 373	. . . . . . . . . . . . . . . . . . . 20 |- (y (_ A -> (A (_ x -> (E.u e. om y ~~ u -> (-. y = (/) -> ((x e. Fil /\ (A (_ P~X /\ X e. V /\ A =/= (/))) -> -. (/) = |^|y)))))
54	53	com23 32	. . . . . . . . . . . . . . . . . . 19 |- (y (_ A -> (E.u e. om y ~~ u -> (A (_ x -> (-. y = (/) -> ((x e. Fil /\ (A (_ P~X /\ X e. V /\ A =/= (/))) -> -. (/) = |^|y)))))
55	54	imp 350	. . . . . . . . . . . . . . . . . 18 |- ((y (_ A /\ E.u e. om y ~~ u) -> (A (_ x -> (-. y = (/) -> ((x e. Fil /\ (A (_ P~X /\ X e. V /\ A =/= (/))) -> -. (/) = |^|y))))
56	55	com14 38	. . . . . . . . . . . . . . . . 17 |- ((x e. Fil /\ (A (_ P~X /\ X e. V /\ A =/= (/))) -> (A (_ x -> (-. y = (/) -> ((y (_ A /\ E.u e. om y ~~ u) -> -. (/) = |^|y))))
57	56	ex 373	. . . . . . . . . . . . . . . 16 |- (x e. Fil -> ((A (_ P~X /\ X e. V /\ A =/= (/)) -> (A (_ x -> (-. y = (/) -> ((y (_ A /\ E.u e. om y ~~ u) -> -. (/) = |^|y)))))
58	57	com23 32	. . . . . . . . . . . . . . 15 |-