defpred S1[ object , object ] means ex s1 being Element of S st
( s1 in C & [$1,$2] in E . s1 );
A1:
E is os-compatible
by Def2;
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
;
ex b1 being Equivalence_Relation of ( the Sorts of A -carrier_of C) st
for x, y being object 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
object 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
object ;
( [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 ) )
;
( 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 )
;
[x,y] in {}
then consider s1 being
Element of
S such that A3:
(
s1 in C &
[x,y] in E . s1 )
;
(
x in the
Sorts of
A . s1 & the
Sorts of
A . s1 in { ( the Sorts of A . s) where s is Element of S : s in C } )
by A3, ZFMISC_1:87;
hence
[x,y] in {}
by A2, TARSKI:def 4;
verum
end; hence
ex
b1 being
Equivalence_Relation of
( the Sorts of A -carrier_of C) st
for
x,
y being
object holds
(
[x,y] in b1 iff ex
s1 being
Element of
S st
(
s1 in C &
[x,y] in E . s1 ) )
by A2, Th9;
verum end; suppose
not the
Sorts of
A -carrier_of C is
empty
;
ex b1 being Equivalence_Relation of ( the Sorts of A -carrier_of C) st
for x, y being object 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] } ;
{ [x,y] where x, y is Element of SAC : S1[x,y] } c= [:SAC,SAC:]
proof
let z be
object ;
TARSKI:def 3 ( not z in { [x,y] where x, y is Element of SAC : S1[x,y] } or z in [:SAC,SAC:] )
assume
z in { [x,y] where x, y is Element of SAC : S1[x,y] }
;
z in [:SAC,SAC:]
then
ex
x,
y being
Element of
SAC st
(
z = [x,y] &
S1[
x,
y] )
;
hence
z in [:SAC,SAC:]
by ZFMISC_1:87;
verum
end; then reconsider P1 =
{ [x,y] where x, y is Element of SAC : S1[x,y] } as
Relation of
SAC ;
now for x, y being object st x in SAC & y in SAC & [x,y] in P1 holds
[y,x] in P1let x,
y be
object ;
( x in SAC & y in SAC & [x,y] in P1 implies [y,x] in P1 )assume that A4:
(
x in SAC &
y in SAC )
and A5:
[x,y] in P1
;
[y,x] in P1reconsider x1 =
x,
y1 =
y as
Element of
SAC by A4;
consider x2,
y2 being
Element of
SAC such that A6:
[x,y] = [x2,y2]
and A7:
S1[
x2,
y2]
by A5;
A8:
(
x = x2 &
y = y2 )
by A6, XTUPLE_0:1;
consider s5 being
Element of
S such that A9:
s5 in C
and A10:
[x2,y2] in E . s5
by A7;
field (E . s5) = the
Sorts of
A . s5
by ORDERS_1:12;
then A11:
E . s5 is_symmetric_in the
Sorts of
A . s5
by RELAT_2:def 11;
(
x2 in the
Sorts of
A . s5 &
y2 in the
Sorts of
A . s5 )
by A10, ZFMISC_1:87;
then
[y,x] in E . s5
by A8, A10, A11, RELAT_2:def 3;
then
[y1,x1] in { [x,y] where x, y is Element of SAC : S1[x,y] }
by A9;
hence
[y,x] in P1
;
verum end; then A12:
P1 is_symmetric_in SAC
by RELAT_2:def 3;
now for x being object st x in SAC holds
[x,x] in P1let x be
object ;
( x in SAC implies [x,x] in P1 )assume A13:
x in SAC
;
[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
and A17:
s in C
by A15;
field (E . s) = the
Sorts of
A . s
by ORDERS_1:12;
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 A17;
hence
[x,x] in P1
;
verum end; then
P1 is_reflexive_in SAC
by RELAT_2:def 1;
then A18:
(
dom P1 = SAC &
field P1 = SAC )
by ORDERS_1:13;
now for x, y, z being object st x in SAC & y in SAC & z in SAC & [x,y] in P1 & [y,z] in P1 holds
[x,z] in P1let x,
y,
z be
object ;
( x in SAC & y in SAC & z in SAC & [x,y] in P1 & [y,z] in P1 implies [x,z] in P1 )assume that
x in SAC
and
y in SAC
and
z in SAC
and A19:
[x,y] in P1
and A20:
[y,z] in P1
;
[x,z] in P1consider x2,
y2 being
Element of
SAC such that A21:
[x,y] = [x2,y2]
and A22:
S1[
x2,
y2]
by A19;
A23:
x = x2
by A21, XTUPLE_0:1;
consider y3,
z3 being
Element of
SAC such that A24:
[y,z] = [y3,z3]
and A25:
S1[
y3,
z3]
by A20;
A26:
y = y3
by A24, XTUPLE_0:1;
consider s5 being
Element of
S such that A27:
s5 in C
and A28:
[x2,y2] in E . s5
by A22;
consider s6 being
Element of
S such that A29:
s6 in C
and A30:
[y3,z3] in E . s6
by A25;
reconsider s51 =
s5,
s61 =
s6 as
Element of
S ;
consider su being
Element of
S such that A31:
su in C
and A32:
s51 <= su
and A33:
s61 <= su
by A27, A29, WAYBEL_0:def 1;
(
y3 in the
Sorts of
A . s6 &
z3 in the
Sorts of
A . s6 )
by A30, ZFMISC_1:87;
then A34:
[y3,z3] in E . su
by A1, A30, A33;
then A35:
z3 in the
Sorts of
A . su
by ZFMISC_1:87;
A36:
z = z3
by A24, XTUPLE_0:1;
A37:
y = y2
by A21, XTUPLE_0:1;
field (E . su) = the
Sorts of
A . su
by ORDERS_1:12;
then A38:
E . su is_transitive_in the
Sorts of
A . su
by RELAT_2:def 16;
(
x2 in the
Sorts of
A . s5 &
y2 in the
Sorts of
A . s5 )
by A28, ZFMISC_1:87;
then A39:
[x2,y2] in E . su
by A1, A28, A32;
then
(
x2 in the
Sorts of
A . su &
y2 in the
Sorts of
A . su )
by ZFMISC_1:87;
then
[x2,z3] in E . su
by A37, A26, A39, A34, A35, A38, RELAT_2:def 8;
hence
[x,z] in P1
by A23, A36, A31;
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 A18, A12, PARTFUN1:def 2, RELAT_2:def 11, RELAT_2:def 16;
take
P1
;
for x, y being object holds
( [x,y] in P1 iff ex s1 being Element of S st
( s1 in C & [x,y] in E . s1 ) )
for
x,
y being
object 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
object ;
( [x,y] in { [x,y] where x, y is Element of SAC : S1[x,y] } iff S1[x,y] )
hereby ( 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] }
;
S1[x,y]then
ex
x1,
y1 being
Element of
SAC st
(
[x,y] = [x1,y1] &
S1[
x1,
y1] )
;
hence
S1[
x,
y]
;
verum
end;
assume A40:
S1[
x,
y]
;
[x,y] in { [x,y] where x, y is Element of SAC : S1[x,y] }
then consider s1 being
Element of
S such that A41:
s1 in C
and A42:
[x,y] in E . s1
;
A43:
y in the
Sorts of
A . s1
by A42, ZFMISC_1:87;
( the
Sorts of
A . s1 in { ( the Sorts of A . s) where s is Element of S : s in C } &
x in the
Sorts of
A . s1 )
by A41, A42, ZFMISC_1:87;
then reconsider x1 =
x,
y1 =
y as
Element of
SAC by A43, TARSKI:def 4;
[x1,y1] in { [x,y] where x, y is Element of SAC : S1[x,y] }
by A40;
hence
[x,y] in { [x,y] where x, y is Element of SAC : S1[x,y] }
;
verum
end; hence
for
x,
y being
object holds
(
[x,y] in P1 iff ex
s1 being
Element of
S st
(
s1 in C &
[x,y] in E . s1 ) )
;
verum end; end;