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

Proof

Step Hyp Ref Expression
1 df-dju ⊢ ( 𝐴 ⊔ 𝐵 ) = ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐵 ) )
2 snex ⊢ { ∅ } ∈ V
3 2 a1i ⊢ ( 𝐵 ∈ 𝑊 → { ∅ } ∈ V )
4 xpexg ⊢ ( ( { ∅ } ∈ V ∧ 𝐴 ∈ 𝑉 ) → ( { ∅ } × 𝐴 ) ∈ V )
5 3 4 sylan ⊢ ( ( 𝐵 ∈ 𝑊 ∧ 𝐴 ∈ 𝑉 ) → ( { ∅ } × 𝐴 ) ∈ V )
6 5 ancoms ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( { ∅ } × 𝐴 ) ∈ V )
7 snex ⊢ { 1o } ∈ V
8 7 a1i ⊢ ( 𝐴 ∈ 𝑉 → { 1o } ∈ V )
9 xpexg ⊢ ( ( { 1o } ∈ V ∧ 𝐵 ∈ 𝑊 ) → ( { 1o } × 𝐵 ) ∈ V )
10 8 9 sylan ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( { 1o } × 𝐵 ) ∈ V )
11 unexg ⊢ ( ( ( { ∅ } × 𝐴 ) ∈ V ∧ ( { 1o } × 𝐵 ) ∈ V ) → ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐵 ) ) ∈ V )
12 6 10 11 syl2anc ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐵 ) ) ∈ V )
13 1 12 eqeltrid ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐴 ⊔ 𝐵 ) ∈ V )