Theorem isfil 10558

Description: The predicate "is a filter."

Hypothesis

Ref	Expression
isfil.1	|- X = U.F

Assertion

Ref	Expression
isfil	|- (F e. A -> (F e. Fil <-> ((-. (/) e. F /\ X e. F) /\ A.xA.y((x e. F /\ y (_ X /\ x (_ y) -> y e. F) /\ A.x e. F A.y e. F (x i^i y) e. F)))

Distinct variable group:   x,F,y

Proof of Theorem isfil

Step	Hyp	Ref	Expression
1		eleq2 1535	. . . . 5 |- (f = F -> ((/) e. f <-> (/) e. F))
2	1	negbid 611	. . . 4 |- (f = F -> (-. (/) e. f <-> -. (/) e. F))
3		unieq 2510	. . . . . 6 |- (f = F -> U.f = U.F)
4		isfil.1	. . . . . . 7 |- X = U.F
5	4	eqcomi 1479	. . . . . 6 |- U.F = X
6	3, 5	syl6eq 1523	. . . . 5 |- (f = F -> U.f = X)
7		id 59	. . . . 5 |- (f = F -> f = F)
8	6, 7	eleq12d 1542	. . . 4 |- (f = F -> (U.f e. f <-> X e. F))
9	2, 8	anbi12d 628	. . 3 |- (f = F -> ((-. (/) e. f /\ U.f e. f) <-> (-. (/) e. F /\ X e. F)))
10		eleq2 1535	. . . . . 6 |- (f = F -> (x e. f <-> x e. F))
11		sseq2 2083	. . . . . . 7 |- (U.f = X -> (y (_ U.f <-> y (_ X))
12	6, 11	syl 10	. . . . . 6 |- (f = F -> (y (_ U.f <-> y (_ X))
13	10, 12	3anbi12d 894	. . . . 5 |- (f = F -> ((x e. f /\ y (_ U.f /\ x (_ y) <-> (x e. F /\ y (_ X /\ x (_ y)))
14		eleq2 1535	. . . . 5 |- (f = F -> (y e. f <-> y e. F))
15	13, 14	imbi12d 626	. . . 4 |- (f = F -> (((x e. f /\ y (_ U.f /\ x (_ y) -> y e. f) <-> ((x e. F /\ y (_ X /\ x (_ y) -> y e. F)))
16	15	2albidv 1280	. . 3 |- (f = F -> (A.xA.y((x e. f /\ y (_ U.f /\ x (_ y) -> y e. f) <-> A.xA.y((x e. F /\ y (_ X /\ x (_ y) -> y e. F)))
17		eleq2 1535	. . . . 5 |- (f = F -> ((x i^i y) e. f <-> (x i^i y) e. F))
18	17	raleqd 1791	. . . 4 |- (f = F -> (A.y e. f (x i^i y) e. f <-> A.y e. F (x i^i y) e. F))
19	18	raleqd 1791	. . 3 |- (f = F -> (A.x e. f A.y e. f (x i^i y) e. f <-> A.x e. F A.y e. F (x i^i y) e. F))
20	9, 16, 19	3anbi123d 893	. 2 |- (f = F -> (((-. (/) e. f /\ U.f e. f) /\ A.xA.y((x e. f /\ y (_ U.f /\ x (_ y) -> y e. f) /\ A.x e. f A.y e. f (x i^i y) e. f) <-> ((-. (/) e. F /\ X e. F) /\ A.xA.y((x e. F /\ y (_ X /\ x (_ y) -> y e. F) /\ A.x e. F A.y e. F (x i^i y) e. F)))
21		df-fil 10557	. 2 |- Fil = {f | ((-. (/) e. f /\ U.f e. f) /\ A.xA.y((x e. f /\ y (_ U.f /\ x (_ y) -> y e. f) /\ A.x e. f A.y e. f (x i^i y) e. f)}
22	20, 21	elab2g 1900	1 |- (F e. A -> (F e. Fil <-> ((-. (/) e. F /\ X e. F) /\ A.xA.y((x e. F /\ y (_ X /\ x (_ y) -> y e. F) /\ A.x e. F A.y e. F (x i^i y) e. F)))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 146   /\ wa 223   /\ w3a 775  A.wal 954   = wceq 956   e. wcel 958  A.wral 1645   i^i cin 2046   (_ wss 2047  (/)c0 2280  U.cuni 2503  Filcfil 10556

This theorem is referenced by:  filesn 10559  fillsb 10560  filusb 10561  filint 10562  fipfil2 10564  fipfil2OLD 10565  oefil2 10567  neifil 10568  filintf 10569  fgsb 10570  fgsbOLD 10571  filint2 10574  filint2OLD 10575  fgsb2 10580  rcfpfil 10597  rcfpfilOLD 10598

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 962  ax-gen 963  ax-8 964  ax-10 966  ax-12 968  ax-17 971  ax-4 973  ax-5o 975  ax-6o 978  ax-9o 1123  ax-10o 1140  ax-16 1210  ax-11o 1218  ax-ext 1459

This theorem depends on definitions:  df-bi 147  df-an 225  df-3an 777  df-ex 981  df-sb 1172  df-clab 1464  df-cleq 1469  df-clel 1472  df-ral 1649  df-v 1812  df-in 2051  df-ss 2053  df-uni 2504  df-fil 10557

Copyright terms: Public domain