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 ↾ 𝐵 ) : 𝐵 ⟶ ( 𝐴 ⊔ 𝐵 )

Proof

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