let Y be non empty set ; :: thesis: for a, b being Function of Y,BOOLEAN holds
( a 'eqv' b = I_el Y iff a = b )
let a, b be Function of Y,BOOLEAN; :: thesis: ( a 'eqv' b = I_el Y iff a = b )
A1: for a, b being Function of Y,BOOLEAN st a 'eqv' b = I_el Y holds
a = b
proof
let a, b be Function of Y,BOOLEAN; :: thesis: ( a 'eqv' b = I_el Y implies a = b )
assume A2: a 'eqv' b = I_el Y ; :: thesis: a = b
A3: for x being Element of Y holds (('not' (a . x)) '&' (b . x)) 'or' ((a . x) '&' ('not' (b . x))) = FALSE
proof
let x be Element of Y; :: thesis: (('not' (a . x)) '&' (b . x)) 'or' ((a . x) '&' ('not' (b . x))) = FALSE
(a 'eqv' b) . x = 'not' ((a . x) 'xor' (b . x)) by Def9;
then 'not' ((a . x) 'xor' (b . x)) = TRUE by A2, Def11;
hence (('not' (a . x)) '&' (b . x)) 'or' ((a . x) '&' ('not' (b . x))) = FALSE ; :: thesis: verum
end;
A4: for x being Element of Y holds
( ('not' (a . x)) '&' (b . x) = FALSE & (a . x) '&' ('not' (b . x)) = FALSE )
proof
let x be Element of Y; :: thesis: ( ('not' (a . x)) '&' (b . x) = FALSE & (a . x) '&' ('not' (b . x)) = FALSE )
A5: ( (a . x) '&' ('not' (b . x)) = TRUE or (a . x) '&' ('not' (b . x)) = FALSE ) by XBOOLEAN:def 3;
(('not' (a . x)) '&' (b . x)) 'or' ((a . x) '&' ('not' (b . x))) = FALSE by A3;
hence ( ('not' (a . x)) '&' (b . x) = FALSE & (a . x) '&' ('not' (b . x)) = FALSE ) by A5; :: thesis: verum
end;
let x be Element of Y; :: according to FUNCT_2:def 8 :: thesis: a . x = b . x
('not' (a . x)) '&' (b . x) = FALSE by A4;
then A6: ( ( 'not' (a . x) = TRUE & b . x = FALSE ) or ( 'not' (a . x) = FALSE & b . x = FALSE ) or ( 'not' (a . x) = FALSE & b . x = TRUE ) ) by MARGREL1:12, XBOOLEAN:def 3;
(a . x) '&' ('not' (b . x)) = FALSE by A4;
hence a . x = b . x by A6; :: thesis: verum
end;
for a, b being Function of Y,BOOLEAN st a = b holds
a 'eqv' b = I_el Y
proof
let a, b be Function of Y,BOOLEAN; :: thesis: ( a = b implies a 'eqv' b = I_el Y )
assume A7: a = b ; :: thesis: a 'eqv' b = I_el Y
A8: for x being Element of Y holds
( ('not' (a . x)) '&' (b . x) = FALSE & (a . x) '&' ('not' (b . x)) = FALSE )
proof
let x be Element of Y; :: thesis: ( ('not' (a . x)) '&' (b . x) = FALSE & (a . x) '&' ('not' (b . x)) = FALSE )
( b . x = TRUE iff 'not' (b . x) = FALSE ) ;
then ( ( a . x = FALSE & 'not' (b . x) = TRUE ) or ( a . x = TRUE & 'not' (b . x) = FALSE ) ) by A7, XBOOLEAN:def 3;
hence ( ('not' (a . x)) '&' (b . x) = FALSE & (a . x) '&' ('not' (b . x)) = FALSE ) ; :: thesis: verum
end;
let x be Element of Y; :: according to FUNCT_2:def 8 :: thesis: (a 'eqv' b) . x = (I_el Y) . x
(a . x) '&' ('not' (b . x)) = FALSE by A8;
then 'not' ((a . x) 'xor' (b . x)) = TRUE by A8;
then (a 'eqv' b) . x = TRUE by Def9;
hence (a 'eqv' b) . x = (I_el Y) . x by Def11; :: thesis: verum
end;
hence ( a 'eqv' b = I_el Y iff a = b ) by A1; :: thesis: verum