let D be non empty set ; :: thesis: for p, q being PartialPredicate of D holds dom (PP_imp (p,q)) = { d where d is Element of D : ( ( d in dom p & p . d = FALSE ) or ( d in dom q & q . d = TRUE ) or ( d in dom p & p . d = TRUE & d in dom q & q . d = FALSE ) ) }
let p, q be PartialPredicate of D; :: thesis: dom (PP_imp (p,q)) = { d where d is Element of D : ( ( d in dom p & p . d = FALSE ) or ( d in dom q & q . d = TRUE ) or ( d in dom p & p . d = TRUE & d in dom q & q . d = FALSE ) ) }
set F = PP_imp (p,q);
set P = PP_not p;
set Dimp = { d1 where d1 is Element of D : ( ( d1 in dom p & p . d1 = FALSE ) or ( d1 in dom q & q . d1 = TRUE ) or ( d1 in dom p & p . d1 = TRUE & d1 in dom q & q . d1 = FALSE ) ) } ;
A1: dom (PP_imp (p,q)) = { d where d is Element of D : ( ( d in dom (PP_not p) & (PP_not p) . d = TRUE ) or ( d in dom q & q . d = TRUE ) or ( d in dom (PP_not p) & (PP_not p) . d = FALSE & d in dom q & q . d = FALSE ) ) } by Def4;
A2: dom (PP_not p) = dom p by Def2;
thus dom (PP_imp (p,q)) c= { d1 where d1 is Element of D : ( ( d1 in dom p & p . d1 = FALSE ) or ( d1 in dom q & q . d1 = TRUE ) or ( d1 in dom p & p . d1 = TRUE & d1 in dom q & q . d1 = FALSE ) ) } :: according to XBOOLE_0:def 10 :: thesis: { d where d is Element of D : ( ( d in dom p & p . d = FALSE ) or ( d in dom q & q . d = TRUE ) or ( d in dom p & p . d = TRUE & d in dom q & q . d = FALSE ) ) } c= dom (PP_imp (p,q))

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (PP_imp (p,q)) or x in { d1 where d1 is Element of D : ( ( d1 in dom p & p . d1 = FALSE ) or ( d1 in dom q & q . d1 = TRUE ) or ( d1 in dom p & p . d1 = TRUE & d1 in dom q & q . d1 = FALSE ) ) } )
assume x in dom (PP_imp (p,q)) ; :: thesis: x in { d1 where d1 is Element of D : ( ( d1 in dom p & p . d1 = FALSE ) or ( d1 in dom q & q . d1 = TRUE ) or ( d1 in dom p & p . d1 = TRUE & d1 in dom q & q . d1 = FALSE ) ) }
then consider d being Element of D such that
A3: x = d and
A4: ( ( d in dom (PP_not p) & (PP_not p) . d = TRUE ) or ( d in dom q & q . d = TRUE ) or ( d in dom (PP_not p) & (PP_not p) . d = FALSE & d in dom q & q . d = FALSE ) ) by A1;

per cases ( ( d in dom (PP_not p) & (PP_not p) . d = TRUE ) or ( d in dom q & q . d = TRUE ) or ( d in dom (PP_not p) & d in dom q & (PP_not p) . d = FALSE & q . d = FALSE ) ) by A4;

suppose that A5: d in dom (PP_not p) and
A6: (PP_not p) . d = TRUE ; :: thesis: x in { d1 where d1 is Element of D : ( ( d1 in dom p & p . d1 = FALSE ) or ( d1 in dom q & q . d1 = TRUE ) or ( d1 in dom p & p . d1 = TRUE & d1 in dom q & q . d1 = FALSE ) ) }

p . d = FALSE by A2, A5, A6, Th5;
hence x in { d1 where d1 is Element of D : ( ( d1 in dom p & p . d1 = FALSE ) or ( d1 in dom q & q . d1 = TRUE ) or ( d1 in dom p & p . d1 = TRUE & d1 in dom q & q . d1 = FALSE ) ) } by A2, A3, A5; :: thesis: verum

end;

suppose ( d in dom q & q . d = TRUE ) ; :: thesis: x in { d1 where d1 is Element of D : ( ( d1 in dom p & p . d1 = FALSE ) or ( d1 in dom q & q . d1 = TRUE ) or ( d1 in dom p & p . d1 = TRUE & d1 in dom q & q . d1 = FALSE ) ) }

hence x in { d1 where d1 is Element of D : ( ( d1 in dom p & p . d1 = FALSE ) or ( d1 in dom q & q . d1 = TRUE ) or ( d1 in dom p & p . d1 = TRUE & d1 in dom q & q . d1 = FALSE ) ) } by A3; :: thesis: verum

end;

suppose that A7: ( d in dom (PP_not p) & d in dom q ) and
A8: (PP_not p) . d = FALSE and
A9: q . d = FALSE ; :: thesis: x in { d1 where d1 is Element of D : ( ( d1 in dom p & p . d1 = FALSE ) or ( d1 in dom q & q . d1 = TRUE ) or ( d1 in dom p & p . d1 = TRUE & d1 in dom q & q . d1 = FALSE ) ) }

p . d = TRUE by A2, A7, A8, Th4;
hence x in { d1 where d1 is Element of D : ( ( d1 in dom p & p . d1 = FALSE ) or ( d1 in dom q & q . d1 = TRUE ) or ( d1 in dom p & p . d1 = TRUE & d1 in dom q & q . d1 = FALSE ) ) } by A2, A3, A7, A9; :: thesis: verum

end;

end;

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { d where d is Element of D : ( ( d in dom p & p . d = FALSE ) or ( d in dom q & q . d = TRUE ) or ( d in dom p & p . d = TRUE & d in dom q & q . d = FALSE ) ) } or x in dom (PP_imp (p,q)) )
assume x in { d1 where d1 is Element of D : ( ( d1 in dom p & p . d1 = FALSE ) or ( d1 in dom q & q . d1 = TRUE ) or ( d1 in dom p & p . d1 = TRUE & d1 in dom q & q . d1 = FALSE ) ) } ; :: thesis: x in dom (PP_imp (p,q))
then consider d being Element of D such that
A10: x = d and
A11: ( ( d in dom p & p . d = FALSE ) or ( d in dom q & q . d = TRUE ) or ( d in dom p & p . d = TRUE & d in dom q & q . d = FALSE ) ) ;

per cases ( ( d in dom p & p . d = FALSE ) or ( d in dom q & q . d = TRUE ) or ( d in dom p & d in dom q & p . d = TRUE & q . d = FALSE ) ) by A11;

suppose that A12: d in dom p and
A13: p . d = FALSE ; :: thesis: x in dom (PP_imp (p,q))

(PP_not p) . d = TRUE by A12, A13, Def2;
hence x in dom (PP_imp (p,q)) by A1, A2, A10, A12; :: thesis: verum

end;

suppose ( d in dom q & q . d = TRUE ) ; :: thesis: x in dom (PP_imp (p,q))

hence x in dom (PP_imp (p,q)) by A1, A10; :: thesis: verum

end;

suppose that A14: d in dom p and
A15: d in dom q and
A16: p . d = TRUE and
A17: q . d = FALSE ; :: thesis: x in dom (PP_imp (p,q))

(PP_not p) . d = FALSE by A14, A16, Def2;
hence x in dom (PP_imp (p,q)) by A1, A2, A10, A14, A15, A17; :: thesis: verum

end;

end;