Metamath Proof Explorer


Theorem fun11uni

Description: The union of a chain (with respect to inclusion) of one-to-one functions is a one-to-one function. (Contributed by NM, 11-Aug-2004)

Ref Expression
Assertion fun11uni f A Fun f Fun f -1 g A f g g f Fun A Fun A -1

Proof

Step Hyp Ref Expression
1 simpl Fun f Fun f -1 Fun f
2 1 anim1i Fun f Fun f -1 g A f g g f Fun f g A f g g f
3 2 ralimi f A Fun f Fun f -1 g A f g g f f A Fun f g A f g g f
4 fununi f A Fun f g A f g g f Fun A
5 3 4 syl f A Fun f Fun f -1 g A f g g f Fun A
6 simpr Fun f Fun f -1 Fun f -1
7 6 anim1i Fun f Fun f -1 g A f g g f Fun f -1 g A f g g f
8 7 ralimi f A Fun f Fun f -1 g A f g g f f A Fun f -1 g A f g g f
9 funcnvuni f A Fun f -1 g A f g g f Fun A -1
10 8 9 syl f A Fun f Fun f -1 g A f g g f Fun A -1
11 5 10 jca f A Fun f Fun f -1 g A f g g f Fun A Fun A -1