# 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 )`