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-> ( { 1o } X. _V )
2 f1ofun 
 |-  ( inr : _V -1-1-onto-> ( { 1o } X. _V ) -> Fun inr )
3 ffvresb 
 |-  ( Fun inr -> ( ( inr |` B ) : B --> ( A |_| B ) <-> A. x e. B ( x e. dom inr /\ ( inr ` x ) e. ( A |_| B ) ) ) )
4 1 2 3 mp2b 
 |-  ( ( inr |` B ) : B --> ( A |_| B ) <-> A. x e. B ( x e. dom inr /\ ( inr ` x ) e. ( A |_| B ) ) )
5 elex 
 |-  ( x e. B -> x e. _V )
6 opex 
 |-  <. 1o , x >. e. _V
7 df-inr 
 |-  inr = ( x e. _V |-> <. 1o , x >. )
8 6 7 dmmpti 
 |-  dom inr = _V
9 5 8 eleqtrrdi 
 |-  ( x e. B -> x e. dom inr )
10 djurcl 
 |-  ( x e. B -> ( inr ` x ) e. ( A |_| B ) )
11 9 10 jca 
 |-  ( x e. B -> ( x e. dom inr /\ ( inr ` x ) e. ( A |_| B ) ) )
12 4 11 mprgbir 
 |-  ( inr |` B ) : B --> ( A |_| B )