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 ∈ V ∧ B ∈ V ↔ A ⊔︀ B ∈ V

Proof

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