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 object ; :: 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 object ; :: 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 object ; :: 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]);
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
H1(y,r) = H1(y,r) ;
thus "\/" ( { ("\/" ( { H1(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 object ; :: 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 object ; :: 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