let v be object ; :: thesis: for V, A being set
for p, q being SCPartialNominativePredicate of V,A holds SC_exists ((PP_or (p,q)),v) = PP_or ((SC_exists (p,v)),(SC_exists (q,v)))
let V, A be set ; :: thesis: for p, q being SCPartialNominativePredicate of V,A holds SC_exists ((PP_or (p,q)),v) = PP_or ((SC_exists (p,v)),(SC_exists (q,v)))
let p, q be SCPartialNominativePredicate of V,A; :: thesis: SC_exists ((PP_or (p,q)),v) = PP_or ((SC_exists (p,v)),(SC_exists (q,v)))
set a = PP_or (p,q);
set f = SC_exists ((PP_or (p,q)),v);
set g = SC_exists (p,v);
set h = SC_exists (q,v);
set b = PP_or ((SC_exists (p,v)),(SC_exists (q,v)));
A1: dom (PP_or (p,q)) = { d where d is TypeSCNominativeData of V,A : ( ( d in dom p & p . d = TRUE ) or ( d in dom q & q . d = TRUE ) or ( d in dom p & p . d = FALSE & d in dom q & q . d = FALSE ) ) } by Th15;
A2: dom (PP_or ((SC_exists (p,v)),(SC_exists (q,v)))) = { d where d is TypeSCNominativeData of V,A : ( ( d in dom (SC_exists (p,v)) & (SC_exists (p,v)) . d = TRUE ) or ( d in dom (SC_exists (q,v)) & (SC_exists (q,v)) . d = TRUE ) or ( d in dom (SC_exists (p,v)) & (SC_exists (p,v)) . d = FALSE & d in dom (SC_exists (q,v)) & (SC_exists (q,v)) . d = FALSE ) ) } by Th15;
A3: dom (SC_exists ((PP_or (p,q)),v)) = { d where d is TypeSCNominativeData of V,A : ( ex d1 being TypeSCNominativeData of V,A st
( local_overlapping (V,A,d,d1,v) in dom (PP_or (p,q)) & (PP_or (p,q)) . (local_overlapping (V,A,d,d1,v)) = TRUE ) or for d1 being TypeSCNominativeData of V,A holds
( local_overlapping (V,A,d,d1,v) in dom (PP_or (p,q)) & (PP_or (p,q)) . (local_overlapping (V,A,d,d1,v)) = FALSE ) ) } by Def1;
A4: dom (SC_exists (p,v)) = { d where d is TypeSCNominativeData of V,A : ( ex d1 being TypeSCNominativeData of V,A st
( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = TRUE ) or for d1 being TypeSCNominativeData of V,A holds
( local_overlapping (V,A,d,d1,v) in dom p & p . (local_overlapping (V,A,d,d1,v)) = FALSE ) ) } by Def1;
A5: dom (SC_exists (q,v)) = { d where d is TypeSCNominativeData of V,A : ( ex d1 being TypeSCNominativeData of V,A st
( local_overlapping (V,A,d,d1,v) in dom q & q . (local_overlapping (V,A,d,d1,v)) = TRUE ) or for d1 being TypeSCNominativeData of V,A holds
( local_overlapping (V,A,d,d1,v) in dom q & q . (local_overlapping (V,A,d,d1,v)) = FALSE ) ) } by Def1;
thus dom (SC_exists ((PP_or (p,q)),v)) = dom (PP_or ((SC_exists (p,v)),(SC_exists (q,v)))) :: according to FUNCT_1:def 11 :: thesis: for b1 being object holds
( not b1 in dom (SC_exists ((PP_or (p,q)),v)) or (SC_exists ((PP_or (p,q)),v)) . b1 = (PP_or ((SC_exists (p,v)),(SC_exists (q,v)))) . b1 )
proof
thus dom (SC_exists ((PP_or (p,q)),v)) c= dom (PP_or ((SC_exists (p,v)),(SC_exists (q,v)))) :: according to XBOOLE_0:def 10 :: thesis: dom (PP_or ((SC_exists (p,v)),(SC_exists (q,v)))) c= dom (SC_exists ((PP_or (p,q)),v))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (SC_exists ((PP_or (p,q)),v)) or x in dom (PP_or ((SC_exists (p,v)),(SC_exists (q,v)))) )
assume A6: x in dom (SC_exists ((PP_or (p,q)),v)) ; :: thesis: x in dom (PP_or ((SC_exists (p,v)),(SC_exists (q,v))))
then A7: x is TypeSCNominativeData of V,A by NOMIN_1:39;
per cases ( ex d1 being TypeSCNominativeData of V,A st
( local_overlapping (V,A,x,d1,v) in dom (PP_or (p,q)) & (PP_or (p,q)) . (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_or (p,q)) & (PP_or (p,q)) . (local_overlapping (V,A,x,d1,v)) = FALSE ) ) by A6, Th18;
suppose ex d1 being TypeSCNominativeData of V,A st
( local_overlapping (V,A,x,d1,v) in dom (PP_or (p,q)) & (PP_or (p,q)) . (local_overlapping (V,A,x,d1,v)) = TRUE ) ; :: thesis: x in dom (PP_or ((SC_exists (p,v)),(SC_exists (q,v))))
then consider d1 being TypeSCNominativeData of V,A such that
A8: local_overlapping (V,A,x,d1,v) in dom (PP_or (p,q)) and
A9: (PP_or (p,q)) . (local_overlapping (V,A,x,d1,v)) = TRUE ;
set L = local_overlapping (V,A,x,d1,v);
per cases ( ( local_overlapping (V,A,x,d1,v) in dom p & p . (local_overlapping (V,A,x,d1,v)) = TRUE ) or ( local_overlapping (V,A,x,d1,v) in dom q & q . (local_overlapping (V,A,x,d1,v)) = TRUE ) or ( local_overlapping (V,A,x,d1,v) in dom p & p . (local_overlapping (V,A,x,d1,v)) = FALSE & local_overlapping (V,A,x,d1,v) in dom q & q . (local_overlapping (V,A,x,d1,v)) = FALSE ) ) by A8, PARTPR_1:8;
suppose A10: ( local_overlapping (V,A,x,d1,v) in dom p & p . (local_overlapping (V,A,x,d1,v)) = TRUE ) ; :: thesis: x in dom (PP_or ((SC_exists (p,v)),(SC_exists (q,v))))
then A11: x in dom (SC_exists (p,v)) by A7, A4;
(SC_exists (p,v)) . x = TRUE by A7, A10, Def1;
hence x in dom (PP_or ((SC_exists (p,v)),(SC_exists (q,v)))) by A2, A7, A11; :: thesis: verum
end;
suppose A12: ( local_overlapping (V,A,x,d1,v) in dom q & q . (local_overlapping (V,A,x,d1,v)) = TRUE ) ; :: thesis: x in dom (PP_or ((SC_exists (p,v)),(SC_exists (q,v))))
then A13: x in dom (SC_exists (q,v)) by A7, A5;
(SC_exists (q,v)) . x = TRUE by A7, A12, Def1;
hence x in dom (PP_or ((SC_exists (p,v)),(SC_exists (q,v)))) by A2, A7, A13; :: thesis: verum
end;
suppose ( local_overlapping (V,A,x,d1,v) in dom p & p . (local_overlapping (V,A,x,d1,v)) = FALSE & local_overlapping (V,A,x,d1,v) in dom q & q . (local_overlapping (V,A,x,d1,v)) = FALSE ) ; :: thesis: x in dom (PP_or ((SC_exists (p,v)),(SC_exists (q,v))))
hence x in dom (PP_or ((SC_exists (p,v)),(SC_exists (q,v)))) by A9, PARTPR_1:9; :: thesis: verum
end;
end;
end;
suppose A14: for d1 being TypeSCNominativeData of V,A holds
( local_overlapping (V,A,x,d1,v) in dom (PP_or (p,q)) & (PP_or (p,q)) . (local_overlapping (V,A,x,d1,v)) = FALSE ) ; :: thesis: x in dom (PP_or ((SC_exists (p,v)),(SC_exists (q,v))))
A15: for d1 being TypeSCNominativeData of V,A holds
( local_overlapping (V,A,x,d1,v) in dom p & p . (local_overlapping (V,A,x,d1,v)) = FALSE )
proof
let d1 be TypeSCNominativeData of V,A; :: thesis: ( local_overlapping (V,A,x,d1,v) in dom p & p . (local_overlapping (V,A,x,d1,v)) = FALSE )
set O = local_overlapping (V,A,x,d1,v);
( local_overlapping (V,A,x,d1,v) in dom (PP_or (p,q)) & (PP_or (p,q)) . (local_overlapping (V,A,x,d1,v)) = FALSE ) by A14;
hence ( local_overlapping (V,A,x,d1,v) in dom p & p . (local_overlapping (V,A,x,d1,v)) = FALSE ) by PARTPR_1:13; :: thesis: verum
end;
then A16: x in dom (SC_exists (p,v)) by A7, A4;
A17: (SC_exists (p,v)) . x = FALSE by A7, A15, Def1;
A18: for d1 being TypeSCNominativeData of V,A holds
( local_overlapping (V,A,x,d1,v) in dom q & q . (local_overlapping (V,A,x,d1,v)) = FALSE )
proof
let d1 be TypeSCNominativeData of V,A; :: thesis: ( local_overlapping (V,A,x,d1,v) in dom q & q . (local_overlapping (V,A,x,d1,v)) = FALSE )
set O = local_overlapping (V,A,x,d1,v);
( local_overlapping (V,A,x,d1,v) in dom (PP_or (p,q)) & (PP_or (p,q)) . (local_overlapping (V,A,x,d1,v)) = FALSE ) by A14;
hence ( local_overlapping (V,A,x,d1,v) in dom q & q . (local_overlapping (V,A,x,d1,v)) = FALSE ) by PARTPR_1:13; :: thesis: verum
end;
then A19: x in dom (SC_exists (q,v)) by A7, A5;
(SC_exists (q,v)) . x = FALSE by A7, A18, Def1;
hence x in dom (PP_or ((SC_exists (p,v)),(SC_exists (q,v)))) by A2, A7, A16, A17, A19; :: thesis: verum
end;
end;
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in dom (PP_or ((SC_exists (p,v)),(SC_exists (q,v)))) or x in dom (SC_exists ((PP_or (p,q)),v)) )
assume A20: x in dom (PP_or ((SC_exists (p,v)),(SC_exists (q,v)))) ; :: thesis: x in dom (SC_exists ((PP_or (p,q)),v))
then A21: x is TypeSCNominativeData of V,A by NOMIN_1:39;
per cases ( ( x in dom (SC_exists (p,v)) & (SC_exists (p,v)) . x = TRUE ) or ( x in dom (SC_exists (q,v)) & (SC_exists (q,v)) . x = TRUE ) or ( x in dom (SC_exists (p,v)) & (SC_exists (p,v)) . x = FALSE & x in dom (SC_exists (q,v)) & (SC_exists (q,v)) . x = FALSE ) ) by A20, PARTPR_1:8;
suppose that A22: x in dom (SC_exists (p,v)) and
A23: (SC_exists (p,v)) . x = TRUE ; :: thesis: x in dom (SC_exists ((PP_or (p,q)),v))
per cases ( ex d1 being TypeSCNominativeData of V,A st
( local_overlapping (V,A,x,d1,v) in dom p & p . (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 p & p . (local_overlapping (V,A,x,d1,v)) = FALSE ) ) by A22, Th18;
suppose ex d1 being TypeSCNominativeData of V,A st
( local_overlapping (V,A,x,d1,v) in dom p & p . (local_overlapping (V,A,x,d1,v)) = TRUE ) ; :: thesis: x in dom (SC_exists ((PP_or (p,q)),v))
then consider d1 being TypeSCNominativeData of V,A such that
A24: local_overlapping (V,A,x,d1,v) in dom p and
A25: p . (local_overlapping (V,A,x,d1,v)) = TRUE ;
set L = local_overlapping (V,A,x,d1,v);
( local_overlapping (V,A,x,d1,v) in dom (PP_or (p,q)) & (PP_or (p,q)) . (local_overlapping (V,A,x,d1,v)) = TRUE ) by A1, A24, A25, PARTPR_1:def 4;
hence x in dom (SC_exists ((PP_or (p,q)),v)) by A3, A21; :: thesis: verum
end;
suppose for d1 being TypeSCNominativeData of V,A holds
( local_overlapping (V,A,x,d1,v) in dom p & p . (local_overlapping (V,A,x,d1,v)) = FALSE ) ; :: thesis: x in dom (SC_exists ((PP_or (p,q)),v))
hence x in dom (SC_exists ((PP_or (p,q)),v)) by A21, A23, Def1; :: thesis: verum
end;
end;
end;
suppose that A26: x in dom (SC_exists (q,v)) and
A27: (SC_exists (q,v)) . x = TRUE ; :: thesis: x in dom (SC_exists ((PP_or (p,q)),v))
per cases ( ex d1 being TypeSCNominativeData of V,A st
( local_overlapping (V,A,x,d1,v) in dom q & q . (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 q & q . (local_overlapping (V,A,x,d1,v)) = FALSE ) ) by A26, Th18;
suppose ex d1 being TypeSCNominativeData of V,A st
( local_overlapping (V,A,x,d1,v) in dom q & q . (local_overlapping (V,A,x,d1,v)) = TRUE ) ; :: thesis: x in dom (SC_exists ((PP_or (p,q)),v))
then consider d1 being TypeSCNominativeData of V,A such that
A28: local_overlapping (V,A,x,d1,v) in dom q and
A29: q . (local_overlapping (V,A,x,d1,v)) = TRUE ;
set L = local_overlapping (V,A,x,d1,v);
( local_overlapping (V,A,x,d1,v) in dom (PP_or (p,q)) & (PP_or (p,q)) . (local_overlapping (V,A,x,d1,v)) = TRUE ) by A1, A28, A29, PARTPR_1:def 4;
hence x in dom (SC_exists ((PP_or (p,q)),v)) by A3, A21; :: thesis: verum
end;
suppose for d1 being TypeSCNominativeData of V,A holds
( local_overlapping (V,A,x,d1,v) in dom q & q . (local_overlapping (V,A,x,d1,v)) = FALSE ) ; :: thesis: x in dom (SC_exists ((PP_or (p,q)),v))
hence x in dom (SC_exists ((PP_or (p,q)),v)) by A21, A27, Def1; :: thesis: verum
end;
end;
end;
suppose that A30: x in dom (SC_exists (p,v)) and
A31: (SC_exists (p,v)) . x = FALSE and
A32: x in dom (SC_exists (q,v)) and
A33: (SC_exists (q,v)) . x = FALSE ; :: thesis: x in dom (SC_exists ((PP_or (p,q)),v))
for d1 being TypeSCNominativeData of V,A holds
( local_overlapping (V,A,x,d1,v) in dom (PP_or (p,q)) & (PP_or (p,q)) . (local_overlapping (V,A,x,d1,v)) = FALSE )
proof
let d1 be TypeSCNominativeData of V,A; :: thesis: ( local_overlapping (V,A,x,d1,v) in dom (PP_or (p,q)) & (PP_or (p,q)) . (local_overlapping (V,A,x,d1,v)) = FALSE )
A34: for d1 being TypeSCNominativeData of V,A holds
( not local_overlapping (V,A,x,d1,v) in dom p or not p . (local_overlapping (V,A,x,d1,v)) = TRUE ) by A21, A31, Def1;
A35: for d1 being TypeSCNominativeData of V,A holds
( not local_overlapping (V,A,x,d1,v) in dom q or not q . (local_overlapping (V,A,x,d1,v)) = TRUE ) by A21, A33, Def1;
set L = local_overlapping (V,A,x,d1,v);
( local_overlapping (V,A,x,d1,v) in dom p & p . (local_overlapping (V,A,x,d1,v)) = FALSE & local_overlapping (V,A,x,d1,v) in dom q & q . (local_overlapping (V,A,x,d1,v)) = FALSE ) by A34, A35, A30, A32, Th18;
hence ( local_overlapping (V,A,x,d1,v) in dom (PP_or (p,q)) & (PP_or (p,q)) . (local_overlapping (V,A,x,d1,v)) = FALSE ) by A1, PARTPR_1:def 4; :: thesis: verum
end;
hence x in dom (SC_exists ((PP_or (p,q)),v)) by A3, A21; :: thesis: verum
end;
end;
end;
let x be object ; :: thesis: ( not x in dom (SC_exists ((PP_or (p,q)),v)) or (SC_exists ((PP_or (p,q)),v)) . x = (PP_or ((SC_exists (p,v)),(SC_exists (q,v)))) . x )
assume A36: x in dom (SC_exists ((PP_or (p,q)),v)) ; :: thesis: (SC_exists ((PP_or (p,q)),v)) . x = (PP_or ((SC_exists (p,v)),(SC_exists (q,v)))) . x
then A37: x is TypeSCNominativeData of V,A by NOMIN_1:39;
per cases ( ex d1 being TypeSCNominativeData of V,A st
( local_overlapping (V,A,x,d1,v) in dom (PP_or (p,q)) & (PP_or (p,q)) . (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_or (p,q)) & (PP_or (p,q)) . (local_overlapping (V,A,x,d1,v)) = FALSE ) ) by A36, Th18;
suppose ex d1 being TypeSCNominativeData of V,A st
( local_overlapping (V,A,x,d1,v) in dom (PP_or (p,q)) & (PP_or (p,q)) . (local_overlapping (V,A,x,d1,v)) = TRUE ) ; :: thesis: (SC_exists ((PP_or (p,q)),v)) . x = (PP_or ((SC_exists (p,v)),(SC_exists (q,v)))) . x
then consider d1 being TypeSCNominativeData of V,A such that
A38: local_overlapping (V,A,x,d1,v) in dom (PP_or (p,q)) and
A39: (PP_or (p,q)) . (local_overlapping (V,A,x,d1,v)) = TRUE ;
set L = local_overlapping (V,A,x,d1,v);
per cases ( ( local_overlapping (V,A,x,d1,v) in dom p & p . (local_overlapping (V,A,x,d1,v)) = TRUE ) or ( local_overlapping (V,A,x,d1,v) in dom q & q . (local_overlapping (V,A,x,d1,v)) = TRUE ) or ( local_overlapping (V,A,x,d1,v) in dom p & p . (local_overlapping (V,A,x,d1,v)) = FALSE & local_overlapping (V,A,x,d1,v) in dom q & q . (local_overlapping (V,A,x,d1,v)) = FALSE ) ) by A38, PARTPR_1:8;
suppose A40: ( local_overlapping (V,A,x,d1,v) in dom p & p . (local_overlapping (V,A,x,d1,v)) = TRUE ) ; :: thesis: (SC_exists ((PP_or (p,q)),v)) . x = (PP_or ((SC_exists (p,v)),(SC_exists (q,v)))) . x
then A41: x in dom (SC_exists (p,v)) by A37, A4;
(SC_exists (p,v)) . x = TRUE by A37, A40, Def1;
hence (PP_or ((SC_exists (p,v)),(SC_exists (q,v)))) . x = TRUE by A41, PARTPR_1:def 4
.= (SC_exists ((PP_or (p,q)),v)) . x by A38, A39, A37, Def1 ;
:: thesis: verum
end;
suppose A42: ( local_overlapping (V,A,x,d1,v) in dom q & q . (local_overlapping (V,A,x,d1,v)) = TRUE ) ; :: thesis: (SC_exists ((PP_or (p,q)),v)) . x = (PP_or ((SC_exists (p,v)),(SC_exists (q,v)))) . x
then A43: x in dom (SC_exists (q,v)) by A37, A5;
(SC_exists (q,v)) . x = TRUE by A37, A42, Def1;
hence (PP_or ((SC_exists (p,v)),(SC_exists (q,v)))) . x = TRUE by A43, PARTPR_1:def 4
.= (SC_exists ((PP_or (p,q)),v)) . x by A38, A39, A37, Def1 ;
:: thesis: verum
end;
suppose ( local_overlapping (V,A,x,d1,v) in dom p & p . (local_overlapping (V,A,x,d1,v)) = FALSE & local_overlapping (V,A,x,d1,v) in dom q & q . (local_overlapping (V,A,x,d1,v)) = FALSE ) ; :: thesis: (SC_exists ((PP_or (p,q)),v)) . x = (PP_or ((SC_exists (p,v)),(SC_exists (q,v)))) . x
hence (SC_exists ((PP_or (p,q)),v)) . x = (PP_or ((SC_exists (p,v)),(SC_exists (q,v)))) . x by A39, PARTPR_1:9; :: thesis: verum
end;
end;
end;
suppose A44: for d1 being TypeSCNominativeData of V,A holds
( local_overlapping (V,A,x,d1,v) in dom (PP_or (p,q)) & (PP_or (p,q)) . (local_overlapping (V,A,x,d1,v)) = FALSE ) ; :: thesis: (SC_exists ((PP_or (p,q)),v)) . x = (PP_or ((SC_exists (p,v)),(SC_exists (q,v)))) . x
A45: for d1 being TypeSCNominativeData of V,A holds
( local_overlapping (V,A,x,d1,v) in dom p & p . (local_overlapping (V,A,x,d1,v)) = FALSE )
proof
let d1 be TypeSCNominativeData of V,A; :: thesis: ( local_overlapping (V,A,x,d1,v) in dom p & p . (local_overlapping (V,A,x,d1,v)) = FALSE )
set O = local_overlapping (V,A,x,d1,v);
( local_overlapping (V,A,x,d1,v) in dom (PP_or (p,q)) & (PP_or (p,q)) . (local_overlapping (V,A,x,d1,v)) = FALSE ) by A44;
hence ( local_overlapping (V,A,x,d1,v) in dom p & p . (local_overlapping (V,A,x,d1,v)) = FALSE ) by PARTPR_1:13; :: thesis: verum
end;
then A46: x in dom (SC_exists (p,v)) by A37, A4;
A47: (SC_exists (p,v)) . x = FALSE by A37, A45, Def1;
A48: for d1 being TypeSCNominativeData of V,A holds
( local_overlapping (V,A,x,d1,v) in dom q & q . (local_overlapping (V,A,x,d1,v)) = FALSE )
proof
let d1 be TypeSCNominativeData of V,A; :: thesis: ( local_overlapping (V,A,x,d1,v) in dom q & q . (local_overlapping (V,A,x,d1,v)) = FALSE )
set O = local_overlapping (V,A,x,d1,v);
( local_overlapping (V,A,x,d1,v) in dom (PP_or (p,q)) & (PP_or (p,q)) . (local_overlapping (V,A,x,d1,v)) = FALSE ) by A44;
hence ( local_overlapping (V,A,x,d1,v) in dom q & q . (local_overlapping (V,A,x,d1,v)) = FALSE ) by PARTPR_1:13; :: thesis: verum
end;
then A49: x in dom (SC_exists (q,v)) by A37, A5;
(SC_exists (q,v)) . x = FALSE by A37, A48, Def1;
hence (PP_or ((SC_exists (p,v)),(SC_exists (q,v)))) . x = FALSE by A46, A47, A49, PARTPR_1:def 4
.= (SC_exists ((PP_or (p,q)),v)) . x by A44, A37, Def1 ;
:: thesis: verum
end;
end;