Theorem filintf 10569

Description: The intersection of two filters is a filter. Use fiint 4559 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 1475	. . . . . 6 |- U.(F i^i G) = U.(F i^i G)
2	1	isfil 10558	. . . . 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 10559	. . . . . . . . 9 |- (F e. Fil -> -. (/) e. F)
4		elin 2207	. . . . . . . . . 10 |- ((/) e. (F i^i G) <-> ((/) e. F /\ (/) e. G))
5	4	pm3.26bi 322	. . . . . . . . 9 |- ((/) e. (F i^i G) -> (/) e. F)
6	3, 5	nsyl 116	. . . . . . . 8 |- (F e. Fil -> -. (/) e. (F i^i G))
7	6	3ad2ant1 800	. . . . . . 7 |- ((F e. Fil /\ G e. Fil /\ U.F = U.G) -> -. (/) e. (F i^i G))
8		ineq2 2211	. . . . . . . . . . . . . 14 |- (U.F = U.G -> (U.F i^i U.F) = (U.F i^i U.G))
9		inidm 2222	. . . . . . . . . . . . . 14 |- (U.F i^i U.F) = U.F
10	8, 9	syl5eqr 1521	. . . . . . . . . . . . 13 |- (U.F = U.G -> U.F = (U.F i^i U.G))
11	10	3ad2ant3 802	. . . . . . . . . . . 12 |- ((F e. Fil /\ G e. Fil /\ U.F = U.G) -> U.F = (U.F i^i U.G))
12		eqid 1475	. . . . . . . . . . . . . . . 16 |- U.G = U.G
13	12	filusb 10561	. . . . . . . . . . . . . . 15 |- (G e. Fil -> U.G e. G)
14		eleq1 1534	. . . . . . . . . . . . . . . . 17 |- (U.F = U.G -> (U.F e. G <-> U.G e. G))
15		elin 2207	. . . . . . . . . . . . . . . . . . 19 |- (U.F e. (F i^i G) <-> (U.F e. F /\ U.F e. G))
16	15	biimpr 152	. . . . . . . . . . . . . . . . . 18 |- ((U.F e. F /\ U.F e. G) -> U.F e. (F i^i G))
17	16	expcom 374	. . . . . . . . . . . . . . . . 17 |- (U.F e. G -> (U.F e. F -> U.F e. (F i^i G)))
18	14, 17	syl6bir 215	. . . . . . . . . . . . . . . 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 1475	. . . . . . . . . . . . . . 15 |- U.F = U.F
22	21	filusb 10561	. . . . . . . . . . . . . 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 827	. . . . . . . . . . . 12 |- ((F e. Fil /\ G e. Fil /\ U.F = U.G) -> U.F e. (F i^i G))
25	11, 24	eqeltrrd 1549	. . . . . . . . . . 11 |- ((F e. Fil /\ G e. Fil /\ U.F = U.G) -> (U.F i^i U.G) e. (F i^i G))
26		elssuni 2526	. . . . . . . . . . 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 2520	. . . . . . . . . 10 |- U.(F i^i G) (_ (U.F i^i U.G)
29	27, 28	jctil 292	. . . . . . . . 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 2077	. . . . . . . . 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 200	. . . . . . . 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 1548	. . . . . . 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 288	. . . . . 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 10560	. . . . . . . . . . 11 |- (F e. Fil -> ((x e. F /\ y (_ U.F /\ x (_ y) -> y e. F))
35	34	3ad2ant1 800	. . . . . . . . . 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 10560	. . . . . . . . . . 11 |- (G e. Fil -> ((x e. G /\ y (_ U.G /\ x (_ y) -> y e. G))
37	36	3ad2ant2 801	. . . . . . . . . 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 558	. . . . . . . . 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 2207	. . . . . . . . . . . 12 |- (x e. (F i^i G) <-> (x e. F /\ x e. G))
40	39	biimp 151	. . . . . . . . . . 11 |- (x e. (F i^i G) -> (x e. F /\ x e. G))
41		sstr2 2071	. . . . . . . . . . . . 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 2232	. . . . . . . . . . . 12 |- ((y (_ U.F /\ y (_ U.G) <-> y (_ (U.F i^i U.G))
44	42, 43	sylibr 200	. . . . . . . . . . 11 |- (y (_ U.(F i^i G) -> (y (_ U.F /\ y (_ U.G))
45		pm4.24 433	. . . . . . . . . . . 12 |- (x (_ y <-> (x (_ y /\ x (_ y))
46	45	biimp 151	. . . . . . . . . . 11 |- (x (_ y -> (x (_ y /\ x (_ y))
47	40, 44, 46	3anim123i 821	. . . . . . . . . 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 902	. . . . . . . . . 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 200	. . . . . . . . 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 2207	. . . . . . . 8 |- (y e. (F i^i G) <-> (y e. F /\ y e. G))
52	50, 51	syl6ibr 213	. . . . . . 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 1287	. . . . . 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 10562	. . . . . . . . . . . . . . 15 |- ((F e. Fil /\ x e. F /\ y e. F) -> (x i^i y) e. F)
55	54	3expib 836	. . . . . . . . . . . . . 14 |- (F e. Fil -> ((x e. F /\ y e. F) -> (x i^i y) e. F))
56		filint 10562	. . . . . . . . . . . . . . 15 |- ((G e. Fil /\ x e. G /\ y e. G) -> (x i^i y) e. G)
57	56	3expib 836	. . . . . . . . . . . . . 14 |- (G e. Fil -> ((x e. G /\ y e. G) -> (x i^i y) e. G))
58	55, 57	im2anan9 563	. . . . . . . . . . . . 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 2207	. . . . . . . . . . . . 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 213	. . . . . . . . . . . 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 508	. . . . . . . . . 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 455	. . . . . . . . 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