This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem fo2ndf

Description: The 2nd (second component of an ordered pair) function restricted to a function F is a function from F onto the range of F . (Contributed by Alexander van der Vekens, 4-Feb-2018)

Ref Expression
Assertion fo2ndf ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 2nd ↾ 𝐹 ) : 𝐹 –onto→ ran 𝐹 )

Proof

Step Hyp Ref Expression
1 ffrn ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 : 𝐴 ⟶ ran 𝐹 )
2 f2ndf ⊢ ( 𝐹 : 𝐴 ⟶ ran 𝐹 → ( 2nd ↾ 𝐹 ) : 𝐹 ⟶ ran 𝐹 )
3 1 2 syl ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 2nd ↾ 𝐹 ) : 𝐹 ⟶ ran 𝐹 )
4 ffn ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 Fn 𝐴 )
5 dffn3 ⊢ ( 𝐹 Fn 𝐴 ↔ 𝐹 : 𝐴 ⟶ ran 𝐹 )
6 5 2 sylbi ⊢ ( 𝐹 Fn 𝐴 → ( 2nd ↾ 𝐹 ) : 𝐹 ⟶ ran 𝐹 )
7 4 6 syl ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 2nd ↾ 𝐹 ) : 𝐹 ⟶ ran 𝐹 )
8 7 frnd ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ran ( 2nd ↾ 𝐹 ) ⊆ ran 𝐹 )
9 elrn2g ⊢ ( 𝑦 ∈ ran 𝐹 → ( 𝑦 ∈ ran 𝐹 ↔ ∃ 𝑥 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) )
10 9 ibi ⊢ ( 𝑦 ∈ ran 𝐹 → ∃ 𝑥 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 )
11 fvres ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → ( ( 2nd ↾ 𝐹 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = ( 2nd ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
12 11 adantl ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) → ( ( 2nd ↾ 𝐹 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = ( 2nd ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
13 vex ⊢ 𝑥 ∈ V
14 vex ⊢ 𝑦 ∈ V
15 13 14 op2nd ⊢ ( 2nd ‘ ⟨ 𝑥 , 𝑦 ⟩ ) = 𝑦
16 12 15 eqtr2di ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) → 𝑦 = ( ( 2nd ↾ 𝐹 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) )
17 f2ndf ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 2nd ↾ 𝐹 ) : 𝐹 ⟶ 𝐵 )
18 17 ffnd ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 2nd ↾ 𝐹 ) Fn 𝐹 )
19 fnfvelrn ⊢ ( ( ( 2nd ↾ 𝐹 ) Fn 𝐹 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) → ( ( 2nd ↾ 𝐹 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ ran ( 2nd ↾ 𝐹 ) )
20 18 19 sylan ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) → ( ( 2nd ↾ 𝐹 ) ‘ ⟨ 𝑥 , 𝑦 ⟩ ) ∈ ran ( 2nd ↾ 𝐹 ) )
21 16 20 eqeltrd ⊢ ( ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ) → 𝑦 ∈ ran ( 2nd ↾ 𝐹 ) )
22 21 ex ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → 𝑦 ∈ ran ( 2nd ↾ 𝐹 ) ) )
23 22 exlimdv ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( ∃ 𝑥 ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 → 𝑦 ∈ ran ( 2nd ↾ 𝐹 ) ) )
24 10 23 syl5 ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝑦 ∈ ran 𝐹 → 𝑦 ∈ ran ( 2nd ↾ 𝐹 ) ) )
25 24 ssrdv ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ran 𝐹 ⊆ ran ( 2nd ↾ 𝐹 ) )
26 8 25 eqssd ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ran ( 2nd ↾ 𝐹 ) = ran 𝐹 )
27 dffo2 ⊢ ( ( 2nd ↾ 𝐹 ) : 𝐹 –onto→ ran 𝐹 ↔ ( ( 2nd ↾ 𝐹 ) : 𝐹 ⟶ ran 𝐹 ∧ ran ( 2nd ↾ 𝐹 ) = ran 𝐹 ) )
28 3 26 27 sylanbrc ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 2nd ↾ 𝐹 ) : 𝐹 –onto→ ran 𝐹 )