let X, Y be non empty set ; :: thesis: for f being Function of X,Y
for F being Filter of X
for B being basis of F holds
( f .: (# B) is filter_base of Y & <.(f .: (# B)).] is Filter of Y & <.(f .: (# B)).] = { M where M is Subset of Y : f " M in F } )
let f be Function of X,Y; :: thesis: for F being Filter of X
for B being basis of F holds
( f .: (# B) is filter_base of Y & <.(f .: (# B)).] is Filter of Y & <.(f .: (# B)).] = { M where M is Subset of Y : f " M in F } )
let F be Filter of X; :: thesis: for B being basis of F holds
( f .: (# B) is filter_base of Y & <.(f .: (# B)).] is Filter of Y & <.(f .: (# B)).] = { M where M is Subset of Y : f " M in F } )
let B be basis of F; :: thesis: ( f .: (# B) is filter_base of Y & <.(f .: (# B)).] is Filter of Y & <.(f .: (# B)).] = { M where M is Subset of Y : f " M in F } )
set FB = f .: (# B);
now :: thesis: not f .: (# B) is empty
set b0 = the Element of B;
f .: the Element of B in f .: (# B) by FUNCT_2:def 10;
hence not f .: (# B) is empty ; :: thesis: verum
end;
then reconsider FB1 = f .: (# B) as non empty Subset-Family of Y ;
A1: f .: (# B) is non empty quasi_basis Subset-Family of Y
proof
now :: thesis: for b1, b2 being Element of f .: (# B) ex b being Element of f .: (# B) st b c= b1 /\ b2
let b1, b2 be Element of f .: (# B); :: thesis: ex b being Element of f .: (# B) st b c= b1 /\ b2
b1 in FB1 ;
then consider M being Subset of X such that
A2: M in # B and
A3: b1 = f .: M by FUNCT_2:def 10;
b2 in FB1 ;
then consider N being Subset of X such that
A4: N in # B and
A5: b2 = f .: N by FUNCT_2:def 10;
( # B is quasi_basis & M in # B & N in # B ) by A2, A4, Th09;
then consider P being Element of B such that
A6: P c= M /\ N ;
A7: f .: P c= f .: (M /\ N) by A6, RELAT_1:123;
f .: (M /\ N) c= (f .: M) /\ (f .: N) by RELAT_1:121;
then A8: f .: P c= b1 /\ b2 by A3, A5, A7;
f .: P is Element of f .: (# B) by FUNCT_2:def 10;
hence ex b being Element of f .: (# B) st b c= b1 /\ b2 by A8; :: thesis: verum
end;
then FB1 is quasi_basis ;
hence f .: (# B) is non empty quasi_basis Subset-Family of Y ; :: thesis: verum
end;
A9: f .: (# B) is with_non-empty_elements
proof
assume not f .: (# B) is with_non-empty_elements ; :: thesis: contradiction
then consider x being Subset of X such that
A10: x in # B and
A11: {} = f .: x by FUNCT_2:def 10;
dom f = X by FUNCT_2:def 1;
then X misses x by A11, RELAT_1:118;
then {} in B by A10, XBOOLE_1:67;
hence contradiction by CARD_FIL:def 1; :: thesis: verum
end;
hence f .: (# B) is filter_base of Y by A1; :: thesis: ( <.(f .: (# B)).] is Filter of Y & <.(f .: (# B)).] = { M where M is Subset of Y : f " M in F } )
thus <.(f .: (# B)).] is Filter of Y by A1, A9, Th08; :: thesis: <.(f .: (# B)).] = { M where M is Subset of Y : f " M in F }
thus <.(f .: (# B)).] = { M where M is Subset of Y : f " M in F } :: thesis: verum
proof
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: { M where M is Subset of Y : f " M in F } c= <.(f .: (# B)).]
let y be object ; :: thesis: ( y in <.(f .: (# B)).] implies y in { M where M is Subset of Y : f " M in F } )
assume A12: y in <.(f .: (# B)).] ; :: thesis: y in { M where M is Subset of Y : f " M in F }
then reconsider y0 = y as Subset of Y ;
consider b being Element of f .: (# B) such that
A13: b c= y0 by A12, def3;
b in FB1 ;
then consider M being Subset of X such that
A14: M in # B and
A15: b = f .: M by FUNCT_2:def 10;
A16: f " (f .: M) c= f " y0 by A13, A15, RELAT_1:143;
M c= f " (f .: M) by FUNCT_2:42;
then M c= f " y0 by A16;
then f " y0 in <.(# B).] by A14, def3;
then f " y0 in F by Th06;
hence y in { M where M is Subset of Y : f " M in F } ; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { M where M is Subset of Y : f " M in F } or x in <.(f .: (# B)).] )
assume x in { M where M is Subset of Y : f " M in F } ; :: thesis: x in <.(f .: (# B)).]
then consider M0 being Subset of Y such that
A17: x = M0 and
A18: f " M0 in F ;
f " M0 in <.(# B).] by A18, Th06;
then consider b0 being Element of # B such that
A19: b0 c= f " M0 by def3;
A20: f .: b0 c= f .: (f " M0) by A19, RELAT_1:123;
reconsider fb = f .: b0 as Element of f .: (# B) by FUNCT_2:def 10;
f .: (f " M0) c= M0 by FUNCT_1:75;
then fb c= M0 by A20;
hence x in <.(f .: (# B)).] by A17, def3; :: thesis: verum
end;