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=\bigcup _{x\in X}\left(\left\{x\right\}\times C\right)$$
	2ndresdju.a	$$⊢\phi \to A\in V$$
	2ndresdju.x	$$⊢\phi \to X\in W$$
	2ndresdju.1	$$⊢\phi \to \underset{x\in X}{Disj}C$$
	2ndresdju.2	$$⊢\phi \to \bigcup _{x\in X}C=A$$
Assertion	2ndresdjuf1o	$$⊢\phi \to \left({2^{nd}\upharpoonright }_U\right):U\underset{1-1\; onto}{⟶}A$$

Proof

Step	Hyp	Ref	Expression
1		2ndresdju.u	$$⊢U=\bigcup _{x\in X}\left(\left\{x\right\}\times C\right)$$
2		2ndresdju.a	$$⊢\phi \to A\in V$$
3		2ndresdju.x	$$⊢\phi \to X\in W$$
4		2ndresdju.1	$$⊢\phi \to \underset{x\in X}{Disj}C$$
5		2ndresdju.2	$$⊢\phi \to \bigcup _{x\in X}C=A$$
6	1 2 3 4 5	2ndresdju	$$⊢\phi \to \left({2^{nd}\upharpoonright }_U\right):U\underset{1-1}{⟶}A$$
7	1	iunfo	$$⊢\left({2^{nd}\upharpoonright }_U\right):U\underset{onto}{⟶}\bigcup _{x\in X}C$$
8		foeq3	$$⊢\bigcup _{x\in X}C=A\to \left(\left({2^{nd}\upharpoonright }_U\right):U\underset{onto}{⟶}\bigcup _{x\in X}C\leftrightarrow \left({2^{nd}\upharpoonright }_U\right):U\underset{onto}{⟶}A\right)$$
9	8	biimpa	$$⊢\left(\bigcup _{x\in X}C=A\wedge \left({2^{nd}\upharpoonright }_U\right):U\underset{onto}{⟶}\bigcup _{x\in X}C\right)\to \left({2^{nd}\upharpoonright }_U\right):U\underset{onto}{⟶}A$$
10	5 7 9	sylancl	$$⊢\phi \to \left({2^{nd}\upharpoonright }_U\right):U\underset{onto}{⟶}A$$
11		df-f1o	$$⊢\left({2^{nd}\upharpoonright }_U\right):U\underset{1-1\; onto}{⟶}A\leftrightarrow \left(\left({2^{nd}\upharpoonright }_U\right):U\underset{1-1}{⟶}A\wedge \left({2^{nd}\upharpoonright }_U\right):U\underset{onto}{⟶}A\right)$$
12	6 10 11	sylanbrc	$$⊢\phi \to \left({2^{nd}\upharpoonright }_U\right):U\underset{1-1\; onto}{⟶}A$$