let L be non empty RelStr ; :: thesis: for X being non empty set
for R being non empty full SubRelStr of L |^ X st ( for a being set holds
( a is Element of R iff ex x being Element of L st a = X --> x ) ) holds
L,R are_isomorphic
let X be non empty set ; :: thesis: for R being non empty full SubRelStr of L |^ X st ( for a being set holds
( a is Element of R iff ex x being Element of L st a = X --> x ) ) holds
L,R are_isomorphic
deffunc H₁( set ) -> Element of bool [:X,{$1}:] = X --> $1;
consider f being ManySortedSet of the carrier of L such that
A1: for i being Element of L holds f . i = H₁(i) from PBOOLE:sch 5();
let R be non empty full SubRelStr of L |^ X; :: thesis: ( ( for a being set holds
( a is Element of R iff ex x being Element of L st a = X --> x ) ) implies L,R are_isomorphic )
assume A2: for a being set holds
( a is Element of R iff ex x being Element of L st a = X --> x ) ; :: thesis: L,R are_isomorphic
A3: rng f c= the carrier of R

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in the carrier of R )
assume y in rng f ; :: thesis: y in the carrier of R
then consider x being object such that
A4: x in dom f and
A5: y = f . x by FUNCT_1:def 3;
reconsider x = x as Element of L by A4;
y = X --> x by A1, A5;
then y is Element of R by A2;
hence y in the carrier of R ; :: thesis: verum

end;

A6: dom f = the carrier of L by PARTFUN1:def 2;
then reconsider f = f as Function of L,R by A3, FUNCT_2:2;
A7: f is one-to-one

proof

let x, y be Element of L; :: according to WAYBEL_1:def 1 :: thesis: ( not f . x = f . y or x = y )
f . y = X --> y by A1;
then A8: f . y = [:X,{y}:] by FUNCOP_1:def 2;
f . x = X --> x by A1;
then f . x = [:X,{x}:] by FUNCOP_1:def 2;
then ( f . x = f . y implies {x} = {y} ) by A8, ZFMISC_1:110;
hence ( not f . x = f . y or x = y ) by ZFMISC_1:3; :: thesis: verum

end;

A9: now :: thesis: for x, y being Element of L holds
( ( x <= y implies f . x <= f . y ) & ( f . x <= f . y implies x <= y ) )

set i = the Element of X;
let x, y be Element of L; :: thesis: ( ( x <= y implies f . x <= f . y ) & ( f . x <= f . y implies x <= y ) )
reconsider a = f . x, b = f . y as Element of (L |^ X) by YELLOW_0:58;
reconsider Xx = X --> x, Xy = X --> y as Function of X,L ;
reconsider a9 = a, b9 = b as Element of (product (X --> L)) ;
A11: f . y = X --> y by A1;
A12: f . x = X --> x by A1;

hereby :: thesis: ( f . x <= f . y implies x <= y )

assume A13: x <= y ; :: thesis: f . x <= f . y
Xx <= Xy

proof

let i be set ; :: according to YELLOW_2:def 1 :: thesis: ( not i in X or ex b₁, b₂ being Element of the carrier of L st
( b₁ = Xx . i & b₂ = Xy . i & b₁ <= b₂ ) )
assume A14: i in X ; :: thesis: ex b₁, b₂ being Element of the carrier of L st
( b₁ = Xx . i & b₂ = Xy . i & b₁ <= b₂ )
then A15: (X --> y) . i = y by FUNCOP_1:7;
(X --> x) . i = x by A14, FUNCOP_1:7;
hence ex b₁, b₂ being Element of the carrier of L st
( b₁ = Xx . i & b₂ = Xy . i & b₁ <= b₂ ) by A13, A15; :: thesis: verum

end;

then a <= b by A12, A11, WAYBEL10:11;
hence f . x <= f . y by YELLOW_0:60; :: thesis: verum

end;

assume f . x <= f . y ; :: thesis: x <= y
then a <= b by YELLOW_0:59;
then a9 . the Element of X <= b9 . the Element of X by WAYBEL_3:28;
then x <= Xy . the Element of X by A12, A11;
hence x <= y ; :: thesis: verum

end;

take f ; :: according to WAYBEL_1:def 8 :: thesis: f is isomorphic
rng f = the carrier of R

proof

thus rng f c= the carrier of R ; :: according to XBOOLE_0:def 10 :: thesis: the carrier of R c= rng f
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of R or x in rng f )
assume x in the carrier of R ; :: thesis: x in rng f
then reconsider a = x as Element of R ;
consider i being Element of L such that
A16: a = X --> i by A2;
a = f . i by A1, A16;
hence x in rng f by A6, FUNCT_1:def 3; :: thesis: verum

end;

hence f is isomorphic by A7, A9, WAYBEL_0:66; :: thesis: verum