let D be non empty set ; :: thesis: for p, q being PartialPredicate of D holds PP_or (((PP_False D) | (dom p)),((PP_True D) | (dom q))) = (PP_True D) | (dom q)
let p, q be PartialPredicate of D; :: thesis: PP_or (((PP_False D) | (dom p)),((PP_True D) | (dom q))) = (PP_True D) | (dom q)
set F = PP_False D;
set T = PP_True D;
set f = (PP_False D) | (dom p);
set g = (PP_True D) | (dom q);
set o = PP_or (((PP_False D) | (dom p)),((PP_True D) | (dom q)));
A1: dom (PP_or (((PP_False D) | (dom p)),((PP_True D) | (dom q)))) = { d where d is Element of D : ( ( d in dom ((PP_False D) | (dom p)) & ((PP_False D) | (dom p)) . d = TRUE ) or ( d in dom ((PP_True D) | (dom q)) & ((PP_True D) | (dom q)) . d = TRUE ) or ( d in dom ((PP_False D) | (dom p)) & ((PP_False D) | (dom p)) . d = FALSE & d in dom ((PP_True D) | (dom q)) & ((PP_True D) | (dom q)) . d = FALSE ) ) } by Def4;
dom (PP_True D) = D ;
then A2: dom ((PP_True D) | (dom q)) = dom q by RELAT_1:62;
thus dom (PP_or (((PP_False D) | (dom p)),((PP_True D) | (dom q)))) = dom ((PP_True D) | (dom q)) :: according to FUNCT_1:def 11 :: thesis: for b1 being object holds
( not b1 in dom (PP_or (((PP_False D) | (dom p)),((PP_True D) | (dom q)))) or (PP_or (((PP_False D) | (dom p)),((PP_True D) | (dom q)))) . b1 = ((PP_True D) | (dom q)) . b1 )
proof
thus dom (PP_or (((PP_False D) | (dom p)),((PP_True D) | (dom q)))) c= dom ((PP_True D) | (dom q)) :: according to XBOOLE_0:def 10 :: thesis: dom ((PP_True D) | (dom q)) c= dom (PP_or (((PP_False D) | (dom p)),((PP_True D) | (dom q))))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (PP_or (((PP_False D) | (dom p)),((PP_True D) | (dom q)))) or x in dom ((PP_True D) | (dom q)) )
assume A3: x in dom (PP_or (((PP_False D) | (dom p)),((PP_True D) | (dom q)))) ; :: thesis: x in dom ((PP_True D) | (dom q))
per cases then ( ( x in dom ((PP_False D) | (dom p)) & ((PP_False D) | (dom p)) . x = TRUE ) or ( x in dom ((PP_True D) | (dom q)) & ((PP_True D) | (dom q)) . x = TRUE ) or ( x in dom ((PP_False D) | (dom p)) & ((PP_False D) | (dom p)) . x = FALSE & x in dom ((PP_True D) | (dom q)) & ((PP_True D) | (dom q)) . x = FALSE ) ) by Th8;
suppose that A4: x in dom ((PP_False D) | (dom p)) and
A5: ((PP_False D) | (dom p)) . x = TRUE ; :: thesis: x in dom ((PP_True D) | (dom q))
((PP_False D) | (dom p)) . x = (PP_False D) . x by A4, FUNCT_1:47;
hence x in dom ((PP_True D) | (dom q)) by A3, A5, FUNCOP_1:7; :: thesis: verum
end;
suppose ( ( x in dom ((PP_True D) | (dom q)) & ((PP_True D) | (dom q)) . x = TRUE ) or ( x in dom ((PP_False D) | (dom p)) & ((PP_False D) | (dom p)) . x = FALSE & x in dom ((PP_True D) | (dom q)) & ((PP_True D) | (dom q)) . x = FALSE ) ) ; :: thesis: x in dom ((PP_True D) | (dom q))
hence x in dom ((PP_True D) | (dom q)) ; :: thesis: verum
end;
end;
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom ((PP_True D) | (dom q)) or x in dom (PP_or (((PP_False D) | (dom p)),((PP_True D) | (dom q)))) )
assume A6: x in dom ((PP_True D) | (dom q)) ; :: thesis: x in dom (PP_or (((PP_False D) | (dom p)),((PP_True D) | (dom q))))
then ((PP_True D) | (dom q)) . x = (PP_True D) . x by A2, FUNCT_1:49
.= TRUE by A6, FUNCOP_1:7 ;
hence x in dom (PP_or (((PP_False D) | (dom p)),((PP_True D) | (dom q)))) by A1, A6; :: thesis: verum
end;
let x be object ; :: thesis: ( not x in dom (PP_or (((PP_False D) | (dom p)),((PP_True D) | (dom q)))) or (PP_or (((PP_False D) | (dom p)),((PP_True D) | (dom q)))) . x = ((PP_True D) | (dom q)) . x )
assume A7: x in dom (PP_or (((PP_False D) | (dom p)),((PP_True D) | (dom q)))) ; :: thesis: (PP_or (((PP_False D) | (dom p)),((PP_True D) | (dom q)))) . x = ((PP_True D) | (dom q)) . x
per cases then ( ( x in dom ((PP_False D) | (dom p)) & ((PP_False D) | (dom p)) . x = TRUE ) or ( x in dom ((PP_True D) | (dom q)) & ((PP_True D) | (dom q)) . x = TRUE ) or ( x in dom ((PP_False D) | (dom p)) & ((PP_False D) | (dom p)) . x = FALSE & x in dom ((PP_True D) | (dom q)) & ((PP_True D) | (dom q)) . x = FALSE ) ) by Th8;
suppose that A8: x in dom ((PP_False D) | (dom p)) and
A9: ((PP_False D) | (dom p)) . x = TRUE ; :: thesis: (PP_or (((PP_False D) | (dom p)),((PP_True D) | (dom q)))) . x = ((PP_True D) | (dom q)) . x
((PP_False D) | (dom p)) . x = (PP_False D) . x by A8, FUNCT_1:47;
hence (PP_or (((PP_False D) | (dom p)),((PP_True D) | (dom q)))) . x = ((PP_True D) | (dom q)) . x by A7, A9, FUNCOP_1:7; :: thesis: verum
end;
suppose ( ( x in dom ((PP_True D) | (dom q)) & ((PP_True D) | (dom q)) . x = TRUE ) or ( x in dom ((PP_False D) | (dom p)) & ((PP_False D) | (dom p)) . x = FALSE & x in dom ((PP_True D) | (dom q)) & ((PP_True D) | (dom q)) . x = FALSE ) ) ; :: thesis: (PP_or (((PP_False D) | (dom p)),((PP_True D) | (dom q)))) . x = ((PP_True D) | (dom q)) . x
hence (PP_or (((PP_False D) | (dom p)),((PP_True D) | (dom q)))) . x = ((PP_True D) | (dom q)) . x by Def4; :: thesis: verum
end;
end;