| Step | Hyp | Ref
| Expression |
| 1 | | dffo2 6824 |
. 2
⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ran 𝐹 = 𝐵)) |
| 2 | | ffn 6736 |
. . . . 5
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) |
| 3 | | fnrnfv 6968 |
. . . . . . 7
⊢ (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑤 ∈ 𝐴 𝑦 = (𝐹‘𝑤)}) |
| 4 | | dffo3f.1 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥𝐹 |
| 5 | | nfcv 2905 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥𝑤 |
| 6 | 4, 5 | nffv 6916 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝐹‘𝑤) |
| 7 | 6 | nfeq2 2923 |
. . . . . . . . 9
⊢
Ⅎ𝑥 𝑦 = (𝐹‘𝑤) |
| 8 | | nfv 1914 |
. . . . . . . . 9
⊢
Ⅎ𝑤 𝑦 = (𝐹‘𝑥) |
| 9 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑥 → (𝐹‘𝑤) = (𝐹‘𝑥)) |
| 10 | 9 | eqeq2d 2748 |
. . . . . . . . 9
⊢ (𝑤 = 𝑥 → (𝑦 = (𝐹‘𝑤) ↔ 𝑦 = (𝐹‘𝑥))) |
| 11 | 7, 8, 10 | cbvrexw 3307 |
. . . . . . . 8
⊢
(∃𝑤 ∈
𝐴 𝑦 = (𝐹‘𝑤) ↔ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)) |
| 12 | 11 | abbii 2809 |
. . . . . . 7
⊢ {𝑦 ∣ ∃𝑤 ∈ 𝐴 𝑦 = (𝐹‘𝑤)} = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} |
| 13 | 3, 12 | eqtrdi 2793 |
. . . . . 6
⊢ (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)}) |
| 14 | 13 | eqeq1d 2739 |
. . . . 5
⊢ (𝐹 Fn 𝐴 → (ran 𝐹 = 𝐵 ↔ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} = 𝐵)) |
| 15 | 2, 14 | syl 17 |
. . . 4
⊢ (𝐹:𝐴⟶𝐵 → (ran 𝐹 = 𝐵 ↔ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} = 𝐵)) |
| 16 | | dfbi2 474 |
. . . . . . 7
⊢
((∃𝑥 ∈
𝐴 𝑦 = (𝐹‘𝑥) ↔ 𝑦 ∈ 𝐵) ↔ ((∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) → 𝑦 ∈ 𝐵) ∧ (𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)))) |
| 17 | | nfcv 2905 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝐴 |
| 18 | | nfcv 2905 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝐵 |
| 19 | 4, 17, 18 | nff 6732 |
. . . . . . . . 9
⊢
Ⅎ𝑥 𝐹:𝐴⟶𝐵 |
| 20 | | nfv 1914 |
. . . . . . . . 9
⊢
Ⅎ𝑥 𝑦 ∈ 𝐵 |
| 21 | | simpr 484 |
. . . . . . . . . . 11
⊢ (((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 = (𝐹‘𝑥)) → 𝑦 = (𝐹‘𝑥)) |
| 22 | | ffvelcdm 7101 |
. . . . . . . . . . . 12
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵) |
| 23 | 22 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 = (𝐹‘𝑥)) → (𝐹‘𝑥) ∈ 𝐵) |
| 24 | 21, 23 | eqeltrd 2841 |
. . . . . . . . . 10
⊢ (((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 = (𝐹‘𝑥)) → 𝑦 ∈ 𝐵) |
| 25 | 24 | exp31 419 |
. . . . . . . . 9
⊢ (𝐹:𝐴⟶𝐵 → (𝑥 ∈ 𝐴 → (𝑦 = (𝐹‘𝑥) → 𝑦 ∈ 𝐵))) |
| 26 | 19, 20, 25 | rexlimd 3266 |
. . . . . . . 8
⊢ (𝐹:𝐴⟶𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) → 𝑦 ∈ 𝐵)) |
| 27 | 26 | biantrurd 532 |
. . . . . . 7
⊢ (𝐹:𝐴⟶𝐵 → ((𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)) ↔ ((∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) → 𝑦 ∈ 𝐵) ∧ (𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥))))) |
| 28 | 16, 27 | bitr4id 290 |
. . . . . 6
⊢ (𝐹:𝐴⟶𝐵 → ((∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) ↔ 𝑦 ∈ 𝐵) ↔ (𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)))) |
| 29 | 28 | albidv 1920 |
. . . . 5
⊢ (𝐹:𝐴⟶𝐵 → (∀𝑦(∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) ↔ 𝑦 ∈ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)))) |
| 30 | | eqabcb 2883 |
. . . . 5
⊢ ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} = 𝐵 ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) ↔ 𝑦 ∈ 𝐵)) |
| 31 | | df-ral 3062 |
. . . . 5
⊢
(∀𝑦 ∈
𝐵 ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) ↔ ∀𝑦(𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥))) |
| 32 | 29, 30, 31 | 3bitr4g 314 |
. . . 4
⊢ (𝐹:𝐴⟶𝐵 → ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} = 𝐵 ↔ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥))) |
| 33 | 15, 32 | bitrd 279 |
. . 3
⊢ (𝐹:𝐴⟶𝐵 → (ran 𝐹 = 𝐵 ↔ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥))) |
| 34 | 33 | pm5.32i 574 |
. 2
⊢ ((𝐹:𝐴⟶𝐵 ∧ ran 𝐹 = 𝐵) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥))) |
| 35 | 1, 34 | bitri 275 |
1
⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥))) |