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

Metamath Proof Explorer

Theorem inrresf

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

Ref Expression
Assertion inrresf ⊢ inr ↾ B : B ⟶ A ⊔︀ B

Proof

Step Hyp Ref Expression
1 djurf1o ⊢ inr : V ⟶ 1-1 onto 1 𝑜 × V
2 f1ofun ⊢ inr : V ⟶ 1-1 onto 1 𝑜 × V → Fun ⁡ inr
3 ffvresb ⊢ Fun ⁡ inr → inr ↾ B : B ⟶ A ⊔︀ B ↔ ∀ x ∈ B x ∈ dom ⁡ inr ∧ inr ⁡ x ∈ A ⊔︀ B
4 1 2 3 mp2b ⊢ inr ↾ B : B ⟶ A ⊔︀ B ↔ ∀ x ∈ B x ∈ dom ⁡ inr ∧ inr ⁡ x ∈ A ⊔︀ B
5 elex ⊢ x ∈ B → x ∈ V
6 opex ⊢ 1 𝑜 x ∈ V
7 df-inr ⊢ inr = x ∈ V ⟼ 1 𝑜 x
8 6 7 dmmpti ⊢ dom ⁡ inr = V
9 5 8 eleqtrrdi ⊢ x ∈ B → x ∈ dom ⁡ inr
10 djurcl ⊢ x ∈ B → inr ⁡ x ∈ A ⊔︀ B
11 9 10 jca ⊢ x ∈ B → x ∈ dom ⁡ inr ∧ inr ⁡ x ∈ A ⊔︀ B
12 4 11 mprgbir ⊢ inr ↾ B : B ⟶ A ⊔︀ B