This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )