This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 2ndresdjuf1o

Description: The 2nd function restricted to a disjoint union is a bijection. See also e.g. 2ndconst . (Contributed by Thierry Arnoux, 23-Jun-2024)

Ref Expression
Hypotheses 2ndresdju.u 
|- U = U_ x e. X ( { x } X. C )
2ndresdju.a 
|- ( ph -> A e. V )
2ndresdju.x 
|- ( ph -> X e. W )
2ndresdju.1 
|- ( ph -> Disj_ x e. X C )
2ndresdju.2 
|- ( ph -> U_ x e. X C = A )
Assertion 2ndresdjuf1o 
|- ( ph -> ( 2nd |` U ) : U -1-1-onto-> A )

Proof

Step Hyp Ref Expression
1 2ndresdju.u 
 |-  U = U_ x e. X ( { x } X. C )
2 2ndresdju.a 
 |-  ( ph -> A e. V )
3 2ndresdju.x 
 |-  ( ph -> X e. W )
4 2ndresdju.1 
 |-  ( ph -> Disj_ x e. X C )
5 2ndresdju.2 
 |-  ( ph -> U_ x e. X C = A )
6 1 2 3 4 5 2ndresdju 
 |-  ( ph -> ( 2nd |` U ) : U -1-1-> A )
7 1 iunfo 
 |-  ( 2nd |` U ) : U -onto-> U_ x e. X C
8 foeq3 
 |-  ( U_ x e. X C = A -> ( ( 2nd |` U ) : U -onto-> U_ x e. X C <-> ( 2nd |` U ) : U -onto-> A ) )
9 8 biimpa 
 |-  ( ( U_ x e. X C = A /\ ( 2nd |` U ) : U -onto-> U_ x e. X C ) -> ( 2nd |` U ) : U -onto-> A )
10 5 7 9 sylancl 
 |-  ( ph -> ( 2nd |` U ) : U -onto-> A )
11 df-f1o 
 |-  ( ( 2nd |` U ) : U -1-1-onto-> A <-> ( ( 2nd |` U ) : U -1-1-> A /\ ( 2nd |` U ) : U -onto-> A ) )
12 6 10 11 sylanbrc 
 |-  ( ph -> ( 2nd |` U ) : U -1-1-onto-> A )