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

Proof

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