Theorem efilcp 10556

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 /\ y e. Fin /\ 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   x,B,y,z   x,X,y,z

Proof of Theorem efilcp

Step	Hyp	Ref	Expression
1		sseq2 2086	. . . . 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 1880	. . . 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 /\ y e. Fin /\ z = |^|y)}
4	3	fgsb 10555	. . . . 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 790	. . . . . . 7 |- ((A (_ P~X /\ X e. V /\ A =/= (/)) -> A (_ P~X)
7	6	adantr 391	. . . . . 6 |- (((A (_ P~X /\ X e. V /\ A =/= (/)) /\ -. (/) e. B) -> A (_ P~X)
8		abfi 10443	. . . . . . . . 9 |- A (_ {z | E.y(y (_ A /\ y e. Fin /\ z = |^|y)}
9	8, 3	sseqtr4 2097	. . . . . . . 8 |- A (_ B
10		ssel2 2067	. . . . . . . . 9 |- ((A (_ B /\ z e. A) -> z e. B)
11		ssid 2083	. . . . . . . . . 10 |- z (_ z
12		sseq1 2085	. . . . . . . . . . 11 |- (y = z -> (y (_ z <-> z (_ z))
13	12	rcla4ev 1880	. . . . . . . . . 10 |- ((z e. B /\ z (_ z) -> E.y e. B y (_ z)
14	11, 13	mpan2 698	. . . . . . . . 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 697	. . . . . . 7 |- (z e. A -> E.y e. B y (_ z)
17	16	rgen 1701	. . . . . 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 2128	. . . . 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 473	. . 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 2075	. . . . . . . . . . . . . . . . . . 19 |- ((y (_ A /\ A (_ x) -> y (_ x)
24		df-ne 1590	. . . . . . . . . . . . . . . . . . . . 21 |- (y =/= (/) <-> -. y = (/))
25		fipfil2 10550	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (x e. Fil -> ((y (_ x /\ y =/= (/) /\ y e. Fin) -> |^|y =/= (/)))
26		pm2.27 62	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((y (_ x /\ y =/= (/) /\ y e. Fin) -> (((y (_ x /\ y =/= (/) /\ y e. Fin) -> |^|y =/= (/)) -> |^|y =/= (/)))
27		necom 1639	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ((/) =/= |^|y <-> |^|y =/= (/))
28		df-ne 1590	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 =/= (/) /\ y e. Fin) -> (((y (_ x /\ y =/= (/) /\ y e. Fin) -> |^|y =/= (/)) -> -. (/) = |^|y))
32	31	3exp 834	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (y (_ x -> (y =/= (/) -> (y e. Fin -> (((y (_ x /\ y =/= (/) /\ y e. Fin) -> |^|y =/= (/)) -> -. (/) = |^|y))))
33	32	com34 36	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (y (_ x -> (y =/= (/) -> (((y (_ x /\ y =/= (/) /\ y e. Fin) -> |^|y =/= (/)) -> (y e. Fin -> -. (/) = |^|y))))
34	33	com4t 40	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((y (_ x /\ y =/= (/) /\ y e. Fin) -> |^|y =/= (/)) -> (y e. Fin -> (y (_ x -> (y =/= (/) -> -. (/) = |^|y))))
35	25, 34	syl 10	. . . . . . . . . . . . . . . . . . . . . . 23 |- (x e. Fil -> (y e. Fin -> (y (_ x -> (y =/= (/) -> -. (/) = |^|y))))
36	35	adantr 391	. . . . . . . . . . . . . . . . . . . . . 22 |- ((x e. Fil /\ (A (_ P~X /\ X e. V /\ A =/= (/))) -> (y e. Fin -> (y (_ x -> (y =/= (/) -> -. (/) = |^|y))))
37	36	com14 38	. . . . . . . . . . . . . . . . . . . . 21 |- (y =/= (/) -> (y e. Fin -> (y (_ x -> ((x e. Fil /\ (A (_ P~X /\ X e. V /\ A =/= (/))) -> -. (/) = |^|y))))
38	24, 37	sylbir 201	. . . . . . . . . . . . . . . . . . . 20 |- (-. y = (/) -> (y e. Fin -> (y (_ x -> ((x e. Fil /\ (A (_ P~X /\ X e. V /\ A =/= (/))) -> -. (/) = |^|y))))
39	38	com13 33	. . . . . . . . . . . . . . . . . . 19 |- (y (_ x -> (y e. Fin -> (-. y = (/) -> ((x e. Fil /\ (A (_ P~X /\ X e. V /\ A =/= (/))) -> -. (/) = |^|y))))
40	23, 39	syl 10	. . . . . . . . . . . . . . . . . 18 |- ((y (_ A /\ A (_ x) -> (y e. Fin -> (-. y = (/) -> ((x e. Fil /\ (A (_ P~X /\ X e. V /\ A =/= (/))) -> -. (/) = |^|y))))
41	40	ex 373	. . . . . . . . . . . . . . . . 17 |- (y (_ A -> (A (_ x -> (y e. Fin -> (-. y = (/) -> ((x e. Fil /\ (A (_ P~X /\ X e. V /\ A =/= (/))) -> -. (/) = |^|y)))))
42	41	com23 32	. . . . . . . . . . . . . . . 16 |- (y (_ A -> (y e. Fin -> (A (_ x -> (-. y = (/) -> ((x e. Fil /\ (A (_ P~X /\ X e. V /\ A =/= (/))) -> -. (/) = |^|y)))))
43	42	imp 350	. . . . . . . . . . . . . . 15 |- ((y (_ A /\ y e. Fin) -> (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 /\ y e. Fin) -> -. (/) = |^|y))))
45	44	ex 373	. . . . . . . . . . . . 13 |- (x e. Fil -> ((A (_ P~X /\ X e. V /\ A =/= (/)) -> (A (_ x -> (-. y = (/) -> ((y (_ A /\ y e. Fin) -> -. (/) = |^|y)))))
46	45	com23 32	. . . . . . . . . . . 12 |- (x e. Fil -> (A (_ x -> ((A (_ P~X /\ X e. V /\ A =/= (/)) -> (-. y = (/) -> ((y (_ A /\ y e. Fin) -> -. (/) = |^|y)))))
47	46	imp31 362	. . . . . . . . . . 11 |- (((x e. Fil /\ A (_ x) /\ (A (_ P~X /\ X e. V /\ A =/= (/))) -> (-. y = (/) -> ((y (_ A /\ y e. Fin) -> -. (/) = |^|y)))
48		inteq 2540	. . . . . . . . . . . . . . . 16 |- ((/) = y -> |^|(/) = |^|y)
49		int0 2551	. . . . . . . . . . . . . . . . . 18 |- |^|(/) = V
50	49	eqeq1i 1485	. . . . . . . . . . . . . . . . 17 |- (|^|(/) = |^|y <-> V = |^|y)
51		vne0 2290	. . . . . . . . . . . . . . . . . 18 |- V =/= (/)
52		neeq1 1593	. . . . . . . . . . . . . . . . . 18 |- (V = |^|y -> (V =/= (/) <-> |^|y =/= (/)))
53	51, 52	mpbii 193	. . . . . . . . . . . . . . . . 17 |- (V = |^|y -> |^|y =/= (/))
54	50, 53	sylbi 199	. . . . . . . . . . . . . . . 16 |- (|^|(/) = |^|y -> |^|y =/= (/))
55	48, 54	syl 10	. . . . . . . . . . . . . . 15 |- ((/) = y -> |^|y =/= (/))
56	55	eqcoms 1481	. . . . . . . . . . . . . 14 |- (y = (/) -> |^|y =/= (/))
57	56	necomd 1640	. . . . . . . . . . . . 13 |- (y = (/) -> (/) =/= |^|y)
58	57, 28	sylib 198	. . . . . . . . . . . 12 |- (y = (/) -> -. (/) = |^|y)
59	58	a1d 12	. . . . . . . . . . 11 |- (y = (/) -> ((y (_ A /\ y e. Fin) -> -. (/) = |^|y))
60	47, 59	pm2.61d2 129	. . . . . . . . . 10 |- (((x e. Fil /\ A (_ x) /\ (A (_ P~X /\ X e. V /\ A =/= (/))) -> ((y (_ A /\ y e. Fin) -> -. (/) = |^|y))
61	60	imp 350	. . . . . . . . 9 |- ((((x e. Fil /\ A (_ x) /\ (A (_ P~X /\ X e. V /\ A =/= (/))) /\ (y (_ A /\ y e. Fin)) -> -. (/) = |^|y)
62		nan 691	. . . . . . . . 9 |- ((((x e. Fil /\ A (_ x) /\ (A (_ P~X /\ X e. V /\ A =/= (/))) -> -. ((y (_ A /\ y e. Fin) /\ (/) = |^|y)) <-> ((((x e. Fil /\ A (_ x) /\ (A (_ P~X /\ X e. V /\ A =/= (/))) /\ (y (_ A /\ y e. Fin)) -> -. (/) =