let R, S be Relation; for F being Function st F is_isomorphism_of R,S holds
for a being object st a in field R holds
ex b being object st
( b in field S & F .: (R -Seg a) = S -Seg b )
let F be Function; ( F is_isomorphism_of R,S implies for a being object st a in field R holds
ex b being object st
( b in field S & F .: (R -Seg a) = S -Seg b ) )
assume A1:
F is_isomorphism_of R,S
; for a being object st a in field R holds
ex b being object st
( b in field S & F .: (R -Seg a) = S -Seg b )
then A2:
dom F = field R
;
let a be object ; ( a in field R implies ex b being object st
( b in field S & F .: (R -Seg a) = S -Seg b ) )
assume A3:
a in field R
; ex b being object st
( b in field S & F .: (R -Seg a) = S -Seg b )
take b = F . a; ( b in field S & F .: (R -Seg a) = S -Seg b )
A4:
rng F = field S
by A1;
hence
b in field S
by A3, A2, FUNCT_1:def 3; F .: (R -Seg a) = S -Seg b
A5:
F is one-to-one
by A1;
A6:
for c being object st c in S -Seg b holds
c in F .: (R -Seg a)
proof
let c be
object ;
( c in S -Seg b implies c in F .: (R -Seg a) )
assume A7:
c in S -Seg b
;
c in F .: (R -Seg a)
then A8:
c <> b
by Th1;
A9:
[c,b] in S
by A7, Th1;
then A10:
c in field S
by RELAT_1:15;
then A11:
c = F . ((F ") . c)
by A4, A5, FUNCT_1:35;
(
rng (F ") = dom F &
dom (F ") = rng F )
by A5, FUNCT_1:33;
then A12:
(F ") . c in field R
by A2, A4, A10, FUNCT_1:def 3;
then
[((F ") . c),a] in R
by A1, A3, A9, A11;
then
(F ") . c in R -Seg a
by A8, A11, Th1;
hence
c in F .: (R -Seg a)
by A2, A11, A12, FUNCT_1:def 6;
verum
end;
for c being object st c in F .: (R -Seg a) holds
c in S -Seg b
proof
let c be
object ;
( c in F .: (R -Seg a) implies c in S -Seg b )
assume
c in F .: (R -Seg a)
;
c in S -Seg b
then consider d being
object such that A13:
d in dom F
and A14:
d in R -Seg a
and A15:
c = F . d
by FUNCT_1:def 6;
[d,a] in R
by A14, Th1;
then A16:
[c,b] in S
by A1, A15;
d <> a
by A14, Th1;
then
c <> b
by A3, A2, A5, A13, A15;
hence
c in S -Seg b
by A16, Th1;
verum
end;
hence
F .: (R -Seg a) = S -Seg b
by A6, TARSKI:2; verum