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 𝐹 )