set f = Yager_implication ;
ai: for x1, x2, y being Element of [.0,1.] st x1 <= x2 holds
Yager_implication . (x1,y) >= Yager_implication . (x2,y)

proof

let x1, x2, y be Element of [.0,1.]; :: thesis: ( x1 <= x2 implies Yager_implication . (x1,y) >= Yager_implication . (x2,y) )
JI: ( 0 <= x1 & 0 <= x2 ) by XXREAL_1:1;
ZZ: ( 0 <= y & y <= 1 ) by XXREAL_1:1;
assume Z0: x1 <= x2 ; :: thesis: Yager_implication . (x1,y) >= Yager_implication . (x2,y)

per cases ( ( x2 = 0 & y = 0 ) or ( x2 <> 0 & x1 = 0 & y = 0 ) or ( x2 <> 0 & x1 <> 0 & y = 0 ) or y <> 0 ) ;

suppose ( x2 = 0 & y = 0 ) ; :: thesis: Yager_implication . (x1,y) >= Yager_implication . (x2,y)

hence Yager_implication . (x1,y) >= Yager_implication . (x2,y) by JI, Z0; :: thesis: verum

end;

suppose ( x2 <> 0 & x1 = 0 & y = 0 ) ; :: thesis: Yager_implication . (x1,y) >= Yager_implication . (x2,y)

then Yager_implication . (x1,y) = 1 by Yager;
hence Yager_implication . (x1,y) >= Yager_implication . (x2,y) by XXREAL_1:1; :: thesis: verum

end;

suppose U6: ( x2 <> 0 & x1 <> 0 & y = 0 ) ; :: thesis: Yager_implication . (x1,y) >= Yager_implication . (x2,y)

then u6: ( x1 > 0 & x2 > 0 ) by XXREAL_1:1;
u2: Yager_implication . (x1,y) = y to_power x1 by Yager, U6, JI
.= 0 by u6, U6, POWER:def 2 ;
Yager_implication . (x2,y) = y to_power x2 by Yager, U6, JI
.= 0 by JI, U6, POWER:def 2 ;
hence Yager_implication . (x1,y) >= Yager_implication . (x2,y) by u2; :: thesis: verum

end;

suppose za: y <> 0 ; :: thesis: Yager_implication . (x1,y) >= Yager_implication . (x2,y)

then u2: Yager_implication . (x1,y) = y to_power x1 by ZZ, Yager;
U2: Yager_implication . (x2,y) = y to_power x2 by Yager, za, ZZ;

per cases ( ( x1 <> x2 & y <> 1 ) or ( x1 <> x2 & y = 1 ) or x1 = x2 ) ;

suppose zz: ( x1 <> x2 & y <> 1 ) ; :: thesis: Yager_implication . (x1,y) >= Yager_implication . (x2,y)

( 0 < y & y < 1 & x1 < x2 ) by zz, za, ZZ, Z0, XXREAL_0:1;
hence Yager_implication . (x1,y) >= Yager_implication . (x2,y) by U2, u2, POWER:40; :: thesis: verum

end;

suppose zz: ( x1 <> x2 & y = 1 ) ; :: thesis: Yager_implication . (x1,y) >= Yager_implication . (x2,y)

1 >= 1 to_power x2 by POWER:26;
hence Yager_implication . (x1,y) >= Yager_implication . (x2,y) by U2, u2, zz, POWER:26; :: thesis: verum

end;

suppose x1 = x2 ; :: thesis: Yager_implication . (x1,y) >= Yager_implication . (x2,y)

hence Yager_implication . (x1,y) >= Yager_implication . (x2,y) ; :: thesis: verum

end;

end;

end;

end;

end;

b0: for x, y1, y2 being Element of [.0,1.] st y1 <= y2 holds
Yager_implication . (x,y1) <= Yager_implication . (x,y2)

proof

let x, y1, y2 be Element of [.0,1.]; :: thesis: ( y1 <= y2 implies Yager_implication . (x,y1) <= Yager_implication . (x,y2) )
assume Z2: y1 <= y2 ; :: thesis: Yager_implication . (x,y1) <= Yager_implication . (x,y2)

per cases ( ( x = 0 & y2 = 0 ) or x <> 0 or y2 <> 0 ) ;

suppose P2: ( x = 0 & y2 = 0 ) ; :: thesis: Yager_implication . (x,y1) <= Yager_implication . (x,y2)

0 <= y1 by XXREAL_1:1;
hence Yager_implication . (x,y1) <= Yager_implication . (x,y2) by P2, Z2; :: thesis: verum

end;

suppose P8: x <> 0 ; :: thesis: Yager_implication . (x,y1) <= Yager_implication . (x,y2)

su: ( x >= 0 & y2 >= 0 ) by XXREAL_1:1;
then P4: Yager_implication . (x,y2) = y2 to_power x by Yager, P8;

per cases ( ( y1 = 0 & x = 0 ) or ( y1 = 0 & x <> 0 ) or y1 <> 0 ) ;

suppose ( y1 = 0 & x = 0 ) ; :: thesis: Yager_implication . (x,y1) <= Yager_implication . (x,y2)

hence Yager_implication . (x,y1) <= Yager_implication . (x,y2) by P8; :: thesis: verum

end;

suppose ( y1 = 0 & x <> 0 ) ; :: thesis: Yager_implication . (x,y1) <= Yager_implication . (x,y2)

then p4: Yager_implication . (x,y1) = y1 to_power x by Yager, su;
y1 >= 0 by XXREAL_1:1;
hence Yager_implication . (x,y1) <= Yager_implication . (x,y2) by p4, P4, HOLDER_1:3, Z2, su; :: thesis: verum

end;

suppose sy: y1 <> 0 ; :: thesis: Yager_implication . (x,y1) <= Yager_implication . (x,y2)

y1 >= 0 by XXREAL_1:1;
then p4: Yager_implication . (x,y1) = y1 to_power x by Yager, sy;
y1 >= 0 by XXREAL_1:1;
hence Yager_implication . (x,y1) <= Yager_implication . (x,y2) by p4, P4, HOLDER_1:3, Z2, su; :: thesis: verum

end;

end;

end;

suppose P8: y2 <> 0 ; :: thesis: Yager_implication . (x,y1) <= Yager_implication . (x,y2)

su: ( x >= 0 & y2 >= 0 ) by XXREAL_1:1;
then P4: Yager_implication . (x,y2) = y2 to_power x by Yager, P8;

per cases ( ( y1 = 0 & x = 0 ) or ( y1 = 0 & x <> 0 ) or y1 <> 0 ) ;

suppose pg: ( y1 = 0 & x = 0 ) ; :: thesis: Yager_implication . (x,y1) <= Yager_implication . (x,y2)

then Yager_implication . (x,y1) = 1 by Yager;
hence Yager_implication . (x,y1) <= Yager_implication . (x,y2) by P4, POWER:24, pg; :: thesis: verum

end;

suppose ( y1 = 0 & x <> 0 ) ; :: thesis: Yager_implication . (x,y1) <= Yager_implication . (x,y2)

then p4: Yager_implication . (x,y1) = y1 to_power x by Yager, su;
y1 >= 0 by XXREAL_1:1;
hence Yager_implication . (x,y1) <= Yager_implication . (x,y2) by p4, P4, HOLDER_1:3, Z2, su; :: thesis: verum

end;

suppose sy: y1 <> 0 ; :: thesis: Yager_implication . (x,y1) <= Yager_implication . (x,y2)

y1 >= 0 by XXREAL_1:1;
then p4: Yager_implication . (x,y1) = y1 to_power x by Yager, sy;
y1 >= 0 by XXREAL_1:1;
hence Yager_implication . (x,y1) <= Yager_implication . (x,y2) by p4, P4, HOLDER_1:3, Z2, su; :: thesis: verum

end;

end;

end;

end;

end;

AA: ( 0 in [.0,1.] & 1 in [.0,1.] ) by XXREAL_1:1;
A2: Yager_implication . (1,1) = 1 to_power 1 by AA, Yager
.= 1 by POWER:26 ;
Yager_implication . (1,0) = 0 to_power 1 by AA, Yager
.= 0 by POWER:def 2 ;
hence ( Yager_implication is decreasing_on_1st & Yager_implication is increasing_on_2nd & Yager_implication is 00-dominant & Yager_implication is 11-dominant & Yager_implication is 10-weak ) by AA, A2, ai, b0, Yager; :: thesis: verum