let F, G be set ; :: thesis: ( F <> {} & G <> {} implies (union F) \/ (union G) = union (UNION (F,G)) )
assume that
A1: F <> {} and
A2: G <> {} ; :: thesis: (union F) \/ (union G) = union (UNION (F,G))
thus (union F) \/ (union G) c= union (UNION (F,G)) :: according to XBOOLE_0:def 10 :: thesis: union (UNION (F,G)) c= (union F) \/ (union G)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (union F) \/ (union G) or x in union (UNION (F,G)) )
assume A3: x in (union F) \/ (union G) ; :: thesis: x in union (UNION (F,G))
per cases ( x in union F or x in union G ) by A3, XBOOLE_0:def 3;
suppose A4: x in union F ; :: thesis: x in union (UNION (F,G))
consider W being object such that
A5: W in G by A2, XBOOLE_0:def 1;
consider Y being set such that
A6: x in Y and
A7: Y in F by A4, TARSKI:def 4;
reconsider Y = Y, W = W as set by TARSKI:1;
set YW = Y \/ W;
( Y c= Y \/ W & Y \/ W in UNION (F,G) ) by A7, A5, SETFAM_1:def 4, XBOOLE_1:7;
hence x in union (UNION (F,G)) by A6, TARSKI:def 4; :: thesis: verum
end;
suppose A8: x in union G ; :: thesis: x in union (UNION (F,G))
consider W being object such that
A9: W in F by A1, XBOOLE_0:def 1;
consider Y being set such that
A10: x in Y and
A11: Y in G by A8, TARSKI:def 4;
reconsider Y = Y, W = W as set by TARSKI:1;
set YW = W \/ Y;
( Y c= W \/ Y & W \/ Y in UNION (F,G) ) by A11, A9, SETFAM_1:def 4, XBOOLE_1:7;
hence x in union (UNION (F,G)) by A10, TARSKI:def 4; :: thesis: verum
end;
end;
end;
thus union (UNION (F,G)) c= (union F) \/ (union G) by Th27; :: thesis: verum