This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝐶 ) ∈ ( 𝐴 ⊔ 𝐵 ) )