djuss

Description: A disjoint union is a subclass of a Cartesian product. (Contributed by AV, 25-Jun-2022)

		Ref	Expression
	Assertion	djuss	$⊢ (A ⊔︀ B) \subseteq \{\emptyset, 1_{𝑜}\} \times (A \cup B)$

Proof

Step	Hyp	Ref	Expression
1		djur	$⊢ x \in (A ⊔︀ B) \to (\exists y \in A x = inl (y) \lor \exists y \in B x = inr (y))$
2		simpr	$⊢ (y \in A \land x = inl (y)) \to x = inl (y)$
3		df-inl	$⊢ inl = (x \in V ⟼ ⟨\emptyset, x⟩)$
4		opeq2	$⊢ x = y \to ⟨\emptyset, x⟩ = ⟨\emptyset, y⟩$
5		elex	$⊢ y \in A \to y \in V$
6		opex	$⊢ ⟨\emptyset, y⟩ \in V$
7	6	a1i	$⊢ y \in A \to ⟨\emptyset, y⟩ \in V$
8	3 4 5 7	fvmptd3	$⊢ y \in A \to inl (y) = ⟨\emptyset, y⟩$
9	8	adantr	$⊢ (y \in A \land x = inl (y)) \to inl (y) = ⟨\emptyset, y⟩$
10	2 9	eqtrd	$⊢ (y \in A \land x = inl (y)) \to x = ⟨\emptyset, y⟩$
11		elun1	$⊢ y \in A \to y \in (A \cup B)$
12		0ex	$⊢ \emptyset \in V$
13	12	prid1	$⊢ \emptyset \in \{\emptyset, 1_{𝑜}\}$
14	11 13	jctil	$⊢ y \in A \to (\emptyset \in \{\emptyset, 1_{𝑜}\} \land y \in (A \cup B))$
15	14	adantr	$⊢ (y \in A \land x = inl (y)) \to (\emptyset \in \{\emptyset, 1_{𝑜}\} \land y \in (A \cup B))$
16		opelxp	$⊢ ⟨\emptyset, y⟩ \in (\{\emptyset, 1_{𝑜}\} \times (A \cup B)) \leftrightarrow (\emptyset \in \{\emptyset, 1_{𝑜}\} \land y \in (A \cup B))$
17	15 16	sylibr	$⊢ (y \in A \land x = inl (y)) \to ⟨\emptyset, y⟩ \in (\{\emptyset, 1_{𝑜}\} \times (A \cup B))$
18	10 17	eqeltrd	$⊢ (y \in A \land x = inl (y)) \to x \in (\{\emptyset, 1_{𝑜}\} \times (A \cup B))$
19	18	rexlimiva	$⊢ \exists y \in A x = inl (y) \to x \in (\{\emptyset, 1_{𝑜}\} \times (A \cup B))$
20		simpr	$⊢ (y \in B \land x = inr (y)) \to x = inr (y)$
21		df-inr	$⊢ inr = (x \in V ⟼ ⟨1_{𝑜}, x⟩)$
22		opeq2	$⊢ x = y \to ⟨1_{𝑜}, x⟩ = ⟨1_{𝑜}, y⟩$
23		elex	$⊢ y \in B \to y \in V$
24		opex	$⊢ ⟨1_{𝑜}, y⟩ \in V$
25	24	a1i	$⊢ y \in B \to ⟨1_{𝑜}, y⟩ \in V$
26	21 22 23 25	fvmptd3	$⊢ y \in B \to inr (y) = ⟨1_{𝑜}, y⟩$
27	26	adantr	$⊢ (y \in B \land x = inr (y)) \to inr (y) = ⟨1_{𝑜}, y⟩$
28	20 27	eqtrd	$⊢ (y \in B \land x = inr (y)) \to x = ⟨1_{𝑜}, y⟩$
29		elun2	$⊢ y \in B \to y \in (A \cup B)$
30	29	adantr	$⊢ (y \in B \land x = inr (y)) \to y \in (A \cup B)$
31		1oelpr	$⊢ 1_{𝑜} \in \{\emptyset, 1_{𝑜}\}$
32	30 31	jctil	$⊢ (y \in B \land x = inr (y)) \to (1_{𝑜} \in \{\emptyset, 1_{𝑜}\} \land y \in (A \cup B))$
33		opelxp	$⊢ ⟨1_{𝑜}, y⟩ \in (\{\emptyset, 1_{𝑜}\} \times (A \cup B)) \leftrightarrow (1_{𝑜} \in \{\emptyset, 1_{𝑜}\} \land y \in (A \cup B))$
34	32 33	sylibr	$⊢ (y \in B \land x = inr (y)) \to ⟨1_{𝑜}, y⟩ \in (\{\emptyset, 1_{𝑜}\} \times (A \cup B))$
35	28 34	eqeltrd	$⊢ (y \in B \land x = inr (y)) \to x \in (\{\emptyset, 1_{𝑜}\} \times (A \cup B))$
36	35	rexlimiva	$⊢ \exists y \in B x = inr (y) \to x \in (\{\emptyset, 1_{𝑜}\} \times (A \cup B))$
37	19 36	jaoi	$⊢ (\exists y \in A x = inl (y) \lor \exists y \in B x = inr (y)) \to x \in (\{\emptyset, 1_{𝑜}\} \times (A \cup B))$
38	1 37	syl	$⊢ x \in (A ⊔︀ B) \to x \in (\{\emptyset, 1_{𝑜}\} \times (A \cup B))$
39	38	ssriv	$⊢ (A ⊔︀ B) \subseteq \{\emptyset, 1_{𝑜}\} \times (A \cup B)$

Metamath Proof Explorer

Theorem djuss

Proof