let D be non empty set ; :: thesis: PP_and ((PP_BottomPred D),(PP_False D)) = PP_False D
set B = PP_BottomPred D;
set F = PP_False D;
set o = PP_and ((PP_BottomPred D),(PP_False D));
A1: dom (PP_and ((PP_BottomPred D),(PP_False D))) = { d where d is Element of D : ( ( d in dom (PP_BottomPred D) & (PP_BottomPred D) . d = FALSE ) or ( d in dom (PP_False D) & (PP_False D) . d = FALSE ) or ( d in dom (PP_BottomPred D) & (PP_BottomPred D) . d = TRUE & d in dom (PP_False D) & (PP_False D) . d = TRUE ) ) } by Th16;
thus dom (PP_and ((PP_BottomPred D),(PP_False D))) = dom (PP_False D) :: according to FUNCT_1:def 11 :: thesis: for b1 being object holds
( not b1 in dom (PP_and ((PP_BottomPred D),(PP_False D))) or (PP_and ((PP_BottomPred D),(PP_False D))) . b1 = (PP_False D) . b1 )
proof
thus dom (PP_and ((PP_BottomPred D),(PP_False D))) c= dom (PP_False D) ; :: according to XBOOLE_0:def 10 :: thesis: dom (PP_False D) c= dom (PP_and ((PP_BottomPred D),(PP_False D)))
thus dom (PP_False D) c= dom (PP_and ((PP_BottomPred D),(PP_False D))) :: thesis: verum
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (PP_False D) or x in dom (PP_and ((PP_BottomPred D),(PP_False D))) )
assume A2: x in dom (PP_False D) ; :: thesis: x in dom (PP_and ((PP_BottomPred D),(PP_False D)))
then (PP_False D) . x = FALSE by FUNCOP_1:7;
hence x in dom (PP_and ((PP_BottomPred D),(PP_False D))) by A1, A2; :: thesis: verum
end;
end;
let x be object ; :: thesis: ( not x in dom (PP_and ((PP_BottomPred D),(PP_False D))) or (PP_and ((PP_BottomPred D),(PP_False D))) . x = (PP_False D) . x )
assume x in dom (PP_and ((PP_BottomPred D),(PP_False D))) ; :: thesis: (PP_and ((PP_BottomPred D),(PP_False D))) . x = (PP_False D) . x
per cases then ( ( x in dom (PP_BottomPred D) & (PP_BottomPred D) . x = FALSE ) or ( x in dom (PP_BottomPred D) & (PP_BottomPred D) . x = TRUE & x in dom (PP_False D) & (PP_False D) . x = TRUE ) or ( x in dom (PP_False D) & (PP_False D) . x = FALSE ) ) ;
suppose ( ( x in dom (PP_BottomPred D) & (PP_BottomPred D) . x = FALSE ) or ( x in dom (PP_BottomPred D) & (PP_BottomPred D) . x = TRUE & x in dom (PP_False D) & (PP_False D) . x = TRUE ) ) ; :: thesis: (PP_and ((PP_BottomPred D),(PP_False D))) . x = (PP_False D) . x
hence (PP_and ((PP_BottomPred D),(PP_False D))) . x = (PP_False D) . x ; :: thesis: verum
end;
suppose ( x in dom (PP_False D) & (PP_False D) . x = FALSE ) ; :: thesis: (PP_and ((PP_BottomPred D),(PP_False D))) . x = (PP_False D) . x
hence (PP_and ((PP_BottomPred D),(PP_False D))) . x = (PP_False D) . x by Th19; :: thesis: verum
end;
end;