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
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 A1: 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
deffunc H₁( set ) -> Element of bool [:X,{$1}:] = X --> $1;
consider f being ManySortedSet of such that
A2: for i being Element of L holds f . i = H₁(i) from PBOOLE:sch 5();
A3: dom f = the carrier of L by PARTFUN1:def 4;
rng f c= the carrier of R

proof

let y be set ; :: 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 set such that
A4: ( x in dom f & y = f . x ) by FUNCT_1:def 5;
reconsider x = x as Element of L by A4, PARTFUN1:def 4;
y = X --> x by A2, A4;
then y is Element of R by A1;
hence y in the carrier of R ; :: thesis: verum

end;

then reconsider f = f as Function of L,R by A3, FUNCT_2:4;
take f ; :: according to WAYBEL_1:def 8 :: thesis: f is isomorphic
A5: 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 set ; :: 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
A6: a = X --> i by A1;
a = f . i by A2, A6;
hence x in rng f by A3, FUNCT_1:def 5; :: thesis: verum

end;

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 . x = X --> x & f . y = X --> y ) by A2;
then ( f . x = [:X,{x}:] & f . y = [:X,{y}:] ) by FUNCOP_1:def 2;
then ( f . x = f . y implies {x} = {y} ) by ZFMISC_1:134;
hence ( not f . x = f . y or x = y ) by ZFMISC_1:6; :: thesis: verum

end;

now

let x, y be Element of L; :: thesis: ( ( x <= y implies f . x <= f . y ) & ( f . x <= f . y implies x <= y ) )
A8: ( f . x = X --> x & f . y = X --> y ) by A2;
reconsider a = f . x, b = f . y as Element of (L |^ X) by YELLOW_0:59;
reconsider Xx = X --> x, Xy = X --> y as Function of X,L ;

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

assume A9: 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 i in X ; :: thesis: ex b₁, b₂ being Element of the carrier of L st
( b₁ = Xx . i & b₂ = Xy . i & b₁ <= b₂ )
then ( (X --> x) . i = x & (X --> y) . i = y ) by FUNCOP_1:13;
hence ex b₁, b₂ being Element of the carrier of L st
( b₁ = Xx . i & b₂ = Xy . i & b₁ <= b₂ ) by A9; :: thesis: verum

end;

then ( a <= b & f . x in the carrier of R ) by A8, WAYBEL10:12;
hence f . x <= f . y by YELLOW_0:61; :: thesis: verum

end;

reconsider a' = a, b' = b as Element of (product (X --> L)) ;
consider i being Element of X;
A10: (X --> L) . i = L by FUNCOP_1:13;
assume f . x <= f . y ; :: thesis: x <= y
then a <= b by YELLOW_0:60;
then a' . i <= b' . i by WAYBEL_3:28;
then x <= Xy . i by A8, A10, FUNCOP_1:13;
hence x <= y by FUNCOP_1:13; :: thesis: verum

end;

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