Theorem djuex

Description: The disjoint union of sets is a set. For a shorter proof using djuss see djuexALT . (Contributed by AV, 28-Jun-2022)

	Ref	Expression
Assertion	djuex	|- ( ( A e. V /\ B e. W ) -> ( A |_| B ) e. _V )

Proof

Step	Hyp	Ref	Expression
1		df-dju	|- ( A |_| B ) = ( ( { (/) } X. A ) u. ( { 1o } X. B ) )
2		snex	|- { (/) } e. _V
3	2	a1i	|- ( B e. W -> { (/) } e. _V )
4		xpexg	|- ( ( { (/) } e. _V /\ A e. V ) -> ( { (/) } X. A ) e. _V )
5	3 4	sylan	|- ( ( B e. W /\ A e. V ) -> ( { (/) } X. A ) e. _V )
6	5	ancoms	|- ( ( A e. V /\ B e. W ) -> ( { (/) } X. A ) e. _V )
7		snex	|- { 1o } e. _V
8	7	a1i	|- ( A e. V -> { 1o } e. _V )
9		xpexg	|- ( ( { 1o } e. _V /\ B e. W ) -> ( { 1o } X. B ) e. _V )
10	8 9	sylan	|- ( ( A e. V /\ B e. W ) -> ( { 1o } X. B ) e. _V )
11		unexg	|- ( ( ( { (/) } X. A ) e. _V /\ ( { 1o } X. B ) e. _V ) -> ( ( { (/) } X. A ) u. ( { 1o } X. B ) ) e. _V )
12	6 10 11	syl2anc	|- ( ( A e. V /\ B e. W ) -> ( ( { (/) } X. A ) u. ( { 1o } X. B ) ) e. _V )
13	1 12	eqeltrid	|- ( ( A e. V /\ B e. W ) -> ( A |_| B ) e. _V )