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 |` A ) : A --> ( A |_| B )

Proof

Step Hyp Ref Expression
1 djulf1o 
 |-  inl : _V -1-1-onto-> ( { (/) } X. _V )
2 f1ofun 
 |-  ( inl : _V -1-1-onto-> ( { (/) } X. _V ) -> Fun inl )
3 ffvresb 
 |-  ( Fun inl -> ( ( inl |` A ) : A --> ( A |_| B ) <-> A. x e. A ( x e. dom inl /\ ( inl ` x ) e. ( A |_| B ) ) ) )
4 1 2 3 mp2b 
 |-  ( ( inl |` A ) : A --> ( A |_| B ) <-> A. x e. A ( x e. dom inl /\ ( inl ` x ) e. ( A |_| B ) ) )
5 elex 
 |-  ( x e. A -> x e. _V )
6 opex 
 |-  <. (/) , x >. e. _V
7 df-inl 
 |-  inl = ( x e. _V |-> <. (/) , x >. )
8 6 7 dmmpti 
 |-  dom inl = _V
9 5 8 eleqtrrdi 
 |-  ( x e. A -> x e. dom inl )
10 djulcl 
 |-  ( x e. A -> ( inl ` x ) e. ( A |_| B ) )
11 9 10 jca 
 |-  ( x e. A -> ( x e. dom inl /\ ( inl ` x ) e. ( A |_| B ) ) )
12 4 11 mprgbir 
 |-  ( inl |` A ) : A --> ( A |_| B )