let X, Y be non empty set ; :: thesis: for f being Function of X,Y
for F being Filter of X holds
( f .: F is Filter of Y iff Y = rng f )
let f be Function of X,Y; :: thesis: for F being Filter of X holds
( f .: F is Filter of Y iff Y = rng f )
let F be Filter of X; :: thesis: ( f .: F is Filter of Y iff Y = rng f )
hereby :: thesis: ( Y = rng f implies f .: F is Filter of Y )
assume f .: F is Filter of Y ; :: thesis: Y = rng f
then Y in f .: F by CARD_FIL:5;
then consider B being Subset of X such that
B in F and
A1: Y = f .: B by FUNCT_2:def 10;
now :: thesis: for y being object st y in Y holds
y in rng f
let y be object ; :: thesis: ( y in Y implies y in rng f )
assume y in Y ; :: thesis: y in rng f
then consider x being object such that
A2: x in dom f and
x in B and
A3: y = f . x by A1, FUNCT_1:def 6;
thus y in rng f by A2, A3, FUNCT_1:def 3; :: thesis: verum
end;
then Y c= rng f ;
hence Y = rng f ; :: thesis: verum
end;
assume A4: Y = rng f ; :: thesis: f .: F is Filter of Y
reconsider fF = f .: F as filter_base of Y by Th13;
A5: fF c= <.fF.) by def3;
<.fF.) c= fF
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in <.fF.) or x in fF )
assume A6: x in <.fF.) ; :: thesis: x in fF
then reconsider x1 = x as Subset of Y ;
consider b2 being Element of fF such that
A7: b2 c= x1 by A6, def3;
consider bx being Subset of X such that
A8: bx in F and
A9: b2 = f .: bx by FUNCT_2:def 10;
reconsider fx1 = f " x1 as Subset of X ;
A10: dom f = X by FUNCT_2:def 1;
A11: f " (f .: bx) c= f " x1 by A7, A9, RELAT_1:143;
bx c= f " (f .: bx) by A10, FUNCT_1:76;
then bx c= f " x1 by A11;
then fx1 in F by A8, CARD_FIL:def 1;
then f .: fx1 in fF by FUNCT_2:def 10;
hence x in fF by A4, FUNCT_1:77; :: thesis: verum
end;
then fF = <.fF.) by A5;
hence f .: F is Filter of Y ; :: thesis: verum