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

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 ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ↔ ( 𝐴 ⊔ 𝐵 ) ∈ V )

Proof

Step Hyp Ref Expression
1 djuex ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) → ( 𝐴 ⊔ 𝐵 ) ∈ V )
2 df-dju ⊢ ( 𝐴 ⊔ 𝐵 ) = ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐵 ) )
3 2 eleq1i ⊢ ( ( 𝐴 ⊔ 𝐵 ) ∈ V ↔ ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐵 ) ) ∈ V )
4 unexb ⊢ ( ( ( { ∅ } × 𝐴 ) ∈ V ∧ ( { 1o } × 𝐵 ) ∈ V ) ↔ ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐵 ) ) ∈ V )
5 3 4 bitr4i ⊢ ( ( 𝐴 ⊔ 𝐵 ) ∈ V ↔ ( ( { ∅ } × 𝐴 ) ∈ V ∧ ( { 1o } × 𝐵 ) ∈ V ) )
6 0nep0 ⊢ ∅ ≠ { ∅ }
7 6 necomi ⊢ { ∅ } ≠ ∅
8 rnexg ⊢ ( ( { ∅ } × 𝐴 ) ∈ V → ran ( { ∅ } × 𝐴 ) ∈ V )
9 rnxp ⊢ ( { ∅ } ≠ ∅ → ran ( { ∅ } × 𝐴 ) = 𝐴 )
10 9 eleq1d ⊢ ( { ∅ } ≠ ∅ → ( ran ( { ∅ } × 𝐴 ) ∈ V ↔ 𝐴 ∈ V ) )
11 8 10 imbitrid ⊢ ( { ∅ } ≠ ∅ → ( ( { ∅ } × 𝐴 ) ∈ V → 𝐴 ∈ V ) )
12 7 11 ax-mp ⊢ ( ( { ∅ } × 𝐴 ) ∈ V → 𝐴 ∈ V )
13 1oex ⊢ 1o ∈ V
14 13 snnz ⊢ { 1o } ≠ ∅
15 rnexg ⊢ ( ( { 1o } × 𝐵 ) ∈ V → ran ( { 1o } × 𝐵 ) ∈ V )
16 rnxp ⊢ ( { 1o } ≠ ∅ → ran ( { 1o } × 𝐵 ) = 𝐵 )
17 16 eleq1d ⊢ ( { 1o } ≠ ∅ → ( ran ( { 1o } × 𝐵 ) ∈ V ↔ 𝐵 ∈ V ) )
18 15 17 imbitrid ⊢ ( { 1o } ≠ ∅ → ( ( { 1o } × 𝐵 ) ∈ V → 𝐵 ∈ V ) )
19 14 18 ax-mp ⊢ ( ( { 1o } × 𝐵 ) ∈ V → 𝐵 ∈ V )
20 12 19 anim12i ⊢ ( ( ( { ∅ } × 𝐴 ) ∈ V ∧ ( { 1o } × 𝐵 ) ∈ V ) → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
21 5 20 sylbi ⊢ ( ( 𝐴 ⊔ 𝐵 ) ∈ V → ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) )
22 1 21 impbii ⊢ ( ( 𝐴 ∈ V ∧ 𝐵 ∈ V ) ↔ ( 𝐴 ⊔ 𝐵 ) ∈ V )