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

Metamath Proof Explorer

Theorem inlresf

Description: The left injection restricted to the left class of a disjoint union is a function from the left class into the disjoint union. (Contributed by AV, 27-Jun-2022)

Ref Expression
Assertion inlresf ( inl ↾ 𝐴 ) : 𝐴 ⟶ ( 𝐴 ⊔ 𝐵 )

Proof

Step Hyp Ref Expression
1 djulf1o ⊢ inl : V –1-1-onto→ ( { ∅ } × V )
2 f1ofun ⊢ ( inl : V –1-1-onto→ ( { ∅ } × V ) → Fun inl )
3 ffvresb ⊢ ( Fun inl → ( ( inl ↾ 𝐴 ) : 𝐴 ⟶ ( 𝐴 ⊔ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom inl ∧ ( inl ‘ 𝑥 ) ∈ ( 𝐴 ⊔ 𝐵 ) ) ) )
4 1 2 3 mp2b ⊢ ( ( inl ↾ 𝐴 ) : 𝐴 ⟶ ( 𝐴 ⊔ 𝐵 ) ↔ ∀ 𝑥 ∈ 𝐴 ( 𝑥 ∈ dom inl ∧ ( inl ‘ 𝑥 ) ∈ ( 𝐴 ⊔ 𝐵 ) ) )
5 elex ⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ V )
6 opex ⊢ ⟨ ∅ , 𝑥 ⟩ ∈ V
7 df-inl ⊢ inl = ( 𝑥 ∈ V ↦ ⟨ ∅ , 𝑥 ⟩ )
8 6 7 dmmpti ⊢ dom inl = V
9 5 8 eleqtrrdi ⊢ ( 𝑥 ∈ 𝐴 → 𝑥 ∈ dom inl )
10 djulcl ⊢ ( 𝑥 ∈ 𝐴 → ( inl ‘ 𝑥 ) ∈ ( 𝐴 ⊔ 𝐵 ) )
11 9 10 jca ⊢ ( 𝑥 ∈ 𝐴 → ( 𝑥 ∈ dom inl ∧ ( inl ‘ 𝑥 ) ∈ ( 𝐴 ⊔ 𝐵 ) ) )
12 4 11 mprgbir ⊢ ( inl ↾ 𝐴 ) : 𝐴 ⟶ ( 𝐴 ⊔ 𝐵 )