Theorem filintf 10707

Description: The intersection of two filters is a filter. Use fiint 4644 to extend this property to the intersection of a finite set of filters. Bourbaki TG I.36 par. 3.

Assertion

Ref	Expression
filintf	|- ((F e. Fil /\ G e. Fil /\ U.F = U.G) -> (F i^i G) e. Fil)

Proof of Theorem filintf

Step	Hyp	Ref	Expression
1		eqid 1512	. . . . . 6 |- U.(F i^i G) = U.(F i^i G)
2	1	isfil 10697	. . . . 5 |- ((F i^i G) e. V -> ((F i^i G) e. Fil <-> ((-. (/) e. (F i^i G) /\ U.(F i^i G) e. (F i^i G)) /\ A.xA.y((x e. (F i^i G) /\ y (_ U.(F i^i G) /\ x (_ y) -> y e. (F i^i G)) /\ A.x e. (F i^i G)A.y e. (F i^i G)(x i^i y) e. (F i^i G))))
3		filesn 10698	. . . . . . . . 9 |- (F e. Fil -> -. (/) e. F)
4		elin 2251	. . . . . . . . . 10 |- ((/) e. (F i^i G) <-> ((/) e. F /\ (/) e. G))
5	4	pm3.26bi 320	. . . . . . . . 9 |- ((/) e. (F i^i G) -> (/) e. F)
6	3, 5	nsyl 115	. . . . . . . 8 |- (F e. Fil -> -. (/) e. (F i^i G))
7	6	3ad2ant1 803	. . . . . . 7 |- ((F e. Fil /\ G e. Fil /\ U.F = U.G) -> -. (/) e. (F i^i G))
8		ineq2 2255	. . . . . . . . . . . . . 14 |- (U.F = U.G -> (U.F i^i U.F) = (U.F i^i U.G))
9		inidm 2266	. . . . . . . . . . . . . 14 |- (U.F i^i U.F) = U.F
10	8, 9	syl5eqr 1558	. . . . . . . . . . . . 13 |- (U.F = U.G -> U.F = (U.F i^i U.G))
11	10	3ad2ant3 805	. . . . . . . . . . . 12 |- ((F e. Fil /\ G e. Fil /\ U.F = U.G) -> U.F = (U.F i^i U.G))
12		eqid 1512	. . . . . . . . . . . . . . . 16 |- U.G = U.G
13	12	filusb 10700	. . . . . . . . . . . . . . 15 |- (G e. Fil -> U.G e. G)
14		eleq1 1571	. . . . . . . . . . . . . . . . 17 |- (U.F = U.G -> (U.F e. G <-> U.G e. G))
15		elin 2251	. . . . . . . . . . . . . . . . . . 19 |- (U.F e. (F i^i G) <-> (U.F e. F /\ U.F e. G))
16	15	biimpri 150	. . . . . . . . . . . . . . . . . 18 |- ((U.F e. F /\ U.F e. G) -> U.F e. (F i^i G))
17	16	expcom 372	. . . . . . . . . . . . . . . . 17 |- (U.F e. G -> (U.F e. F -> U.F e. (F i^i G)))
18	14, 17	syl6bir 213	. . . . . . . . . . . . . . . 16 |- (U.F = U.G -> (U.G e. G -> (U.F e. F -> U.F e. (F i^i G))))
19	18	com3l 34	. . . . . . . . . . . . . . 15 |- (U.G e. G -> (U.F e. F -> (U.F = U.G -> U.F e. (F i^i G))))
20	13, 19	syl 10	. . . . . . . . . . . . . 14 |- (G e. Fil -> (U.F e. F -> (U.F = U.G -> U.F e. (F i^i G))))
21		eqid 1512	. . . . . . . . . . . . . . 15 |- U.F = U.F
22	21	filusb 10700	. . . . . . . . . . . . . 14 |- (F e. Fil -> U.F e. F)
23	20, 22	syl5com 52	. . . . . . . . . . . . 13 |- (F e. Fil -> (G e. Fil -> (U.F = U.G -> U.F e. (F i^i G))))
24	23	3imp 830	. . . . . . . . . . . 12 |- ((F e. Fil /\ G e. Fil /\ U.F = U.G) -> U.F e. (F i^i G))
25	11, 24	eqeltrrd 1586	. . . . . . . . . . 11 |- ((F e. Fil /\ G e. Fil /\ U.F = U.G) -> (U.F i^i U.G) e. (F i^i G))
26		elssuni 2574	. . . . . . . . . . 11 |- ((U.F i^i U.G) e. (F i^i G) -> (U.F i^i U.G) (_ U.(F i^i G))
27	25, 26	syl 10	. . . . . . . . . 10 |- ((F e. Fil /\ G e. Fil /\ U.F = U.G) -> (U.F i^i U.G) (_ U.(F i^i G))
28		uniin 2568	. . . . . . . . . 10 |- U.(F i^i G) (_ (U.F i^i U.G)
29	27, 28	jctil 290	. . . . . . . . 9 |- ((F e. Fil /\ G e. Fil /\ U.F = U.G) -> (U.(F i^i G) (_ (U.F i^i U.G) /\ (U.F i^i U.G) (_ U.(F i^i G)))
30		eqss 2121	. . . . . . . . 9 |- (U.(F i^i G) = (U.F i^i U.G) <-> (U.(F i^i G) (_ (U.F i^i U.G) /\ (U.F i^i U.G) (_ U.(F i^i G)))
31	29, 30	sylibr 198	. . . . . . . 8 |- ((F e. Fil /\ G e. Fil /\ U.F = U.G) -> U.(F i^i G) = (U.F i^i U.G))
32	31, 25	eqeltrd 1585	. . . . . . 7 |- ((F e. Fil /\ G e. Fil /\ U.F = U.G) -> U.(F i^i G) e. (F i^i G))
33	7, 32	jca 286	. . . . . 6 |- ((F e. Fil /\ G e. Fil /\ U.F = U.G) -> (-. (/) e. (F i^i G) /\ U.(F i^i G) e. (F i^i G)))
34	21	fillsb 10699	. . . . . . . . . . 11 |- (F e. Fil -> ((x e. F /\ y (_ U.F /\ x (_ y) -> y e. F))
35	34	3ad2ant1 803	. . . . . . . . . 10 |- ((F e. Fil /\ G e. Fil /\ U.F = U.G) -> ((x e. F /\ y (_ U.F /\ x (_ y) -> y e. F))
36	12	fillsb 10699	. . . . . . . . . . 11 |- (G e. Fil -> ((x e. G /\ y (_ U.G /\ x (_ y) -> y e. G))
37	36	3ad2ant2 804	. . . . . . . . . 10 |- ((F e. Fil /\ G e. Fil /\ U.F = U.G) -> ((x e. G /\ y (_ U.G /\ x (_ y) -> y e. G))
38	35, 37	anim12d 560	. . . . . . . . 9 |- ((F e. Fil /\ G e. Fil /\ U.F = U.G) -> (((x e. F /\ y (_ U.F /\ x (_ y) /\ (x e. G /\ y (_ U.G /\ x (_ y)) -> (y e. F /\ y e. G)))
39		elin 2251	. . . . . . . . . . . 12 |- (x e. (F i^i G) <-> (x e. F /\ x e. G))
40	39	biimpi 149	. . . . . . . . . . 11 |- (x e. (F i^i G) -> (x e. F /\ x e. G))
41		sstr2 2115	. . . . . . . . . . . . 13 |- (y (_ U.(F i^i G) -> (U.(F i^i G) (_ (U.F i^i U.G) -> y (_ (U.F i^i U.G)))
42	28, 41	mpi 44	. . . . . . . . . . . 12 |- (y (_ U.(F i^i G) -> y (_ (U.F i^i U.G))
43		ssin 2276	. . . . . . . . . . . 12 |- ((y (_ U.F /\ y (_ U.G) <-> y (_ (U.F i^i U.G))
44	42, 43	sylibr 198	. . . . . . . . . . 11 |- (y (_ U.(F i^i G) -> (y (_ U.F /\ y (_ U.G))
45		pm4.24 434	. . . . . . . . . . . 12 |- (x (_ y <-> (x (_ y /\ x (_ y))
46	45	biimpi 149	. . . . . . . . . . 11 |- (x (_ y -> (x (_ y /\ x (_ y))
47	40, 44, 46	3anim123i 824	. . . . . . . . . 10 |- ((x e. (F i^i G) /\ y (_ U.(F i^i G) /\ x (_ y) -> ((x e. F /\ x e. G) /\ (y (_ U.F /\ y (_ U.G) /\ (x (_ y /\ x (_ y)))
48		an6 905	. . . . . . . . . 10 |- (((x e. F /\ y (_ U.F /\ x (_ y) /\ (x e. G /\ y (_ U.G /\ x (_ y)) <-> ((x e. F /\ x e. G) /\ (y (_ U.F /\ y (_ U.G) /\ (x (_ y /\ x (_ y)))
49	47, 48	sylibr 198	. . . . . . . . 9 |- ((x e. (F i^i G) /\ y (_ U.(F i^i G) /\ x (_ y) -> ((x e. F /\ y (_ U.F /\ x (_ y) /\ (x e. G /\ y (_ U.G /\ x (_ y)))
50	38, 49	syl5 21	. . . . . . . 8 |- ((F e. Fil /\ G e. Fil /\ U.F = U.G) -> ((x e. (F i^i G) /\ y (_ U.(F i^i G) /\ x (_ y) -> (y e. F /\ y e. G)))
51		elin 2251	. . . . . . . 8 |- (y e. (F i^i G) <-> (y e. F /\ y e. G))
52	50, 51	syl6ibr 211	. . . . . . 7 |- ((F e. Fil /\ G e. Fil /\ U.F = U.G) -> ((x e. (F i^i G) /\ y (_ U.(F i^i G) /\ x (_ y) -> y e. (F i^i G)))
53	52	19.21aivv 1320	. . . . . 6 |- ((F e. Fil /\ G e. Fil /\ U.F = U.G) -> A.xA.y((x e. (F i^i G) /\ y (_ U.(F i^i G) /\ x (_ y) -> y e. (F i^i G)))
54		filint 10701	. . . . . . . . . . . . . . 15 |- ((F e. Fil /\ x e. F /\ y e. F) -> (x i^i y) e. F)
55	54	3expib 839	. . . . . . . . . . . . . 14 |- (F e. Fil -> ((x e. F /\ y e. F) -> (x i^i y) e. F))
56		filint 10701	. . . . . . . . . . . . . . 15 |- ((G e. Fil /\ x e. G /\ y e. G) -> (x i^i y) e. G)
57	56	3expib 839	. . . . . . . . . . . . . 14 |- (G e. Fil -> ((x e. G /\ y e. G) -> (x i^i y) e. G))
58	55, 57	im2anan9 565	. . . . . . . . . . . . 13 |- ((F e. Fil /\ G e. Fil) -> (((x e. F /\ y e. F) /\ (x e. G /\ y e. G)) -> ((x i^i y) e. F /\ (x i^i y) e. G)))
59		elin 2251	. . . . . . . . . . . . 13 |- ((x i^i y) e. (F i^i G) <-> ((x i^i y) e. F /\ (x i^i y) e. G))
60	58, 59	syl6ibr 211	. . . . . . . . . . . 12 |- ((F e. Fil /\ G e. Fil) -> (((x e. F /\ y e. F) /\ (x e. G /\ y e. G)) -> (x i^i y) e. (F i^i G)))
61	60	com12 11	. . . . . . . . . . 11 |- (((x e. F /\ y e. F) /\ (x e. G /\ y e. G)) -> ((F e. Fil /\ G e. Fil) -> (x i^i y) e. (F i^i G)))
62	61	an4s 510	. . . . . . . . . 10 |- (((x e. F /\ x e. G) /\ (y e. F /\ y e. G)) -> ((F e. Fil /\ G e. Fil) -> (x i^i y) e. (F i^i G)))
63	62, 39, 51	syl2anb 457	. . . . . . . . 9 |- ((x e. (F i^i G) /\ y e. (F i^i G)) -> ((F e. Fil /\ G e. Fil) -> (x i^i y) e. (F i^i G