Theorem djurcl

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

	Ref	Expression
Assertion	djurcl	$$⊢C\in B\to inr\left(C\right)\in \left(A\mathrm{\bigsqcup ︀}B\right)$$

Proof

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