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	⊢ 𝑈 = ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 )
	2ndresdju.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
	2ndresdju.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑊 )
	2ndresdju.1	⊢ ( 𝜑 → Disj 𝑥 ∈ 𝑋 𝐶 )
	2ndresdju.2	⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝑋 𝐶 = 𝐴 )
Assertion	2ndresdjuf1o	⊢ ( 𝜑 → ( 2nd ↾ 𝑈 ) : 𝑈 –1-1-onto→ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		2ndresdju.u	⊢ 𝑈 = ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 )
2		2ndresdju.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
3		2ndresdju.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑊 )
4		2ndresdju.1	⊢ ( 𝜑 → Disj 𝑥 ∈ 𝑋 𝐶 )
5		2ndresdju.2	⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝑋 𝐶 = 𝐴 )
6	1 2 3 4 5	2ndresdju	⊢ ( 𝜑 → ( 2nd ↾ 𝑈 ) : 𝑈 –1-1→ 𝐴 )
7	1	iunfo	⊢ ( 2nd ↾ 𝑈 ) : 𝑈 –onto→ ∪ 𝑥 ∈ 𝑋 𝐶
8		foeq3	⊢ ( ∪ 𝑥 ∈ 𝑋 𝐶 = 𝐴 → ( ( 2nd ↾ 𝑈 ) : 𝑈 –onto→ ∪ 𝑥 ∈ 𝑋 𝐶 ↔ ( 2nd ↾ 𝑈 ) : 𝑈 –onto→ 𝐴 ) )
9	8	biimpa	⊢ ( ( ∪ 𝑥 ∈ 𝑋 𝐶 = 𝐴 ∧ ( 2nd ↾ 𝑈 ) : 𝑈 –onto→ ∪ 𝑥 ∈ 𝑋 𝐶 ) → ( 2nd ↾ 𝑈 ) : 𝑈 –onto→ 𝐴 )
10	5 7 9	sylancl	⊢ ( 𝜑 → ( 2nd ↾ 𝑈 ) : 𝑈 –onto→ 𝐴 )
11		df-f1o	⊢ ( ( 2nd ↾ 𝑈 ) : 𝑈 –1-1-onto→ 𝐴 ↔ ( ( 2nd ↾ 𝑈 ) : 𝑈 –1-1→ 𝐴 ∧ ( 2nd ↾ 𝑈 ) : 𝑈 –onto→ 𝐴 ) )
12	6 10 11	sylanbrc	⊢ ( 𝜑 → ( 2nd ↾ 𝑈 ) : 𝑈 –1-1-onto→ 𝐴 )