let V, A be set ; :: thesis: for p, q being SCPartialNominativePredicate of V,A holds dom (PP_imp (p,q)) = { d where d is TypeSCNominativeData of V,A : ( ( 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 SCPartialNominativePredicate of V,A; :: thesis: dom (PP_imp (p,q)) = { d where d is TypeSCNominativeData of V,A : ( ( 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 D = { d where d is TypeSCNominativeData of V,A : ( ( 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 ) ) } ;
A1: dom (PP_imp (p,q)) = { d where d is Element of ND (V,A) : ( ( 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 PARTPR_1:def 4;
A2: dom (PP_not p) = dom p by PARTPR_1:def 2;
thus dom (PP_imp (p,q)) c= { d where d is TypeSCNominativeData of V,A : ( ( 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 ) ) } :: according to XBOOLE_0:def 10 :: thesis: { d where d is TypeSCNominativeData of V,A : ( ( 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 { d where d is TypeSCNominativeData of V,A : ( ( 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 ) ) } )
assume x in dom (PP_imp (p,q)) ; :: thesis: x in { d where d is TypeSCNominativeData of V,A : ( ( 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 ) ) }
then consider d being Element of ND (V,A) 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;
reconsider d = d as TypeSCNominativeData of V,A by NOMIN_1:39;

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 { d where d is TypeSCNominativeData of V,A : ( ( 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 ) ) }

p . d = FALSE by A2, A5, A6, PARTPR_1:5;
hence x in { d where d is TypeSCNominativeData of V,A : ( ( 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 ) ) } by A2, A3, A5; :: thesis: verum

end;

suppose ( d in dom q & q . d = TRUE ) ; :: thesis: x in { d where d is TypeSCNominativeData of V,A : ( ( 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 ) ) }

hence x in { d where d is TypeSCNominativeData of V,A : ( ( 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 ) ) } 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 { d where d is TypeSCNominativeData of V,A : ( ( 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 ) ) }

p . d = TRUE by A2, A7, A8, PARTPR_1:4;
hence x in { d where d is TypeSCNominativeData of V,A : ( ( 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 ) ) } 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 TypeSCNominativeData of V,A : ( ( 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 { d where d is TypeSCNominativeData of V,A : ( ( 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 ) ) } ; :: thesis: x in dom (PP_imp (p,q))
then consider d being TypeSCNominativeData of V,A 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, PARTPR_1:def 2;
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, PARTPR_1:def 2;
hence x in dom (PP_imp (p,q)) by A1, A2, A10, A14, A15, A17; :: thesis: verum

end;

end;