let S, T be non empty TopPoset; :: thesis: for X being non empty filtered Subset of S
for f being monotone Function of S,T
for Y being non empty filtered Subset of T st Y = f .: X holds
f * (X opp+id ) is subnet of Y opp+id
let X be non empty filtered Subset of S; :: thesis: for f being monotone Function of S,T
for Y being non empty filtered Subset of T st Y = f .: X holds
f * (X opp+id ) is subnet of Y opp+id
let f be monotone Function of S,T; :: thesis: for Y being non empty filtered Subset of T st Y = f .: X holds
f * (X opp+id ) is subnet of Y opp+id
let Y be non empty filtered Subset of T; :: thesis: ( Y = f .: X implies f * (X opp+id ) is subnet of Y opp+id )
assume A1: Y = f .: X ; :: thesis: f * (X opp+id ) is subnet of Y opp+id
set N = f * (X opp+id );
set M = Y opp+id ;
A2: ( RelStr(# the carrier of (f * (X opp+id )),the InternalRel of (f * (X opp+id )) #) = RelStr(# the carrier of (X opp+id ),the InternalRel of (X opp+id ) #) & the mapping of (f * (X opp+id )) = f * the mapping of (X opp+id ) ) by WAYBEL_9:def 8;
A3: ( the carrier of (Y opp+id ) = Y & Y opp+id is full SubRelStr of T opp & the mapping of (Y opp+id ) = id Y ) by WAYBEL19:27, YELLOW_9:7;
A4: ( the carrier of (X opp+id ) = X & X opp+id is full SubRelStr of S opp & the mapping of (X opp+id ) = id X ) by WAYBEL19:27, YELLOW_9:7;
then A5: ( the mapping of (f * (X opp+id )) = f | X & the carrier of T <> {} ) by A2, RELAT_1:94;
then A6: ( rng the mapping of (f * (X opp+id )) = f .: X & dom the mapping of (f * (X opp+id )) = X ) by A2, A4, FUNCT_2:def 1, RELAT_1:148;
then reconsider g = f | X as Function of (f * (X opp+id )),(Y opp+id ) by A1, A2, A3, A4, A5, FUNCT_2:def 1, RELSET_1:11;
take g ; :: according to YELLOW_6:def 12 :: thesis: ( the mapping of (f * (X opp+id )) = the mapping of (Y opp+id ) * g & ( for b₁ being Element of the carrier of (Y opp+id ) ex b₂ being Element of the carrier of (f * (X opp+id )) st
for b₃ being Element of the carrier of (f * (X opp+id )) holds
( not b₂ <= b₃ or b₁ <= g . b₃ ) ) )
thus the mapping of (f * (X opp+id )) = the mapping of (Y opp+id ) * g by A1, A3, A5, A6, RELAT_1:79; :: thesis: for b₁ being Element of the carrier of (Y opp+id ) ex b₂ being Element of the carrier of (f * (X opp+id )) st
for b₃ being Element of the carrier of (f * (X opp+id )) holds
( not b₂ <= b₃ or b₁ <= g . b₃ )
let m be Element of (Y opp+id ); :: thesis: ex b₁ being Element of the carrier of (f * (X opp+id )) st
for b₂ being Element of the carrier of (f * (X opp+id )) holds
( not b₁ <= b₂ or m <= g . b₂ )
consider n being set such that
A7: ( n in the carrier of S & n in X & m = f . n ) by A1, A3, FUNCT_2:115;
reconsider n = n as Element of (f * (X opp+id )) by A2, A7, YELLOW_9:7;
take n ; :: thesis: for b₁ being Element of the carrier of (f * (X opp+id )) holds
( not n <= b₁ or m <= g . b₁ )
let p be Element of (f * (X opp+id )); :: thesis: ( not n <= p or m <= g . p )
p in X by A2, A4;
then reconsider n' = n, p' = p as Element of S by A7;
reconsider fp = f . p' as Element of (Y opp+id ) by A1, A2, A3, A4, FUNCT_2:43;
X opp+id is SubRelStr of S opp by YELLOW_9:7;
then A8: ( f * (X opp+id ) is SubRelStr of S opp & n' ~ = n' & p' ~ = p' ) by A2, Th12;
A9: Y opp+id is full SubRelStr of T opp by YELLOW_9:7;
assume n <= p ; :: thesis: m <= g . p
then n' ~ <= p' ~ by A8, YELLOW_0:60;
then n' >= p' by LATTICE3:9;
then f . n' >= f . p' by WAYBEL_1:def 2;
then ( (f . n') ~ <= (f . p') ~ & (f . n') ~ = m & (f . p') ~ = fp & the carrier of (Y opp+id ) <> {} ) by A7, LATTICE3:9;
then fp >= m by A9, YELLOW_0:61;
hence m <= g . p by A2, A4, FUNCT_1:72; :: thesis: verum