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 )