let S, T be non empty TopSpace; :: thesis: for f being Function of S,T st f is bijective & ex K being prebasis of S ex L being prebasis of T st f .: K = L holds

f is being_homeomorphism

let f be Function of S,T; :: thesis: ( f is bijective & ex K being prebasis of S ex L being prebasis of T st f .: K = L implies f is being_homeomorphism )

assume A1: f is bijective ; :: thesis: ( for K being prebasis of S

for L being prebasis of T holds not f .: K = L or f is being_homeomorphism )

given K being prebasis of S, L being prebasis of T such that A2: f .: K = L ; :: thesis: f is being_homeomorphism

reconsider K0 = FinMeetCl K as Basis of S by YELLOW_9:23;

reconsider L0 = FinMeetCl L as Basis of T by YELLOW_9:23;

reconsider g = f " as Function of T,S ;

reconsider f0 = f as one-to-one Function by A1;

a3: f0 " = g by A1, TOPS_2:def 4;

for W being Subset of T holds

( W in L0 iff ex V being Subset of S st

( V in K0 & f .: V = W ) )

hence f is being_homeomorphism by A1, Th47; :: thesis: verum

f is being_homeomorphism

let f be Function of S,T; :: thesis: ( f is bijective & ex K being prebasis of S ex L being prebasis of T st f .: K = L implies f is being_homeomorphism )

assume A1: f is bijective ; :: thesis: ( for K being prebasis of S

for L being prebasis of T holds not f .: K = L or f is being_homeomorphism )

given K being prebasis of S, L being prebasis of T such that A2: f .: K = L ; :: thesis: f is being_homeomorphism

reconsider K0 = FinMeetCl K as Basis of S by YELLOW_9:23;

reconsider L0 = FinMeetCl L as Basis of T by YELLOW_9:23;

reconsider g = f " as Function of T,S ;

reconsider f0 = f as one-to-one Function by A1;

a3: f0 " = g by A1, TOPS_2:def 4;

for W being Subset of T holds

( W in L0 iff ex V being Subset of S st

( V in K0 & f .: V = W ) )

proof

then
f .: K0 = L0
by FUNCT_2:def 10;
let W be Subset of T; :: thesis: ( W in L0 iff ex V being Subset of S st

( V in K0 & f .: V = W ) )

thus ( W in L0 implies ex V being Subset of S st

( V in K0 & f .: V = W ) ) :: thesis: ( ex V being Subset of S st

( V in K0 & f .: V = W ) implies W in L0 )

consider X being Subset-Family of S such that

A18: ( X c= K & X is finite & V = Intersect X ) by A17, CANTOR_1:def 3;

end;( V in K0 & f .: V = W ) )

thus ( W in L0 implies ex V being Subset of S st

( V in K0 & f .: V = W ) ) :: thesis: ( ex V being Subset of S st

( V in K0 & f .: V = W ) implies W in L0 )

proof

given V being Subset of S such that A17:
( V in K0 & f .: V = W )
; :: thesis: W in L0
assume
W in L0
; :: thesis: ex V being Subset of S st

( V in K0 & f .: V = W )

then consider Y being Subset-Family of T such that

A4: ( Y c= L & Y is finite & W = Intersect Y ) by CANTOR_1:def 3;

end;( V in K0 & f .: V = W )

then consider Y being Subset-Family of T such that

A4: ( Y c= L & Y is finite & W = Intersect Y ) by CANTOR_1:def 3;

per cases
( Y <> {} or Y = {} )
;

end;

suppose A5:
Y <> {}
; :: thesis: ex V being Subset of S st

( V in K0 & f .: V = W )

( V in K0 & f .: V = W )

then A6:
W = meet Y
by A4, SETFAM_1:def 9;

reconsider X = g .: Y as Subset-Family of S ;

reconsider V = meet X as Subset of S ;

take V ; :: thesis: ( V in K0 & f .: V = W )

ex Z being Subset-Family of S st

( Z c= K & Z is finite & V = Intersect Z )

set Z = { (f .: A) where A is Subset of S : A in X } ;

for x being object holds

( x in { (f .: A) where A is Subset of S : A in X } iff x in Y )

hence f .: V = W by A1, A6, Th4; :: thesis: verum

end;reconsider X = g .: Y as Subset-Family of S ;

reconsider V = meet X as Subset of S ;

take V ; :: thesis: ( V in K0 & f .: V = W )

ex Z being Subset-Family of S st

( Z c= K & Z is finite & V = Intersect Z )

proof

hence
V in K0
by CANTOR_1:def 3; :: thesis: f .: V = W
take
X
; :: thesis: ( X c= K & X is finite & V = Intersect X )

for x being object st x in X holds

x in K

consider B being object such that

A10: B in Y by A5, XBOOLE_0:def 1;

reconsider B = B as Subset of T by A10;

g .: B in X by A10, FUNCT_2:def 10;

hence V = Intersect X by SETFAM_1:def 9; :: thesis: verum

end;for x being object st x in X holds

x in K

proof

hence
( X c= K & X is finite )
by A4, TARSKI:def 3; :: thesis: V = Intersect X
let x be object ; :: thesis: ( x in X implies x in K )

assume x in X ; :: thesis: x in K

then consider B being Subset of T such that

A7: ( B in Y & x = g .: B ) by FUNCT_2:def 10;

consider A being Subset of S such that

A8: ( A in K & B = f .: A ) by A2, A4, A7, FUNCT_2:def 10;

A9: dom f = the carrier of S by FUNCT_2:def 1;

x = f " (f .: A) by a3, FUNCT_1:85, A7, A8

.= A by A1, A9, FUNCT_1:94 ;

hence x in K by A8; :: thesis: verum

end;assume x in X ; :: thesis: x in K

then consider B being Subset of T such that

A7: ( B in Y & x = g .: B ) by FUNCT_2:def 10;

consider A being Subset of S such that

A8: ( A in K & B = f .: A ) by A2, A4, A7, FUNCT_2:def 10;

A9: dom f = the carrier of S by FUNCT_2:def 1;

x = f " (f .: A) by a3, FUNCT_1:85, A7, A8

.= A by A1, A9, FUNCT_1:94 ;

hence x in K by A8; :: thesis: verum

consider B being object such that

A10: B in Y by A5, XBOOLE_0:def 1;

reconsider B = B as Subset of T by A10;

g .: B in X by A10, FUNCT_2:def 10;

hence V = Intersect X by SETFAM_1:def 9; :: thesis: verum

set Z = { (f .: A) where A is Subset of S : A in X } ;

for x being object holds

( x in { (f .: A) where A is Subset of S : A in X } iff x in Y )

proof

then
{ (f .: A) where A is Subset of S : A in X } = Y
by TARSKI:2;
let x be object ; :: thesis: ( x in { (f .: A) where A is Subset of S : A in X } iff x in Y )

A11: rng f = the carrier of T by A1, FUNCT_2:def 3;

then reconsider B = x as Subset of T ;

A15: g .: B in X by A14, FUNCT_2:def 10;

f .: (g .: B) = f .: (f " B) by a3, FUNCT_1:85

.= B by A11, FUNCT_1:77 ;

hence x in { (f .: A) where A is Subset of S : A in X } by A15; :: thesis: verum

end;A11: rng f = the carrier of T by A1, FUNCT_2:def 3;

hereby :: thesis: ( x in Y implies x in { (f .: A) where A is Subset of S : A in X } )

assume A14:
x in Y
; :: thesis: x in { (f .: A) where A is Subset of S : A in X } assume
x in { (f .: A) where A is Subset of S : A in X }
; :: thesis: x in Y

then consider A being Subset of S such that

A12: ( f .: A = x & A in X ) ;

consider B being Subset of T such that

A13: ( B in Y & A = g .: B ) by A12, FUNCT_2:def 10;

x = f .: (f " B) by a3, FUNCT_1:85, A12, A13

.= B by A11, FUNCT_1:77 ;

hence x in Y by A13; :: thesis: verum

end;then consider A being Subset of S such that

A12: ( f .: A = x & A in X ) ;

consider B being Subset of T such that

A13: ( B in Y & A = g .: B ) by A12, FUNCT_2:def 10;

x = f .: (f " B) by a3, FUNCT_1:85, A12, A13

.= B by A11, FUNCT_1:77 ;

hence x in Y by A13; :: thesis: verum

then reconsider B = x as Subset of T ;

A15: g .: B in X by A14, FUNCT_2:def 10;

f .: (g .: B) = f .: (f " B) by a3, FUNCT_1:85

.= B by A11, FUNCT_1:77 ;

hence x in { (f .: A) where A is Subset of S : A in X } by A15; :: thesis: verum

hence f .: V = W by A1, A6, Th4; :: thesis: verum

suppose
Y = {}
; :: thesis: ex V being Subset of S st

( V in K0 & f .: V = W )

( V in K0 & f .: V = W )

then A16:
W = the carrier of T
by A4, SETFAM_1:def 9;

set V = [#] S;

take [#] S ; :: thesis: ( [#] S in K0 & f .: ([#] S) = W )

set Z = the empty Subset-Family of S;

Intersect the empty Subset-Family of S = the carrier of S by SETFAM_1:def 9;

then ( the empty Subset-Family of S c= K & the empty Subset-Family of S is finite & [#] S = Intersect the empty Subset-Family of S ) by XBOOLE_1:2, STRUCT_0:def 3;

hence [#] S in K0 by CANTOR_1:def 3; :: thesis: f .: ([#] S) = W

thus f .: ([#] S) = f .: the carrier of S by STRUCT_0:def 3

.= f .: (dom f) by FUNCT_2:def 1

.= rng f by RELAT_1:113

.= W by A16, A1, FUNCT_2:def 3 ; :: thesis: verum

end;set V = [#] S;

take [#] S ; :: thesis: ( [#] S in K0 & f .: ([#] S) = W )

set Z = the empty Subset-Family of S;

Intersect the empty Subset-Family of S = the carrier of S by SETFAM_1:def 9;

then ( the empty Subset-Family of S c= K & the empty Subset-Family of S is finite & [#] S = Intersect the empty Subset-Family of S ) by XBOOLE_1:2, STRUCT_0:def 3;

hence [#] S in K0 by CANTOR_1:def 3; :: thesis: f .: ([#] S) = W

thus f .: ([#] S) = f .: the carrier of S by STRUCT_0:def 3

.= f .: (dom f) by FUNCT_2:def 1

.= rng f by RELAT_1:113

.= W by A16, A1, FUNCT_2:def 3 ; :: thesis: verum

consider X being Subset-Family of S such that

A18: ( X c= K & X is finite & V = Intersect X ) by A17, CANTOR_1:def 3;

per cases
( X <> {} or X = {} )
;

end;

suppose A19:
X <> {}
; :: thesis: W in L0

then A20:
V = meet X
by A18, SETFAM_1:def 9;

ex Y being Subset-Family of T st

( Y c= L & Y is finite & W = Intersect Y )

end;ex Y being Subset-Family of T st

( Y c= L & Y is finite & W = Intersect Y )

proof

hence
W in L0
by CANTOR_1:def 3; :: thesis: verum
reconsider Y = f .: X as Subset-Family of T ;

take Y ; :: thesis: ( Y c= L & Y is finite & W = Intersect Y )

thus Y c= L :: thesis: ( Y is finite & W = Intersect Y )

set Z = { (f .: A) where A is Subset of S : A in X } ;

for x being object holds

( x in Y iff x in { (f .: A) where A is Subset of S : A in X } )

then A24: meet Y = W by A1, A17, A20, Th4;

consider A being object such that

A25: A in X by A19, XBOOLE_0:def 1;

reconsider A = A as Subset of S by A25;

f .: A in f .: X by A25, FUNCT_2:def 10;

hence W = Intersect Y by A24, SETFAM_1:def 9; :: thesis: verum

end;take Y ; :: thesis: ( Y c= L & Y is finite & W = Intersect Y )

thus Y c= L :: thesis: ( Y is finite & W = Intersect Y )

proof

thus
Y is finite
by A18; :: thesis: W = Intersect Y
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Y or x in L )

assume x in Y ; :: thesis: x in L

then ex A being Subset of S st

( A in X & f .: A = x ) by FUNCT_2:def 10;

hence x in L by A2, FUNCT_2:def 10, A18; :: thesis: verum

end;assume x in Y ; :: thesis: x in L

then ex A being Subset of S st

( A in X & f .: A = x ) by FUNCT_2:def 10;

hence x in L by A2, FUNCT_2:def 10, A18; :: thesis: verum

set Z = { (f .: A) where A is Subset of S : A in X } ;

for x being object holds

( x in Y iff x in { (f .: A) where A is Subset of S : A in X } )

proof

then
Y = { (f .: A) where A is Subset of S : A in X }
by TARSKI:2;
let x be object ; :: thesis: ( x in Y iff x in { (f .: A) where A is Subset of S : A in X } )

then ex A being Subset of S st

( f .: A = x & A in X ) ;

hence x in Y by FUNCT_2:def 10; :: thesis: verum

end;hereby :: thesis: ( x in { (f .: A) where A is Subset of S : A in X } implies x in Y )

assume
x in { (f .: A) where A is Subset of S : A in X }
; :: thesis: x in Yassume
x in Y
; :: thesis: x in { (f .: A) where A is Subset of S : A in X }

then ex A being Subset of S st

( A in X & f .: A = x ) by FUNCT_2:def 10;

hence x in { (f .: A) where A is Subset of S : A in X } ; :: thesis: verum

end;then ex A being Subset of S st

( A in X & f .: A = x ) by FUNCT_2:def 10;

hence x in { (f .: A) where A is Subset of S : A in X } ; :: thesis: verum

then ex A being Subset of S st

( f .: A = x & A in X ) ;

hence x in Y by FUNCT_2:def 10; :: thesis: verum

then A24: meet Y = W by A1, A17, A20, Th4;

consider A being object such that

A25: A in X by A19, XBOOLE_0:def 1;

reconsider A = A as Subset of S by A25;

f .: A in f .: X by A25, FUNCT_2:def 10;

hence W = Intersect Y by A24, SETFAM_1:def 9; :: thesis: verum

suppose
X = {}
; :: thesis: W in L0

then A26:
V = the carrier of S
by A18, SETFAM_1:def 9;

set Y = the empty Subset-Family of T;

B1: ( the empty Subset-Family of T c= L & the empty Subset-Family of T is finite ) by XBOOLE_1:2;

W = f .: (dom f) by A17, A26, FUNCT_2:def 1

.= rng f by RELAT_1:113

.= the carrier of T by A1, FUNCT_2:def 3

.= Intersect the empty Subset-Family of T by SETFAM_1:def 9 ;

hence W in L0 by B1, CANTOR_1:def 3; :: thesis: verum

end;set Y = the empty Subset-Family of T;

B1: ( the empty Subset-Family of T c= L & the empty Subset-Family of T is finite ) by XBOOLE_1:2;

W = f .: (dom f) by A17, A26, FUNCT_2:def 1

.= rng f by RELAT_1:113

.= the carrier of T by A1, FUNCT_2:def 3

.= Intersect the empty Subset-Family of T by SETFAM_1:def 9 ;

hence W in L0 by B1, CANTOR_1:def 3; :: thesis: verum

hence f is being_homeomorphism by A1, Th47; :: thesis: verum