Step | Hyp | Ref
| Expression |
1 | | ffrn 6521 |
. . 3
⊢ (𝐹:𝐴⟶𝐵 → 𝐹:𝐴⟶ran 𝐹) |
2 | | f2ndf 7810 |
. . 3
⊢ (𝐹:𝐴⟶ran 𝐹 → (2nd ↾ 𝐹):𝐹⟶ran 𝐹) |
3 | 1, 2 | syl 17 |
. 2
⊢ (𝐹:𝐴⟶𝐵 → (2nd ↾ 𝐹):𝐹⟶ran 𝐹) |
4 | | ffn 6509 |
. . . . 5
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) |
5 | | dffn3 6520 |
. . . . . 6
⊢ (𝐹 Fn 𝐴 ↔ 𝐹:𝐴⟶ran 𝐹) |
6 | 5, 2 | sylbi 219 |
. . . . 5
⊢ (𝐹 Fn 𝐴 → (2nd ↾ 𝐹):𝐹⟶ran 𝐹) |
7 | 4, 6 | syl 17 |
. . . 4
⊢ (𝐹:𝐴⟶𝐵 → (2nd ↾ 𝐹):𝐹⟶ran 𝐹) |
8 | 7 | frnd 6516 |
. . 3
⊢ (𝐹:𝐴⟶𝐵 → ran (2nd ↾ 𝐹) ⊆ ran 𝐹) |
9 | | elrn2g 5756 |
. . . . . 6
⊢ (𝑦 ∈ ran 𝐹 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥〈𝑥, 𝑦〉 ∈ 𝐹)) |
10 | 9 | ibi 269 |
. . . . 5
⊢ (𝑦 ∈ ran 𝐹 → ∃𝑥〈𝑥, 𝑦〉 ∈ 𝐹) |
11 | | fvres 6684 |
. . . . . . . . . 10
⊢
(〈𝑥, 𝑦〉 ∈ 𝐹 → ((2nd ↾ 𝐹)‘〈𝑥, 𝑦〉) = (2nd ‘〈𝑥, 𝑦〉)) |
12 | 11 | adantl 484 |
. . . . . . . . 9
⊢ ((𝐹:𝐴⟶𝐵 ∧ 〈𝑥, 𝑦〉 ∈ 𝐹) → ((2nd ↾ 𝐹)‘〈𝑥, 𝑦〉) = (2nd ‘〈𝑥, 𝑦〉)) |
13 | | vex 3498 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
14 | | vex 3498 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
15 | 13, 14 | op2nd 7692 |
. . . . . . . . 9
⊢
(2nd ‘〈𝑥, 𝑦〉) = 𝑦 |
16 | 12, 15 | syl6req 2873 |
. . . . . . . 8
⊢ ((𝐹:𝐴⟶𝐵 ∧ 〈𝑥, 𝑦〉 ∈ 𝐹) → 𝑦 = ((2nd ↾ 𝐹)‘〈𝑥, 𝑦〉)) |
17 | | f2ndf 7810 |
. . . . . . . . . 10
⊢ (𝐹:𝐴⟶𝐵 → (2nd ↾ 𝐹):𝐹⟶𝐵) |
18 | 17 | ffnd 6510 |
. . . . . . . . 9
⊢ (𝐹:𝐴⟶𝐵 → (2nd ↾ 𝐹) Fn 𝐹) |
19 | | fnfvelrn 6843 |
. . . . . . . . 9
⊢
(((2nd ↾ 𝐹) Fn 𝐹 ∧ 〈𝑥, 𝑦〉 ∈ 𝐹) → ((2nd ↾ 𝐹)‘〈𝑥, 𝑦〉) ∈ ran (2nd ↾
𝐹)) |
20 | 18, 19 | sylan 582 |
. . . . . . . 8
⊢ ((𝐹:𝐴⟶𝐵 ∧ 〈𝑥, 𝑦〉 ∈ 𝐹) → ((2nd ↾ 𝐹)‘〈𝑥, 𝑦〉) ∈ ran (2nd ↾
𝐹)) |
21 | 16, 20 | eqeltrd 2913 |
. . . . . . 7
⊢ ((𝐹:𝐴⟶𝐵 ∧ 〈𝑥, 𝑦〉 ∈ 𝐹) → 𝑦 ∈ ran (2nd ↾ 𝐹)) |
22 | 21 | ex 415 |
. . . . . 6
⊢ (𝐹:𝐴⟶𝐵 → (〈𝑥, 𝑦〉 ∈ 𝐹 → 𝑦 ∈ ran (2nd ↾ 𝐹))) |
23 | 22 | exlimdv 1930 |
. . . . 5
⊢ (𝐹:𝐴⟶𝐵 → (∃𝑥〈𝑥, 𝑦〉 ∈ 𝐹 → 𝑦 ∈ ran (2nd ↾ 𝐹))) |
24 | 10, 23 | syl5 34 |
. . . 4
⊢ (𝐹:𝐴⟶𝐵 → (𝑦 ∈ ran 𝐹 → 𝑦 ∈ ran (2nd ↾ 𝐹))) |
25 | 24 | ssrdv 3973 |
. . 3
⊢ (𝐹:𝐴⟶𝐵 → ran 𝐹 ⊆ ran (2nd ↾ 𝐹)) |
26 | 8, 25 | eqssd 3984 |
. 2
⊢ (𝐹:𝐴⟶𝐵 → ran (2nd ↾ 𝐹) = ran 𝐹) |
27 | | dffo2 6589 |
. 2
⊢
((2nd ↾ 𝐹):𝐹–onto→ran 𝐹 ↔ ((2nd ↾ 𝐹):𝐹⟶ran 𝐹 ∧ ran (2nd ↾ 𝐹) = ran 𝐹)) |
28 | 3, 26, 27 | sylanbrc 585 |
1
⊢ (𝐹:𝐴⟶𝐵 → (2nd ↾ 𝐹):𝐹–onto→ran 𝐹) |