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)
per cases ( 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;
suppose A1: 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]
per cases ( x = z or not x = z ) ;
suppose A2: 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
per cases ( x = y or not x = y ) ;
suppose A3: 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;
suppose A4: 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;
suppose A5: 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
per cases ( x = y or x <> y ) ;
suppose A6: 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;
suppose A7: 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
per cases ( y = z or y <> z ) ;
suppose A8: 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;
suppose A9: 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 ; :: 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