defpred S1[ set , set ] means ex s1 being Element of S st
( s1 in C & [$1,$2] in E . s1 );
A1:
E is os-compatible
by Def3;
per cases
( the Sorts of A -carrier_of C is empty or not the Sorts of A -carrier_of C is empty )
;
suppose A2:
the
Sorts of
A -carrier_of C is
empty
;
:: thesis: ex b1 being Equivalence_Relation of (the Sorts of A -carrier_of C) st
for x, y being set holds
( [x,y] in b1 iff ex s1 being Element of S st
( s1 in C & [x,y] in E . s1 ) )
for
x,
y being
set holds
(
[x,y] in {} iff ex
s1 being
Element of
S st
(
s1 in C &
[x,y] in E . s1 ) )
proof
let x,
y be
set ;
:: thesis: ( [x,y] in {} iff ex s1 being Element of S st
( s1 in C & [x,y] in E . s1 ) )
thus
(
[x,y] in {} implies ex
s1 being
Element of
S st
(
s1 in C &
[x,y] in E . s1 ) )
;
:: thesis: ( ex s1 being Element of S st
( s1 in C & [x,y] in E . s1 ) implies [x,y] in {} )
assume
ex
s1 being
Element of
S st
(
s1 in C &
[x,y] in E . s1 )
;
:: thesis: [x,y] in {}
then consider s1 being
Element of
S such that A3:
(
s1 in C &
[x,y] in E . s1 )
;
A4:
x in the
Sorts of
A . s1
by A3, ZFMISC_1:106;
the
Sorts of
A . s1 in { (the Sorts of A . s) where s is Element of S : s in C }
by A3;
hence
[x,y] in {}
by A2, A4, TARSKI:def 4;
:: thesis: verum
end; hence
ex
b1 being
Equivalence_Relation of
(the Sorts of A -carrier_of C) st
for
x,
y being
set holds
(
[x,y] in b1 iff ex
s1 being
Element of
S st
(
s1 in C &
[x,y] in E . s1 ) )
by A2, Th10;
:: thesis: verum suppose
not the
Sorts of
A -carrier_of C is
empty
;
:: thesis: ex b1 being Equivalence_Relation of (the Sorts of A -carrier_of C) st
for x, y being set holds
( [x,y] in b1 iff ex s1 being Element of S st
( s1 in C & [x,y] in E . s1 ) )then reconsider SAC = the
Sorts of
A -carrier_of C as non
empty set ;
set CC =
{ [x,y] where x, y is Element of SAC : S1[x,y] } ;
A5:
for
x,
y being
set holds
(
[x,y] in { [x,y] where x, y is Element of SAC : S1[x,y] } iff
S1[
x,
y] )
proof
let x,
y be
set ;
:: thesis: ( [x,y] in { [x,y] where x, y is Element of SAC : S1[x,y] } iff S1[x,y] )
hereby :: thesis: ( S1[x,y] implies [x,y] in { [x,y] where x, y is Element of SAC : S1[x,y] } )
assume
[x,y] in { [x,y] where x, y is Element of SAC : S1[x,y] }
;
:: thesis: S1[x,y]then consider x1,
y1 being
Element of
SAC such that A6:
[x,y] = [x1,y1]
and A7:
S1[
x1,
y1]
;
thus
S1[
x,
y]
by A6, A7;
:: thesis: verum
end;
assume A8:
S1[
x,
y]
;
:: thesis: [x,y] in { [x,y] where x, y is Element of SAC : S1[x,y] }
then consider s1 being
Element of
S such that A9:
(
s1 in C &
[x,y] in E . s1 )
;
A10:
the
Sorts of
A . s1 in { (the Sorts of A . s) where s is Element of S : s in C }
by A9;
(
x in the
Sorts of
A . s1 &
y in the
Sorts of
A . s1 )
by A9, ZFMISC_1:106;
then reconsider x1 =
x,
y1 =
y as
Element of
SAC by A10, TARSKI:def 4;
[x1,y1] in { [x,y] where x, y is Element of SAC : S1[x,y] }
by A8;
hence
[x,y] in { [x,y] where x, y is Element of SAC : S1[x,y] }
;
:: thesis: verum
end;
{ [x,y] where x, y is Element of SAC : S1[x,y] } c= [:SAC,SAC:]
proof
let z be
set ;
:: according to TARSKI:def 3 :: thesis: ( not z in { [x,y] where x, y is Element of SAC : S1[x,y] } or z in [:SAC,SAC:] )
assume A11:
z in { [x,y] where x, y is Element of SAC : S1[x,y] }
;
:: thesis: z in [:SAC,SAC:]
consider x,
y being
Element of
SAC such that A12:
(
z = [x,y] &
S1[
x,
y] )
by A11;
thus
z in [:SAC,SAC:]
by A12, ZFMISC_1:106;
:: thesis: verum
end; then reconsider P1 =
{ [x,y] where x, y is Element of SAC : S1[x,y] } as
Relation of
SAC ;
now let x be
set ;
:: thesis: ( x in SAC implies [x,x] in P1 )assume A13:
x in SAC
;
:: thesis: [x,x] in P1reconsider x1 =
x as
Element of
SAC by A13;
consider X being
set such that A14:
x in X
and A15:
X in { (the Sorts of A . s) where s is Element of S : s in C }
by A13, TARSKI:def 4;
consider s being
Element of
S such that A16:
(
X = the
Sorts of
A . s &
s in C )
by A15;
field (E . s) = the
Sorts of
A . s
by ORDERS_1:97;
then
E . s is_reflexive_in the
Sorts of
A . s
by RELAT_2:def 9;
then
[x,x] in E . s
by A14, A16, RELAT_2:def 1;
then
[x1,x1] in { [x,y] where x, y is Element of SAC : S1[x,y] }
by A16;
hence
[x,x] in P1
;
:: thesis: verum end; then
P1 is_reflexive_in SAC
by RELAT_2:def 1;
then A17:
(
dom P1 = SAC &
field P1 = SAC )
by ORDERS_1:98;
now let x,
y be
set ;
:: thesis: ( x in SAC & y in SAC & [x,y] in P1 implies [y,x] in P1 )assume A18:
(
x in SAC &
y in SAC &
[x,y] in P1 )
;
:: thesis: [y,x] in P1reconsider x1 =
x,
y1 =
y as
Element of
SAC by A18;
consider x2,
y2 being
Element of
SAC such that A19:
(
[x,y] = [x2,y2] &
S1[
x2,
y2] )
by A18;
A20:
(
x = x2 &
y = y2 )
by A19, ZFMISC_1:33;
consider s5 being
Element of
S such that A21:
(
s5 in C &
[x2,y2] in E . s5 )
by A19;
A22:
(
x2 in the
Sorts of
A . s5 &
y2 in the
Sorts of
A . s5 )
by A21, ZFMISC_1:106;
field (E . s5) = the
Sorts of
A . s5
by ORDERS_1:97;
then
E . s5 is_symmetric_in the
Sorts of
A . s5
by RELAT_2:def 11;
then
[y,x] in E . s5
by A20, A21, A22, RELAT_2:def 3;
then
[y1,x1] in { [x,y] where x, y is Element of SAC : S1[x,y] }
by A21;
hence
[y,x] in P1
;
:: thesis: verum end; then A23:
P1 is_symmetric_in SAC
by RELAT_2:def 3;
now let x,
y,
z be
set ;
:: thesis: ( x in SAC & y in SAC & z in SAC & [x,y] in P1 & [y,z] in P1 implies [x,z] in P1 )assume A24:
(
x in SAC &
y in SAC &
z in SAC &
[x,y] in P1 &
[y,z] in P1 )
;
:: thesis: [x,z] in P1consider x2,
y2 being
Element of
SAC such that A25:
(
[x,y] = [x2,y2] &
S1[
x2,
y2] )
by A24;
A26:
(
x = x2 &
y = y2 )
by A25, ZFMISC_1:33;
consider y3,
z3 being
Element of
SAC such that A27:
(
[y,z] = [y3,z3] &
S1[
y3,
z3] )
by A24;
A28:
(
y = y3 &
z = z3 )
by A27, ZFMISC_1:33;
consider s5 being
Element of
S such that A29:
(
s5 in C &
[x2,y2] in E . s5 )
by A25;
A30:
(
x2 in the
Sorts of
A . s5 &
y2 in the
Sorts of
A . s5 )
by A29, ZFMISC_1:106;
consider s6 being
Element of
S such that A31:
(
s6 in C &
[y3,z3] in E . s6 )
by A27;
A32:
(
y3 in the
Sorts of
A . s6 &
z3 in the
Sorts of
A . s6 )
by A31, ZFMISC_1:106;
reconsider s51 =
s5,
s61 =
s6 as
Element of
S ;
consider su being
Element of
S such that A33:
(
su in C &
s51 <= su &
s61 <= su )
by A29, A31, WAYBEL_0:def 1;
A34:
(
[x2,y2] in E . su &
[y3,z3] in E . su )
by A1, A29, A30, A31, A32, A33, Def1;
then A35:
(
x2 in the
Sorts of
A . su &
y2 in the
Sorts of
A . su &
z3 in the
Sorts of
A . su )
by ZFMISC_1:106;
field (E . su) = the
Sorts of
A . su
by ORDERS_1:97;
then
E . su is_transitive_in the
Sorts of
A . su
by RELAT_2:def 16;
then
[x2,z3] in E . su
by A26, A28, A34, A35, RELAT_2:def 8;
hence
[x,z] in P1
by A26, A28, A33;
:: thesis: verum end; then
P1 is_transitive_in SAC
by RELAT_2:def 8;
then reconsider P1 =
P1 as
Equivalence_Relation of
(the Sorts of A -carrier_of C) by A17, A23, PARTFUN1:def 4, RELAT_2:def 11, RELAT_2:def 16;
take
P1
;
:: thesis: for x, y being set holds
( [x,y] in P1 iff ex s1 being Element of S st
( s1 in C & [x,y] in E . s1 ) )thus
for
x,
y being
set holds
(
[x,y] in P1 iff ex
s1 being
Element of
S st
(
s1 in C &
[x,y] in E . s1 ) )
by A5;
:: thesis: verum end;