djurcl

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

		Ref	Expression
	Assertion	djurcl	$⊢ C \in B \to inr (C) \in (A ⊔︀ B)$

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

Metamath Proof Explorer