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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | djulf1o | |
|
2 | f1ofun | |
|
3 | ffvresb | |
|
4 | 1 2 3 | mp2b | |
5 | elex | |
|
6 | opex | |
|
7 | df-inl | |
|
8 | 6 7 | dmmpti | |
9 | 5 8 | eleqtrrdi | |
10 | djulcl | |
|
11 | 9 10 | jca | |
12 | 4 11 | mprgbir | |