Theorem efilcp 10504

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.

Hypothesis

Ref	Expression
efilcp.1	|- B = {z | E.y(y (_ A /\ E.u e. om y ~~ u /\ z = |^|y)}

Assertion

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

Distinct variable groups:   x,A,y,z   u,B,x,y,z   u,X,x,y,z

Proof of Theorem efilcp

Step	Hyp	Ref	Expression
1		sseq2 2080	. . . . 5 |- (x = {z e. P~X | E.y e. B y (_ z} -> (A (_ x <-> A (_ {z e. P~X | E.y e. B y (_ z}))
2	1	rcla4ev 1874	. . . 4 |- (({z e. P~X | E.y e. B y (_ z} e. Fil /\ A (_ {z e. P~X | E.y e. B y (_ z}) -> E.x e. Fil A (_ x)
3		efilcp.1	. . . . . 6 |- B = {z | E.y(y (_ A /\ E.u e. om y ~~ u /\ z = |^|y)}
4	3	fgsb 10503	. . . . 5 |- ((A (_ P~X /\ X e. V /\ A =/= (/)) -> (-. (/) e. B -> {z e. P~X | E.y e. B y (_ z} e. Fil))
5	4	imp 350	. . . 4 |- (((A (_ P~X /\ X e. V /\ A =/= (/)) /\ -. (/) e. B) -> {z e. P~X | E.y e. B y (_ z} e. Fil)
6		3simp1 787	. . . . . . 7 |- ((A (_ P~X /\ X e. V /\ A =/= (/)) -> A (_ P~X)
7	6	adantr 389	. . . . . 6 |- (((A (_ P~X /\ X e. V /\ A =/= (/)) /\ -. (/) e. B) -> A (_ P~X)
8		abfi 10407	. . . . . . . . 9 |- A (_ {z | E.y(y (_ A /\ E.u e. om y ~~ u /\ z = |^|y)}
9	8, 3	sseqtr4 2091	. . . . . . . 8 |- A (_ B
10		ssel2 2061	. . . . . . . . 9 |- ((A (_ B /\ z e. A) -> z e. B)
11		ssid 2077	. . . . . . . . . 10 |- z (_ z
12		sseq1 2079	. . . . . . . . . . 11 |- (y = z -> (y (_ z <-> z (_ z))
13	12	rcla4ev 1874	. . . . . . . . . 10 |- ((z e. B /\ z (_ z) -> E.y e. B y (_ z)
14	11, 13	mpan2 695	. . . . . . . . 9 |- (z e. B -> E.y e. B y (_ z)
15	10, 14	syl 10	. . . . . . . 8 |- ((A (_ B /\ z e. A) -> E.y e. B y (_ z)
16	9, 15	mpan 694	. . . . . . 7 |- (z e. A -> E.y e. B y (_ z)
17	16	rgen 1696	. . . . . 6 |- A.z e. A E.y e. B y (_ z
18	7, 17	jctir 293	. . . . 5 |- (((A (_ P~X /\ X e. V /\ A =/= (/)) /\ -. (/) e. B) -> (A (_ P~X /\ A.z e. A E.y e. B y (_ z))
19		ssrab 2122	. . . . 5 |- (A (_ {z e. P~X | E.y e. B y (_ z} <-> (A (_ P~X /\ A.z e. A E.y e. B y (_ z))
20	18, 19	sylibr 200	. . . 4 |- (((A (_ P~X /\ X e. V /\ A =/= (/)) /\ -. (/) e. B) -> A (_ {z e. P~X | E.y e. B y (_ z})
21	2, 5, 20	sylanc 471	. . 3 |- (((A (_ P~X /\ X e. V /\ A =/= (/)) /\ -. (/) e. B) -> E.x e. Fil A (_ x)
22	21	ex 373	. 2 |- ((A (_ P~X /\ X e. V /\ A =/= (/)) -> (-. (/) e. B -> E.x e. Fil A (_ x))
23		sstr 2069	. . . . . . . . . . . . . . . . . . 19 |- ((y (_ A /\ A (_ x) -> y (_ x)
24		df-ne 1585	. . . . . . . . . . . . . . . . . . . . 21 |- (y =/= (/) <-> -. y = (/))
25		fipfil2 10498	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (x e. Fil -> ((y (_ x /\ y =/= (/) /\ E.u e. om y ~~ u) -> |^|y =/= (/)))
26		pm2.27 62	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((y (_ x /\ y =/= (/) /\ E.u e. om y ~~ u) -> (((y (_ x /\ y =/= (/) /\ E.u e. om y ~~ u) -> |^|y =/= (/)) -> |^|y =/= (/)))
27		necom 1634	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((/) =/= |^|y <-> |^|y =/= (/))
28		df-ne 1585	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ((/) =/= |^|y <-> -. (/) = |^|y)
29	28	biimp 151	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((/) =/= |^|y -> -. (/) = |^|y)
30	27, 29	sylbir 201	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (|^|y =/= (/) -> -. (/) = |^|y)
31	26, 30	syl6 22	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((y (_ x /\ y =/= (/) /\ E.u e. om y ~~ u) -> (((y (_ x /\ y =/= (/) /\ E.u e. om y ~~ u) -> |^|y =/= (/)) -> -. (/) = |^|y))
32	31	3exp 831	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (y (_ x -> (y =/= (/) -> (E.u e. om y ~~ u -> (((y (_ x /\ y =/= (/) /\ E.u e. om y ~~ u) -> |^|y =/= (/)) -> -. (/) = |^|y))))
33	32	com34 36	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (y (_ x -> (y =/= (/) -> (((y (_ x /\ y =/= (/) /\ E.u e. om y ~~ u) -> |^|y =/= (/)) -> (E.u e. om y ~~ u -> -. (/) = |^|y))))
34	33	com4t 40	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((y (_ x /\ y =/= (/) /\ E.u e. om y ~~ u) -> |^|y =/= (/)) -> (E.u e. om y ~~ u -> (y (_ x -> (y =/= (/) -> -. (/) = |^|y))))
35	25, 34	syl 10	. . . . . . . . . . . . . . . . . . . . . . 23 |- (x e. Fil -> (E.u e. om y ~~ u -> (y (_ x -> (y =/= (/) -> -. (/) = |^|y))))
36	35	adantr 389	. . . . . . . . . . . . . . . . . . . . . 22 |- ((x e. Fil /\ (A (_ P~X /\ X e. V /\ A =/= (/))) -> (E.u e. om y ~~ u -> (y (_ x -> (y =/= (/) -> -. (/) = |^|y))))
37	36	com14 38	. . . . . . . . . . . . . . . . . . . . 21 |- (y =/= (/) -> (E.u e. om y ~~ u -> (y (_ x -> ((x e. Fil /\ (A (_ P~X /\ X e. V /\ A =/= (/))) -> -. (/) = |^|y))))
38	24, 37	sylbir 201	. . . . . . . . . . . . . . . . . . . 20 |- (-. y = (/) -> (E.u e. om y ~~ u -> (y (_ x -> ((x e. Fil /\ (A (_ P~X /\ X e. V /\ A =/= (/))) -> -. (/) = |^|y))))
39	38	com13 33	. . . . . . . . . . . . . . . . . . 19 |- (y (_ x -> (E.u e. om y ~~ u -> (-. y = (/) -> ((x e. Fil /\ (A (_ P~X /\ X e. V /\ A =/= (/))) -> -. (/) = |^|y))))
40	23, 39	syl 10	. . . . . . . . . . . . . . . . . 18 |- ((y (_ A /\ A (_ x) -> (E.u e. om y ~~ u -> (-. y = (/) -> ((x e. Fil /\ (A (_ P~X /\ X e. V /\ A =/= (/))) -> -. (/) = |^|y))))
41	40	ex 373	. . . . . . . . . . . . . . . . 17 |- (y (_ A -> (A (_ x -> (E.u e. om y ~~ u -> (-. y = (/) -> ((x e. Fil /\ (A (_ P~X /\ X e. V /\ A =/= (/))) -> -. (/) = |^|y)))))
42	41	com23 32	. . . . . . . . . . . . . . . 16 |- (y (_ A -> (E.u e. om y ~~ u -> (A (_ x -> (-. y = (/) -> ((x e. Fil /\ (A (_ P~X /\ X e. V /\ A =/= (/))) -> -. (/) = |^|y)))))
43	42	imp 350	. . . . . . . . . . . . . . 15 |- ((y (_ A /\ E.u e. om y ~~ u) -> (A (_ x -> (-. y = (/) -> ((x e. Fil /\ (A (_ P~X /\ X e. V /\ A =/= (/))) -> -. (/) = |^|y))))
44	43	com14 38	. . . . . . . . . . . . . 14 |- ((x e. Fil /\ (A (_ P~X /\ X e. V /\ A =/= (/))) -> (A (_ x -> (-. y = (/) -> ((y (_ A /\ E.u e. om y ~~ u) -> -. (/) = |^|y))))
45	44	ex 373	. . . . . . . . . . . . 13 |- (x e. Fil -> ((A (_ P~X /\ X e. V /\ A =/= (/)) -> (A (_ x -> (-. y = (/) -> ((y (_ A /\ E.u e. om y ~~ u) -> -. (/) = |^|y)))))
46	45	com23 32	. . . . . . . . . . . 12 |- (x e. Fil -> (A (_ x -> ((A (_ P~X /\ X e. V /\ A =/= (/)) -> (-. y = (/) -> ((y (_ A /\ E.u e. om y ~~ u) -> -. (/) = |^|y)))))
47	46	imp31 362	. . . . . . . . . . 11 |- (((x e. Fil /\ A (_ x) /\ (A (_ P~X /\ X e. V /\ A =/= (/))) -> (-. y = (/) -> ((y (_ A /\ E.u e. om y ~~ u) -> -. (/) = |^|y)))
48		inteq 2532	. . . . . . . . . . . . . . . 16 |- ((/) = y -> |^|(/) = |^|y)
49		int0 2543	. . . . . . . . . . . . . . . . . 18 |- |^|(/) = V
50	49	eqeq1i 1480	. . . . . . . . . . . . . . . . 17 |- (|^|(/) = |^|y <-> V = |^|y)
51		0ex 2707	. . . . . . . . . . . . . . . . . . 19 |- (/) e. V
52		ne0i 2283	. . . . . . . . . . . . . . . . . . 19 |- ((/) e. V -> V =/= (/))
53	51, 52	ax-mp 7	. . . . . . . . . . . . . . . . . 18 |- V =/= (/)
54		neeq1 1588	. . . . . . . . . . . . . . . . . 18 |- (V = |^|y -> (V =/= (/) <-> |^|y =/= (/)))
55	53, 54	mpbii 193	. . . . . . . . . . . . . . . . 17 |- (V = |^|y -> |^|y =/= (/))
56	50, 55	sylbi 199	. . . . . . . . . . . . . . . 16 |- (|^|(/) = |^|y -> |^|y =/= (/))
57	48, 56	syl 10	. . . . . . . . . . . . . . 15 |- ((/) = y -> |^|y =/= (/))
58	57	eqcoms 1476	. . . . . . . . . . . . . 14 |- (y = (/) -> |^|y =/= (/))
59	58	necomd 1635	. . . . . . . . . . . . 13 |- (y = (/) -> (/) =/= |^|y)
60	59, 28	sylib 198	. . . . . . . . . . . 12 |- (y = (/) -> -. (/) = |^|y)
61	60	a1d 12	. . . . . . . . . . 11 |- (y = (/) -> ((y (_ A /\ E.u e. om y ~~ u) -> -. (/) = |^|y))
62	47, 61	pm2.61d2 129	. . . . . . . . . 10 |- (((x e. Fil /\ A (_ x) /\ (A (_ P~X /\ X e. V /\ A =/= (/))) -> ((y (_ A /\ E.u e. om y ~~ u) -> -. (/) = |^|y))
63	62	imp 350	. . . . . . . . 9 |-