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 ⊢ 𝑈 = ∪ 𝑥 ∈ 𝑋 ( { 𝑥 } × 𝐶 )
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→ 𝐴 )