Theorem djulcl

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

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

Proof

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