Theorem fo2ndf 8071

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

Assertion

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

Proof of Theorem fo2ndf

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ffrn 6681	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹:𝐴⟶ran 𝐹)
2		f2ndf 8070	. . 3 ⊢ (𝐹:𝐴⟶ran 𝐹 → (2nd ↾ 𝐹):𝐹⟶ran 𝐹)
3	1, 2	syl 17	. 2 ⊢ (𝐹:𝐴⟶𝐵 → (2nd ↾ 𝐹):𝐹⟶ran 𝐹)
4		ffn 6668	. . . . 5 ⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴)
5		dffn3 6680	. . . . . 6 ⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶ran 𝐹)
6	5, 2	sylbi 217	. . . . 5 ⊢ (𝐹 Fn 𝐴 → (2nd ↾ 𝐹):𝐹⟶ran 𝐹)
7	4, 6	syl 17	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → (2nd ↾ 𝐹):𝐹⟶ran 𝐹)
8	7	frnd 6676	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → ran (2nd ↾ 𝐹) ⊆ ran 𝐹)
9		elrn2g 5845	. . . . . 6 ⊢ (𝑦 ∈ ran 𝐹 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐹))
10	9	ibi 267	. . . . 5 ⊢ (𝑦 ∈ ran 𝐹 → ∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐹)
11		fvres 6859	. . . . . . . . . 10 ⊢ (⟨𝑥, 𝑦⟩ ∈ 𝐹 → ((2nd ↾ 𝐹)‘⟨𝑥, 𝑦⟩) = (2nd ‘⟨𝑥, 𝑦⟩))
12	11	adantl 481	. . . . . . . . 9 ⊢ ((𝐹:𝐴⟶𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐹) → ((2nd ↾ 𝐹)‘⟨𝑥, 𝑦⟩) = (2nd ‘⟨𝑥, 𝑦⟩))
13		vex 3433	. . . . . . . . . 10 ⊢ 𝑥 ∈ V
14		vex 3433	. . . . . . . . . 10 ⊢ 𝑦 ∈ V
15	13, 14	op2nd 7951	. . . . . . . . 9 ⊢ (2nd ‘⟨𝑥, 𝑦⟩) = 𝑦
16	12, 15	eqtr2di 2788	. . . . . . . 8 ⊢ ((𝐹:𝐴⟶𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐹) → 𝑦 = ((2nd ↾ 𝐹)‘⟨𝑥, 𝑦⟩))
17		f2ndf 8070	. . . . . . . . . 10 ⊢ (𝐹:𝐴⟶𝐵 → (2nd ↾ 𝐹):𝐹⟶𝐵)
18	17	ffnd 6669	. . . . . . . . 9 ⊢ (𝐹:𝐴⟶𝐵 → (2nd ↾ 𝐹) Fn 𝐹)
19		fnfvelrn 7032	. . . . . . . . 9 ⊢ (((2nd ↾ 𝐹) Fn 𝐹 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐹) → ((2nd ↾ 𝐹)‘⟨𝑥, 𝑦⟩) ∈ ran (2nd ↾ 𝐹))
20	18, 19	sylan 581	. . . . . . . 8 ⊢ ((𝐹:𝐴⟶𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐹) → ((2nd ↾ 𝐹)‘⟨𝑥, 𝑦⟩) ∈ ran (2nd ↾ 𝐹))
21	16, 20	eqeltrd 2836	. . . . . . 7 ⊢ ((𝐹:𝐴⟶𝐵 ∧ ⟨𝑥, 𝑦⟩ ∈ 𝐹) → 𝑦 ∈ ran (2nd ↾ 𝐹))
22	21	ex 412	. . . . . 6 ⊢ (𝐹:𝐴⟶𝐵 → (⟨𝑥, 𝑦⟩ ∈ 𝐹 → 𝑦 ∈ ran (2nd ↾ 𝐹)))
23	22	exlimdv 1935	. . . . 5 ⊢ (𝐹:𝐴⟶𝐵 → (∃𝑥⟨𝑥, 𝑦⟩ ∈ 𝐹 → 𝑦 ∈ ran (2nd ↾ 𝐹)))
24	10, 23	syl5 34	. . . 4 ⊢ (𝐹:𝐴⟶𝐵 → (𝑦 ∈ ran 𝐹 → 𝑦 ∈ ran (2nd ↾ 𝐹)))
25	24	ssrdv 3927	. . 3 ⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ ran (2nd ↾ 𝐹))
26	8, 25	eqssd 3939	. 2 ⊢ (𝐹:𝐴⟶𝐵 → ran (2nd ↾ 𝐹) = ran 𝐹)
27		dffo2 6756	. 2 ⊢ ((2nd ↾ 𝐹):𝐹–onto→ran 𝐹 ↔ ((2nd ↾ 𝐹):𝐹⟶ran 𝐹 ∧ ran (2nd ↾ 𝐹) = ran 𝐹))
28	3, 26, 27	sylanbrc 584	1 ⊢ (𝐹:𝐴⟶𝐵 → (2nd ↾ 𝐹):𝐹–onto→ran 𝐹)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1542  ∃wex 1781   ∈ wcel 2114  ⟨cop 4573  ran crn 5632   ↾ cres 5633   Fn wfn 6493  ⟶wf 6494  –onto→wfo 6496  ‘cfv 6498  2^nd c2nd 7941

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-sep 5231  ax-nul 5241  ax-pr 5375  ax-un 7689

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-fo 6504  df-fv 6506  df-2nd 7943

This theorem is referenced by:  f1o2ndf1  8072