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 inlA:AA⊔︀B

Proof

Step Hyp Ref Expression
1 djulf1o inl:V1-1 onto×V
2 f1ofun inl:V1-1 onto×VFuninl
3 ffvresb FuninlinlA:AA⊔︀BxAxdominlinlxA⊔︀B
4 1 2 3 mp2b inlA:AA⊔︀BxAxdominlinlxA⊔︀B
5 elex xAxV
6 opex xV
7 df-inl inl=xVx
8 6 7 dmmpti dominl=V
9 5 8 eleqtrrdi xAxdominl
10 djulcl xAinlxA⊔︀B
11 9 10 jca xAxdominlinlxA⊔︀B
12 4 11 mprgbir inlA:AA⊔︀B