Metamath Proof Explorer

Theorem djuexb

Description: The disjoint union of two classes is a set iff both classes are sets. (Contributed by Jim Kingdon, 6-Sep-2023)

Ref Expression
Assertion djuexb 
|- ( ( A e. _V /\ B e. _V ) <-> ( A |_| B ) e. _V )

Proof

Step Hyp Ref Expression
1 djuex 
 |-  ( ( A e. _V /\ B e. _V ) -> ( A |_| B ) e. _V )
2 df-dju 
 |-  ( A |_| B ) = ( ( { (/) } X. A ) u. ( { 1o } X. B ) )
3 2 eleq1i 
 |-  ( ( A |_| B ) e. _V <-> ( ( { (/) } X. A ) u. ( { 1o } X. B ) ) e. _V )
4 unexb 
 |-  ( ( ( { (/) } X. A ) e. _V /\ ( { 1o } X. B ) e. _V ) <-> ( ( { (/) } X. A ) u. ( { 1o } X. B ) ) e. _V )
5 3 4 bitr4i 
 |-  ( ( A |_| B ) e. _V <-> ( ( { (/) } X. A ) e. _V /\ ( { 1o } X. B ) e. _V ) )
6 0nep0 
 |-  (/) =/= { (/) }
7 6 necomi 
 |-  { (/) } =/= (/)
8 rnexg 
 |-  ( ( { (/) } X. A ) e. _V -> ran ( { (/) } X. A ) e. _V )
9 rnxp 
 |-  ( { (/) } =/= (/) -> ran ( { (/) } X. A ) = A )
10 9 eleq1d 
 |-  ( { (/) } =/= (/) -> ( ran ( { (/) } X. A ) e. _V <-> A e. _V ) )
11 8 10 syl5ib 
 |-  ( { (/) } =/= (/) -> ( ( { (/) } X. A ) e. _V -> A e. _V ) )
12 7 11 ax-mp 
 |-  ( ( { (/) } X. A ) e. _V -> A e. _V )
13 1oex 
 |-  1o e. _V
14 13 snnz 
 |-  { 1o } =/= (/)
15 rnexg 
 |-  ( ( { 1o } X. B ) e. _V -> ran ( { 1o } X. B ) e. _V )
16 rnxp 
 |-  ( { 1o } =/= (/) -> ran ( { 1o } X. B ) = B )
17 16 eleq1d 
 |-  ( { 1o } =/= (/) -> ( ran ( { 1o } X. B ) e. _V <-> B e. _V ) )
18 15 17 syl5ib 
 |-  ( { 1o } =/= (/) -> ( ( { 1o } X. B ) e. _V -> B e. _V ) )
19 14 18 ax-mp 
 |-  ( ( { 1o } X. B ) e. _V -> B e. _V )
20 12 19 anim12i 
 |-  ( ( ( { (/) } X. A ) e. _V /\ ( { 1o } X. B ) e. _V ) -> ( A e. _V /\ B e. _V ) )
21 5 20 sylbi 
 |-  ( ( A |_| B ) e. _V -> ( A e. _V /\ B e. _V ) )
22 1 21 impbii 
 |-  ( ( A e. _V /\ B e. _V ) <-> ( A |_| B ) e. _V )