Theorem filint 10269

Description: A filter is closed under taking intersections. (Contributed by FL, 20-Jul-2007.)

Assertion

Ref	Expression
filint	|- ((F e. Fil /\ A e. F /\ B e. F) -> (A i^i B) e. F)

Proof of Theorem filint

Step	Hyp	Ref	Expression
1		eqid 1884	. . . . . . . 8 |- U.F = U.F
2	1	isfil 10266	. . . . . . 7 |- (F e. Fil -> (F e. Fil <-> ((-. (/) e. F /\ U.F e. F) /\ A.xA.y((x e. F /\ y C_ U.F /\ x C_ y) -> y e. F) /\ A.x e. F A.y e. F (x i^i y) e. F)))
3	2	biimpa 460	. . . . . 6 |- ((F e. Fil /\ F e. Fil) -> ((-. (/) e. F /\ U.F e. F) /\ A.xA.y((x e. F /\ y C_ U.F /\ x C_ y) -> y e. F) /\ A.x e. F A.y e. F (x i^i y) e. F))
4	3	simp3d 890	. . . . 5 |- ((F e. Fil /\ F e. Fil) -> A.x e. F A.y e. F (x i^i y) e. F)
5	4	ex 402	. . . 4 |- (F e. Fil -> (F e. Fil -> A.x e. F A.y e. F (x i^i y) e. F))
6		ineq1 2789	. . . . . . 7 |- (x = A -> (x i^i y) = (A i^i y))
7	6	eleq1d 1963	. . . . . 6 |- (x = A -> ((x i^i y) e. F <-> (A i^i y) e. F))
8		ineq2 2790	. . . . . . 7 |- (y = B -> (A i^i y) = (A i^i B))
9	8	eleq1d 1963	. . . . . 6 |- (y = B -> ((A i^i y) e. F <-> (A i^i B) e. F))
10	7, 9	rcla42v 2384	. . . . 5 |- ((A e. F /\ B e. F) -> (A.x e. F A.y e. F (x i^i y) e. F -> (A i^i B) e. F))
11	10	com12 14	. . . 4 |- (A.x e. F A.y e. F (x i^i y) e. F -> ((A e. F /\ B e. F) -> (A i^i B) e. F))
12	5, 11	syl6 25	. . 3 |- (F e. Fil -> (F e. Fil -> ((A e. F /\ B e. F) -> (A i^i B) e. F)))
13	12	pm2.43i 78	. 2 |- (F e. Fil -> ((A e. F /\ B e. F) -> (A i^i B) e. F))
14	13	3impib 1065	1 |- ((F e. Fil /\ A e. F /\ B e. F) -> (A i^i B) e. F)

Syntax hints:  -. wn 2   -> wi 3   /\ wa 240   /\ w3a 858  A.wal 1296   = wceq 1298   e. wcel 1300  A.wral 2105   i^i cin 2592   C_ wss 2593  (/)c0 2875  U.cuni 3177  Filcfil 10264

This theorem is referenced by:  fipfil 10271  filintf 10274  filfbas 10276  hausfillim 10303  lvsovso 15038  filfinnfr 15561  isufil2 15565  ufprim 15569  filssufillem 15570  ufileu 15573  filufint 15574  ufilen 15579  filcon 15580  flimcls 15588  rnelfmlem 15592  rnelfm 15593  fmfnfmlem2 15595  fmfnfmlem3 15596  fmfnfmlem4 15597  fmfnfm 15598  flimfcls 15613  fcluscomplem 15620  filnetlem3 15642

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-ral 2109  df-rex 2110  df-v 2294  df-in 2603  df-ss 2605  df-uni 3178  df-fil 10265

Copyright terms: Public domain