:: LFUZZY_1 semantic presentation
begin
registration
let X be non empty set ;
cluster[.0,1.] -valued Function-like quasi_total -> real-valued for Element of bool [:X,REAL:];
coherence
for b1 being Membership_Func of X holds b1 is real-valued ;
end;
definition
let X, Y be non empty set ;
let f, g be RMembership_Func of X,Y;
:: original: is_less_than
redefine predf is_less_than g means :Def1: :: LFUZZY_1:def 1
for x being Element of X
for y being Element of Y holds f . (x,y) <= g . (x,y);
compatibility
( f is_less_than g iff for x being Element of X
for y being Element of Y holds f . (x,y) <= g . (x,y) )
proof
thus ( f is_less_than g iff for x being Element of X
for y being Element of Y holds f . (x,y) <= g . (x,y) ) ::_thesis: verum
proof
hereby ::_thesis: ( ( for x being Element of X
for y being Element of Y holds f . (x,y) <= g . (x,y) ) implies f is_less_than g )
assume A1: f is_less_than g ; ::_thesis: for x being Element of X
for y being Element of Y holds f . (x,y) <= g . (x,y)
thus for x being Element of X
for y being Element of Y holds f . (x,y) <= g . (x,y) ::_thesis: verum
proof
let x be Element of X; ::_thesis: for y being Element of Y holds f . (x,y) <= g . (x,y)
let y be Element of Y; ::_thesis: f . (x,y) <= g . (x,y)
( dom f = [:X,Y:] & [x,y] in [:X,Y:] ) by FUNCT_2:def_1;
hence f . (x,y) <= g . (x,y) by A1, FUZZY_1:def_1; ::_thesis: verum
end;
end;
assume A2: for x being Element of X
for y being Element of Y holds f . (x,y) <= g . (x,y) ; ::_thesis: f is_less_than g
A3: for c being set st c in dom f holds
f . c <= g . c
proof
let c be set ; ::_thesis: ( c in dom f implies f . c <= g . c )
assume A4: c in dom f ; ::_thesis: f . c <= g . c
then consider x, y being set such that
A5: [x,y] = c by RELAT_1:def_1;
reconsider y = y as Element of Y by A4, A5, ZFMISC_1:87;
reconsider x = x as Element of X by A4, A5, ZFMISC_1:87;
f . (x,y) <= g . (x,y) by A2;
hence f . c <= g . c by A5; ::_thesis: verum
end;
dom g = [:X,Y:] by FUNCT_2:def_1;
hence f is_less_than g by A3, FUZZY_1:def_1; ::_thesis: verum
end;
end;
end;
:: deftheorem Def1 defines is_less_than LFUZZY_1:def_1_:_
for X, Y being non empty set
for f, g being RMembership_Func of X,Y holds
( f is_less_than g iff for x being Element of X
for y being Element of Y holds f . (x,y) <= g . (x,y) );
theorem Th1: :: LFUZZY_1:1
for X being non empty set
for R, S being Membership_Func of X st ( for x being Element of X holds R . x = S . x ) holds
R = S
proof
let X be non empty set ; ::_thesis: for R, S being Membership_Func of X st ( for x being Element of X holds R . x = S . x ) holds
R = S
let R, S be Membership_Func of X; ::_thesis: ( ( for x being Element of X holds R . x = S . x ) implies R = S )
assume for x being Element of X holds R . x = S . x ; ::_thesis: R = S
then A1: for x being Element of X st x in dom R holds
R . x = S . x ;
( dom R = X & dom S = X ) by FUNCT_2:def_1;
hence R = S by A1, PARTFUN1:5; ::_thesis: verum
end;
theorem Th2: :: LFUZZY_1:2
for X, Y being non empty set
for R, S being RMembership_Func of X,Y st ( for x being Element of X
for y being Element of Y holds R . (x,y) = S . (x,y) ) holds
R = S
proof
let X, Y be non empty set ; ::_thesis: for R, S being RMembership_Func of X,Y st ( for x being Element of X
for y being Element of Y holds R . (x,y) = S . (x,y) ) holds
R = S
let R, S be RMembership_Func of X,Y; ::_thesis: ( ( for x being Element of X
for y being Element of Y holds R . (x,y) = S . (x,y) ) implies R = S )
assume A1: for x being Element of X
for y being Element of Y holds R . (x,y) = S . (x,y) ; ::_thesis: R = S
A2: for x, y being set st [x,y] in dom R holds
R . (x,y) = S . (x,y)
proof
let x, y be set ; ::_thesis: ( [x,y] in dom R implies R . (x,y) = S . (x,y) )
assume A3: [x,y] in dom R ; ::_thesis: R . (x,y) = S . (x,y)
then reconsider x = x as Element of X by ZFMISC_1:87;
reconsider y = y as Element of Y by A3, ZFMISC_1:87;
R . (x,y) = S . (x,y) by A1;
hence R . (x,y) = S . (x,y) ; ::_thesis: verum
end;
( dom R = [:X,Y:] & dom S = [:X,Y:] ) by FUNCT_2:def_1;
hence R = S by A2, BINOP_1:20; ::_thesis: verum
end;
theorem Th3: :: LFUZZY_1:3
for X being non empty set
for R, S being Membership_Func of X holds
( R = S iff ( S c= & R c= ) )
proof
let X be non empty set ; ::_thesis: for R, S being Membership_Func of X holds
( R = S iff ( S c= & R c= ) )
let R, S be Membership_Func of X; ::_thesis: ( R = S iff ( S c= & R c= ) )
thus ( R = S implies ( S c= & R c= ) ) ; ::_thesis: ( S c= & R c= implies R = S )
assume A1: ( S c= & R c= ) ; ::_thesis: R = S
for x being Element of X holds R . x = S . x
proof
let x be Element of X; ::_thesis: R . x = S . x
( R . x <= S . x & S . x <= R . x ) by A1, FUZZY_1:def_2;
hence R . x = S . x by XXREAL_0:1; ::_thesis: verum
end;
hence R = S by Th1; ::_thesis: verum
end;
theorem :: LFUZZY_1:4
for X being non empty set
for R being Membership_Func of X holds R c= ;
theorem Th5: :: LFUZZY_1:5
for X being non empty set
for R, S, T being Membership_Func of X st S c= & T c= holds
T c=
proof
let X be non empty set ; ::_thesis: for R, S, T being Membership_Func of X st S c= & T c= holds
T c=
let R, S, T be Membership_Func of X; ::_thesis: ( S c= & T c= implies T c= )
assume A1: ( S c= & T c= ) ; ::_thesis: T c=
for x being Element of X holds R . x <= T . x
proof
let x be Element of X; ::_thesis: R . x <= T . x
( R . x <= S . x & S . x <= T . x ) by A1, FUZZY_1:def_2;
hence R . x <= T . x by XXREAL_0:2; ::_thesis: verum
end;
hence T c= by FUZZY_1:def_2; ::_thesis: verum
end;
theorem Th6: :: LFUZZY_1:6
for X, Y, Z being non empty set
for R, S being RMembership_Func of X,Y
for T, U being RMembership_Func of Y,Z st S c= & U c= holds
S (#) U c=
proof
let X, Y, Z be non empty set ; ::_thesis: for R, S being RMembership_Func of X,Y
for T, U being RMembership_Func of Y,Z st S c= & U c= holds
S (#) U c=
let R, S be RMembership_Func of X,Y; ::_thesis: for T, U being RMembership_Func of Y,Z st S c= & U c= holds
S (#) U c=
let T, U be RMembership_Func of Y,Z; ::_thesis: ( S c= & U c= implies S (#) U c= )
assume A1: ( S c= & U c= ) ; ::_thesis: S (#) U c=
for c being Element of [:X,Z:] holds (R (#) T) . c <= (S (#) U) . c
proof
let c be Element of [:X,Z:]; ::_thesis: (R (#) T) . c <= (S (#) U) . c
consider x, z being set such that
A2: [x,z] = c by RELAT_1:def_1;
A3: ( x in X & z in Z ) by A2, ZFMISC_1:87;
for y being set st y in Y holds
( R . [x,y] <= S . [x,y] & T . [y,z] <= U . [y,z] )
proof
let y be set ; ::_thesis: ( y in Y implies ( R . [x,y] <= S . [x,y] & T . [y,z] <= U . [y,z] ) )
assume y in Y ; ::_thesis: ( R . [x,y] <= S . [x,y] & T . [y,z] <= U . [y,z] )
then ( [x,y] in [:X,Y:] & [y,z] in [:Y,Z:] ) by A3, ZFMISC_1:87;
hence ( R . [x,y] <= S . [x,y] & T . [y,z] <= U . [y,z] ) by A1, FUZZY_1:def_2; ::_thesis: verum
end;
hence (R (#) T) . c <= (S (#) U) . c by A2, A3, FUZZY_4:18; ::_thesis: verum
end;
hence S (#) U c= by FUZZY_1:def_2; ::_thesis: verum
end;
definition
let X be non empty set ;
let f, g be Membership_Func of X;
:: original: min
redefine func min (f,g) -> Element of bool [:X,REAL:];
commutativity
for f, g being Membership_Func of X holds min (f,g) = min (g,f) ;
:: original: max
redefine func max (f,g) -> Element of bool [:X,REAL:];
commutativity
for f, g being Membership_Func of X holds max (f,g) = max (g,f) ;
end;
theorem :: LFUZZY_1:7
for X being non empty set
for f, g being Membership_Func of X holds f c=
proof
let X be non empty set ; ::_thesis: for f, g being Membership_Func of X holds f c=
let f, g be Membership_Func of X; ::_thesis: f c=
let x be Element of X; :: according to FUZZY_1:def_2 ::_thesis: (min (f,g)) . x <= f . x
(min (f,g)) . x = min ((f . x),(g . x)) by FUZZY_1:def_3;
hence (min (f,g)) . x <= f . x by XXREAL_0:17; ::_thesis: verum
end;
theorem :: LFUZZY_1:8
for X being non empty set
for f, g being Membership_Func of X holds max (f,g) c=
proof
let X be non empty set ; ::_thesis: for f, g being Membership_Func of X holds max (f,g) c=
let f, g be Membership_Func of X; ::_thesis: max (f,g) c=
let x be Element of X; :: according to FUZZY_1:def_2 ::_thesis: f . x <= (max (f,g)) . x
(max (f,g)) . x = max ((f . x),(g . x)) by FUZZY_1:def_4;
hence f . x <= (max (f,g)) . x by XXREAL_0:25; ::_thesis: verum
end;
begin
definition
let X be non empty set ;
let R be RMembership_Func of X,X;
attrR is reflexive means :Def2: :: LFUZZY_1:def 2
R c= ;
end;
:: deftheorem Def2 defines reflexive LFUZZY_1:def_2_:_
for X being non empty set
for R being RMembership_Func of X,X holds
( R is reflexive iff R c= );
definition
let X be non empty set ;
let R be RMembership_Func of X,X;
redefine attr R is reflexive means :Def3: :: LFUZZY_1:def 3
for x being Element of X holds R . (x,x) = 1;
compatibility
( R is reflexive iff for x being Element of X holds R . (x,x) = 1 )
proof
hereby ::_thesis: ( ( for x being Element of X holds R . (x,x) = 1 ) implies R is reflexive )
assume R is reflexive ; ::_thesis: for x being Element of X holds R . (x,x) = 1
then A1: R c= by Def2;
thus for x being Element of X holds R . (x,x) = 1 ::_thesis: verum
proof
let x be Element of X; ::_thesis: R . (x,x) = 1
(Imf (X,X)) . (x,x) <= R . (x,x) by A1, Def1;
then ( R . (x,x) <= 1 & R . (x,x) >= 1 ) by FUZZY_4:4, FUZZY_4:25;
hence R . (x,x) = 1 by XXREAL_0:1; ::_thesis: verum
end;
end;
assume A2: for x being Element of X holds R . (x,x) = 1 ; ::_thesis: R is reflexive
let x, y be Element of X; :: according to LFUZZY_1:def_1,LFUZZY_1:def_2 ::_thesis: (Imf (X,X)) . (x,y) <= R . (x,y)
percases ( x = y or x <> y ) ;
supposeA3: x = y ; ::_thesis: (Imf (X,X)) . (x,y) <= R . (x,y)
then (Imf (X,X)) . (x,y) = 1 by FUZZY_4:25;
hence (Imf (X,X)) . (x,y) <= R . (x,y) by A2, A3; ::_thesis: verum
end;
suppose x <> y ; ::_thesis: (Imf (X,X)) . (x,y) <= R . (x,y)
then (Imf (X,X)) . (x,y) = 0 by FUZZY_4:25;
hence (Imf (X,X)) . (x,y) <= R . (x,y) by FUZZY_4:4; ::_thesis: verum
end;
end;
end;
end;
:: deftheorem Def3 defines reflexive LFUZZY_1:def_3_:_
for X being non empty set
for R being RMembership_Func of X,X holds
( R is reflexive iff for x being Element of X holds R . (x,x) = 1 );
definition
let X be non empty set ;
let R be RMembership_Func of X,X;
attrR is symmetric means :Def4: :: LFUZZY_1:def 4
converse R = R;
end;
:: deftheorem Def4 defines symmetric LFUZZY_1:def_4_:_
for X being non empty set
for R being RMembership_Func of X,X holds
( R is symmetric iff converse R = R );
definition
let X be non empty set ;
let R be RMembership_Func of X,X;
redefine attr R is symmetric means :Def5: :: LFUZZY_1:def 5
for x, y being Element of X holds R . (x,y) = R . (y,x);
compatibility
( R is symmetric iff for x, y being Element of X holds R . (x,y) = R . (y,x) )
proof
thus ( R is symmetric iff for x, y being Element of X holds R . (x,y) = R . (y,x) ) ::_thesis: verum
proof
hereby ::_thesis: ( ( for x, y being Element of X holds R . (x,y) = R . (y,x) ) implies R is symmetric )
assume R is symmetric ; ::_thesis: for x, y being Element of X holds R . (x,y) = R . (y,x)
then converse R = R by Def4;
hence for x, y being Element of X holds R . (x,y) = R . (y,x) by FUZZY_4:26; ::_thesis: verum
end;
assume A1: for x, y being Element of X holds R . (x,y) = R . (y,x) ; ::_thesis: R is symmetric
A2: for x, y being set st [x,y] in dom R holds
(converse R) . (x,y) = R . (x,y)
proof
let x, y be set ; ::_thesis: ( [x,y] in dom R implies (converse R) . (x,y) = R . (x,y) )
assume [x,y] in dom R ; ::_thesis: (converse R) . (x,y) = R . (x,y)
then reconsider x = x, y = y as Element of X by ZFMISC_1:87;
R . (x,y) = R . (y,x) by A1;
hence (converse R) . (x,y) = R . (x,y) by FUZZY_4:26; ::_thesis: verum
end;
( dom (converse R) = [:X,X:] & dom R = [:X,X:] ) by FUNCT_2:def_1;
then converse R = R by A2, BINOP_1:20;
hence R is symmetric by Def4; ::_thesis: verum
end;
end;
end;
:: deftheorem Def5 defines symmetric LFUZZY_1:def_5_:_
for X being non empty set
for R being RMembership_Func of X,X holds
( R is symmetric iff for x, y being Element of X holds R . (x,y) = R . (y,x) );
definition
let X be non empty set ;
let R be RMembership_Func of X,X;
attrR is transitive means :Def6: :: LFUZZY_1:def 6
R c= ;
end;
:: deftheorem Def6 defines transitive LFUZZY_1:def_6_:_
for X being non empty set
for R being RMembership_Func of X,X holds
( R is transitive iff R c= );
Lm1: for X, Y, Z being non empty set
for R being RMembership_Func of X,Y
for S being RMembership_Func of Y,Z
for x being Element of X
for z being Element of Z holds
( rng (min (R,S,x,z)) = { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } & rng (min (R,S,x,z)) <> {} )
proof
let X, Y, Z be non empty set ; ::_thesis: for R being RMembership_Func of X,Y
for S being RMembership_Func of Y,Z
for x being Element of X
for z being Element of Z holds
( rng (min (R,S,x,z)) = { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } & rng (min (R,S,x,z)) <> {} )
let R be RMembership_Func of X,Y; ::_thesis: for S being RMembership_Func of Y,Z
for x being Element of X
for z being Element of Z holds
( rng (min (R,S,x,z)) = { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } & rng (min (R,S,x,z)) <> {} )
let S be RMembership_Func of Y,Z; ::_thesis: for x being Element of X
for z being Element of Z holds
( rng (min (R,S,x,z)) = { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } & rng (min (R,S,x,z)) <> {} )
let x be Element of X; ::_thesis: for z being Element of Z holds
( rng (min (R,S,x,z)) = { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } & rng (min (R,S,x,z)) <> {} )
let z be Element of Z; ::_thesis: ( rng (min (R,S,x,z)) = { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } & rng (min (R,S,x,z)) <> {} )
set L = { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } ;
A1: ( Y = dom (min (R,S,x,z)) & min (R,S,x,z) is PartFunc of (dom (min (R,S,x,z))),(rng (min (R,S,x,z))) ) by FUNCT_2:def_1, RELSET_1:4;
for c being set holds
( c in { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } iff c in rng (min (R,S,x,z)) )
proof
let c be set ; ::_thesis: ( c in { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } iff c in rng (min (R,S,x,z)) )
hereby ::_thesis: ( c in rng (min (R,S,x,z)) implies c in { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } )
assume c in { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } ; ::_thesis: c in rng (min (R,S,x,z))
then consider y being Element of Y such that
A2: c = (R . [x,y]) "/\" (S . [y,z]) ;
c = (min (R,S,x,z)) . y by A2, FUZZY_4:def_2;
hence c in rng (min (R,S,x,z)) by A1, PARTFUN1:4; ::_thesis: verum
end;
assume c in rng (min (R,S,x,z)) ; ::_thesis: c in { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum }
then consider y being Element of Y such that
y in dom (min (R,S,x,z)) and
A3: c = (min (R,S,x,z)) . y by PARTFUN1:3;
c = (R . [x,y]) "/\" (S . [y,z]) by A3, FUZZY_4:def_2;
hence c in { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } ; ::_thesis: verum
end;
hence rng (min (R,S,x,z)) = { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } by TARSKI:1; ::_thesis: rng (min (R,S,x,z)) <> {}
thus rng (min (R,S,x,z)) <> {} ; ::_thesis: verum
end;
definition
let X be non empty set ;
let R be RMembership_Func of X,X;
redefine attr R is transitive means :: LFUZZY_1:def 7
for x, y, z being Element of X holds (R . [x,y]) "/\" (R . [y,z]) <<= R . [x,z];
compatibility
( R is transitive iff for x, y, z being Element of X holds (R . [x,y]) "/\" (R . [y,z]) <<= R . [x,z] )
proof
thus ( R is transitive iff for x, y, z being Element of X holds (R . [x,y]) "/\" (R . [y,z]) <<= R . [x,z] ) ::_thesis: verum
proof
hereby ::_thesis: ( ( for x, y, z being Element of X holds (R . [x,y]) "/\" (R . [y,z]) <<= R . [x,z] ) implies R is transitive )
assume R is transitive ; ::_thesis: for x, y, z being Element of X holds (R . [x,y]) "/\" (R . [y,z]) <<= R . [x,z]
then A1: R c= by Def6;
thus for x, y, z being Element of X holds (R . [x,y]) "/\" (R . [y,z]) <<= R . [x,z] ::_thesis: verum
proof
let x, y, z be Element of X; ::_thesis: (R . [x,y]) "/\" (R . [y,z]) <<= R . [x,z]
(R . (x,y)) "/\" (R . (y,z)) in { ((R . (x,y9)) "/\" (R . (y9,z))) where y9 is Element of X : verum } ;
then (R . (x,y)) "/\" (R . (y,z)) <<= "\/" ( { ((R . (x,y9)) "/\" (R . (y9,z))) where y9 is Element of X : verum } ,(RealPoset [.0,1.])) by YELLOW_2:22;
then (R . (x,y)) "/\" (R . (y,z)) <<= (R (#) R) . (x,z) by LFUZZY_0:22;
then A2: (R . (x,y)) "/\" (R . (y,z)) <= (R (#) R) . (x,z) by LFUZZY_0:3;
(R (#) R) . (x,z) <= R . (x,z) by A1, Def1;
then (R . [x,y]) "/\" (R . [y,z]) <= R . [x,z] by A2, XXREAL_0:2;
hence (R . [x,y]) "/\" (R . [y,z]) <<= R . [x,z] by LFUZZY_0:3; ::_thesis: verum
end;
end;
assume A3: for x, y, z being Element of X holds (R . [x,y]) "/\" (R . [y,z]) <<= R . [x,z] ; ::_thesis: R is transitive
thus R c= :: according to LFUZZY_1:def_6 ::_thesis: verum
proof
let x, z be Element of X; :: according to LFUZZY_1:def_1 ::_thesis: (R (#) R) . (x,z) <= R . (x,z)
set W = rng (min (R,R,x,z));
for r being real number st r in rng (min (R,R,x,z)) holds
r <= R . [x,z]
proof
let r be real number ; ::_thesis: ( r in rng (min (R,R,x,z)) implies r <= R . [x,z] )
assume r in rng (min (R,R,x,z)) ; ::_thesis: r <= R . [x,z]
then r in { ((R . [x,y9]) "/\" (R . [y9,z])) where y9 is Element of X : verum } by Lm1;
then consider y being Element of X such that
A4: r = (R . [x,y]) "/\" (R . [y,z]) ;
(R . [x,y]) "/\" (R . [y,z]) <<= R . [x,z] by A3;
hence r <= R . [x,z] by A4, LFUZZY_0:3; ::_thesis: verum
end;
then upper_bound (rng (min (R,R,x,z))) <= R . [x,z] by SEQ_4:144;
hence (R (#) R) . (x,z) <= R . (x,z) by FUZZY_4:def_3; ::_thesis: verum
end;
end;
end;
end;
:: deftheorem defines transitive LFUZZY_1:def_7_:_
for X being non empty set
for R being RMembership_Func of X,X holds
( R is transitive iff for x, y, z being Element of X holds (R . [x,y]) "/\" (R . [y,z]) <<= R . [x,z] );
definition
let X be non empty set ;
let R be RMembership_Func of X,X;
attrR is antisymmetric means :Def8: :: LFUZZY_1:def 8
for x, y being Element of X st R . (x,y) <> 0 & R . (y,x) <> 0 holds
x = y;
end;
:: deftheorem Def8 defines antisymmetric LFUZZY_1:def_8_:_
for X being non empty set
for R being RMembership_Func of X,X holds
( R is antisymmetric iff for x, y being Element of X st R . (x,y) <> 0 & R . (y,x) <> 0 holds
x = y );
registration
let X be non empty set ;
cluster Imf (X,X) -> reflexive symmetric transitive antisymmetric ;
coherence
( Imf (X,X) is symmetric & Imf (X,X) is transitive & Imf (X,X) is reflexive & Imf (X,X) is antisymmetric )
proof
thus Imf (X,X) is symmetric ::_thesis: ( Imf (X,X) is transitive & Imf (X,X) is reflexive & Imf (X,X) is antisymmetric )
proof
let x, y be Element of X; :: according to LFUZZY_1:def_5 ::_thesis: (Imf (X,X)) . (x,y) = (Imf (X,X)) . (y,x)
percases ( x = y or not x = y ) ;
suppose x = y ; ::_thesis: (Imf (X,X)) . (x,y) = (Imf (X,X)) . (y,x)
hence (Imf (X,X)) . (x,y) = (Imf (X,X)) . (y,x) ; ::_thesis: verum
end;
supposeA1: not x = y ; ::_thesis: (Imf (X,X)) . (x,y) = (Imf (X,X)) . (y,x)
hence (Imf (X,X)) . (x,y) = 0 by FUZZY_4:25
.= (Imf (X,X)) . (y,x) by A1, FUZZY_4:25 ;
::_thesis: verum
end;
end;
end;
thus Imf (X,X) is transitive ::_thesis: ( Imf (X,X) is reflexive & Imf (X,X) is antisymmetric )
proof
let x, y, z be Element of X; :: according to LFUZZY_1:def_7 ::_thesis: ((Imf (X,X)) . [x,y]) "/\" ((Imf (X,X)) . [y,z]) <<= (Imf (X,X)) . [x,z]
percases ( x = z or not x = z ) ;
supposeA2: x = z ; ::_thesis: ((Imf (X,X)) . [x,y]) "/\" ((Imf (X,X)) . [y,z]) <<= (Imf (X,X)) . [x,z]
thus ((Imf (X,X)) . [x,y]) "/\" ((Imf (X,X)) . [y,z]) <<= (Imf (X,X)) . [x,z] ::_thesis: verum
proof
percases ( x = y or not x = y ) ;
supposeA3: x = y ; ::_thesis: ((Imf (X,X)) . [x,y]) "/\" ((Imf (X,X)) . [y,z]) <<= (Imf (X,X)) . [x,z]
((Imf (X,X)) . [x,y]) "/\" ((Imf (X,X)) . [y,z]) = min (((Imf (X,X)) . (x,y)),((Imf (X,X)) . (y,z)))
.= 1 by A2, A3, FUZZY_4:25 ;
then ((Imf (X,X)) . (x,y)) "/\" ((Imf (X,X)) . (y,z)) <= (Imf (X,X)) . (x,z) by A2, FUZZY_4:25;
hence ((Imf (X,X)) . [x,y]) "/\" ((Imf (X,X)) . [y,z]) <<= (Imf (X,X)) . [x,z] by LFUZZY_0:3; ::_thesis: verum
end;
supposeA4: not x = y ; ::_thesis: ((Imf (X,X)) . [x,y]) "/\" ((Imf (X,X)) . [y,z]) <<= (Imf (X,X)) . [x,z]
((Imf (X,X)) . [x,y]) "/\" ((Imf (X,X)) . [y,z]) = min (((Imf (X,X)) . (x,y)),((Imf (X,X)) . (y,z)))
.= min (((Imf (X,X)) . (x,y)),0) by A2, A4, FUZZY_4:25
.= min (0,0) by A4, FUZZY_4:25
.= 0 ;
then ((Imf (X,X)) . (x,y)) "/\" ((Imf (X,X)) . (y,z)) <= (Imf (X,X)) . (x,z) by A2, FUZZY_4:25;
hence ((Imf (X,X)) . [x,y]) "/\" ((Imf (X,X)) . [y,z]) <<= (Imf (X,X)) . [x,z] by LFUZZY_0:3; ::_thesis: verum
end;
end;
end;
end;
supposeA5: not x = z ; ::_thesis: ((Imf (X,X)) . [x,y]) "/\" ((Imf (X,X)) . [y,z]) <<= (Imf (X,X)) . [x,z]
thus ((Imf (X,X)) . [x,y]) "/\" ((Imf (X,X)) . [y,z]) <<= (Imf (X,X)) . [x,z] ::_thesis: verum
proof
percases ( x = y or x <> y ) ;
supposeA6: x = y ; ::_thesis: ((Imf (X,X)) . [x,y]) "/\" ((Imf (X,X)) . [y,z]) <<= (Imf (X,X)) . [x,z]
((Imf (X,X)) . [x,y]) "/\" ((Imf (X,X)) . [y,z]) = min (((Imf (X,X)) . (x,y)),((Imf (X,X)) . (y,z)))
.= min (((Imf (X,X)) . (x,y)),0) by A5, A6, FUZZY_4:25
.= min (1,0) by A6, FUZZY_4:25
.= 0 by XXREAL_0:def_9 ;
then ((Imf (X,X)) . (x,y)) "/\" ((Imf (X,X)) . (y,z)) <= (Imf (X,X)) . (x,z) by A5, FUZZY_4:25;
hence ((Imf (X,X)) . [x,y]) "/\" ((Imf (X,X)) . [y,z]) <<= (Imf (X,X)) . [x,z] by LFUZZY_0:3; ::_thesis: verum
end;
supposeA7: x <> y ; ::_thesis: ((Imf (X,X)) . [x,y]) "/\" ((Imf (X,X)) . [y,z]) <<= (Imf (X,X)) . [x,z]
thus ((Imf (X,X)) . [x,y]) "/\" ((Imf (X,X)) . [y,z]) <<= (Imf (X,X)) . [x,z] ::_thesis: verum
proof
percases ( y = z or y <> z ) ;
supposeA8: y = z ; ::_thesis: ((Imf (X,X)) . [x,y]) "/\" ((Imf (X,X)) . [y,z]) <<= (Imf (X,X)) . [x,z]
((Imf (X,X)) . [x,y]) "/\" ((Imf (X,X)) . [y,z]) = min (((Imf (X,X)) . (x,y)),((Imf (X,X)) . (y,z)))
.= min (((Imf (X,X)) . (x,y)),1) by A8, FUZZY_4:25
.= min (0,1) by A7, FUZZY_4:25
.= 0 by XXREAL_0:def_9 ;
then ((Imf (X,X)) . (x,y)) "/\" ((Imf (X,X)) . (y,z)) <= (Imf (X,X)) . (x,z) by A5, FUZZY_4:25;
hence ((Imf (X,X)) . [x,y]) "/\" ((Imf (X,X)) . [y,z]) <<= (Imf (X,X)) . [x,z] by LFUZZY_0:3; ::_thesis: verum
end;
supposeA9: y <> z ; ::_thesis: ((Imf (X,X)) . [x,y]) "/\" ((Imf (X,X)) . [y,z]) <<= (Imf (X,X)) . [x,z]
((Imf (X,X)) . [x,y]) "/\" ((Imf (X,X)) . [y,z]) = min (((Imf (X,X)) . (x,y)),((Imf (X,X)) . (y,z)))
.= min (((Imf (X,X)) . (x,y)),0) by A9, FUZZY_4:25
.= min (0,0) by A7, FUZZY_4:25
.= 0 ;
then ((Imf (X,X)) . (x,y)) "/\" ((Imf (X,X)) . (y,z)) <= (Imf (X,X)) . (x,z) by A5, FUZZY_4:25;
hence ((Imf (X,X)) . [x,y]) "/\" ((Imf (X,X)) . [y,z]) <<= (Imf (X,X)) . [x,z] by LFUZZY_0:3; ::_thesis: verum
end;
end;
end;
end;
end;
end;
end;
end;
end;
thus Imf (X,X) is reflexive by Def2; ::_thesis: Imf (X,X) is antisymmetric
thus for x, y being Element of X st (Imf (X,X)) . (x,y) <> 0 & (Imf (X,X)) . (y,x) <> 0 holds
x = y by FUZZY_4:25; :: according to LFUZZY_1:def_8 ::_thesis: verum
end;
end;
registration
let X be non empty set ;
cluster non empty Relation-like [:X,X:] -defined REAL -valued [.0,1.] -valued Function-like total quasi_total real-valued reflexive symmetric transitive antisymmetric for Element of bool [:[:X,X:],REAL:];
existence
ex b1 being RMembership_Func of X,X st
( b1 is reflexive & b1 is transitive & b1 is symmetric & b1 is antisymmetric )
proof
take Imf (X,X) ; ::_thesis: ( Imf (X,X) is reflexive & Imf (X,X) is transitive & Imf (X,X) is symmetric & Imf (X,X) is antisymmetric )
thus ( Imf (X,X) is reflexive & Imf (X,X) is transitive & Imf (X,X) is symmetric & Imf (X,X) is antisymmetric ) ; ::_thesis: verum
end;
end;
theorem Th9: :: LFUZZY_1:9
for X being non empty set
for R, S being RMembership_Func of X,X st R is symmetric & S is symmetric holds
converse (min (R,S)) = min (R,S)
proof
let X be non empty set ; ::_thesis: for R, S being RMembership_Func of X,X st R is symmetric & S is symmetric holds
converse (min (R,S)) = min (R,S)
let R, S be RMembership_Func of X,X; ::_thesis: ( R is symmetric & S is symmetric implies converse (min (R,S)) = min (R,S) )
assume ( R is symmetric & S is symmetric ) ; ::_thesis: converse (min (R,S)) = min (R,S)
then ( converse R = R & converse S = S ) by Def4;
hence converse (min (R,S)) = min (R,S) by FUZZY_4:8; ::_thesis: verum
end;
theorem Th10: :: LFUZZY_1:10
for X being non empty set
for R, S being RMembership_Func of X,X st R is symmetric & S is symmetric holds
converse (max (R,S)) = max (R,S)
proof
let X be non empty set ; ::_thesis: for R, S being RMembership_Func of X,X st R is symmetric & S is symmetric holds
converse (max (R,S)) = max (R,S)
let R, S be RMembership_Func of X,X; ::_thesis: ( R is symmetric & S is symmetric implies converse (max (R,S)) = max (R,S) )
assume ( R is symmetric & S is symmetric ) ; ::_thesis: converse (max (R,S)) = max (R,S)
then ( converse R = R & converse S = S ) by Def4;
hence converse (max (R,S)) = max (R,S) by FUZZY_4:7; ::_thesis: verum
end;
registration
let X be non empty set ;
let R, S be symmetric RMembership_Func of X,X;
cluster min (R,S) -> symmetric ;
coherence
min (R,S) is symmetric
proof
converse (min (R,S)) = min (R,S) by Th9;
hence min (R,S) is symmetric by Def4; ::_thesis: verum
end;
cluster max (R,S) -> symmetric ;
coherence
max (R,S) is symmetric
proof
converse (max (R,S)) = max (R,S) by Th10;
hence max (R,S) is symmetric by Def4; ::_thesis: verum
end;
end;
theorem Th11: :: LFUZZY_1:11
for X being non empty set
for R, S being RMembership_Func of X,X st R is transitive & S is transitive holds
min (R,S) c=
proof
let X be non empty set ; ::_thesis: for R, S being RMembership_Func of X,X st R is transitive & S is transitive holds
min (R,S) c=
let R, S be RMembership_Func of X,X; ::_thesis: ( R is transitive & S is transitive implies min (R,S) c= )
assume that
A1: R is transitive and
A2: S is transitive ; ::_thesis: min (R,S) c=
let x be Element of X; :: according to LFUZZY_1:def_1 ::_thesis: for y being Element of X holds ((min (R,S)) (#) (min (R,S))) . (x,y) <= (min (R,S)) . (x,y)
let y be Element of X; ::_thesis: ((min (R,S)) (#) (min (R,S))) . (x,y) <= (min (R,S)) . (x,y)
(min ((R (#) S),(S (#) S))) . [x,y] = min (((S (#) S) . [x,y]),((R (#) S) . [x,y])) by FUZZY_1:def_3;
then A3: (min ((R (#) S),(S (#) S))) . [x,y] <= (S (#) S) . [x,y] by XXREAL_0:17;
S c= by A2, Def6;
then (S (#) S) . (x,y) <= S . (x,y) by Def1;
then A4: (min ((R (#) S),(S (#) S))) . [x,y] <= S . [x,y] by A3, XXREAL_0:2;
(min ((R (#) R),(S (#) R))) . [x,y] = min (((R (#) R) . [x,y]),((S (#) R) . [x,y])) by FUZZY_1:def_3;
then A5: (min ((R (#) R),(S (#) R))) . [x,y] <= (R (#) R) . [x,y] by XXREAL_0:17;
R c= by A1, Def6;
then (R (#) R) . (x,y) <= R . (x,y) by Def1;
then (min ((R (#) R),(S (#) R))) . [x,y] <= R . [x,y] by A5, XXREAL_0:2;
then A6: min (((min ((R (#) R),(S (#) R))) . [x,y]),((min ((R (#) S),(S (#) S))) . [x,y])) <= min ((R . [x,y]),(S . [x,y])) by A4, XXREAL_0:18;
min (((min (R,S)) (#) R),((min (R,S)) (#) S)) c= by FUZZY_4:15;
then A7: ((min (R,S)) (#) (min (R,S))) . [x,y] <= (min (((min (R,S)) (#) R),((min (R,S)) (#) S))) . [x,y] by FUZZY_1:def_2;
min ((R (#) S),(S (#) S)) c= by FUZZY_4:16;
then A8: ((min (R,S)) (#) S) . [x,y] <= (min ((R (#) S),(S (#) S))) . [x,y] by FUZZY_1:def_2;
min ((R (#) R),(S (#) R)) c= by FUZZY_4:16;
then ( (min (((min (R,S)) (#) R),((min (R,S)) (#) S))) . [x,y] = min ((((min (R,S)) (#) R) . [x,y]),(((min (R,S)) (#) S) . [x,y])) & ((min (R,S)) (#) R) . [x,y] <= (min ((R (#) R),(S (#) R))) . [x,y] ) by FUZZY_1:def_2, FUZZY_1:def_3;
then (min (((min (R,S)) (#) R),((min (R,S)) (#) S))) . [x,y] <= min (((min ((R (#) R),(S (#) R))) . [x,y]),((min ((R (#) S),(S (#) S))) . [x,y])) by A8, XXREAL_0:18;
then ((min (R,S)) (#) (min (R,S))) . [x,y] <= min (((min ((R (#) R),(S (#) R))) . [x,y]),((min ((R (#) S),(S (#) S))) . [x,y])) by A7, XXREAL_0:2;
then ((min (R,S)) (#) (min (R,S))) . [x,y] <= min ((R . [x,y]),(S . [x,y])) by A6, XXREAL_0:2;
hence ((min (R,S)) (#) (min (R,S))) . (x,y) <= (min (R,S)) . (x,y) by FUZZY_1:def_3; ::_thesis: verum
end;
registration
let X be non empty set ;
let R, S be transitive RMembership_Func of X,X;
cluster min (R,S) -> transitive ;
coherence
min (R,S) is transitive
proof
min (R,S) c= by Th11;
hence min (R,S) is transitive by Def6; ::_thesis: verum
end;
end;
definition
let A be set ;
let X be non empty set ;
:: original: chi
redefine func chi (A,X) -> Membership_Func of X;
coherence
chi (A,X) is Membership_Func of X
proof
dom (chi (A,X)) = X by FUNCT_3:def_3;
hence chi (A,X) is Membership_Func of X by FUNCT_2:def_1; ::_thesis: verum
end;
end;
theorem :: LFUZZY_1:12
for X being non empty set
for r being Relation of X st r is_reflexive_in X holds
chi (r,[:X,X:]) is reflexive
proof
let X be non empty set ; ::_thesis: for r being Relation of X st r is_reflexive_in X holds
chi (r,[:X,X:]) is reflexive
let r be Relation of X; ::_thesis: ( r is_reflexive_in X implies chi (r,[:X,X:]) is reflexive )
assume A1: r is_reflexive_in X ; ::_thesis: chi (r,[:X,X:]) is reflexive
for x being Element of X holds (chi (r,[:X,X:])) . (x,x) = 1
proof
let x be Element of X; ::_thesis: (chi (r,[:X,X:])) . (x,x) = 1
[x,x] in r by A1, RELAT_2:def_1;
hence (chi (r,[:X,X:])) . (x,x) = 1 by FUNCT_3:def_3; ::_thesis: verum
end;
hence chi (r,[:X,X:]) is reflexive by Def3; ::_thesis: verum
end;
theorem :: LFUZZY_1:13
for X being non empty set
for r being Relation of X st r is antisymmetric holds
chi (r,[:X,X:]) is antisymmetric
proof
let X be non empty set ; ::_thesis: for r being Relation of X st r is antisymmetric holds
chi (r,[:X,X:]) is antisymmetric
let r be Relation of X; ::_thesis: ( r is antisymmetric implies chi (r,[:X,X:]) is antisymmetric )
assume r is antisymmetric ; ::_thesis: chi (r,[:X,X:]) is antisymmetric
then A1: r is_antisymmetric_in field r by RELAT_2:def_12;
for x, y being Element of X st (chi (r,[:X,X:])) . (x,y) <> 0 & (chi (r,[:X,X:])) . (y,x) <> 0 holds
x = y
proof
let x, y be Element of X; ::_thesis: ( (chi (r,[:X,X:])) . (x,y) <> 0 & (chi (r,[:X,X:])) . (y,x) <> 0 implies x = y )
assume that
A2: (chi (r,[:X,X:])) . (x,y) <> 0 and
A3: (chi (r,[:X,X:])) . (y,x) <> 0 ; ::_thesis: x = y
A4: ( x in field r & y in field r & [x,y] in r & [y,x] in r implies x = y ) by A1, RELAT_2:def_4;
[x,y] in r by A2, FUNCT_3:def_3;
hence x = y by A3, A4, FUNCT_3:def_3, RELAT_1:15; ::_thesis: verum
end;
hence chi (r,[:X,X:]) is antisymmetric by Def8; ::_thesis: verum
end;
theorem :: LFUZZY_1:14
for X being non empty set
for r being Relation of X st r is symmetric holds
chi (r,[:X,X:]) is symmetric
proof
let X be non empty set ; ::_thesis: for r being Relation of X st r is symmetric holds
chi (r,[:X,X:]) is symmetric
let r be Relation of X; ::_thesis: ( r is symmetric implies chi (r,[:X,X:]) is symmetric )
assume r is symmetric ; ::_thesis: chi (r,[:X,X:]) is symmetric
then A1: r is_symmetric_in field r by RELAT_2:def_11;
let x, y be Element of X; :: according to LFUZZY_1:def_5 ::_thesis: (chi (r,[:X,X:])) . (x,y) = (chi (r,[:X,X:])) . (y,x)
A2: ( x in field r & y in field r & [x,y] in r implies [y,x] in r ) by A1, RELAT_2:def_3;
A3: ( x in field r & y in field r & [y,x] in r implies [x,y] in r ) by A1, RELAT_2:def_3;
percases ( [x,y] in r or not [x,y] in r ) ;
supposeA4: [x,y] in r ; ::_thesis: (chi (r,[:X,X:])) . (x,y) = (chi (r,[:X,X:])) . (y,x)
then (chi (r,[:X,X:])) . [x,y] = 1 by FUNCT_3:def_3;
hence (chi (r,[:X,X:])) . (x,y) = (chi (r,[:X,X:])) . (y,x) by A2, A4, FUNCT_3:def_3, RELAT_1:15; ::_thesis: verum
end;
suppose not [x,y] in r ; ::_thesis: (chi (r,[:X,X:])) . (x,y) = (chi (r,[:X,X:])) . (y,x)
then ( not [y,x] in r & (chi (r,[:X,X:])) . [x,y] = 0 ) by A3, FUNCT_3:def_3, RELAT_1:15;
hence (chi (r,[:X,X:])) . (x,y) = (chi (r,[:X,X:])) . (y,x) by FUNCT_3:def_3; ::_thesis: verum
end;
end;
end;
theorem :: LFUZZY_1:15
for X being non empty set
for r being Relation of X st r is transitive holds
chi (r,[:X,X:]) is transitive
proof
let X be non empty set ; ::_thesis: for r being Relation of X st r is transitive holds
chi (r,[:X,X:]) is transitive
let r be Relation of X; ::_thesis: ( r is transitive implies chi (r,[:X,X:]) is transitive )
assume A1: r is transitive ; ::_thesis: chi (r,[:X,X:]) is transitive
let x, y, z be Element of X; :: according to LFUZZY_1:def_7 ::_thesis: ((chi (r,[:X,X:])) . [x,y]) "/\" ((chi (r,[:X,X:])) . [y,z]) <<= (chi (r,[:X,X:])) . [x,z]
r is_transitive_in field r by A1, RELAT_2:def_16;
then A2: ( x in field r & y in field r & z in field r & [x,y] in r & [y,z] in r implies [x,z] in r ) by RELAT_2:def_8;
percases ( [x,y] in r or not [x,y] in r ) ;
supposeA3: [x,y] in r ; ::_thesis: ((chi (r,[:X,X:])) . [x,y]) "/\" ((chi (r,[:X,X:])) . [y,z]) <<= (chi (r,[:X,X:])) . [x,z]
thus ((chi (r,[:X,X:])) . [x,y]) "/\" ((chi (r,[:X,X:])) . [y,z]) <<= (chi (r,[:X,X:])) . [x,z] ::_thesis: verum
proof
percases ( [y,z] in r or not [y,z] in r ) ;
supposeA4: [y,z] in r ; ::_thesis: ((chi (r,[:X,X:])) . [x,y]) "/\" ((chi (r,[:X,X:])) . [y,z]) <<= (chi (r,[:X,X:])) . [x,z]
((chi (r,[:X,X:])) . [x,y]) "/\" ((chi (r,[:X,X:])) . [y,z]) = min (1,((chi (r,[:X,X:])) . [y,z])) by A3, FUNCT_3:def_3
.= min (1,1) by A4, FUNCT_3:def_3
.= (chi (r,[:X,X:])) . [x,z] by A2, A3, A4, FUNCT_3:def_3, RELAT_1:15 ;
hence ((chi (r,[:X,X:])) . [x,y]) "/\" ((chi (r,[:X,X:])) . [y,z]) <<= (chi (r,[:X,X:])) . [x,z] by LFUZZY_0:3; ::_thesis: verum
end;
supposeA5: not [y,z] in r ; ::_thesis: ((chi (r,[:X,X:])) . [x,y]) "/\" ((chi (r,[:X,X:])) . [y,z]) <<= (chi (r,[:X,X:])) . [x,z]
((chi (r,[:X,X:])) . [x,y]) "/\" ((chi (r,[:X,X:])) . [y,z]) = min (1,((chi (r,[:X,X:])) . [y,z])) by A3, FUNCT_3:def_3
.= min (1,0) by A5, FUNCT_3:def_3
.= 0 by XXREAL_0:def_9 ;
then ((chi (r,[:X,X:])) . [x,y]) "/\" ((chi (r,[:X,X:])) . [y,z]) <= (chi (r,[:X,X:])) . [x,z] by FUZZY_2:1;
hence ((chi (r,[:X,X:])) . [x,y]) "/\" ((chi (r,[:X,X:])) . [y,z]) <<= (chi (r,[:X,X:])) . [x,z] by LFUZZY_0:3; ::_thesis: verum
end;
end;
end;
end;
supposeA6: not [x,y] in r ; ::_thesis: ((chi (r,[:X,X:])) . [x,y]) "/\" ((chi (r,[:X,X:])) . [y,z]) <<= (chi (r,[:X,X:])) . [x,z]
thus ((chi (r,[:X,X:])) . [x,y]) "/\" ((chi (r,[:X,X:])) . [y,z]) <<= (chi (r,[:X,X:])) . [x,z] ::_thesis: verum
proof
percases ( [y,z] in r or not [y,z] in r ) ;
supposeA7: [y,z] in r ; ::_thesis: ((chi (r,[:X,X:])) . [x,y]) "/\" ((chi (r,[:X,X:])) . [y,z]) <<= (chi (r,[:X,X:])) . [x,z]
((chi (r,[:X,X:])) . [x,y]) "/\" ((chi (r,[:X,X:])) . [y,z]) = min (0,((chi (r,[:X,X:])) . [y,z])) by A6, FUNCT_3:def_3
.= min (0,1) by A7, FUNCT_3:def_3
.= 0 by XXREAL_0:def_9 ;
then ((chi (r,[:X,X:])) . [x,y]) "/\" ((chi (r,[:X,X:])) . [y,z]) <= (chi (r,[:X,X:])) . [x,z] by FUZZY_2:1;
hence ((chi (r,[:X,X:])) . [x,y]) "/\" ((chi (r,[:X,X:])) . [y,z]) <<= (chi (r,[:X,X:])) . [x,z] by LFUZZY_0:3; ::_thesis: verum
end;
supposeA8: not [y,z] in r ; ::_thesis: ((chi (r,[:X,X:])) . [x,y]) "/\" ((chi (r,[:X,X:])) . [y,z]) <<= (chi (r,[:X,X:])) . [x,z]
((chi (r,[:X,X:])) . [x,y]) "/\" ((chi (r,[:X,X:])) . [y,z]) = min (0,((chi (r,[:X,X:])) . [y,z])) by A6, FUNCT_3:def_3
.= min (0,0) by A8, FUNCT_3:def_3
.= 0 ;
then ((chi (r,[:X,X:])) . [x,y]) "/\" ((chi (r,[:X,X:])) . [y,z]) <= (chi (r,[:X,X:])) . [x,z] by FUZZY_2:1;
hence ((chi (r,[:X,X:])) . [x,y]) "/\" ((chi (r,[:X,X:])) . [y,z]) <<= (chi (r,[:X,X:])) . [x,z] by LFUZZY_0:3; ::_thesis: verum
end;
end;
end;
end;
end;
end;
theorem :: LFUZZY_1:16
for X being non empty set holds
( Zmf (X,X) is symmetric & Zmf (X,X) is antisymmetric & Zmf (X,X) is transitive )
proof
let X be non empty set ; ::_thesis: ( Zmf (X,X) is symmetric & Zmf (X,X) is antisymmetric & Zmf (X,X) is transitive )
thus Zmf (X,X) is symmetric ::_thesis: ( Zmf (X,X) is antisymmetric & Zmf (X,X) is transitive )
proof
let x, y be Element of X; :: according to LFUZZY_1:def_5 ::_thesis: (Zmf (X,X)) . (x,y) = (Zmf (X,X)) . (y,x)
( (Zmf (X,X)) . [x,y] = 0 & (Zmf (X,X)) . [y,x] = 0 ) by FUZZY_4:21;
hence (Zmf (X,X)) . (x,y) = (Zmf (X,X)) . (y,x) ; ::_thesis: verum
end;
thus Zmf (X,X) is antisymmetric ::_thesis: Zmf (X,X) is transitive
proof
let x, y be Element of X; :: according to LFUZZY_1:def_8 ::_thesis: ( (Zmf (X,X)) . (x,y) <> 0 & (Zmf (X,X)) . (y,x) <> 0 implies x = y )
(Zmf (X,X)) . [x,y] = 0 by FUZZY_4:21;
hence ( (Zmf (X,X)) . (x,y) <> 0 & (Zmf (X,X)) . (y,x) <> 0 implies x = y ) ; ::_thesis: verum
end;
thus Zmf (X,X) is transitive ::_thesis: verum
proof
let x, y, z be Element of X; :: according to LFUZZY_1:def_7 ::_thesis: ((Zmf (X,X)) . [x,y]) "/\" ((Zmf (X,X)) . [y,z]) <<= (Zmf (X,X)) . [x,z]
A1: (Zmf (X,X)) . [x,z] = 0 by FUZZY_4:20;
((Zmf (X,X)) . [x,y]) "/\" ((Zmf (X,X)) . [y,z]) = min (0,((Zmf (X,X)) . [y,z])) by FUZZY_4:20
.= min (0,0) by FUZZY_4:20
.= 0 ;
hence ((Zmf (X,X)) . [x,y]) "/\" ((Zmf (X,X)) . [y,z]) <<= (Zmf (X,X)) . [x,z] by A1, LFUZZY_0:3; ::_thesis: verum
end;
end;
theorem :: LFUZZY_1:17
for X being non empty set holds
( Umf (X,X) is symmetric & Umf (X,X) is transitive & Umf (X,X) is reflexive )
proof
let X be non empty set ; ::_thesis: ( Umf (X,X) is symmetric & Umf (X,X) is transitive & Umf (X,X) is reflexive )
thus Umf (X,X) is symmetric ::_thesis: ( Umf (X,X) is transitive & Umf (X,X) is reflexive )
proof
let x, y be Element of X; :: according to LFUZZY_1:def_5 ::_thesis: (Umf (X,X)) . (x,y) = (Umf (X,X)) . (y,x)
thus (Umf (X,X)) . (x,y) = (Umf (X,X)) . [x,y]
.= 1 by FUZZY_4:21
.= (Umf (X,X)) . [y,x] by FUZZY_4:21
.= (Umf (X,X)) . (y,x) ; ::_thesis: verum
end;
thus Umf (X,X) is transitive ::_thesis: Umf (X,X) is reflexive
proof
let x, y, z be Element of X; :: according to LFUZZY_1:def_7 ::_thesis: ((Umf (X,X)) . [x,y]) "/\" ((Umf (X,X)) . [y,z]) <<= (Umf (X,X)) . [x,z]
((Umf (X,X)) . [x,y]) "/\" ((Umf (X,X)) . [y,z]) = min (1,((Umf (X,X)) . [y,z])) by FUZZY_4:20
.= min (1,1) by FUZZY_4:20
.= 1 ;
then ((Umf (X,X)) . [x,y]) "/\" ((Umf (X,X)) . [y,z]) <= (Umf (X,X)) . [x,z] by FUZZY_4:20;
hence ((Umf (X,X)) . [x,y]) "/\" ((Umf (X,X)) . [y,z]) <<= (Umf (X,X)) . [x,z] by LFUZZY_0:3; ::_thesis: verum
end;
thus Umf (X,X) is reflexive ::_thesis: verum
proof
let x be Element of X; :: according to LFUZZY_1:def_3 ::_thesis: (Umf (X,X)) . (x,x) = 1
(Umf (X,X)) . [x,x] = 1 by FUZZY_4:21;
hence (Umf (X,X)) . (x,x) = 1 ; ::_thesis: verum
end;
end;
theorem :: LFUZZY_1:18
for X being non empty set
for R being RMembership_Func of X,X holds max (R,(converse R)) is symmetric
proof
let X be non empty set ; ::_thesis: for R being RMembership_Func of X,X holds max (R,(converse R)) is symmetric
let R be RMembership_Func of X,X; ::_thesis: max (R,(converse R)) is symmetric
set S = max (R,(converse R));
let x, y be Element of X; :: according to LFUZZY_1:def_5 ::_thesis: (max (R,(converse R))) . (x,y) = (max (R,(converse R))) . (y,x)
thus (max (R,(converse R))) . (x,y) = (max (R,(converse R))) . [x,y]
.= max ((R . (x,y)),((converse R) . (x,y))) by FUZZY_1:def_4
.= max ((R . (x,y)),(R . (y,x))) by FUZZY_4:26
.= max (((converse R) . (y,x)),(R . (y,x))) by FUZZY_4:26
.= (max (R,(converse R))) . [y,x] by FUZZY_1:def_4
.= (max (R,(converse R))) . (y,x) ; ::_thesis: verum
end;
theorem :: LFUZZY_1:19
for X being non empty set
for R being RMembership_Func of X,X holds min (R,(converse R)) is symmetric
proof
let X be non empty set ; ::_thesis: for R being RMembership_Func of X,X holds min (R,(converse R)) is symmetric
let R be RMembership_Func of X,X; ::_thesis: min (R,(converse R)) is symmetric
set S = min (R,(converse R));
let x, y be Element of X; :: according to LFUZZY_1:def_5 ::_thesis: (min (R,(converse R))) . (x,y) = (min (R,(converse R))) . (y,x)
thus (min (R,(converse R))) . (x,y) = (min (R,(converse R))) . [x,y]
.= min ((R . (x,y)),((converse R) . (x,y))) by FUZZY_1:def_3
.= min ((R . (x,y)),(R . (y,x))) by FUZZY_4:26
.= min (((converse R) . (y,x)),(R . (y,x))) by FUZZY_4:26
.= (min (R,(converse R))) . [y,x] by FUZZY_1:def_3
.= (min (R,(converse R))) . (y,x) ; ::_thesis: verum
end;
theorem :: LFUZZY_1:20
for X being non empty set
for R, R9 being RMembership_Func of X,X st R9 is symmetric & R9 c= holds
R9 c=
proof
let X be non empty set ; ::_thesis: for R, R9 being RMembership_Func of X,X st R9 is symmetric & R9 c= holds
R9 c=
let R, T be RMembership_Func of X,X; ::_thesis: ( T is symmetric & T c= implies T c= )
assume that
A1: T is symmetric and
A2: T c= ; ::_thesis: T c=
let x, y be Element of X; :: according to LFUZZY_1:def_1 ::_thesis: (max (R,(converse R))) . (x,y) <= T . (x,y)
R . [y,x] <= T . [y,x] by A2, FUZZY_1:def_2;
then R . (y,x) <= T . (y,x) ;
then A3: R . (y,x) <= T . (x,y) by A1, Def5;
R . [x,y] <= T . [x,y] by A2, FUZZY_1:def_2;
then max ((R . (x,y)),(R . (y,x))) <= T . (x,y) by A3, XXREAL_0:28;
then max ((R . (x,y)),((converse R) . (x,y))) <= T . (x,y) by FUZZY_4:26;
then max ((R . [x,y]),((converse R) . [x,y])) <= T . [x,y] ;
hence (max (R,(converse R))) . (x,y) <= T . (x,y) by FUZZY_1:def_4; ::_thesis: verum
end;
theorem :: LFUZZY_1:21
for X being non empty set
for R, R9 being RMembership_Func of X,X st R9 is symmetric & R c= holds
min (R,(converse R)) c=
proof
let X be non empty set ; ::_thesis: for R, R9 being RMembership_Func of X,X st R9 is symmetric & R c= holds
min (R,(converse R)) c=
let R, T be RMembership_Func of X,X; ::_thesis: ( T is symmetric & R c= implies min (R,(converse R)) c= )
assume that
A1: T is symmetric and
A2: R c= ; ::_thesis: min (R,(converse R)) c=
let x, y be Element of X; :: according to LFUZZY_1:def_1 ::_thesis: T . (x,y) <= (min (R,(converse R))) . (x,y)
T . [y,x] <= R . [y,x] by A2, FUZZY_1:def_2;
then T . (y,x) <= R . (y,x) ;
then A3: T . (x,y) <= R . (y,x) by A1, Def5;
T . [x,y] <= R . [x,y] by A2, FUZZY_1:def_2;
then T . (x,y) <= min ((R . (x,y)),(R . (y,x))) by A3, XXREAL_0:20;
then T . (x,y) <= min ((R . (x,y)),((converse R) . (x,y))) by FUZZY_4:26;
then T . [x,y] <= min ((R . [x,y]),((converse R) . [x,y])) ;
hence T . (x,y) <= (min (R,(converse R))) . (x,y) by FUZZY_1:def_3; ::_thesis: verum
end;
begin
definition
let X be non empty set ;
let R be RMembership_Func of X,X;
let n be Nat;
funcn iter R -> RMembership_Func of X,X means :Def9: :: LFUZZY_1:def 9
ex F being Function of NAT,(Funcs ([:X,X:],[.0,1.])) st
( it = F . n & F . 0 = Imf (X,X) & ( for k being Nat ex Q being RMembership_Func of X,X st
( F . k = Q & F . (k + 1) = Q (#) R ) ) );
existence
ex b1 being RMembership_Func of X,X ex F being Function of NAT,(Funcs ([:X,X:],[.0,1.])) st
( b1 = F . n & F . 0 = Imf (X,X) & ( for k being Nat ex Q being RMembership_Func of X,X st
( F . k = Q & F . (k + 1) = Q (#) R ) ) )
proof
reconsider n9 = n as Element of NAT by ORDINAL1:def_12;
set D = the carrier of (FuzzyLattice [:X,X:]);
defpred S1[ set , set , set ] means ex Q being Element of the carrier of (FuzzyLattice [:X,X:]) st
( $2 = Q & $3 = (@ Q) (#) R );
A1: for k being Element of NAT
for x being Element of the carrier of (FuzzyLattice [:X,X:]) ex y being Element of the carrier of (FuzzyLattice [:X,X:]) st S1[k,x,y]
proof
let k be Element of NAT ; ::_thesis: for x being Element of the carrier of (FuzzyLattice [:X,X:]) ex y being Element of the carrier of (FuzzyLattice [:X,X:]) st S1[k,x,y]
let Q be Element of the carrier of (FuzzyLattice [:X,X:]); ::_thesis: ex y being Element of the carrier of (FuzzyLattice [:X,X:]) st S1[k,Q,y]
set y = (@ Q) (#) R;
reconsider y9 = ([:X,X:],((@ Q) (#) R)) @ as Element of the carrier of (FuzzyLattice [:X,X:]) ;
take y9 ; ::_thesis: S1[k,Q,y9]
thus S1[k,Q,y9] by LFUZZY_0:def_6; ::_thesis: verum
end;
consider F being Function of NAT, the carrier of (FuzzyLattice [:X,X:]) such that
A2: ( F . 0 = ([:X,X:],(Imf (X,X))) @ & ( for k being Element of NAT holds S1[k,F . k,F . (k + 1)] ) ) from RECDEF_1:sch_2(A1);
reconsider F = F as Function of NAT,(Funcs ([:X,X:],[.0,1.])) by LFUZZY_0:14;
reconsider IT = F . n9 as Element of (FuzzyLattice [:X,X:]) by LFUZZY_0:14;
reconsider IT9 = @ IT as RMembership_Func of X,X ;
take IT9 ; ::_thesis: ex F being Function of NAT,(Funcs ([:X,X:],[.0,1.])) st
( IT9 = F . n & F . 0 = Imf (X,X) & ( for k being Nat ex Q being RMembership_Func of X,X st
( F . k = Q & F . (k + 1) = Q (#) R ) ) )
thus ex F being Function of NAT,(Funcs ([:X,X:],[.0,1.])) st
( IT9 = F . n & F . 0 = Imf (X,X) & ( for k being Nat ex Q being RMembership_Func of X,X st
( F . k = Q & F . (k + 1) = Q (#) R ) ) ) ::_thesis: verum
proof
take F ; ::_thesis: ( IT9 = F . n & F . 0 = Imf (X,X) & ( for k being Nat ex Q being RMembership_Func of X,X st
( F . k = Q & F . (k + 1) = Q (#) R ) ) )
thus IT9 = F . n by LFUZZY_0:def_5; ::_thesis: ( F . 0 = Imf (X,X) & ( for k being Nat ex Q being RMembership_Func of X,X st
( F . k = Q & F . (k + 1) = Q (#) R ) ) )
thus F . 0 = Imf (X,X) by A2, LFUZZY_0:def_6; ::_thesis: for k being Nat ex Q being RMembership_Func of X,X st
( F . k = Q & F . (k + 1) = Q (#) R )
thus for k being Nat ex Q being RMembership_Func of X,X st
( F . k = Q & F . (k + 1) = Q (#) R ) ::_thesis: verum
proof
let k be Nat; ::_thesis: ex Q being RMembership_Func of X,X st
( F . k = Q & F . (k + 1) = Q (#) R )
reconsider n = k as Element of NAT by ORDINAL1:def_12;
reconsider Q9 = F . n as Element of the carrier of (FuzzyLattice [:X,X:]) by LFUZZY_0:14;
reconsider Q = @ Q9 as RMembership_Func of X,X ;
take Q ; ::_thesis: ( F . k = Q & F . (k + 1) = Q (#) R )
thus F . k = Q by LFUZZY_0:def_5; ::_thesis: F . (k + 1) = Q (#) R
S1[n,F . n,F . (n + 1)] by A2;
hence F . (k + 1) = Q (#) R ; ::_thesis: verum
end;
end;
end;
uniqueness
for b1, b2 being RMembership_Func of X,X st ex F being Function of NAT,(Funcs ([:X,X:],[.0,1.])) st
( b1 = F . n & F . 0 = Imf (X,X) & ( for k being Nat ex Q being RMembership_Func of X,X st
( F . k = Q & F . (k + 1) = Q (#) R ) ) ) & ex F being Function of NAT,(Funcs ([:X,X:],[.0,1.])) st
( b2 = F . n & F . 0 = Imf (X,X) & ( for k being Nat ex Q being RMembership_Func of X,X st
( F . k = Q & F . (k + 1) = Q (#) R ) ) ) holds
b1 = b2
proof
let S, T be RMembership_Func of X,X; ::_thesis: ( ex F being Function of NAT,(Funcs ([:X,X:],[.0,1.])) st
( S = F . n & F . 0 = Imf (X,X) & ( for k being Nat ex Q being RMembership_Func of X,X st
( F . k = Q & F . (k + 1) = Q (#) R ) ) ) & ex F being Function of NAT,(Funcs ([:X,X:],[.0,1.])) st
( T = F . n & F . 0 = Imf (X,X) & ( for k being Nat ex Q being RMembership_Func of X,X st
( F . k = Q & F . (k + 1) = Q (#) R ) ) ) implies S = T )
given F being Function of NAT,(Funcs ([:X,X:],[.0,1.])) such that A3: S = F . n and
A4: F . 0 = Imf (X,X) and
A5: for k being Nat ex Q being RMembership_Func of X,X st
( F . k = Q & F . (k + 1) = Q (#) R ) ; ::_thesis: ( for F being Function of NAT,(Funcs ([:X,X:],[.0,1.])) holds
( not T = F . n or not F . 0 = Imf (X,X) or ex k being Nat st
for Q being RMembership_Func of X,X holds
( not F . k = Q or not F . (k + 1) = Q (#) R ) ) or S = T )
given G being Function of NAT,(Funcs ([:X,X:],[.0,1.])) such that A6: T = G . n and
A7: G . 0 = Imf (X,X) and
A8: for k being Nat ex Q being RMembership_Func of X,X st
( G . k = Q & G . (k + 1) = Q (#) R ) ; ::_thesis: S = T
defpred S1[ Nat] means F . $1 = G . $1;
A9: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A10: F . k = G . k ; ::_thesis: S1[k + 1]
( ex Q being RMembership_Func of X,X st
( G . k = Q & G . (k + 1) = Q (#) R ) & ex Q9 being RMembership_Func of X,X st
( F . k = Q9 & F . (k + 1) = Q9 (#) R ) ) by A5, A8;
hence S1[k + 1] by A10; ::_thesis: verum
end;
A11: S1[ 0 ] by A4, A7;
for k being Nat holds S1[k] from NAT_1:sch_2(A11, A9);
hence S = T by A3, A6; ::_thesis: verum
end;
end;
:: deftheorem Def9 defines iter LFUZZY_1:def_9_:_
for X being non empty set
for R being RMembership_Func of X,X
for n being Nat
for b4 being RMembership_Func of X,X holds
( b4 = n iter R iff ex F being Function of NAT,(Funcs ([:X,X:],[.0,1.])) st
( b4 = F . n & F . 0 = Imf (X,X) & ( for k being Nat ex Q being RMembership_Func of X,X st
( F . k = Q & F . (k + 1) = Q (#) R ) ) ) );
theorem Th22: :: LFUZZY_1:22
for X being non empty set
for R being RMembership_Func of X,X holds (Imf (X,X)) (#) R = R
proof
let X be non empty set ; ::_thesis: for R being RMembership_Func of X,X holds (Imf (X,X)) (#) R = R
let R be RMembership_Func of X,X; ::_thesis: (Imf (X,X)) (#) R = R
A1: for x, y being set st [x,y] in dom ((Imf (X,X)) (#) R) holds
((Imf (X,X)) (#) R) . (x,y) = R . (x,y)
proof
let x, y be set ; ::_thesis: ( [x,y] in dom ((Imf (X,X)) (#) R) implies ((Imf (X,X)) (#) R) . (x,y) = R . (x,y) )
assume [x,y] in dom ((Imf (X,X)) (#) R) ; ::_thesis: ((Imf (X,X)) (#) R) . (x,y) = R . (x,y)
then reconsider x = x, y = y as Element of X by ZFMISC_1:87;
set S = { (((Imf (X,X)) . (x,z)) "/\" (R . (z,y))) where z is Element of X : verum } ;
for c being Element of (RealPoset [.0,1.]) st c in { (((Imf (X,X)) . (x,z)) "/\" (R . (z,y))) where z is Element of X : verum } holds
c <<= R . [x,y]
proof
let c be Element of (RealPoset [.0,1.]); ::_thesis: ( c in { (((Imf (X,X)) . (x,z)) "/\" (R . (z,y))) where z is Element of X : verum } implies c <<= R . [x,y] )
assume c in { (((Imf (X,X)) . (x,z)) "/\" (R . (z,y))) where z is Element of X : verum } ; ::_thesis: c <<= R . [x,y]
then consider z being Element of X such that
A2: c = ((Imf (X,X)) . (x,z)) "/\" (R . (z,y)) ;
percases ( x = z or x <> z ) ;
supposeA3: x = z ; ::_thesis: c <<= R . [x,y]
A4: R . (z,y) <= 1 by FUZZY_4:4;
c = min ((R . [z,y]),1) by A2, A3, FUZZY_4:25
.= R . [x,y] by A3, A4, XXREAL_0:def_9 ;
hence c <<= R . [x,y] by LFUZZY_0:3; ::_thesis: verum
end;
supposeA5: x <> z ; ::_thesis: c <<= R . [x,y]
A6: 0 <= R . (z,y) by FUZZY_4:4;
c = min ((R . [z,y]),0) by A2, A5, FUZZY_4:25
.= 0 by A6, XXREAL_0:def_9 ;
then c <= R . (x,y) by FUZZY_4:4;
hence c <<= R . [x,y] by LFUZZY_0:3; ::_thesis: verum
end;
end;
end;
then A7: ( ((Imf (X,X)) (#) R) . (x,y) = "\/" ( { (((Imf (X,X)) . (x,z)) "/\" (R . (z,y))) where z is Element of X : verum } ,(RealPoset [.0,1.])) & R . (x,y) is_>=_than { (((Imf (X,X)) . (x,z)) "/\" (R . (z,y))) where z is Element of X : verum } ) by LATTICE3:def_9, LFUZZY_0:22;
for b being Element of (RealPoset [.0,1.]) st b is_>=_than { (((Imf (X,X)) . (x,z)) "/\" (R . (z,y))) where z is Element of X : verum } holds
R . (x,y) <<= b
proof
let b be Element of (RealPoset [.0,1.]); ::_thesis: ( b is_>=_than { (((Imf (X,X)) . (x,z)) "/\" (R . (z,y))) where z is Element of X : verum } implies R . (x,y) <<= b )
A8: R . (x,y) <= 1 by FUZZY_4:4;
((Imf (X,X)) . (x,x)) "/\" (R . [x,y]) = min (1,(R . (x,y))) by FUZZY_4:25
.= R . [x,y] by A8, XXREAL_0:def_9 ;
then A9: R . (x,y) in { (((Imf (X,X)) . (x,z)) "/\" (R . (z,y))) where z is Element of X : verum } ;
assume b is_>=_than { (((Imf (X,X)) . (x,z)) "/\" (R . (z,y))) where z is Element of X : verum } ; ::_thesis: R . (x,y) <<= b
hence R . (x,y) <<= b by A9, LATTICE3:def_9; ::_thesis: verum
end;
hence ((Imf (X,X)) (#) R) . (x,y) = R . (x,y) by A7, YELLOW_0:32; ::_thesis: verum
end;
dom ((Imf (X,X)) (#) R) = [:X,X:] by FUNCT_2:def_1
.= dom R by FUNCT_2:def_1 ;
hence (Imf (X,X)) (#) R = R by A1, BINOP_1:20; ::_thesis: verum
end;
theorem Th23: :: LFUZZY_1:23
for X being non empty set
for R being RMembership_Func of X,X holds R (#) (Imf (X,X)) = R
proof
let X be non empty set ; ::_thesis: for R being RMembership_Func of X,X holds R (#) (Imf (X,X)) = R
let R be RMembership_Func of X,X; ::_thesis: R (#) (Imf (X,X)) = R
A1: for x, y being set st [x,y] in dom (R (#) (Imf (X,X))) holds
(R (#) (Imf (X,X))) . (x,y) = R . (x,y)
proof
let x, y be set ; ::_thesis: ( [x,y] in dom (R (#) (Imf (X,X))) implies (R (#) (Imf (X,X))) . (x,y) = R . (x,y) )
assume [x,y] in dom (R (#) (Imf (X,X))) ; ::_thesis: (R (#) (Imf (X,X))) . (x,y) = R . (x,y)
then reconsider x = x, y = y as Element of X by ZFMISC_1:87;
set S = { ((R . (x,z)) "/\" ((Imf (X,X)) . (z,y))) where z is Element of X : verum } ;
for c being Element of (RealPoset [.0,1.]) st c in { ((R . (x,z)) "/\" ((Imf (X,X)) . (z,y))) where z is Element of X : verum } holds
c <<= R . [x,y]
proof
let c be Element of (RealPoset [.0,1.]); ::_thesis: ( c in { ((R . (x,z)) "/\" ((Imf (X,X)) . (z,y))) where z is Element of X : verum } implies c <<= R . [x,y] )
assume c in { ((R . (x,z)) "/\" ((Imf (X,X)) . (z,y))) where z is Element of X : verum } ; ::_thesis: c <<= R . [x,y]
then consider z being Element of X such that
A2: c = (R . (x,z)) "/\" ((Imf (X,X)) . (z,y)) ;
percases ( y = z or not y = z ) ;
supposeA3: y = z ; ::_thesis: c <<= R . [x,y]
A4: R . (x,z) <= 1 by FUZZY_4:4;
c = min ((R . [x,z]),1) by A2, A3, FUZZY_4:25
.= R . [x,y] by A3, A4, XXREAL_0:def_9 ;
hence c <<= R . [x,y] by LFUZZY_0:3; ::_thesis: verum
end;
supposeA5: not y = z ; ::_thesis: c <<= R . [x,y]
A6: 0 <= R . (x,z) by FUZZY_4:4;
c = min ((R . [x,z]),0) by A2, A5, FUZZY_4:25
.= 0 by A6, XXREAL_0:def_9 ;
then c <= R . (x,y) by FUZZY_4:4;
hence c <<= R . [x,y] by LFUZZY_0:3; ::_thesis: verum
end;
end;
end;
then A7: ( (R (#) (Imf (X,X))) . (x,y) = "\/" ( { ((R . (x,z)) "/\" ((Imf (X,X)) . (z,y))) where z is Element of X : verum } ,(RealPoset [.0,1.])) & R . (x,y) is_>=_than { ((R . (x,z)) "/\" ((Imf (X,X)) . (z,y))) where z is Element of X : verum } ) by LATTICE3:def_9, LFUZZY_0:22;
for b being Element of (RealPoset [.0,1.]) st b is_>=_than { ((R . (x,z)) "/\" ((Imf (X,X)) . (z,y))) where z is Element of X : verum } holds
R . (x,y) <<= b
proof
let b be Element of (RealPoset [.0,1.]); ::_thesis: ( b is_>=_than { ((R . (x,z)) "/\" ((Imf (X,X)) . (z,y))) where z is Element of X : verum } implies R . (x,y) <<= b )
A8: R . (x,y) <= 1 by FUZZY_4:4;
(R . [x,y]) "/\" ((Imf (X,X)) . (y,y)) = min ((R . [x,y]),1) by FUZZY_4:25
.= R . [x,y] by A8, XXREAL_0:def_9 ;
then A9: R . (x,y) in { ((R . (x,z)) "/\" ((Imf (X,X)) . (z,y))) where z is Element of X : verum } ;
assume b is_>=_than { ((R . (x,z)) "/\" ((Imf (X,X)) . (z,y))) where z is Element of X : verum } ; ::_thesis: R . (x,y) <<= b
hence R . (x,y) <<= b by A9, LATTICE3:def_9; ::_thesis: verum
end;
hence (R (#) (Imf (X,X))) . (x,y) = R . (x,y) by A7, YELLOW_0:32; ::_thesis: verum
end;
dom (R (#) (Imf (X,X))) = [:X,X:] by FUNCT_2:def_1
.= dom R by FUNCT_2:def_1 ;
hence R (#) (Imf (X,X)) = R by A1, BINOP_1:20; ::_thesis: verum
end;
theorem Th24: :: LFUZZY_1:24
for X being non empty set
for R being RMembership_Func of X,X holds 0 iter R = Imf (X,X)
proof
let X be non empty set ; ::_thesis: for R being RMembership_Func of X,X holds 0 iter R = Imf (X,X)
let R be RMembership_Func of X,X; ::_thesis: 0 iter R = Imf (X,X)
ex F being Function of NAT,(Funcs ([:X,X:],[.0,1.])) st
( 0 iter R = F . 0 & F . 0 = Imf (X,X) & ( for k being Nat ex Q being RMembership_Func of X,X st
( F . k = Q & F . (k + 1) = Q (#) R ) ) ) by Def9;
hence 0 iter R = Imf (X,X) ; ::_thesis: verum
end;
theorem Th25: :: LFUZZY_1:25
for X being non empty set
for R being RMembership_Func of X,X holds 1 iter R = R
proof
let X be non empty set ; ::_thesis: for R being RMembership_Func of X,X holds 1 iter R = R
let R be RMembership_Func of X,X; ::_thesis: 1 iter R = R
consider F being Function of NAT,(Funcs ([:X,X:],[.0,1.])) such that
A1: ( 1 iter R = F . 1 & F . 0 = Imf (X,X) ) and
A2: for k being Nat ex Q being RMembership_Func of X,X st
( F . k = Q & F . (k + 1) = Q (#) R ) by Def9;
ex Q being RMembership_Func of X,X st
( F . 0 = Q & F . (0 + 1) = Q (#) R ) by A2;
hence 1 iter R = R by A1, Th22; ::_thesis: verum
end;
theorem Th26: :: LFUZZY_1:26
for X being non empty set
for R being RMembership_Func of X,X
for n being Nat holds (n + 1) iter R = (n iter R) (#) R
proof
let X be non empty set ; ::_thesis: for R being RMembership_Func of X,X
for n being Nat holds (n + 1) iter R = (n iter R) (#) R
let R be RMembership_Func of X,X; ::_thesis: for n being Nat holds (n + 1) iter R = (n iter R) (#) R
let n be Nat; ::_thesis: (n + 1) iter R = (n iter R) (#) R
consider f being Function of NAT,(Funcs ([:X,X:],[.0,1.])) such that
A1: ( (n + 1) iter R = f . (n + 1) & f . 0 = Imf (X,X) ) and
A2: for k being Nat ex Q being RMembership_Func of X,X st
( f . k = Q & f . (k + 1) = Q (#) R ) by Def9;
ex Q being RMembership_Func of X,X st
( f . n = Q & f . (n + 1) = Q (#) R ) by A2;
hence (n + 1) iter R = (n iter R) (#) R by A1, A2, Def9; ::_thesis: verum
end;
theorem Th27: :: LFUZZY_1:27
for X being non empty set
for R being RMembership_Func of X,X
for m, n being Nat holds (m + n) iter R = (m iter R) (#) (n iter R)
proof
let X be non empty set ; ::_thesis: for R being RMembership_Func of X,X
for m, n being Nat holds (m + n) iter R = (m iter R) (#) (n iter R)
let R be RMembership_Func of X,X; ::_thesis: for m, n being Nat holds (m + n) iter R = (m iter R) (#) (n iter R)
let m, n be Nat; ::_thesis: (m + n) iter R = (m iter R) (#) (n iter R)
defpred S1[ Nat] means (m + $1) iter R = (m iter R) (#) ($1 iter R);
A1: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] )
assume A2: (m + n) iter R = (m iter R) (#) (n iter R) ; ::_thesis: S1[n + 1]
thus (m iter R) (#) ((n + 1) iter R) = (m iter R) (#) ((n iter R) (#) R) by Th26
.= ((m + n) iter R) (#) R by A2, LFUZZY_0:23
.= ((m + n) + 1) iter R by Th26
.= (m + (n + 1)) iter R ; ::_thesis: verum
end;
(m iter R) (#) (0 iter R) = (m iter R) (#) (Imf (X,X)) by Th24
.= m iter R by Th23 ;
then A3: S1[ 0 ] ;
for m being Nat holds S1[m] from NAT_1:sch_2(A3, A1);
hence (m + n) iter R = (m iter R) (#) (n iter R) ; ::_thesis: verum
end;
theorem :: LFUZZY_1:28
for X being non empty set
for R being RMembership_Func of X,X
for m, n being Nat holds (m * n) iter R = m iter (n iter R)
proof
let X be non empty set ; ::_thesis: for R being RMembership_Func of X,X
for m, n being Nat holds (m * n) iter R = m iter (n iter R)
let R be RMembership_Func of X,X; ::_thesis: for m, n being Nat holds (m * n) iter R = m iter (n iter R)
let m, n be Nat; ::_thesis: (m * n) iter R = m iter (n iter R)
defpred S1[ Nat] means ($1 * n) iter R = $1 iter (n iter R);
A1: for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be Nat; ::_thesis: ( S1[m] implies S1[m + 1] )
assume A2: (m * n) iter R = m iter (n iter R) ; ::_thesis: S1[m + 1]
A3: (m + 1) iter (n iter R) = (m iter (n iter R)) (#) (1 iter (n iter R)) by Th27
.= (m iter (n iter R)) (#) (n iter R) by Th25 ;
((m + 1) * n) iter R = ((m * n) + (1 * n)) iter R
.= (m iter (n iter R)) (#) (n iter R) by A2, Th27 ;
hence S1[m + 1] by A3; ::_thesis: verum
end;
(0 * n) iter R = Imf (X,X) by Th24
.= 0 iter (n iter R) by Th24 ;
then A4: S1[ 0 ] ;
for m being Nat holds S1[m] from NAT_1:sch_2(A4, A1);
hence (m * n) iter R = m iter (n iter R) ; ::_thesis: verum
end;
definition
let X be non empty set ;
let R be RMembership_Func of X,X;
func TrCl R -> RMembership_Func of X,X equals :: LFUZZY_1:def 10
"\/" ( { (n iter R) where n is Element of NAT : n > 0 } ,(FuzzyLattice [:X,X:]));
coherence
"\/" ( { (n iter R) where n is Element of NAT : n > 0 } ,(FuzzyLattice [:X,X:])) is RMembership_Func of X,X
proof
set S = "\/" ( { (n iter R) where n is Element of NAT : n > 0 } ,(FuzzyLattice [:X,X:]));
"\/" ( { (n iter R) where n is Element of NAT : n > 0 } ,(FuzzyLattice [:X,X:])) = @ ("\/" ( { (n iter R) where n is Element of NAT : n > 0 } ,(FuzzyLattice [:X,X:]))) by LFUZZY_0:def_5;
hence "\/" ( { (n iter R) where n is Element of NAT : n > 0 } ,(FuzzyLattice [:X,X:])) is RMembership_Func of X,X ; ::_thesis: verum
end;
end;
:: deftheorem defines TrCl LFUZZY_1:def_10_:_
for X being non empty set
for R being RMembership_Func of X,X holds TrCl R = "\/" ( { (n iter R) where n is Element of NAT : n > 0 } ,(FuzzyLattice [:X,X:]));
theorem Th29: :: LFUZZY_1:29
for X being non empty set
for R being RMembership_Func of X,X
for x, y being Element of X holds (TrCl R) . [x,y] = "\/" ((pi ( { (n iter R) where n is Element of NAT : n > 0 } ,[x,y])),(RealPoset [.0,1.]))
proof
let X be non empty set ; ::_thesis: for R being RMembership_Func of X,X
for x, y being Element of X holds (TrCl R) . [x,y] = "\/" ((pi ( { (n iter R) where n is Element of NAT : n > 0 } ,[x,y])),(RealPoset [.0,1.]))
let R be RMembership_Func of X,X; ::_thesis: for x, y being Element of X holds (TrCl R) . [x,y] = "\/" ((pi ( { (n iter R) where n is Element of NAT : n > 0 } ,[x,y])),(RealPoset [.0,1.]))
set Q = { (n iter R) where n is Element of NAT : n > 0 } ;
{ (n iter R) where n is Element of NAT : n > 0 } c= the carrier of (FuzzyLattice [:X,X:])
proof
let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in { (n iter R) where n is Element of NAT : n > 0 } or t in the carrier of (FuzzyLattice [:X,X:]) )
assume t in { (n iter R) where n is Element of NAT : n > 0 } ; ::_thesis: t in the carrier of (FuzzyLattice [:X,X:])
then ex n being Element of NAT st
( t = n iter R & n > 0 ) ;
then reconsider t = t as Membership_Func of [:X,X:] ;
([:X,X:],t) @ is Element of (FuzzyLattice [:X,X:]) ;
then reconsider t = t as Element of (FuzzyLattice [:X,X:]) by LFUZZY_0:def_6;
t in the carrier of (FuzzyLattice [:X,X:]) ;
hence t in the carrier of (FuzzyLattice [:X,X:]) ; ::_thesis: verum
end;
then reconsider Q = { (n iter R) where n is Element of NAT : n > 0 } as Subset of (FuzzyLattice [:X,X:]) ;
let x, z be Element of X; ::_thesis: (TrCl R) . [x,z] = "\/" ((pi ( { (n iter R) where n is Element of NAT : n > 0 } ,[x,z])),(RealPoset [.0,1.]))
reconsider i = [x,z] as Element of [:X,X:] ;
A1: for a being Element of [:X,X:] holds ([:X,X:] --> (RealPoset [.0,1.])) . a is complete LATTICE by FUNCOP_1:7;
FuzzyLattice [:X,X:] = (RealPoset [.0,1.]) |^ [:X,X:] by LFUZZY_0:def_4
.= product ([:X,X:] --> (RealPoset [.0,1.])) by YELLOW_1:def_5 ;
then (sup Q) . i = "\/" ((pi (Q,i)),(([:X,X:] --> (RealPoset [.0,1.])) . i)) by A1, WAYBEL_3:32;
hence (TrCl R) . [x,z] = "\/" ((pi ( { (n iter R) where n is Element of NAT : n > 0 } ,[x,z])),(RealPoset [.0,1.])) by FUNCOP_1:7; ::_thesis: verum
end;
theorem Th30: :: LFUZZY_1:30
for X being non empty set
for R being RMembership_Func of X,X holds TrCl R c=
proof
let X be non empty set ; ::_thesis: for R being RMembership_Func of X,X holds TrCl R c=
let R be RMembership_Func of X,X; ::_thesis: TrCl R c=
for c being Element of [:X,X:] holds R . c <= (TrCl R) . c
proof
set Q = { (n iter R) where n is Element of NAT : n > 0 } ;
let c be Element of [:X,X:]; ::_thesis: R . c <= (TrCl R) . c
consider x, y being set such that
A1: [x,y] = c by RELAT_1:def_1;
reconsider x = x, y = y as Element of X by A1, ZFMISC_1:87;
R = 1 iter R by Th25;
then R in { (n iter R) where n is Element of NAT : n > 0 } ;
then A2: R . [x,y] in pi ( { (n iter R) where n is Element of NAT : n > 0 } ,[x,y]) by CARD_3:def_6;
(TrCl R) . [x,y] = "\/" ((pi ( { (n iter R) where n is Element of NAT : n > 0 } ,[x,y])),(RealPoset [.0,1.])) by Th29;
then R . [x,y] <<= (TrCl R) . [x,y] by A2, YELLOW_2:22;
hence R . c <= (TrCl R) . c by A1, LFUZZY_0:3; ::_thesis: verum
end;
hence TrCl R c= by FUZZY_1:def_2; ::_thesis: verum
end;
theorem Th31: :: LFUZZY_1:31
for X being non empty set
for R being RMembership_Func of X,X
for n being Nat st n > 0 holds
TrCl R c=
proof
let X be non empty set ; ::_thesis: for R being RMembership_Func of X,X
for n being Nat st n > 0 holds
TrCl R c=
let R be RMembership_Func of X,X; ::_thesis: for n being Nat st n > 0 holds
TrCl R c=
let n9 be Nat; ::_thesis: ( n9 > 0 implies TrCl R c= )
assume A1: n9 > 0 ; ::_thesis: TrCl R c=
for c being Element of [:X,X:] holds (n9 iter R) . c <= (TrCl R) . c
proof
reconsider n9 = n9 as Element of NAT by ORDINAL1:def_12;
set Q = { (n iter R) where n is Element of NAT : n > 0 } ;
let c be Element of [:X,X:]; ::_thesis: (n9 iter R) . c <= (TrCl R) . c
consider x, y being set such that
A2: [x,y] = c by RELAT_1:def_1;
reconsider x = x, y = y as Element of X by A2, ZFMISC_1:87;
n9 iter R in { (n iter R) where n is Element of NAT : n > 0 } by A1;
then A3: (n9 iter R) . [x,y] in pi ( { (n iter R) where n is Element of NAT : n > 0 } ,[x,y]) by CARD_3:def_6;
(TrCl R) . [x,y] = "\/" ((pi ( { (n iter R) where n is Element of NAT : n > 0 } ,[x,y])),(RealPoset [.0,1.])) by Th29;
then (n9 iter R) . [x,y] <<= (TrCl R) . [x,y] by A3, YELLOW_2:22;
hence (n9 iter R) . c <= (TrCl R) . c by A2, LFUZZY_0:3; ::_thesis: verum
end;
hence TrCl R c= by FUZZY_1:def_2; ::_thesis: verum
end;
theorem Th32: :: LFUZZY_1:32
for X being non empty set
for Q being Subset of (FuzzyLattice X)
for x being Element of X holds ("\/" (Q,(FuzzyLattice X))) . x = "\/" ((pi (Q,x)),(RealPoset [.0,1.]))
proof
let X be non empty set ; ::_thesis: for Q being Subset of (FuzzyLattice X)
for x being Element of X holds ("\/" (Q,(FuzzyLattice X))) . x = "\/" ((pi (Q,x)),(RealPoset [.0,1.]))
let Q be Subset of (FuzzyLattice X); ::_thesis: for x being Element of X holds ("\/" (Q,(FuzzyLattice X))) . x = "\/" ((pi (Q,x)),(RealPoset [.0,1.]))
let x be Element of X; ::_thesis: ("\/" (Q,(FuzzyLattice X))) . x = "\/" ((pi (Q,x)),(RealPoset [.0,1.]))
A1: for a being Element of X holds (X --> (RealPoset [.0,1.])) . a is complete LATTICE by FUNCOP_1:7;
FuzzyLattice X = (RealPoset [.0,1.]) |^ X by LFUZZY_0:def_4
.= product (X --> (RealPoset [.0,1.])) by YELLOW_1:def_5 ;
then (sup Q) . x = "\/" ((pi (Q,x)),((X --> (RealPoset [.0,1.])) . x)) by A1, WAYBEL_3:32;
hence ("\/" (Q,(FuzzyLattice X))) . x = "\/" ((pi (Q,x)),(RealPoset [.0,1.])) by FUNCOP_1:7; ::_thesis: verum
end;
Lm2: for X being non empty set
for R being RMembership_Func of X,X
for Q being Subset of (FuzzyLattice [:X,X:])
for x, z being Element of X holds { ((R . (x,y)) "/\" ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . (y,z))) where y is Element of X : verum } = { ((R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.])))) where y is Element of X : verum }
proof
let X be non empty set ; ::_thesis: for R being RMembership_Func of X,X
for Q being Subset of (FuzzyLattice [:X,X:])
for x, z being Element of X holds { ((R . (x,y)) "/\" ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . (y,z))) where y is Element of X : verum } = { ((R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.])))) where y is Element of X : verum }
let R be RMembership_Func of X,X; ::_thesis: for Q being Subset of (FuzzyLattice [:X,X:])
for x, z being Element of X holds { ((R . (x,y)) "/\" ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . (y,z))) where y is Element of X : verum } = { ((R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.])))) where y is Element of X : verum }
let Q be Subset of (FuzzyLattice [:X,X:]); ::_thesis: for x, z being Element of X holds { ((R . (x,y)) "/\" ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . (y,z))) where y is Element of X : verum } = { ((R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.])))) where y is Element of X : verum }
let x, z be Element of X; ::_thesis: { ((R . (x,y)) "/\" ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . (y,z))) where y is Element of X : verum } = { ((R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.])))) where y is Element of X : verum }
defpred S1[ Element of X] means verum;
deffunc H1( Element of X) -> Element of the carrier of (RealPoset [.0,1.]) = (R . (x,$1)) "/\" ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . ($1,z));
deffunc H2( Element of X) -> Element of the carrier of (RealPoset [.0,1.]) = (R . [x,$1]) "/\" ("\/" ((pi (Q,[$1,z])),(RealPoset [.0,1.])));
for y being Element of X holds (R . [x,y]) "/\" ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . [y,z]) = (R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.])))
proof
let y be Element of X; ::_thesis: (R . [x,y]) "/\" ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . [y,z]) = (R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.])))
(@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . [y,z] = ("\/" (Q,(FuzzyLattice [:X,X:]))) . [y,z] by LFUZZY_0:def_5
.= "\/" ((pi (Q,[y,z])),(RealPoset [.0,1.])) by Th32 ;
hence (R . [x,y]) "/\" ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . [y,z]) = (R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.]))) ; ::_thesis: verum
end;
then A1: for y being Element of X holds H1(y) = H2(y) ;
thus { H1(y) where y is Element of X : S1[y] } = { H2(y9) where y9 is Element of X : S1[y9] } from FRAENKEL:sch_5(A1); ::_thesis: verum
end;
theorem Th33: :: LFUZZY_1:33
for R being complete Heyting LATTICE
for X being Subset of R
for y being Element of R holds y "/\" ("\/" (X,R)) = "\/" ( { (y "/\" x) where x is Element of R : x in X } ,R)
proof
let R be complete Heyting LATTICE; ::_thesis: for X being Subset of R
for y being Element of R holds y "/\" ("\/" (X,R)) = "\/" ( { (y "/\" x) where x is Element of R : x in X } ,R)
let X be Subset of R; ::_thesis: for y being Element of R holds y "/\" ("\/" (X,R)) = "\/" ( { (y "/\" x) where x is Element of R : x in X } ,R)
let y be Element of R; ::_thesis: y "/\" ("\/" (X,R)) = "\/" ( { (y "/\" x) where x is Element of R : x in X } ,R)
for z being Element of R holds z "/\" is lower_adjoint by WAYBEL_1:def_19;
hence y "/\" ("\/" (X,R)) = "\/" ( { (y "/\" x) where x is Element of R : x in X } ,R) by WAYBEL_1:64; ::_thesis: verum
end;
Lm3: for X being non empty set
for R being RMembership_Func of X,X
for Q being Subset of (FuzzyLattice [:X,X:])
for x, z being Element of X holds { ((R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.])))) where y is Element of X : verum } = { ("\/" ( { ((R . [x,y9]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[y9,z]) } ,(RealPoset [.0,1.]))) where y9 is Element of X : verum }
proof
let X be non empty set ; ::_thesis: for R being RMembership_Func of X,X
for Q being Subset of (FuzzyLattice [:X,X:])
for x, z being Element of X holds { ((R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.])))) where y is Element of X : verum } = { ("\/" ( { ((R . [x,y9]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[y9,z]) } ,(RealPoset [.0,1.]))) where y9 is Element of X : verum }
let R be RMembership_Func of X,X; ::_thesis: for Q being Subset of (FuzzyLattice [:X,X:])
for x, z being Element of X holds { ((R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.])))) where y is Element of X : verum } = { ("\/" ( { ((R . [x,y9]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[y9,z]) } ,(RealPoset [.0,1.]))) where y9 is Element of X : verum }
let Q be Subset of (FuzzyLattice [:X,X:]); ::_thesis: for x, z being Element of X holds { ((R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.])))) where y is Element of X : verum } = { ("\/" ( { ((R . [x,y9]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[y9,z]) } ,(RealPoset [.0,1.]))) where y9 is Element of X : verum }
let x, z be Element of X; ::_thesis: { ((R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.])))) where y is Element of X : verum } = { ("\/" ( { ((R . [x,y9]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[y9,z]) } ,(RealPoset [.0,1.]))) where y9 is Element of X : verum }
defpred S1[ Element of X] means verum;
deffunc H1( Element of X) -> Element of the carrier of (RealPoset [.0,1.]) = (R . [x,$1]) "/\" ("\/" ((pi (Q,[$1,z])),(RealPoset [.0,1.])));
deffunc H2( Element of X) -> Element of the carrier of (RealPoset [.0,1.]) = "\/" ( { ((R . [x,$1]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[$1,z]) } ,(RealPoset [.0,1.]));
for y being Element of X holds (R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.]))) = "\/" ( { ((R . [x,y]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[y,z]) } ,(RealPoset [.0,1.]))
proof
let y be Element of X; ::_thesis: (R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.]))) = "\/" ( { ((R . [x,y]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[y,z]) } ,(RealPoset [.0,1.]))
FuzzyLattice [:X,X:] = (RealPoset [.0,1.]) |^ [:X,X:] by LFUZZY_0:def_4
.= product ([:X,X:] --> (RealPoset [.0,1.])) by YELLOW_1:def_5 ;
then reconsider Q = Q as Subset of (product ([:X,X:] --> (RealPoset [.0,1.]))) ;
pi (Q,[y,z]) is Subset of (RealPoset [.0,1.]) by FUNCOP_1:7;
hence (R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.]))) = "\/" ( { ((R . [x,y]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[y,z]) } ,(RealPoset [.0,1.])) by Th33; ::_thesis: verum
end;
then A1: for y being Element of X holds H1(y) = H2(y) ;
{ H1(y) where y is Element of X : S1[y] } = { H2(y) where y is Element of X : S1[y] } from FRAENKEL:sch_5(A1);
hence { ((R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.])))) where y is Element of X : verum } = { ("\/" ( { ((R . [x,y9]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[y9,z]) } ,(RealPoset [.0,1.]))) where y9 is Element of X : verum } ; ::_thesis: verum
end;
Lm4: for X being non empty set
for R being RMembership_Func of X,X
for Q being Subset of (FuzzyLattice [:X,X:])
for x, z being Element of X holds { ("\/" ( { ((R . [x,y]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[y,z]) } ,(RealPoset [.0,1.]))) where y is Element of X : verum } = { ("\/" ( { ((R . [x,y9]) "/\" (r . [y9,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0,1.]))) where y9 is Element of X : verum }
proof
let X be non empty set ; ::_thesis: for R being RMembership_Func of X,X
for Q being Subset of (FuzzyLattice [:X,X:])
for x, z being Element of X holds { ("\/" ( { ((R . [x,y]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[y,z]) } ,(RealPoset [.0,1.]))) where y is Element of X : verum } = { ("\/" ( { ((R . [x,y9]) "/\" (r . [y9,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0,1.]))) where y9 is Element of X : verum }
let R be RMembership_Func of X,X; ::_thesis: for Q being Subset of (FuzzyLattice [:X,X:])
for x, z being Element of X holds { ("\/" ( { ((R . [x,y]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[y,z]) } ,(RealPoset [.0,1.]))) where y is Element of X : verum } = { ("\/" ( { ((R . [x,y9]) "/\" (r . [y9,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0,1.]))) where y9 is Element of X : verum }
let Q be Subset of (FuzzyLattice [:X,X:]); ::_thesis: for x, z being Element of X holds { ("\/" ( { ((R . [x,y]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[y,z]) } ,(RealPoset [.0,1.]))) where y is Element of X : verum } = { ("\/" ( { ((R . [x,y9]) "/\" (r . [y9,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0,1.]))) where y9 is Element of X : verum }
let x, z be Element of X; ::_thesis: { ("\/" ( { ((R . [x,y]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[y,z]) } ,(RealPoset [.0,1.]))) where y is Element of X : verum } = { ("\/" ( { ((R . [x,y9]) "/\" (r . [y9,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0,1.]))) where y9 is Element of X : verum }
set RP = RealPoset [.0,1.];
set FL = FuzzyLattice [:X,X:];
defpred S1[ Element of X] means verum;
deffunc H1( Element of X) -> Element of the carrier of (RealPoset [.0,1.]) = "\/" ( { ((R . [x,$1]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[$1,z]) } ,(RealPoset [.0,1.]));
deffunc H2( Element of X) -> Element of the carrier of (RealPoset [.0,1.]) = "\/" ( { ((R . [x,$1]) "/\" (r . [$1,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0,1.]));
for y being Element of X holds "\/" ( { ((R . [x,y]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[y,z]) } ,(RealPoset [.0,1.])) = "\/" ( { ((R . [x,y]) "/\" (r . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0,1.]))
proof
let y be Element of X; ::_thesis: "\/" ( { ((R . [x,y]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[y,z]) } ,(RealPoset [.0,1.])) = "\/" ( { ((R . [x,y]) "/\" (r . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0,1.]))
set A = { ((R . [x,y]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[y,z]) } ;
set B = { ((R . [x,y]) "/\" (r . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ;
A1: { ((R . [x,y]) "/\" (r . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } c= { ((R . [x,y]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[y,z]) }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { ((R . [x,y]) "/\" (r . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } or a in { ((R . [x,y]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[y,z]) } )
assume a in { ((R . [x,y]) "/\" (r . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ; ::_thesis: a in { ((R . [x,y]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[y,z]) }
then consider r being Element of (FuzzyLattice [:X,X:]) such that
A2: a = (R . [x,y]) "/\" (r . [y,z]) and
A3: r in Q ;
r . [y,z] in pi (Q,[y,z]) by A3, CARD_3:def_6;
hence a in { ((R . [x,y]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[y,z]) } by A2; ::_thesis: verum
end;
{ ((R . [x,y]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[y,z]) } c= { ((R . [x,y]) "/\" (r . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { ((R . [x,y]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[y,z]) } or a in { ((R . [x,y]) "/\" (r . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } )
assume a in { ((R . [x,y]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[y,z]) } ; ::_thesis: a in { ((R . [x,y]) "/\" (r . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q }
then consider b being Element of (RealPoset [.0,1.]) such that
A4: a = (R . [x,y]) "/\" b and
A5: b in pi (Q,[y,z]) ;
ex f being Function st
( f in Q & b = f . [y,z] ) by A5, CARD_3:def_6;
hence a in { ((R . [x,y]) "/\" (r . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } by A4; ::_thesis: verum
end;
hence "\/" ( { ((R . [x,y]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[y,z]) } ,(RealPoset [.0,1.])) = "\/" ( { ((R . [x,y]) "/\" (r . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0,1.])) by A1, XBOOLE_0:def_10; ::_thesis: verum
end;
then A6: for y being Element of X holds H1(y) = H2(y) ;
thus { H1(y) where y is Element of X : S1[y] } = { H2(y) where y is Element of X : S1[y] } from FRAENKEL:sch_5(A6); ::_thesis: verum
end;
Lm5: for X, Y, Z being non empty set
for R being RMembership_Func of X,Y
for S being RMembership_Func of Y,Z
for x being Element of X
for z being Element of Z holds
( rng (min (R,S,x,z)) = { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } & rng (min (R,S,x,z)) <> {} )
proof
let X, Y, Z be non empty set ; ::_thesis: for R being RMembership_Func of X,Y
for S being RMembership_Func of Y,Z
for x being Element of X
for z being Element of Z holds
( rng (min (R,S,x,z)) = { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } & rng (min (R,S,x,z)) <> {} )
let R be RMembership_Func of X,Y; ::_thesis: for S being RMembership_Func of Y,Z
for x being Element of X
for z being Element of Z holds
( rng (min (R,S,x,z)) = { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } & rng (min (R,S,x,z)) <> {} )
let S be RMembership_Func of Y,Z; ::_thesis: for x being Element of X
for z being Element of Z holds
( rng (min (R,S,x,z)) = { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } & rng (min (R,S,x,z)) <> {} )
let x be Element of X; ::_thesis: for z being Element of Z holds
( rng (min (R,S,x,z)) = { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } & rng (min (R,S,x,z)) <> {} )
let z be Element of Z; ::_thesis: ( rng (min (R,S,x,z)) = { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } & rng (min (R,S,x,z)) <> {} )
set L = { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } ;
A1: ( Y = dom (min (R,S,x,z)) & min (R,S,x,z) is PartFunc of (dom (min (R,S,x,z))),(rng (min (R,S,x,z))) ) by FUNCT_2:def_1, RELSET_1:4;
for c being set holds
( c in { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } iff c in rng (min (R,S,x,z)) )
proof
let c be set ; ::_thesis: ( c in { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } iff c in rng (min (R,S,x,z)) )
hereby ::_thesis: ( c in rng (min (R,S,x,z)) implies c in { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } )
assume c in { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } ; ::_thesis: c in rng (min (R,S,x,z))
then consider y being Element of Y such that
A2: c = (R . [x,y]) "/\" (S . [y,z]) ;
c = (min (R,S,x,z)) . y by A2, FUZZY_4:def_2;
hence c in rng (min (R,S,x,z)) by A1, PARTFUN1:4; ::_thesis: verum
end;
assume c in rng (min (R,S,x,z)) ; ::_thesis: c in { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum }
then consider y being Element of Y such that
y in dom (min (R,S,x,z)) and
A3: c = (min (R,S,x,z)) . y by PARTFUN1:3;
c = (R . [x,y]) "/\" (S . [y,z]) by A3, FUZZY_4:def_2;
hence c in { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } ; ::_thesis: verum
end;
hence rng (min (R,S,x,z)) = { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } by TARSKI:1; ::_thesis: rng (min (R,S,x,z)) <> {}
thus rng (min (R,S,x,z)) <> {} ; ::_thesis: verum
end;
Lm6: for X, Y, Z being non empty set
for R being RMembership_Func of X,Y
for S being RMembership_Func of Y,Z
for x being Element of X
for z being Element of Z holds (R (#) S) . [x,z] = "\/" ( { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } ,(RealPoset [.0,1.]))
proof
let X, Y, Z be non empty set ; ::_thesis: for R being RMembership_Func of X,Y
for S being RMembership_Func of Y,Z
for x being Element of X
for z being Element of Z holds (R (#) S) . [x,z] = "\/" ( { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } ,(RealPoset [.0,1.]))
let R be RMembership_Func of X,Y; ::_thesis: for S being RMembership_Func of Y,Z
for x being Element of X
for z being Element of Z holds (R (#) S) . [x,z] = "\/" ( { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } ,(RealPoset [.0,1.]))
let S be RMembership_Func of Y,Z; ::_thesis: for x being Element of X
for z being Element of Z holds (R (#) S) . [x,z] = "\/" ( { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } ,(RealPoset [.0,1.]))
let x be Element of X; ::_thesis: for z being Element of Z holds (R (#) S) . [x,z] = "\/" ( { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } ,(RealPoset [.0,1.]))
let z be Element of Z; ::_thesis: (R (#) S) . [x,z] = "\/" ( { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } ,(RealPoset [.0,1.]))
set L = { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } ;
[x,z] in [:X,Z:] ;
then A1: (R (#) S) . (x,z) = upper_bound (rng (min (R,S,x,z))) by FUZZY_4:def_3;
A2: for b being Element of (RealPoset [.0,1.]) st b is_>=_than { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } holds
(R (#) S) . [x,z] <<= b
proof
let b be Element of (RealPoset [.0,1.]); ::_thesis: ( b is_>=_than { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } implies (R (#) S) . [x,z] <<= b )
assume A3: b is_>=_than { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } ; ::_thesis: (R (#) S) . [x,z] <<= b
A4: rng (min (R,S,x,z)) c= [.0,1.] by RELAT_1:def_19;
A5: { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } = rng (min (R,S,x,z)) by Lm5;
for r being real number st r in rng (min (R,S,x,z)) holds
r <= b
proof
let r be real number ; ::_thesis: ( r in rng (min (R,S,x,z)) implies r <= b )
assume A6: r in rng (min (R,S,x,z)) ; ::_thesis: r <= b
then reconsider r = r as Element of (RealPoset [.0,1.]) by A4, LFUZZY_0:def_3;
r <<= b by A3, A5, A6, LATTICE3:def_9;
hence r <= b by LFUZZY_0:3; ::_thesis: verum
end;
then upper_bound (rng (min (R,S,x,z))) <= b by SEQ_4:144;
hence (R (#) S) . [x,z] <<= b by A1, LFUZZY_0:3; ::_thesis: verum
end;
for b being Element of (RealPoset [.0,1.]) st b in { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } holds
(R (#) S) . [x,z] >>= b
proof
let b be Element of (RealPoset [.0,1.]); ::_thesis: ( b in { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } implies (R (#) S) . [x,z] >>= b )
assume b in { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } ; ::_thesis: (R (#) S) . [x,z] >>= b
then consider y being Element of Y such that
A7: b = (R . [x,y]) "/\" (S . [y,z]) and
verum ;
( dom (min (R,S,x,z)) = Y & b = (min (R,S,x,z)) . y ) by A7, FUNCT_2:def_1, FUZZY_4:def_2;
then b <= upper_bound (rng (min (R,S,x,z))) by FUZZY_4:1;
hence (R (#) S) . [x,z] >>= b by A1, LFUZZY_0:3; ::_thesis: verum
end;
then (R (#) S) . [x,z] is_>=_than { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } by LATTICE3:def_9;
hence (R (#) S) . [x,z] = "\/" ( { ((R . [x,y]) "/\" (S . [y,z])) where y is Element of Y : verum } ,(RealPoset [.0,1.])) by A2, YELLOW_0:32; ::_thesis: verum
end;
Lm7: for X being non empty set
for R being RMembership_Func of X,X
for Q being Subset of (FuzzyLattice [:X,X:])
for x, z being Element of X holds { ("\/" ( { ((R . [x,y]) "/\" (r . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } = { ("\/" ( { ((R . [x,y]) "/\" ((@ r9) . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in Q }
proof
let X be non empty set ; ::_thesis: for R being RMembership_Func of X,X
for Q being Subset of (FuzzyLattice [:X,X:])
for x, z being Element of X holds { ("\/" ( { ((R . [x,y]) "/\" (r . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } = { ("\/" ( { ((R . [x,y]) "/\" ((@ r9) . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in Q }
let R be RMembership_Func of X,X; ::_thesis: for Q being Subset of (FuzzyLattice [:X,X:])
for x, z being Element of X holds { ("\/" ( { ((R . [x,y]) "/\" (r . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } = { ("\/" ( { ((R . [x,y]) "/\" ((@ r9) . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in Q }
let Q be Subset of (FuzzyLattice [:X,X:]); ::_thesis: for x, z being Element of X holds { ("\/" ( { ((R . [x,y]) "/\" (r . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } = { ("\/" ( { ((R . [x,y]) "/\" ((@ r9) . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in Q }
let x, z be Element of X; ::_thesis: { ("\/" ( { ((R . [x,y]) "/\" (r . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } = { ("\/" ( { ((R . [x,y]) "/\" ((@ r9) . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in Q }
set FL = FuzzyLattice [:X,X:];
defpred S1[ Element of (FuzzyLattice [:X,X:])] means $1 in Q;
deffunc H1( Element of (FuzzyLattice [:X,X:])) -> Element of the carrier of (RealPoset [.0,1.]) = "\/" ( { ((R . [x,y]) "/\" ($1 . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]));
deffunc H2( Element of (FuzzyLattice [:X,X:])) -> Element of the carrier of (RealPoset [.0,1.]) = "\/" ( { ((R . [x,y]) "/\" ((@ $1) . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]));
for r being Element of (FuzzyLattice [:X,X:]) st r in Q holds
"\/" ( { ((R . [x,y]) "/\" (r . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.])) = "\/" ( { ((R . [x,y]) "/\" ((@ r) . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))
proof
let r be Element of (FuzzyLattice [:X,X:]); ::_thesis: ( r in Q implies "\/" ( { ((R . [x,y]) "/\" (r . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.])) = "\/" ( { ((R . [x,y]) "/\" ((@ r) . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.])) )
assume r in Q ; ::_thesis: "\/" ( { ((R . [x,y]) "/\" (r . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.])) = "\/" ( { ((R . [x,y]) "/\" ((@ r) . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))
{ ((R . [x,y]) "/\" (r . [y,z])) where y is Element of X : verum } = { ((R . [x,y]) "/\" ((@ r) . [y,z])) where y is Element of X : verum }
proof
deffunc H3( Element of X) -> Element of the carrier of (RealPoset [.0,1.]) = (R . [x,$1]) "/\" ((@ r) . [$1,z]);
deffunc H4( Element of X) -> Element of the carrier of (RealPoset [.0,1.]) = (R . [x,$1]) "/\" (r . [$1,z]);
defpred S2[ Element of X] means verum;
A1: for y being Element of X holds H4(y) = H3(y) by LFUZZY_0:def_5;
thus { H4(y) where y is Element of X : S2[y] } = { H3(y) where y is Element of X : S2[y] } from FRAENKEL:sch_5(A1); ::_thesis: verum
end;
hence "\/" ( { ((R . [x,y]) "/\" (r . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.])) = "\/" ( { ((R . [x,y]) "/\" ((@ r) . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.])) ; ::_thesis: verum
end;
then A2: for r being Element of (FuzzyLattice [:X,X:]) st S1[r] holds
H1(r) = H2(r) ;
thus { H1(r) where r is Element of (FuzzyLattice [:X,X:]) : S1[r] } = { H2(r) where r is Element of (FuzzyLattice [:X,X:]) : S1[r] } from FRAENKEL:sch_6(A2); ::_thesis: verum
end;
Lm8: for X being non empty set
for R being RMembership_Func of X,X
for Q being Subset of (FuzzyLattice [:X,X:])
for x, z being Element of X holds { ("\/" ( { ((R . [x,y]) "/\" ((@ r) . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } = { ((R (#) (@ r)) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q }
proof
let X be non empty set ; ::_thesis: for R being RMembership_Func of X,X
for Q being Subset of (FuzzyLattice [:X,X:])
for x, z being Element of X holds { ("\/" ( { ((R . [x,y]) "/\" ((@ r) . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } = { ((R (#) (@ r)) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q }
let R be RMembership_Func of X,X; ::_thesis: for Q being Subset of (FuzzyLattice [:X,X:])
for x, z being Element of X holds { ("\/" ( { ((R . [x,y]) "/\" ((@ r) . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } = { ((R (#) (@ r)) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q }
let Q be Subset of (FuzzyLattice [:X,X:]); ::_thesis: for x, z being Element of X holds { ("\/" ( { ((R . [x,y]) "/\" ((@ r) . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } = { ((R (#) (@ r)) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q }
let x, z be Element of X; ::_thesis: { ("\/" ( { ((R . [x,y]) "/\" ((@ r) . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } = { ((R (#) (@ r)) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q }
set FL = FuzzyLattice [:X,X:];
defpred S1[ Element of (FuzzyLattice [:X,X:])] means $1 in Q;
deffunc H1( Element of (FuzzyLattice [:X,X:])) -> Element of the carrier of (RealPoset [.0,1.]) = "\/" ( { ((R . [x,y]) "/\" ((@ $1) . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]));
deffunc H2( Element of (FuzzyLattice [:X,X:])) -> Element of the carrier of (RealPoset [.0,1.]) = (R (#) (@ $1)) . [x,z];
A1: for r being Element of (FuzzyLattice [:X,X:]) st S1[r] holds
H1(r) = H2(r) by Lm6;
thus { H1(r) where r is Element of (FuzzyLattice [:X,X:]) : S1[r] } = { H2(r) where r is Element of (FuzzyLattice [:X,X:]) : S1[r] } from FRAENKEL:sch_6(A1); ::_thesis: verum
end;
Lm9: for X being non empty set
for R being RMembership_Func of X,X
for Q being Subset of (FuzzyLattice [:X,X:])
for x, z being Element of X holds { ((R (#) (@ r)) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } = pi ( { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z])
proof
let X be non empty set ; ::_thesis: for R being RMembership_Func of X,X
for Q being Subset of (FuzzyLattice [:X,X:])
for x, z being Element of X holds { ((R (#) (@ r)) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } = pi ( { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z])
let R be RMembership_Func of X,X; ::_thesis: for Q being Subset of (FuzzyLattice [:X,X:])
for x, z being Element of X holds { ((R (#) (@ r)) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } = pi ( { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z])
let Q be Subset of (FuzzyLattice [:X,X:]); ::_thesis: for x, z being Element of X holds { ((R (#) (@ r)) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } = pi ( { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z])
let x, z be Element of X; ::_thesis: { ((R (#) (@ r)) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } = pi ( { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z])
set FL = FuzzyLattice [:X,X:];
set A = { ((R (#) (@ r)) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ;
set B = pi ( { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]);
thus { ((R (#) (@ r)) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } c= pi ( { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]) :: according to XBOOLE_0:def_10 ::_thesis: pi ( { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]) c= { ((R (#) (@ r)) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { ((R (#) (@ r)) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } or a in pi ( { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]) )
assume a in { ((R (#) (@ r)) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ; ::_thesis: a in pi ( { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z])
then consider r being Element of (FuzzyLattice [:X,X:]) such that
A1: a = (R (#) (@ r)) . [x,z] and
A2: r in Q ;
R (#) (@ r) in { (R (#) (@ r9)) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in Q } by A2;
hence a in pi ( { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]) by A1, CARD_3:def_6; ::_thesis: verum
end;
thus pi ( { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]) c= { ((R (#) (@ r)) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ::_thesis: verum
proof
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in pi ( { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]) or b in { ((R (#) (@ r)) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } )
assume b in pi ( { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]) ; ::_thesis: b in { ((R (#) (@ r)) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q }
then consider f being Function such that
A3: f in { (R (#) (@ r9)) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in Q } and
A4: b = f . [x,z] by CARD_3:def_6;
ex r being Element of (FuzzyLattice [:X,X:]) st
( f = R (#) (@ r) & r in Q ) by A3;
hence b in { ((R (#) (@ r)) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } by A4; ::_thesis: verum
end;
end;
Lm10: for X being non empty set
for R being RMembership_Func of X,X
for Q being Subset of (FuzzyLattice [:X,X:])
for x, z being Element of X holds "\/" ( { ("\/" ( { ((R . [x,y]) "/\" (r . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0,1.]))) where y is Element of X : verum } ,(RealPoset [.0,1.])) = "\/" ( { ("\/" ( { ((R . [x,y]) "/\" (r9 . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in Q } ,(RealPoset [.0,1.]))
proof
let X be non empty set ; ::_thesis: for R being RMembership_Func of X,X
for Q being Subset of (FuzzyLattice [:X,X:])
for x, z being Element of X holds "\/" ( { ("\/" ( { ((R . [x,y]) "/\" (r . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0,1.]))) where y is Element of X : verum } ,(RealPoset [.0,1.])) = "\/" ( { ("\/" ( { ((R . [x,y]) "/\" (r9 . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in Q } ,(RealPoset [.0,1.]))
let R be RMembership_Func of X,X; ::_thesis: for Q being Subset of (FuzzyLattice [:X,X:])
for x, z being Element of X holds "\/" ( { ("\/" ( { ((R . [x,y]) "/\" (r . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0,1.]))) where y is Element of X : verum } ,(RealPoset [.0,1.])) = "\/" ( { ("\/" ( { ((R . [x,y]) "/\" (r9 . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in Q } ,(RealPoset [.0,1.]))
let Q be Subset of (FuzzyLattice [:X,X:]); ::_thesis: for x, z being Element of X holds "\/" ( { ("\/" ( { ((R . [x,y]) "/\" (r . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0,1.]))) where y is Element of X : verum } ,(RealPoset [.0,1.])) = "\/" ( { ("\/" ( { ((R . [x,y]) "/\" (r9 . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in Q } ,(RealPoset [.0,1.]))
let x, z be Element of X; ::_thesis: "\/" ( { ("\/" ( { ((R . [x,y]) "/\" (r . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0,1.]))) where y is Element of X : verum } ,(RealPoset [.0,1.])) = "\/" ( { ("\/" ( { ((R . [x,y]) "/\" (r9 . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in Q } ,(RealPoset [.0,1.]))
set FL = FuzzyLattice [:X,X:];
set RP = RealPoset [.0,1.];
defpred S1[ Element of X] means verum;
defpred S2[ Element of (FuzzyLattice [:X,X:])] means $1 in Q;
deffunc H1( Element of X, Element of (FuzzyLattice [:X,X:])) -> Element of the carrier of (RealPoset [.0,1.]) = (R . [x,$1]) "/\" ($2 . [$1,z]);
deffunc H2( Element of X, Element of (FuzzyLattice [:X,X:])) -> Element of the carrier of (RealPoset [.0,1.]) = (R . [x,$1]) "/\" ($2 . [$1,z]);
A1: for y being Element of X
for r being Element of (FuzzyLattice [:X,X:]) st S1[y] & S2[r] holds
H1(y,r) = H2(y,r) ;
thus "\/" ( { ("\/" ( { H1(y,r) where r is Element of (FuzzyLattice [:X,X:]) : S2[r] } ,(RealPoset [.0,1.]))) where y is Element of X : S1[y] } ,(RealPoset [.0,1.])) = "\/" ( { ("\/" ( { H2(y9,r9) where y9 is Element of X : S1[y9] } ,(RealPoset [.0,1.]))) where r9 is Element of (FuzzyLattice [:X,X:]) : S2[r9] } ,(RealPoset [.0,1.])) from LFUZZY_0:sch_5(A1); ::_thesis: verum
end;
theorem Th34: :: LFUZZY_1:34
for X being non empty set
for R being RMembership_Func of X,X
for Q being Subset of (FuzzyLattice [:X,X:]) holds R (#) (@ ("\/" (Q,(FuzzyLattice [:X,X:])))) = "\/" ( { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(FuzzyLattice [:X,X:]))
proof
let X be non empty set ; ::_thesis: for R being RMembership_Func of X,X
for Q being Subset of (FuzzyLattice [:X,X:]) holds R (#) (@ ("\/" (Q,(FuzzyLattice [:X,X:])))) = "\/" ( { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(FuzzyLattice [:X,X:]))
let R be RMembership_Func of X,X; ::_thesis: for Q being Subset of (FuzzyLattice [:X,X:]) holds R (#) (@ ("\/" (Q,(FuzzyLattice [:X,X:])))) = "\/" ( { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(FuzzyLattice [:X,X:]))
let Q be Subset of (FuzzyLattice [:X,X:]); ::_thesis: R (#) (@ ("\/" (Q,(FuzzyLattice [:X,X:])))) = "\/" ( { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(FuzzyLattice [:X,X:]))
set FL = FuzzyLattice [:X,X:];
set RP = RealPoset [.0,1.];
"\/" ( { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(FuzzyLattice [:X,X:])) = @ ("\/" ( { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(FuzzyLattice [:X,X:]))) by LFUZZY_0:def_5;
then reconsider F = "\/" ( { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(FuzzyLattice [:X,X:])) as RMembership_Func of X,X ;
for x, z being Element of X holds (R (#) (@ ("\/" (Q,(FuzzyLattice [:X,X:]))))) . (x,z) = F . (x,z)
proof
let x, z be Element of X; ::_thesis: (R (#) (@ ("\/" (Q,(FuzzyLattice [:X,X:]))))) . (x,z) = F . (x,z)
A1: { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } c= the carrier of (FuzzyLattice [:X,X:])
proof
let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } or t in the carrier of (FuzzyLattice [:X,X:]) )
assume t in { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ; ::_thesis: t in the carrier of (FuzzyLattice [:X,X:])
then consider r being Element of (FuzzyLattice [:X,X:]) such that
A2: t = R (#) (@ r) and
r in Q ;
([:X,X:],(R (#) (@ r))) @ = R (#) (@ r) by LFUZZY_0:def_6;
hence t in the carrier of (FuzzyLattice [:X,X:]) by A2; ::_thesis: verum
end;
thus (R (#) (@ ("\/" (Q,(FuzzyLattice [:X,X:]))))) . (x,z) = "\/" ( { ((R . (x,y)) "/\" ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . (y,z))) where y is Element of X : verum } ,(RealPoset [.0,1.])) by LFUZZY_0:22
.= "\/" ( { ((R . [x,y]) "/\" ("\/" ((pi (Q,[y,z])),(RealPoset [.0,1.])))) where y is Element of X : verum } ,(RealPoset [.0,1.])) by Lm2
.= "\/" ( { ("\/" ( { ((R . [x,y]) "/\" b) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[y,z]) } ,(RealPoset [.0,1.]))) where y is Element of X : verum } ,(RealPoset [.0,1.])) by Lm3
.= "\/" ( { ("\/" ( { ((R . [x,y]) "/\" (r . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0,1.]))) where y is Element of X : verum } ,(RealPoset [.0,1.])) by Lm4
.= "\/" ( { ("\/" ( { ((R . [x,y]) "/\" (r . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0,1.])) by Lm10
.= "\/" ( { ("\/" ( { ((R . [x,y]) "/\" ((@ r) . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0,1.])) by Lm7
.= "\/" ( { ((R (#) (@ r)) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0,1.])) by Lm8
.= "\/" ((pi ( { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z])),(RealPoset [.0,1.])) by Lm9
.= F . (x,z) by A1, Th32 ; ::_thesis: verum
end;
hence R (#) (@ ("\/" (Q,(FuzzyLattice [:X,X:])))) = "\/" ( { (R (#) (@ r)) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(FuzzyLattice [:X,X:])) by Th2; ::_thesis: verum
end;
theorem Th35: :: LFUZZY_1:35
for X being non empty set
for R being RMembership_Func of X,X
for Q being Subset of (FuzzyLattice [:X,X:]) holds (@ ("\/" (Q,(FuzzyLattice [:X,X:])))) (#) R = "\/" ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(FuzzyLattice [:X,X:]))
proof
let X be non empty set ; ::_thesis: for R being RMembership_Func of X,X
for Q being Subset of (FuzzyLattice [:X,X:]) holds (@ ("\/" (Q,(FuzzyLattice [:X,X:])))) (#) R = "\/" ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(FuzzyLattice [:X,X:]))
let R be RMembership_Func of X,X; ::_thesis: for Q being Subset of (FuzzyLattice [:X,X:]) holds (@ ("\/" (Q,(FuzzyLattice [:X,X:])))) (#) R = "\/" ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(FuzzyLattice [:X,X:]))
let Q be Subset of (FuzzyLattice [:X,X:]); ::_thesis: (@ ("\/" (Q,(FuzzyLattice [:X,X:])))) (#) R = "\/" ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(FuzzyLattice [:X,X:]))
set FL = FuzzyLattice [:X,X:];
set RP = RealPoset [.0,1.];
"\/" ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(FuzzyLattice [:X,X:])) = @ ("\/" ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(FuzzyLattice [:X,X:]))) by LFUZZY_0:def_5;
then reconsider F = "\/" ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(FuzzyLattice [:X,X:])) as RMembership_Func of X,X ;
for x, z being Element of X holds ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) (#) R) . (x,z) = F . (x,z)
proof
let x, z be Element of X; ::_thesis: ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) (#) R) . (x,z) = F . (x,z)
A1: { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } c= the carrier of (FuzzyLattice [:X,X:])
proof
let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } or t in the carrier of (FuzzyLattice [:X,X:]) )
assume t in { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ; ::_thesis: t in the carrier of (FuzzyLattice [:X,X:])
then consider r being Element of (FuzzyLattice [:X,X:]) such that
A2: t = (@ r) (#) R and
r in Q ;
([:X,X:],((@ r) (#) R)) @ = (@ r) (#) R by LFUZZY_0:def_6;
hence t in the carrier of (FuzzyLattice [:X,X:]) by A2; ::_thesis: verum
end;
A3: { (("\/" ((pi (Q,[x,y])),(RealPoset [.0,1.]))) "/\" (R . [y,z])) where y is Element of X : verum } = { ("\/" ( { (b "/\" (R . [y9,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y9]) } ,(RealPoset [.0,1.]))) where y9 is Element of X : verum }
proof
deffunc H1( Element of X) -> Element of the carrier of (RealPoset [.0,1.]) = "\/" ( { (b "/\" (R . [$1,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,$1]) } ,(RealPoset [.0,1.]));
deffunc H2( Element of X) -> Element of the carrier of (RealPoset [.0,1.]) = ("\/" ((pi (Q,[x,$1])),(RealPoset [.0,1.]))) "/\" (R . [$1,z]);
defpred S1[ Element of X] means verum;
for y being Element of X holds ("\/" ((pi (Q,[x,y])),(RealPoset [.0,1.]))) "/\" (R . [y,z]) = "\/" ( { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y]) } ,(RealPoset [.0,1.]))
proof
FuzzyLattice [:X,X:] = (RealPoset [.0,1.]) |^ [:X,X:] by LFUZZY_0:def_4
.= product ([:X,X:] --> (RealPoset [.0,1.])) by YELLOW_1:def_5 ;
then reconsider Q = Q as Subset of (product ([:X,X:] --> (RealPoset [.0,1.]))) ;
let y be Element of X; ::_thesis: ("\/" ((pi (Q,[x,y])),(RealPoset [.0,1.]))) "/\" (R . [y,z]) = "\/" ( { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y]) } ,(RealPoset [.0,1.]))
pi (Q,[x,y]) is Subset of (RealPoset [.0,1.]) by FUNCOP_1:7;
hence ("\/" ((pi (Q,[x,y])),(RealPoset [.0,1.]))) "/\" (R . [y,z]) = "\/" ( { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y]) } ,(RealPoset [.0,1.])) by LFUZZY_0:15; ::_thesis: verum
end;
then A4: for y being Element of X holds H2(y) = H1(y) ;
{ H2(y) where y is Element of X : S1[y] } = { H1(y9) where y9 is Element of X : S1[y9] } from FRAENKEL:sch_5(A4);
hence { (("\/" ((pi (Q,[x,y])),(RealPoset [.0,1.]))) "/\" (R . [y,z])) where y is Element of X : verum } = { ("\/" ( { (b "/\" (R . [y9,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y9]) } ,(RealPoset [.0,1.]))) where y9 is Element of X : verum } ; ::_thesis: verum
end;
A5: { ("\/" ( { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y]) } ,(RealPoset [.0,1.]))) where y is Element of X : verum } = { ("\/" ( { ((r . [x,y9]) "/\" (R . [y9,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0,1.]))) where y9 is Element of X : verum }
proof
deffunc H1( Element of X) -> Element of the carrier of (RealPoset [.0,1.]) = "\/" ( { ((r . [x,$1]) "/\" (R . [$1,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0,1.]));
deffunc H2( Element of X) -> Element of the carrier of (RealPoset [.0,1.]) = "\/" ( { (b "/\" (R . [$1,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,$1]) } ,(RealPoset [.0,1.]));
defpred S1[ Element of X] means verum;
for y being Element of X holds "\/" ( { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y]) } ,(RealPoset [.0,1.])) = "\/" ( { ((r . [x,y]) "/\" (R . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0,1.]))
proof
let y be Element of X; ::_thesis: "\/" ( { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y]) } ,(RealPoset [.0,1.])) = "\/" ( { ((r . [x,y]) "/\" (R . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0,1.]))
set A = { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y]) } ;
set B = { ((r . [x,y]) "/\" (R . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ;
A6: { ((r . [x,y]) "/\" (R . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } c= { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y]) }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { ((r . [x,y]) "/\" (R . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } or a in { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y]) } )
assume a in { ((r . [x,y]) "/\" (R . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ; ::_thesis: a in { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y]) }
then consider r being Element of (FuzzyLattice [:X,X:]) such that
A7: a = (r . [x,y]) "/\" (R . [y,z]) and
A8: r in Q ;
r . [x,y] in pi (Q,[x,y]) by A8, CARD_3:def_6;
hence a in { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y]) } by A7; ::_thesis: verum
end;
{ (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y]) } c= { ((r . [x,y]) "/\" (R . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y]) } or a in { ((r . [x,y]) "/\" (R . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } )
assume a in { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y]) } ; ::_thesis: a in { ((r . [x,y]) "/\" (R . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q }
then consider b being Element of (RealPoset [.0,1.]) such that
A9: a = b "/\" (R . [y,z]) and
A10: b in pi (Q,[x,y]) ;
ex f being Function st
( f in Q & b = f . [x,y] ) by A10, CARD_3:def_6;
hence a in { ((r . [x,y]) "/\" (R . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } by A9; ::_thesis: verum
end;
hence "\/" ( { (b "/\" (R . [y,z])) where b is Element of (RealPoset [.0,1.]) : b in pi (Q,[x,y]) } ,(RealPoset [.0,1.])) = "\/" ( { ((r . [x,y]) "/\" (R . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0,1.])) by A6, XBOOLE_0:def_10; ::_thesis: verum
end;
then A11: for y being Element of X holds H2(y) = H1(y) ;
thus { H2(y) where y is Element of X : S1[y] } = { H1(y) where y is Element of X : S1[y] } from FRAENKEL:sch_5(A11); ::_thesis: verum
end;
A12: "\/" ( { ("\/" ( { ((r . [x,y]) "/\" (R . [y,z])) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(RealPoset [.0,1.]))) where y is Element of X : verum } ,(RealPoset [.0,1.])) = "\/" ( { ("\/" ( { ((r9 . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in Q } ,(RealPoset [.0,1.]))
proof
deffunc H1( Element of X, Element of (FuzzyLattice [:X,X:])) -> Element of the carrier of (RealPoset [.0,1.]) = ($2 . [x,$1]) "/\" (R . [$1,z]);
deffunc H2( Element of X, Element of (FuzzyLattice [:X,X:])) -> Element of the carrier of (RealPoset [.0,1.]) = ($2 . [x,$1]) "/\" (R . [$1,z]);
defpred S1[ Element of (FuzzyLattice [:X,X:])] means $1 in Q;
defpred S2[ Element of X] means verum;
A13: for y being Element of X
for r being Element of (FuzzyLattice [:X,X:]) st S2[y] & S1[r] holds
H2(y,r) = H1(y,r) ;
thus "\/" ( { ("\/" ( { H2(y,r) where r is Element of (FuzzyLattice [:X,X:]) : S1[r] } ,(RealPoset [.0,1.]))) where y is Element of X : S2[y] } ,(RealPoset [.0,1.])) = "\/" ( { ("\/" ( { H1(y9,r9) where y9 is Element of X : S2[y9] } ,(RealPoset [.0,1.]))) where r9 is Element of (FuzzyLattice [:X,X:]) : S1[r9] } ,(RealPoset [.0,1.])) from LFUZZY_0:sch_5(A13); ::_thesis: verum
end;
A14: { ("\/" ( { ((r . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } = { ("\/" ( { (((@ r9) . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in Q }
proof
deffunc H1( Element of (FuzzyLattice [:X,X:])) -> Element of the carrier of (RealPoset [.0,1.]) = "\/" ( { (((@ $1) . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]));
deffunc H2( Element of (FuzzyLattice [:X,X:])) -> Element of the carrier of (RealPoset [.0,1.]) = "\/" ( { (($1 . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]));
defpred S1[ Element of (FuzzyLattice [:X,X:])] means $1 in Q;
for r being Element of (FuzzyLattice [:X,X:]) st r in Q holds
"\/" ( { ((r . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.])) = "\/" ( { (((@ r) . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))
proof
let r be Element of (FuzzyLattice [:X,X:]); ::_thesis: ( r in Q implies "\/" ( { ((r . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.])) = "\/" ( { (((@ r) . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.])) )
assume r in Q ; ::_thesis: "\/" ( { ((r . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.])) = "\/" ( { (((@ r) . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))
{ ((r . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } = { (((@ r) . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum }
proof
deffunc H3( Element of X) -> Element of the carrier of (RealPoset [.0,1.]) = ((@ r) . [x,$1]) "/\" (R . [$1,z]);
deffunc H4( Element of X) -> Element of the carrier of (RealPoset [.0,1.]) = (r . [x,$1]) "/\" (R . [$1,z]);
defpred S2[ Element of X] means verum;
A15: for y being Element of X holds H4(y) = H3(y) by LFUZZY_0:def_5;
thus { H4(y) where y is Element of X : S2[y] } = { H3(y) where y is Element of X : S2[y] } from FRAENKEL:sch_5(A15); ::_thesis: verum
end;
hence "\/" ( { ((r . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.])) = "\/" ( { (((@ r) . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.])) ; ::_thesis: verum
end;
then A16: for r being Element of (FuzzyLattice [:X,X:]) st S1[r] holds
H2(r) = H1(r) ;
thus { H2(r) where r is Element of (FuzzyLattice [:X,X:]) : S1[r] } = { H1(r) where r is Element of (FuzzyLattice [:X,X:]) : S1[r] } from FRAENKEL:sch_6(A16); ::_thesis: verum
end;
A17: { (((@ r) (#) R) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } = pi ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z])
proof
set A = { (((@ r) (#) R) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ;
set B = pi ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]);
thus { (((@ r) (#) R) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } c= pi ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]) :: according to XBOOLE_0:def_10 ::_thesis: pi ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]) c= { (((@ r) (#) R) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { (((@ r) (#) R) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } or a in pi ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]) )
assume a in { (((@ r) (#) R) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ; ::_thesis: a in pi ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z])
then consider r being Element of (FuzzyLattice [:X,X:]) such that
A18: a = ((@ r) (#) R) . [x,z] and
A19: r in Q ;
(@ r) (#) R in { ((@ r9) (#) R) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in Q } by A19;
hence a in pi ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]) by A18, CARD_3:def_6; ::_thesis: verum
end;
thus pi ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]) c= { (((@ r) (#) R) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ::_thesis: verum
proof
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in pi ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]) or b in { (((@ r) (#) R) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } )
assume b in pi ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,[x,z]) ; ::_thesis: b in { (((@ r) (#) R) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q }
then consider f being Function such that
A20: f in { ((@ r9) (#) R) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in Q } and
A21: b = f . [x,z] by CARD_3:def_6;
ex r being Element of (FuzzyLattice [:X,X:]) st
( f = (@ r) (#) R & r in Q ) by A20;
hence b in { (((@ r) (#) R) . [x,z]) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } by A21; ::_thesis: verum
end;
end;
A22: { (((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } = { (("\/" ((pi (Q,[x,y])),(RealPoset [.0,1.]))) "/\" (R . [y,z])) where y is Element of X : verum }
proof
deffunc H1( Element of X) -> Element of the carrier of (RealPoset [.0,1.]) = ("\/" ((pi (Q,[x,$1])),(RealPoset [.0,1.]))) "/\" (R . [$1,z]);
deffunc H2( Element of X) -> Element of the carrier of (RealPoset [.0,1.]) = ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . [x,$1]) "/\" (R . [$1,z]);
defpred S1[ Element of X] means verum;
for y being Element of X holds ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . [x,y]) "/\" (R . [y,z]) = ("\/" ((pi (Q,[x,y])),(RealPoset [.0,1.]))) "/\" (R . [y,z])
proof
let y be Element of X; ::_thesis: ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . [x,y]) "/\" (R . [y,z]) = ("\/" ((pi (Q,[x,y])),(RealPoset [.0,1.]))) "/\" (R . [y,z])
(@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . [x,y] = ("\/" (Q,(FuzzyLattice [:X,X:]))) . [x,y] by LFUZZY_0:def_5
.= "\/" ((pi (Q,[x,y])),(RealPoset [.0,1.])) by Th32 ;
hence ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . [x,y]) "/\" (R . [y,z]) = ("\/" ((pi (Q,[x,y])),(RealPoset [.0,1.]))) "/\" (R . [y,z]) ; ::_thesis: verum
end;
then A23: for y being Element of X holds H2(y) = H1(y) ;
thus { H2(y) where y is Element of X : S1[y] } = { H1(y9) where y9 is Element of X : S1[y9] } from FRAENKEL:sch_5(A23); ::_thesis: verum
end;
A24: { ("\/" ( { (((@ r) . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]))) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } = { (((@ r9) (#) R) . [x,z]) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in Q }
proof
deffunc H1( Element of (FuzzyLattice [:X,X:])) -> Element of the carrier of (RealPoset [.0,1.]) = ((@ $1) (#) R) . [x,z];
deffunc H2( Element of (FuzzyLattice [:X,X:])) -> Element of the carrier of (RealPoset [.0,1.]) = "\/" ( { (((@ $1) . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.]));
defpred S1[ Element of (FuzzyLattice [:X,X:])] means $1 in Q;
A25: for r being Element of (FuzzyLattice [:X,X:]) st S1[r] holds
H2(r) = H1(r) by Lm6;
thus { H2(r) where r is Element of (FuzzyLattice [:X,X:]) : S1[r] } = { H1(r) where r is Element of (FuzzyLattice [:X,X:]) : S1[r] } from FRAENKEL:sch_6(A25); ::_thesis: verum
end;
thus ((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) (#) R) . (x,z) = "\/" ( { (((@ ("\/" (Q,(FuzzyLattice [:X,X:])))) . [x,y]) "/\" (R . [y,z])) where y is Element of X : verum } ,(RealPoset [.0,1.])) by Lm6
.= F . (x,z) by A1, A22, A3, A5, A12, A14, A24, A17, Th32 ; ::_thesis: verum
end;
hence (@ ("\/" (Q,(FuzzyLattice [:X,X:])))) (#) R = "\/" ( { ((@ r) (#) R) where r is Element of (FuzzyLattice [:X,X:]) : r in Q } ,(FuzzyLattice [:X,X:])) by Th2; ::_thesis: verum
end;
theorem Th36: :: LFUZZY_1:36
for X being non empty set
for R being RMembership_Func of X,X holds (TrCl R) (#) (TrCl R) = "\/" ( { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } ,(FuzzyLattice [:X,X:]))
proof
let X be non empty set ; ::_thesis: for R being RMembership_Func of X,X holds (TrCl R) (#) (TrCl R) = "\/" ( { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } ,(FuzzyLattice [:X,X:]))
let R be RMembership_Func of X,X; ::_thesis: (TrCl R) (#) (TrCl R) = "\/" ( { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } ,(FuzzyLattice [:X,X:]))
set Q = { (n iter R) where n is Element of NAT : n > 0 } ;
set FL = FuzzyLattice [:X,X:];
A1: { (n iter R) where n is Element of NAT : n > 0 } c= the carrier of (FuzzyLattice [:X,X:])
proof
let q be set ; :: according to TARSKI:def_3 ::_thesis: ( not q in { (n iter R) where n is Element of NAT : n > 0 } or q in the carrier of (FuzzyLattice [:X,X:]) )
assume q in { (n iter R) where n is Element of NAT : n > 0 } ; ::_thesis: q in the carrier of (FuzzyLattice [:X,X:])
then consider i being Element of NAT such that
A2: q = i iter R and
i > 0 ;
([:X,X:],(i iter R)) @ = i iter R by LFUZZY_0:def_6;
hence q in the carrier of (FuzzyLattice [:X,X:]) by A2; ::_thesis: verum
end;
A3: { ("\/" ( { ((@ r) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]))) where r is Element of (FuzzyLattice [:X,X:]) : r in { (n iter R) where n is Element of NAT : n > 0 } } = { ("\/" ( { (([:X,X:],((@ r9) (#) (@ s9))) @) where s9 is Element of (FuzzyLattice [:X,X:]) : s9 in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in { (n iter R) where n is Element of NAT : n > 0 } }
proof
deffunc H1( Element of (FuzzyLattice [:X,X:])) -> Element of the carrier of (FuzzyLattice [:X,X:]) = "\/" ( { (([:X,X:],((@ $1) (#) (@ s))) @) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]));
deffunc H2( Element of (FuzzyLattice [:X,X:])) -> Element of the carrier of (FuzzyLattice [:X,X:]) = "\/" ( { ((@ $1) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]));
defpred S1[ Element of (FuzzyLattice [:X,X:])] means $1 in { (n iter R) where n is Element of NAT : n > 0 } ;
for r being Element of (FuzzyLattice [:X,X:]) holds "\/" ( { ((@ r) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:])) = "\/" ( { (([:X,X:],((@ r) (#) (@ s))) @) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]))
proof
let r be Element of (FuzzyLattice [:X,X:]); ::_thesis: "\/" ( { ((@ r) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:])) = "\/" ( { (([:X,X:],((@ r) (#) (@ s))) @) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]))
{ ((@ r) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } = { (([:X,X:],((@ r) (#) (@ s))) @) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } }
proof
deffunc H3( Element of (FuzzyLattice [:X,X:])) -> Element of the carrier of (FuzzyLattice [:X,X:]) = ([:X,X:],((@ r) (#) (@ $1))) @ ;
deffunc H4( Element of (FuzzyLattice [:X,X:])) -> Element of bool [:[:X,X:],REAL:] = (@ r) (#) (@ $1);
defpred S2[ Element of (FuzzyLattice [:X,X:])] means $1 in { (n iter R) where n is Element of NAT : n > 0 } ;
A4: for s being Element of (FuzzyLattice [:X,X:]) holds H4(s) = H3(s) by LFUZZY_0:def_6;
{ H4(s) where s is Element of (FuzzyLattice [:X,X:]) : S2[s] } = { H3(s) where s is Element of (FuzzyLattice [:X,X:]) : S2[s] } from FRAENKEL:sch_5(A4);
hence { ((@ r) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } = { (([:X,X:],((@ r) (#) (@ s))) @) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ; ::_thesis: verum
end;
hence "\/" ( { ((@ r) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:])) = "\/" ( { (([:X,X:],((@ r) (#) (@ s))) @) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:])) ; ::_thesis: verum
end;
then A5: for r being Element of (FuzzyLattice [:X,X:]) holds H2(r) = H1(r) ;
{ H2(r) where r is Element of (FuzzyLattice [:X,X:]) : S1[r] } = { H1(r) where r is Element of (FuzzyLattice [:X,X:]) : S1[r] } from FRAENKEL:sch_5(A5);
hence { ("\/" ( { ((@ r) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]))) where r is Element of (FuzzyLattice [:X,X:]) : r in { (n iter R) where n is Element of NAT : n > 0 } } = { ("\/" ( { (([:X,X:],((@ r9) (#) (@ s9))) @) where s9 is Element of (FuzzyLattice [:X,X:]) : s9 in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in { (n iter R) where n is Element of NAT : n > 0 } } ; ::_thesis: verum
end;
defpred S1[ Element of (FuzzyLattice [:X,X:])] means $1 in { (n iter R) where n is Element of NAT : n > 0 } ;
defpred S2[ Element of (FuzzyLattice [:X,X:])] means $1 in { (n iter R) where n is Element of NAT : n > 0 } ;
deffunc H1( Element of (FuzzyLattice [:X,X:]), Element of (FuzzyLattice [:X,X:])) -> Element of the carrier of (FuzzyLattice [:X,X:]) = ([:X,X:],((@ $1) (#) (@ $2))) @ ;
A6: { ((@ r) (#) (@ s)) where r, s is Element of (FuzzyLattice [:X,X:]) : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) } = { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) }
proof
set A = { ((@ r) (#) (@ s)) where r, s is Element of (FuzzyLattice [:X,X:]) : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) } ;
set B = { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } ;
thus { ((@ r) (#) (@ s)) where r, s is Element of (FuzzyLattice [:X,X:]) : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) } c= { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } :: according to XBOOLE_0:def_10 ::_thesis: { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } c= { ((@ r) (#) (@ s)) where r, s is Element of (FuzzyLattice [:X,X:]) : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { ((@ r) (#) (@ s)) where r, s is Element of (FuzzyLattice [:X,X:]) : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) } or a in { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } )
assume a in { ((@ r) (#) (@ s)) where r, s is Element of (FuzzyLattice [:X,X:]) : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) } ; ::_thesis: a in { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) }
then consider r, s being Element of (FuzzyLattice [:X,X:]) such that
A7: a = (@ r) (#) (@ s) and
A8: ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) ;
A9: ( r = @ r & s = @ s ) by LFUZZY_0:def_5;
( ex i being Element of NAT st
( r = i iter R & i > 0 ) & ex j being Element of NAT st
( s = j iter R & j > 0 ) ) by A8;
hence a in { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } by A7, A9; ::_thesis: verum
end;
thus { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } c= { ((@ r) (#) (@ s)) where r, s is Element of (FuzzyLattice [:X,X:]) : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) } ::_thesis: verum
proof
let b be set ; :: according to TARSKI:def_3 ::_thesis: ( not b in { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } or b in { ((@ r) (#) (@ s)) where r, s is Element of (FuzzyLattice [:X,X:]) : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) } )
assume b in { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } ; ::_thesis: b in { ((@ r) (#) (@ s)) where r, s is Element of (FuzzyLattice [:X,X:]) : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) }
then consider i, j being Element of NAT such that
A10: b = (i iter R) (#) (j iter R) and
A11: ( i > 0 & j > 0 ) ;
j iter R = ([:X,X:],(j iter R)) @ by LFUZZY_0:def_6;
then reconsider s = j iter R as Element of (FuzzyLattice [:X,X:]) ;
i iter R = ([:X,X:],(i iter R)) @ by LFUZZY_0:def_6;
then reconsider r = i iter R as Element of (FuzzyLattice [:X,X:]) ;
A12: ( @ r = r & @ s = s ) by LFUZZY_0:def_5;
( i iter R in { (n iter R) where n is Element of NAT : n > 0 } & j iter R in { (n iter R) where n is Element of NAT : n > 0 } ) by A11;
hence b in { ((@ r) (#) (@ s)) where r, s is Element of (FuzzyLattice [:X,X:]) : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) } by A10, A12; ::_thesis: verum
end;
end;
A13: { (([:X,X:],((@ r) (#) (@ s))) @) where r, s is Element of (FuzzyLattice [:X,X:]) : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) } = { ((@ r) (#) (@ s)) where r, s is Element of (FuzzyLattice [:X,X:]) : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) }
proof
deffunc H2( Element of (FuzzyLattice [:X,X:]), Element of (FuzzyLattice [:X,X:])) -> Element of bool [:[:X,X:],REAL:] = (@ $1) (#) (@ $2);
deffunc H3( Element of (FuzzyLattice [:X,X:]), Element of (FuzzyLattice [:X,X:])) -> Element of the carrier of (FuzzyLattice [:X,X:]) = ([:X,X:],((@ $1) (#) (@ $2))) @ ;
defpred S3[ Element of (FuzzyLattice [:X,X:]), Element of (FuzzyLattice [:X,X:])] means ( $1 in { (n iter R) where n is Element of NAT : n > 0 } & $2 in { (n iter R) where n is Element of NAT : n > 0 } );
A14: for r, s being Element of (FuzzyLattice [:X,X:]) holds H3(r,s) = H2(r,s) by LFUZZY_0:def_6;
{ H3(r,s) where r, s is Element of (FuzzyLattice [:X,X:]) : S3[r,s] } = { H2(r,s) where r, s is Element of (FuzzyLattice [:X,X:]) : S3[r,s] } from FRAENKEL:sch_7(A14);
hence { (([:X,X:],((@ r) (#) (@ s))) @) where r, s is Element of (FuzzyLattice [:X,X:]) : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) } = { ((@ r) (#) (@ s)) where r, s is Element of (FuzzyLattice [:X,X:]) : ( r in { (n iter R) where n is Element of NAT : n > 0 } & s in { (n iter R) where n is Element of NAT : n > 0 } ) } ; ::_thesis: verum
end;
A15: "\/" ( { (n iter R) where n is Element of NAT : n > 0 } ,(FuzzyLattice [:X,X:])) = @ ("\/" ( { (n iter R) where n is Element of NAT : n > 0 } ,(FuzzyLattice [:X,X:]))) by LFUZZY_0:def_5;
{ ((@ r) (#) (TrCl R)) where r is Element of (FuzzyLattice [:X,X:]) : r in { (n iter R) where n is Element of NAT : n > 0 } } = { ("\/" ( { ((@ r9) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in { (n iter R) where n is Element of NAT : n > 0 } }
proof
set A = { ((@ r) (#) (TrCl R)) where r is Element of (FuzzyLattice [:X,X:]) : r in { (n iter R) where n is Element of NAT : n > 0 } } ;
set B = { ("\/" ( { ((@ r9) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in { (n iter R) where n is Element of NAT : n > 0 } } ;
thus { ((@ r) (#) (TrCl R)) where r is Element of (FuzzyLattice [:X,X:]) : r in { (n iter R) where n is Element of NAT : n > 0 } } c= { ("\/" ( { ((@ r9) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in { (n iter R) where n is Element of NAT : n > 0 } } :: according to XBOOLE_0:def_10 ::_thesis: { ("\/" ( { ((@ r9) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in { (n iter R) where n is Element of NAT : n > 0 } } c= { ((@ r) (#) (TrCl R)) where r is Element of (FuzzyLattice [:X,X:]) : r in { (n iter R) where n is Element of NAT : n > 0 } }
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { ((@ r) (#) (TrCl R)) where r is Element of (FuzzyLattice [:X,X:]) : r in { (n iter R) where n is Element of NAT : n > 0 } } or a in { ("\/" ( { ((@ r9) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in { (n iter R) where n is Element of NAT : n > 0 } } )
assume a in { ((@ r) (#) (TrCl R)) where r is Element of (FuzzyLattice [:X,X:]) : r in { (n iter R) where n is Element of NAT : n > 0 } } ; ::_thesis: a in { ("\/" ( { ((@ r9) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in { (n iter R) where n is Element of NAT : n > 0 } }
then consider r being Element of (FuzzyLattice [:X,X:]) such that
A16: a = (@ r) (#) (TrCl R) and
A17: r in { (n iter R) where n is Element of NAT : n > 0 } ;
a = "\/" ( { ((@ r) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:])) by A15, A1, A16, Th34;
hence a in { ("\/" ( { ((@ r9) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in { (n iter R) where n is Element of NAT : n > 0 } } by A17; ::_thesis: verum
end;
thus { ("\/" ( { ((@ r9) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in { (n iter R) where n is Element of NAT : n > 0 } } c= { ((@ r) (#) (TrCl R)) where r is Element of (FuzzyLattice [:X,X:]) : r in { (n iter R) where n is Element of NAT : n > 0 } } ::_thesis: verum
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in { ("\/" ( { ((@ r9) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in { (n iter R) where n is Element of NAT : n > 0 } } or a in { ((@ r) (#) (TrCl R)) where r is Element of (FuzzyLattice [:X,X:]) : r in { (n iter R) where n is Element of NAT : n > 0 } } )
assume a in { ("\/" ( { ((@ r9) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:]))) where r9 is Element of (FuzzyLattice [:X,X:]) : r9 in { (n iter R) where n is Element of NAT : n > 0 } } ; ::_thesis: a in { ((@ r) (#) (TrCl R)) where r is Element of (FuzzyLattice [:X,X:]) : r in { (n iter R) where n is Element of NAT : n > 0 } }
then consider r being Element of (FuzzyLattice [:X,X:]) such that
A18: a = "\/" ( { ((@ r) (#) (@ s)) where s is Element of (FuzzyLattice [:X,X:]) : s in { (n iter R) where n is Element of NAT : n > 0 } } ,(FuzzyLattice [:X,X:])) and
A19: r in { (n iter R) where n is Element of NAT : n > 0 } ;
a = (@ r) (#) (TrCl R) by A15, A1, A18, Th34;
hence a in { ((@ r) (#) (TrCl R)) where r is Element of (FuzzyLattice [:X,X:]) : r in { (n iter R) where n is Element of NAT : n > 0 } } by A19; ::_thesis: verum
end;
end;
hence (TrCl R) (#) (TrCl R) = "\/" ( { ("\/" ( { H1(r,s) where s is Element of (FuzzyLattice [:X,X:]) : S1[s] } ,(FuzzyLattice [:X,X:]))) where r is Element of (FuzzyLattice [:X,X:]) : S2[r] } ,(FuzzyLattice [:X,X:])) by A15, A1, A3, Th35
.= "\/" ( { H1(r,s) where r, s is Element of (FuzzyLattice [:X,X:]) : ( S2[r] & S1[s] ) } ,(FuzzyLattice [:X,X:])) from LFUZZY_0:sch_1()
.= "\/" ( { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } ,(FuzzyLattice [:X,X:])) by A6, A13 ;
::_thesis: verum
end;
registration
let X be non empty set ;
let R be RMembership_Func of X,X;
cluster TrCl R -> transitive ;
coherence
TrCl R is transitive
proof
set FL = FuzzyLattice [:X,X:];
set RP = RealPoset [.0,1.];
set A = { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } ;
for c being Element of [:X,X:] holds ((TrCl R) (#) (TrCl R)) . c <= (TrCl R) . c
proof
let c be Element of [:X,X:]; ::_thesis: ((TrCl R) (#) (TrCl R)) . c <= (TrCl R) . c
A1: { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } c= the carrier of (FuzzyLattice [:X,X:])
proof
let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } or t in the carrier of (FuzzyLattice [:X,X:]) )
assume t in { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } ; ::_thesis: t in the carrier of (FuzzyLattice [:X,X:])
then consider i, j being Element of NAT such that
A2: t = (i iter R) (#) (j iter R) and
i > 0 and
j > 0 ;
([:X,X:],((i iter R) (#) (j iter R))) @ = (i iter R) (#) (j iter R) by LFUZZY_0:def_6;
hence t in the carrier of (FuzzyLattice [:X,X:]) by A2; ::_thesis: verum
end;
for b being Element of (RealPoset [.0,1.]) st b in pi ( { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } ,c) holds
b <<= (TrCl R) . c
proof
let b be Element of (RealPoset [.0,1.]); ::_thesis: ( b in pi ( { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } ,c) implies b <<= (TrCl R) . c )
assume b in pi ( { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } ,c) ; ::_thesis: b <<= (TrCl R) . c
then consider f being Function such that
A3: f in { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } and
A4: b = f . c by CARD_3:def_6;
consider i, j being Element of NAT such that
A5: f = (i iter R) (#) (j iter R) and
A6: i > 0 and
j > 0 by A3;
A7: f = (i + j) iter R by A5, Th27;
reconsider f = f as RMembership_Func of X,X by A5;
TrCl R c= by A6, A7, Th31;
then f . c <= (TrCl R) . c by FUZZY_1:def_2;
hence b <<= (TrCl R) . c by A4, LFUZZY_0:3; ::_thesis: verum
end;
then (TrCl R) . c is_>=_than pi ( { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } ,c) by LATTICE3:def_9;
then A8: "\/" ((pi ( { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } ,c)),(RealPoset [.0,1.])) <<= (TrCl R) . c by YELLOW_0:32;
((TrCl R) (#) (TrCl R)) . c = ("\/" ( { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } ,(FuzzyLattice [:X,X:]))) . c by Th36
.= "\/" ((pi ( { ((i iter R) (#) (j iter R)) where i, j is Element of NAT : ( i > 0 & j > 0 ) } ,c)),(RealPoset [.0,1.])) by A1, Th32 ;
hence ((TrCl R) (#) (TrCl R)) . c <= (TrCl R) . c by A8, LFUZZY_0:3; ::_thesis: verum
end;
then TrCl R c= by FUZZY_1:def_2;
hence TrCl R is transitive by Def6; ::_thesis: verum
end;
end;
theorem Th37: :: LFUZZY_1:37
for X being non empty set
for R being RMembership_Func of X,X
for n being Nat st R is transitive & n > 0 holds
R c=
proof
let X be non empty set ; ::_thesis: for R being RMembership_Func of X,X
for n being Nat st R is transitive & n > 0 holds
R c=
let R be RMembership_Func of X,X; ::_thesis: for n being Nat st R is transitive & n > 0 holds
R c=
let n be Nat; ::_thesis: ( R is transitive & n > 0 implies R c= )
assume that
A1: R is transitive and
A2: n > 0 ; ::_thesis: R c=
reconsider n = n as non empty Element of NAT by A2, ORDINAL1:def_12;
defpred S1[ Nat] means R c= ;
A3: R c= by A1, Def6;
A4: for k being non empty Nat st S1[k] holds
S1[k + 1]
proof
let k be non empty Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume S1[k] ; ::_thesis: S1[k + 1]
then R (#) R c= by Th6;
then R (#) R c= by Th26;
hence S1[k + 1] by A3, Th5; ::_thesis: verum
end;
A5: S1[1] by Th25;
for k being non empty Nat holds S1[k] from NAT_1:sch_10(A5, A4);
then S1[n] ;
hence R c= ; ::_thesis: verum
end;
theorem Th38: :: LFUZZY_1:38
for X being non empty set
for R being RMembership_Func of X,X st R is transitive holds
R = TrCl R
proof
let X be non empty set ; ::_thesis: for R being RMembership_Func of X,X st R is transitive holds
R = TrCl R
let R be RMembership_Func of X,X; ::_thesis: ( R is transitive implies R = TrCl R )
assume A1: R is transitive ; ::_thesis: R = TrCl R
for c being Element of [:X,X:] holds (TrCl R) . c <= R . c
proof
set Q = { (n iter R) where n is Element of NAT : n > 0 } ;
set RP = RealPoset [.0,1.];
let c be Element of [:X,X:]; ::_thesis: (TrCl R) . c <= R . c
for b being Element of (RealPoset [.0,1.]) st b in pi ( { (n iter R) where n is Element of NAT : n > 0 } ,c) holds
b <<= R . c
proof
let b be Element of (RealPoset [.0,1.]); ::_thesis: ( b in pi ( { (n iter R) where n is Element of NAT : n > 0 } ,c) implies b <<= R . c )
assume b in pi ( { (n iter R) where n is Element of NAT : n > 0 } ,c) ; ::_thesis: b <<= R . c
then consider f being Function such that
A2: f in { (n iter R) where n is Element of NAT : n > 0 } and
A3: b = f . c by CARD_3:def_6;
consider n being Element of NAT such that
A4: f = n iter R and
A5: n > 0 by A2;
R c= by A1, A5, Th37;
then (n iter R) . c <= R . c by FUZZY_1:def_2;
hence b <<= R . c by A3, A4, LFUZZY_0:3; ::_thesis: verum
end;
then A6: R . c is_>=_than pi ( { (n iter R) where n is Element of NAT : n > 0 } ,c) by LATTICE3:def_9;
{ (n iter R) where n is Element of NAT : n > 0 } c= the carrier of (FuzzyLattice [:X,X:])
proof
let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in { (n iter R) where n is Element of NAT : n > 0 } or t in the carrier of (FuzzyLattice [:X,X:]) )
assume t in { (n iter R) where n is Element of NAT : n > 0 } ; ::_thesis: t in the carrier of (FuzzyLattice [:X,X:])
then consider i being Element of NAT such that
A7: t = i iter R and
i > 0 ;
([:X,X:],(i iter R)) @ = i iter R by LFUZZY_0:def_6;
hence t in the carrier of (FuzzyLattice [:X,X:]) by A7; ::_thesis: verum
end;
then (TrCl R) . c = "\/" ((pi ( { (n iter R) where n is Element of NAT : n > 0 } ,c)),(RealPoset [.0,1.])) by Th32;
then (TrCl R) . c <<= R . c by A6, YELLOW_0:32;
hence (TrCl R) . c <= R . c by LFUZZY_0:3; ::_thesis: verum
end;
then A8: R c= by FUZZY_1:def_2;
TrCl R c= by Th30;
hence R = TrCl R by A8, Th3; ::_thesis: verum
end;
theorem Th39: :: LFUZZY_1:39
for X being non empty set
for R, S being RMembership_Func of X,X
for n being Nat st S c= holds
n iter S c=
proof
let X be non empty set ; ::_thesis: for R, S being RMembership_Func of X,X
for n being Nat st S c= holds
n iter S c=
let R, S be RMembership_Func of X,X; ::_thesis: for n being Nat st S c= holds
n iter S c=
let n be Nat; ::_thesis: ( S c= implies n iter S c= )
defpred S1[ Nat] means $1 iter S c= ;
assume A1: S c= ; ::_thesis: n iter S c=
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: S1[k] ; ::_thesis: S1[k + 1]
( (k iter R) (#) R = (k + 1) iter R & (k iter S) (#) S = (k + 1) iter S ) by Th26;
hence S1[k + 1] by A1, A3, Th6; ::_thesis: verum
end;
0 iter R = Imf (X,X) by Th24
.= 0 iter S by Th24 ;
then A4: S1[ 0 ] ;
for k being Nat holds S1[k] from NAT_1:sch_2(A4, A2);
hence n iter S c= ; ::_thesis: verum
end;
theorem :: LFUZZY_1:40
for X being non empty set
for R, S being RMembership_Func of X,X st S is transitive & S c= holds
S c=
proof
let X be non empty set ; ::_thesis: for R, S being RMembership_Func of X,X st S is transitive & S c= holds
S c=
let R, S be RMembership_Func of X,X; ::_thesis: ( S is transitive & S c= implies S c= )
assume that
A1: S is transitive and
A2: S c= ; ::_thesis: S c=
for c being Element of [:X,X:] holds (TrCl R) . c <= (TrCl S) . c
proof
set Q = { (n iter R) where n is Element of NAT : n > 0 } ;
set RP = RealPoset [.0,1.];
let c be Element of [:X,X:]; ::_thesis: (TrCl R) . c <= (TrCl S) . c
for b being Element of (RealPoset [.0,1.]) st b in pi ( { (n iter R) where n is Element of NAT : n > 0 } ,c) holds
b <<= (TrCl S) . c
proof
let b be Element of (RealPoset [.0,1.]); ::_thesis: ( b in pi ( { (n iter R) where n is Element of NAT : n > 0 } ,c) implies b <<= (TrCl S) . c )
assume b in pi ( { (n iter R) where n is Element of NAT : n > 0 } ,c) ; ::_thesis: b <<= (TrCl S) . c
then consider f being Function such that
A3: f in { (n iter R) where n is Element of NAT : n > 0 } and
A4: b = f . c by CARD_3:def_6;
consider n being Element of NAT such that
A5: f = n iter R and
A6: n > 0 by A3;
A7: TrCl S c= by A6, Th31;
n iter S c= by A2, Th39;
then TrCl S c= by A7, Th5;
then (n iter R) . c <= (TrCl S) . c by FUZZY_1:def_2;
hence b <<= (TrCl S) . c by A4, A5, LFUZZY_0:3; ::_thesis: verum
end;
then (TrCl S) . c is_>=_than pi ( { (n iter R) where n is Element of NAT : n > 0 } ,c) by LATTICE3:def_9;
then A8: "\/" ((pi ( { (n iter R) where n is Element of NAT : n > 0 } ,c)),(RealPoset [.0,1.])) <<= (TrCl S) . c by YELLOW_0:32;
{ (n iter R) where n is Element of NAT : n > 0 } c= the carrier of (FuzzyLattice [:X,X:])
proof
let t be set ; :: according to TARSKI:def_3 ::_thesis: ( not t in { (n iter R) where n is Element of NAT : n > 0 } or t in the carrier of (FuzzyLattice [:X,X:]) )
assume t in { (n iter R) where n is Element of NAT : n > 0 } ; ::_thesis: t in the carrier of (FuzzyLattice [:X,X:])
then consider i being Element of NAT such that
A9: t = i iter R and
i > 0 ;
([:X,X:],(i iter R)) @ = i iter R by LFUZZY_0:def_6;
hence t in the carrier of (FuzzyLattice [:X,X:]) by A9; ::_thesis: verum
end;
then (TrCl R) . c = "\/" ((pi ( { (n iter R) where n is Element of NAT : n > 0 } ,c)),(RealPoset [.0,1.])) by Th32;
hence (TrCl R) . c <= (TrCl S) . c by A8, LFUZZY_0:3; ::_thesis: verum
end;
then TrCl S c= by FUZZY_1:def_2;
hence S c= by A1, Th38; ::_thesis: verum
end;