Step | Hyp | Ref
| Expression |
1 | | dffo2 6596 |
. 2
⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ran 𝐹 = 𝐵)) |
2 | | ffn 6504 |
. . . . 5
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) |
3 | | fnrnfv 6729 |
. . . . . . 7
⊢ (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑤 ∈ 𝐴 𝑦 = (𝐹‘𝑤)}) |
4 | | dffo3f.1 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥𝐹 |
5 | | nfcv 2899 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥𝑤 |
6 | 4, 5 | nffv 6684 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝐹‘𝑤) |
7 | 6 | nfeq2 2916 |
. . . . . . . . 9
⊢
Ⅎ𝑥 𝑦 = (𝐹‘𝑤) |
8 | | nfv 1921 |
. . . . . . . . 9
⊢
Ⅎ𝑤 𝑦 = (𝐹‘𝑥) |
9 | | fveq2 6674 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑥 → (𝐹‘𝑤) = (𝐹‘𝑥)) |
10 | 9 | eqeq2d 2749 |
. . . . . . . . 9
⊢ (𝑤 = 𝑥 → (𝑦 = (𝐹‘𝑤) ↔ 𝑦 = (𝐹‘𝑥))) |
11 | 7, 8, 10 | cbvrexw 3341 |
. . . . . . . 8
⊢
(∃𝑤 ∈
𝐴 𝑦 = (𝐹‘𝑤) ↔ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)) |
12 | 11 | abbii 2803 |
. . . . . . 7
⊢ {𝑦 ∣ ∃𝑤 ∈ 𝐴 𝑦 = (𝐹‘𝑤)} = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} |
13 | 3, 12 | eqtrdi 2789 |
. . . . . 6
⊢ (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)}) |
14 | 13 | eqeq1d 2740 |
. . . . 5
⊢ (𝐹 Fn 𝐴 → (ran 𝐹 = 𝐵 ↔ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} = 𝐵)) |
15 | 2, 14 | syl 17 |
. . . 4
⊢ (𝐹:𝐴⟶𝐵 → (ran 𝐹 = 𝐵 ↔ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} = 𝐵)) |
16 | | dfbi2 478 |
. . . . . . 7
⊢
((∃𝑥 ∈
𝐴 𝑦 = (𝐹‘𝑥) ↔ 𝑦 ∈ 𝐵) ↔ ((∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) → 𝑦 ∈ 𝐵) ∧ (𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)))) |
17 | | nfcv 2899 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝐴 |
18 | | nfcv 2899 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝐵 |
19 | 4, 17, 18 | nff 6500 |
. . . . . . . . 9
⊢
Ⅎ𝑥 𝐹:𝐴⟶𝐵 |
20 | | nfv 1921 |
. . . . . . . . 9
⊢
Ⅎ𝑥 𝑦 ∈ 𝐵 |
21 | | simpr 488 |
. . . . . . . . . 10
⊢ (((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 = (𝐹‘𝑥)) → 𝑦 = (𝐹‘𝑥)) |
22 | | ffvelrn 6859 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵) |
23 | 22 | adantr 484 |
. . . . . . . . . 10
⊢ (((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 = (𝐹‘𝑥)) → (𝐹‘𝑥) ∈ 𝐵) |
24 | 21, 23 | eqeltrd 2833 |
. . . . . . . . 9
⊢ (((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 = (𝐹‘𝑥)) → 𝑦 ∈ 𝐵) |
25 | 19, 20, 24 | rexlimd3 42231 |
. . . . . . . 8
⊢ (𝐹:𝐴⟶𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) → 𝑦 ∈ 𝐵)) |
26 | 25 | biantrurd 536 |
. . . . . . 7
⊢ (𝐹:𝐴⟶𝐵 → ((𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)) ↔ ((∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) → 𝑦 ∈ 𝐵) ∧ (𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥))))) |
27 | 16, 26 | bitr4id 293 |
. . . . . 6
⊢ (𝐹:𝐴⟶𝐵 → ((∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) ↔ 𝑦 ∈ 𝐵) ↔ (𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)))) |
28 | 27 | albidv 1927 |
. . . . 5
⊢ (𝐹:𝐴⟶𝐵 → (∀𝑦(∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) ↔ 𝑦 ∈ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)))) |
29 | | abeq1 2865 |
. . . . 5
⊢ ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} = 𝐵 ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) ↔ 𝑦 ∈ 𝐵)) |
30 | | df-ral 3058 |
. . . . 5
⊢
(∀𝑦 ∈
𝐵 ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) ↔ ∀𝑦(𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥))) |
31 | 28, 29, 30 | 3bitr4g 317 |
. . . 4
⊢ (𝐹:𝐴⟶𝐵 → ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} = 𝐵 ↔ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥))) |
32 | 15, 31 | bitrd 282 |
. . 3
⊢ (𝐹:𝐴⟶𝐵 → (ran 𝐹 = 𝐵 ↔ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥))) |
33 | 32 | pm5.32i 578 |
. 2
⊢ ((𝐹:𝐴⟶𝐵 ∧ ran 𝐹 = 𝐵) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥))) |
34 | 1, 33 | bitri 278 |
1
⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥))) |