Theorem djulcl

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

	Ref	Expression
Assertion	djulcl	⊢ ( 𝐶 ∈ 𝐴 → ( inl ‘ 𝐶 ) ∈ ( 𝐴 ⊔ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		df-inl	⊢ inl = ( 𝑥 ∈ V ↦ ⟨ ∅ , 𝑥 ⟩ )
2		opeq2	⊢ ( 𝑥 = 𝐶 → ⟨ ∅ , 𝑥 ⟩ = ⟨ ∅ , 𝐶 ⟩ )
3		elex	⊢ ( 𝐶 ∈ 𝐴 → 𝐶 ∈ V )
4		0ex	⊢ ∅ ∈ V
5	4	snid	⊢ ∅ ∈ { ∅ }
6		opelxpi	⊢ ( ( ∅ ∈ { ∅ } ∧ 𝐶 ∈ 𝐴 ) → ⟨ ∅ , 𝐶 ⟩ ∈ ( { ∅ } × 𝐴 ) )
7	5 6	mpan	⊢ ( 𝐶 ∈ 𝐴 → ⟨ ∅ , 𝐶 ⟩ ∈ ( { ∅ } × 𝐴 ) )
8	1 2 3 7	fvmptd3	⊢ ( 𝐶 ∈ 𝐴 → ( inl ‘ 𝐶 ) = ⟨ ∅ , 𝐶 ⟩ )
9		elun1	⊢ ( ⟨ ∅ , 𝐶 ⟩ ∈ ( { ∅ } × 𝐴 ) → ⟨ ∅ , 𝐶 ⟩ ∈ ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐵 ) ) )
10	7 9	syl	⊢ ( 𝐶 ∈ 𝐴 → ⟨ ∅ , 𝐶 ⟩ ∈ ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐵 ) ) )
11		df-dju	⊢ ( 𝐴 ⊔ 𝐵 ) = ( ( { ∅ } × 𝐴 ) ∪ ( { 1o } × 𝐵 ) )
12	10 11	eleqtrrdi	⊢ ( 𝐶 ∈ 𝐴 → ⟨ ∅ , 𝐶 ⟩ ∈ ( 𝐴 ⊔ 𝐵 ) )
13	8 12	eqeltrd	⊢ ( 𝐶 ∈ 𝐴 → ( inl ‘ 𝐶 ) ∈ ( 𝐴 ⊔ 𝐵 ) )