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 )