djulcl

Description: Left closure of disjoint union. (Contributed by Jim Kingdon, 21-Jun-2022)

		Ref	Expression
	Assertion	djulcl	$⊢ C \in A \to inl (C) \in (A ⊔︀ B)$

Step	Hyp	Ref	Expression
1		df-inl	$⊢ inl = (x \in V ⟼ ⟨\emptyset, x⟩)$
2		opeq2	$⊢ x = C \to ⟨\emptyset, x⟩ = ⟨\emptyset, C⟩$
3		elex	$⊢ C \in A \to C \in V$
4		0ex	$⊢ \emptyset \in V$
5	4	snid	$⊢ \emptyset \in \{\emptyset\}$
6		opelxpi	$⊢ (\emptyset \in \{\emptyset\} \land C \in A) \to ⟨\emptyset, C⟩ \in (\{\emptyset\} \times A)$
7	5 6	mpan	$⊢ C \in A \to ⟨\emptyset, C⟩ \in (\{\emptyset\} \times A)$
8	1 2 3 7	fvmptd3	$⊢ C \in A \to inl (C) = ⟨\emptyset, C⟩$
9		elun1	$⊢ ⟨\emptyset, C⟩ \in (\{\emptyset\} \times A) \to ⟨\emptyset, C⟩ \in ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times B))$
10	7 9	syl	$⊢ C \in A \to ⟨\emptyset, C⟩ \in ((\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times B))$
11		df-dju	$⊢ (A ⊔︀ B) = (\{\emptyset\} \times A) \cup (\{1_{𝑜}\} \times B)$
12	10 11	eleqtrrdi	$⊢ C \in A \to ⟨\emptyset, C⟩ \in (A ⊔︀ B)$
13	8 12	eqeltrd	$⊢ C \in A \to inl (C) \in (A ⊔︀ B)$

Metamath Proof Explorer