let v be object ; for V, A being set holds SC_exists ((PP_BottomPred (ND (V,A))),v) = PP_BottomPred (ND (V,A))
let V, A be set ; SC_exists ((PP_BottomPred (ND (V,A))),v) = PP_BottomPred (ND (V,A))
set B = PP_BottomPred (ND (V,A));
set T = PP_True (ND (V,A));
set o = SC_exists ((PP_BottomPred (ND (V,A))),v);
thus
dom (SC_exists ((PP_BottomPred (ND (V,A))),v)) = dom (PP_BottomPred (ND (V,A)))
FUNCT_1:def 11 for b1 being object holds
( not b1 in dom (SC_exists ((PP_BottomPred (ND (V,A))),v)) or (SC_exists ((PP_BottomPred (ND (V,A))),v)) . b1 = (PP_BottomPred (ND (V,A))) . b1 )proof
thus
dom (SC_exists ((PP_BottomPred (ND (V,A))),v)) c= dom (PP_BottomPred (ND (V,A)))
XBOOLE_0:def 10 dom (PP_BottomPred (ND (V,A))) c= dom (SC_exists ((PP_BottomPred (ND (V,A))),v))proof
let x be
object ;
TARSKI:def 3 ( not x in dom (SC_exists ((PP_BottomPred (ND (V,A))),v)) or x in dom (PP_BottomPred (ND (V,A))) )
assume
x in dom (SC_exists ((PP_BottomPred (ND (V,A))),v))
;
x in dom (PP_BottomPred (ND (V,A)))
then
( ex
d1 being
TypeSCNominativeData of
V,
A st
(
local_overlapping (
V,
A,
x,
d1,
v)
in dom (PP_BottomPred (ND (V,A))) &
(PP_BottomPred (ND (V,A))) . (local_overlapping (V,A,x,d1,v)) = TRUE ) or for
d1 being
TypeSCNominativeData of
V,
A holds
(
local_overlapping (
V,
A,
x,
d1,
v)
in dom (PP_BottomPred (ND (V,A))) &
(PP_BottomPred (ND (V,A))) . (local_overlapping (V,A,x,d1,v)) = FALSE ) )
by Th18;
hence
x in dom (PP_BottomPred (ND (V,A)))
;
verum
end;
thus
dom (PP_BottomPred (ND (V,A))) c= dom (SC_exists ((PP_BottomPred (ND (V,A))),v))
;
verum
end;
let x be object ; ( not x in dom (SC_exists ((PP_BottomPred (ND (V,A))),v)) or (SC_exists ((PP_BottomPred (ND (V,A))),v)) . x = (PP_BottomPred (ND (V,A))) . x )
assume
x in dom (SC_exists ((PP_BottomPred (ND (V,A))),v))
; (SC_exists ((PP_BottomPred (ND (V,A))),v)) . x = (PP_BottomPred (ND (V,A))) . x
then
( ex d1 being TypeSCNominativeData of V,A st
( local_overlapping (V,A,x,d1,v) in dom (PP_BottomPred (ND (V,A))) & (PP_BottomPred (ND (V,A))) . (local_overlapping (V,A,x,d1,v)) = TRUE ) or for d1 being TypeSCNominativeData of V,A holds
( local_overlapping (V,A,x,d1,v) in dom (PP_BottomPred (ND (V,A))) & (PP_BottomPred (ND (V,A))) . (local_overlapping (V,A,x,d1,v)) = FALSE ) )
by Th18;
hence
(SC_exists ((PP_BottomPred (ND (V,A))),v)) . x = (PP_BottomPred (ND (V,A))) . x
; verum