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 = x X x × C
2ndresdju.a φ A V
2ndresdju.x φ X W
2ndresdju.1 φ Disj x X C
2ndresdju.2 φ x X C = A
Assertion 2ndresdjuf1o φ 2 nd U : U 1-1 onto A

Proof

Step Hyp Ref Expression
1 2ndresdju.u U = x X x × C
2 2ndresdju.a φ A V
3 2ndresdju.x φ X W
4 2ndresdju.1 φ Disj x X C
5 2ndresdju.2 φ x X C = A
6 1 2 3 4 5 2ndresdju φ 2 nd U : U 1-1 A
7 1 iunfo 2 nd U : U onto x X C
8 foeq3 x X C = A 2 nd U : U onto x X C 2 nd U : U onto A
9 8 biimpa x X C = A 2 nd U : U onto x X C 2 nd U : U onto A
10 5 7 9 sylancl φ 2 nd U : U onto A
11 df-f1o 2 nd U : U 1-1 onto A 2 nd U : U 1-1 A 2 nd U : U onto A
12 6 10 11 sylanbrc φ 2 nd U : U 1-1 onto A