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 \in V \land B \in W) \to (A ⊔︀ B) \in V$

Step	Hyp	Ref	Expression
1		df-dju	$⊢ (A ⊔︀ B) = (\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times B)$
2		snex	$⊢ \{\emptyset\} \in V$
3	2	a1i	$⊢ B \in W \to \{\emptyset\} \in V$
4		xpexg	$⊢ (\{\emptyset\} \in V \land A \in V) \to \{\emptyset\} \times A \in V$
5	3 4	sylan	$⊢ (B \in W \land A \in V) \to \{\emptyset\} \times A \in V$
6	5	ancoms	$⊢ (A \in V \land B \in W) \to \{\emptyset\} \times A \in V$
7		snex	$⊢ \{1_{𝑜}\} \in V$
8	7	a1i	$⊢ A \in V \to \{1_{𝑜}\} \in V$
9		xpexg	$⊢ (\{1_{𝑜}\} \in V \land B \in W) \to \{1_{𝑜}\} \times B \in V$
10	8 9	sylan	$⊢ (A \in V \land B \in W) \to \{1_{𝑜}\} \times B \in V$
11		unexg	$⊢ (\{\emptyset\} \times A \in V \land \{1_{𝑜}\} \times B \in V) \to (\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times B) \in V$
12	6 10 11	syl2anc	$⊢ (A \in V \land B \in W) \to (\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times B) \in V$
13	1 12	eqeltrid	$⊢ (A \in V \land B \in W) \to (A ⊔︀ B) \in V$

Metamath Proof Explorer