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

Proof

Step	Hyp	Ref	Expression
1		djuex	$⊢ (A \in V \land B \in V) \to (A ⊔︀ B) \in V$
2		df-dju	$⊢ (A ⊔︀ B) = (\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times B)$
3	2	eleq1i	$⊢ (A ⊔︀ B) \in V \leftrightarrow (\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times B) \in V$
4		unexb	$⊢ (\{\emptyset\} \times A \in V \land \{1_{𝑜}\} \times B \in V) \leftrightarrow (\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times B) \in V$
5	3 4	bitr4i	$⊢ (A ⊔︀ B) \in V \leftrightarrow (\{\emptyset\} \times A \in V \land \{1_{𝑜}\} \times B \in V)$
6		0nep0	$⊢ \emptyset \neq \{\emptyset\}$
7	6	necomi	$⊢ \{\emptyset\} \neq \emptyset$
8		rnexg	$⊢ \{\emptyset\} \times A \in V \to ran (\{\emptyset\} \times A) \in V$
9		rnxp	$⊢ \{\emptyset\} \neq \emptyset \to ran (\{\emptyset\} \times A) = A$
10	9	eleq1d	$⊢ \{\emptyset\} \neq \emptyset \to (ran (\{\emptyset\} \times A) \in V \leftrightarrow A \in V)$
11	8 10	imbitrid	$⊢ \{\emptyset\} \neq \emptyset \to (\{\emptyset\} \times A \in V \to A \in V)$
12	7 11	ax-mp	$⊢ \{\emptyset\} \times A \in V \to A \in V$
13		1oex	$⊢ 1_{𝑜} \in V$
14	13	snnz	$⊢ \{1_{𝑜}\} \neq \emptyset$
15		rnexg	$⊢ \{1_{𝑜}\} \times B \in V \to ran (\{1_{𝑜}\} \times B) \in V$
16		rnxp	$⊢ \{1_{𝑜}\} \neq \emptyset \to ran (\{1_{𝑜}\} \times B) = B$
17	16	eleq1d	$⊢ \{1_{𝑜}\} \neq \emptyset \to (ran (\{1_{𝑜}\} \times B) \in V \leftrightarrow B \in V)$
18	15 17	imbitrid	$⊢ \{1_{𝑜}\} \neq \emptyset \to (\{1_{𝑜}\} \times B \in V \to B \in V)$
19	14 18	ax-mp	$⊢ \{1_{𝑜}\} \times B \in V \to B \in V$
20	12 19	anim12i	$⊢ (\{\emptyset\} \times A \in V \land \{1_{𝑜}\} \times B \in V) \to (A \in V \land B \in V)$
21	5 20	sylbi	$⊢ (A ⊔︀ B) \in V \to (A \in V \land B \in V)$
22	1 21	impbii	$⊢ (A \in V \land B \in V) \leftrightarrow (A ⊔︀ B) \in V$

Metamath Proof Explorer

Theorem djuexb

Proof