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

Proof

Step Hyp Ref Expression
1 df-dju ⊢ A ⊔︀ B = ∅ × A ∪ 1 𝑜 × B
2 snex ⊢ ∅ ∈ V
3 2 a1i ⊢ B ∈ W → ∅ ∈ V
4 xpexg ⊢ ∅ ∈ V ∧ A ∈ V → ∅ × A ∈ V
5 3 4 sylan ⊢ B ∈ W ∧ A ∈ V → ∅ × A ∈ V
6 5 ancoms ⊢ A ∈ V ∧ B ∈ W → ∅ × A ∈ V
7 snex ⊢ 1 𝑜 ∈ V
8 7 a1i ⊢ A ∈ V → 1 𝑜 ∈ V
9 xpexg ⊢ 1 𝑜 ∈ V ∧ B ∈ W → 1 𝑜 × B ∈ V
10 8 9 sylan ⊢ A ∈ V ∧ B ∈ W → 1 𝑜 × B ∈ V
11 unexg ⊢ ∅ × A ∈ V ∧ 1 𝑜 × B ∈ V → ∅ × A ∪ 1 𝑜 × B ∈ V
12 6 10 11 syl2anc ⊢ A ∈ V ∧ B ∈ W → ∅ × A ∪ 1 𝑜 × B ∈ V
13 1 12 eqeltrid ⊢ A ∈ V ∧ B ∈ W → A ⊔︀ B ∈ V