let D be non empty set ; :: thesis: for p, q being PartialPredicate of D holds PP_or ((PP_and (p,q)),q) = q
let p, q be PartialPredicate of D; :: thesis: PP_or ((PP_and (p,q)),q) = q
set a = PP_and (p,q);
set o = PP_or ((PP_and (p,q)),q);
A1: dom (PP_and (p,q)) = { d where d is Element of D : ( ( d in dom p & p . d = FALSE ) or ( d in dom q & q . d = FALSE ) or ( d in dom p & p . d = TRUE & d in dom q & q . d = TRUE ) ) } by Th16;
A2: dom (PP_or ((PP_and (p,q)),q)) = { d where d is Element of D : ( ( d in dom (PP_and (p,q)) & (PP_and (p,q)) . d = TRUE ) or ( d in dom q & q . d = TRUE ) or ( d in dom (PP_and (p,q)) & (PP_and (p,q)) . d = FALSE & d in dom q & q . d = FALSE ) ) } by Def4;
thus dom (PP_or ((PP_and (p,q)),q)) = dom q :: according to FUNCT_1:def 11 :: thesis: for b1 being object holds
( not b1 in dom (PP_or ((PP_and (p,q)),q)) or (PP_or ((PP_and (p,q)),q)) . b1 = q . b1 )
proof
thus dom (PP_or ((PP_and (p,q)),q)) c= dom q :: according to XBOOLE_0:def 10 :: thesis: dom q c= dom (PP_or ((PP_and (p,q)),q))
proof
let d be object ; :: according to TARSKI:def 3 :: thesis: ( not d in dom (PP_or ((PP_and (p,q)),q)) or d in dom q )
assume d in dom (PP_or ((PP_and (p,q)),q)) ; :: thesis: d in dom q
per cases then ( ( d in dom (PP_and (p,q)) & (PP_and (p,q)) . d = TRUE ) or ( d in dom q & q . d = TRUE ) or ( d in dom (PP_and (p,q)) & (PP_and (p,q)) . d = FALSE & d in dom q & q . d = FALSE ) ) by Th8;
suppose that A3: d in dom (PP_and (p,q)) and
A4: (PP_and (p,q)) . d = TRUE ; :: thesis: d in dom q
per cases ( ( d in dom p & p . d = FALSE ) or ( d in dom q & q . d = FALSE ) or ( d in dom p & p . d = TRUE & d in dom q & q . d = TRUE ) ) by A3, Th17;
suppose ( d in dom p & p . d = FALSE ) ; :: thesis: d in dom q
hence d in dom q by A4, Th19; :: thesis: verum
end;
suppose ( ( d in dom q & q . d = FALSE ) or ( d in dom p & p . d = TRUE & d in dom q & q . d = TRUE ) ) ; :: thesis: d in dom q
hence d in dom q ; :: thesis: verum
end;
end;
end;
suppose ( ( d in dom q & q . d = TRUE ) or ( d in dom (PP_and (p,q)) & (PP_and (p,q)) . d = FALSE & d in dom q & q . d = FALSE ) ) ; :: thesis: d in dom q
hence d in dom q ; :: thesis: verum
end;
end;
end;
let d be object ; :: according to TARSKI:def 3 :: thesis: ( not d in dom q or d in dom (PP_or ((PP_and (p,q)),q)) )
assume A5: d in dom q ; :: thesis: d in dom (PP_or ((PP_and (p,q)),q))
per cases then ( q . d = FALSE or q . d = TRUE ) by Th3;
suppose A6: q . d = FALSE ; :: thesis: d in dom (PP_or ((PP_and (p,q)),q))
then A7: (PP_and (p,q)) . d = FALSE by A5, Th19;
d in dom (PP_and (p,q)) by A1, A5, A6;
hence d in dom (PP_or ((PP_and (p,q)),q)) by A2, A5, A6, A7; :: thesis: verum
end;
suppose q . d = TRUE ; :: thesis: d in dom (PP_or ((PP_and (p,q)),q))
hence d in dom (PP_or ((PP_and (p,q)),q)) by A2, A5; :: thesis: verum
end;
end;
end;
let d be object ; :: thesis: ( not d in dom (PP_or ((PP_and (p,q)),q)) or (PP_or ((PP_and (p,q)),q)) . d = q . d )
assume d in dom (PP_or ((PP_and (p,q)),q)) ; :: thesis: (PP_or ((PP_and (p,q)),q)) . d = q . d
per cases then ( ( d in dom (PP_and (p,q)) & (PP_and (p,q)) . d = TRUE ) or ( d in dom q & q . d = TRUE ) or ( d in dom (PP_and (p,q)) & (PP_and (p,q)) . d = FALSE & d in dom q & q . d = FALSE ) ) by Th8;
suppose that A8: d in dom (PP_and (p,q)) and
A9: (PP_and (p,q)) . d = TRUE ; :: thesis: (PP_or ((PP_and (p,q)),q)) . d = q . d
per cases ( ( d in dom p & p . d = FALSE ) or ( d in dom q & q . d = FALSE ) or ( d in dom p & p . d = TRUE & d in dom q & q . d = TRUE ) ) by A8, Th17;
suppose ( d in dom p & p . d = FALSE ) ; :: thesis: (PP_or ((PP_and (p,q)),q)) . d = q . d
hence (PP_or ((PP_and (p,q)),q)) . d = q . d by A9, Th19; :: thesis: verum
end;
suppose ( d in dom q & q . d = FALSE ) ; :: thesis: (PP_or ((PP_and (p,q)),q)) . d = q . d
hence (PP_or ((PP_and (p,q)),q)) . d = q . d by A9, Th19; :: thesis: verum
end;
suppose ( d in dom p & p . d = TRUE & d in dom q & q . d = TRUE ) ; :: thesis: (PP_or ((PP_and (p,q)),q)) . d = q . d
hence (PP_or ((PP_and (p,q)),q)) . d = q . d by Def4; :: thesis: verum
end;
end;
end;
suppose ( d in dom q & q . d = TRUE ) ; :: thesis: (PP_or ((PP_and (p,q)),q)) . d = q . d
hence (PP_or ((PP_and (p,q)),q)) . d = q . d by Def4; :: thesis: verum
end;
suppose ( d in dom (PP_and (p,q)) & (PP_and (p,q)) . d = FALSE & d in dom q & q . d = FALSE ) ; :: thesis: (PP_or ((PP_and (p,q)),q)) . d = q . d
hence (PP_or ((PP_and (p,q)),q)) . d = q . d by Def4; :: thesis: verum
end;
end;