Step | Hyp | Ref
| Expression |
1 | | dffo2 6838 |
. 2
⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ran 𝐹 = 𝐵)) |
2 | | ffn 6747 |
. . . . 5
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) |
3 | | fnrnfv 6981 |
. . . . . . 7
⊢ (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑤 ∈ 𝐴 𝑦 = (𝐹‘𝑤)}) |
4 | | dffo3f.1 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥𝐹 |
5 | | nfcv 2908 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥𝑤 |
6 | 4, 5 | nffv 6930 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝐹‘𝑤) |
7 | 6 | nfeq2 2926 |
. . . . . . . . 9
⊢
Ⅎ𝑥 𝑦 = (𝐹‘𝑤) |
8 | | nfv 1913 |
. . . . . . . . 9
⊢
Ⅎ𝑤 𝑦 = (𝐹‘𝑥) |
9 | | fveq2 6920 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑥 → (𝐹‘𝑤) = (𝐹‘𝑥)) |
10 | 9 | eqeq2d 2751 |
. . . . . . . . 9
⊢ (𝑤 = 𝑥 → (𝑦 = (𝐹‘𝑤) ↔ 𝑦 = (𝐹‘𝑥))) |
11 | 7, 8, 10 | cbvrexw 3313 |
. . . . . . . 8
⊢
(∃𝑤 ∈
𝐴 𝑦 = (𝐹‘𝑤) ↔ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)) |
12 | 11 | abbii 2812 |
. . . . . . 7
⊢ {𝑦 ∣ ∃𝑤 ∈ 𝐴 𝑦 = (𝐹‘𝑤)} = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} |
13 | 3, 12 | eqtrdi 2796 |
. . . . . 6
⊢ (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)}) |
14 | 13 | eqeq1d 2742 |
. . . . 5
⊢ (𝐹 Fn 𝐴 → (ran 𝐹 = 𝐵 ↔ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} = 𝐵)) |
15 | 2, 14 | syl 17 |
. . . 4
⊢ (𝐹:𝐴⟶𝐵 → (ran 𝐹 = 𝐵 ↔ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} = 𝐵)) |
16 | | dfbi2 474 |
. . . . . . 7
⊢
((∃𝑥 ∈
𝐴 𝑦 = (𝐹‘𝑥) ↔ 𝑦 ∈ 𝐵) ↔ ((∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) → 𝑦 ∈ 𝐵) ∧ (𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)))) |
17 | | nfcv 2908 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝐴 |
18 | | nfcv 2908 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝐵 |
19 | 4, 17, 18 | nff 6743 |
. . . . . . . . 9
⊢
Ⅎ𝑥 𝐹:𝐴⟶𝐵 |
20 | | nfv 1913 |
. . . . . . . . 9
⊢
Ⅎ𝑥 𝑦 ∈ 𝐵 |
21 | | simpr 484 |
. . . . . . . . . . 11
⊢ (((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 = (𝐹‘𝑥)) → 𝑦 = (𝐹‘𝑥)) |
22 | | ffvelcdm 7115 |
. . . . . . . . . . . 12
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵) |
23 | 22 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 = (𝐹‘𝑥)) → (𝐹‘𝑥) ∈ 𝐵) |
24 | 21, 23 | eqeltrd 2844 |
. . . . . . . . . 10
⊢ (((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 = (𝐹‘𝑥)) → 𝑦 ∈ 𝐵) |
25 | 24 | exp31 419 |
. . . . . . . . 9
⊢ (𝐹:𝐴⟶𝐵 → (𝑥 ∈ 𝐴 → (𝑦 = (𝐹‘𝑥) → 𝑦 ∈ 𝐵))) |
26 | 19, 20, 25 | rexlimd 3272 |
. . . . . . . 8
⊢ (𝐹:𝐴⟶𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) → 𝑦 ∈ 𝐵)) |
27 | 26 | biantrurd 532 |
. . . . . . 7
⊢ (𝐹:𝐴⟶𝐵 → ((𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)) ↔ ((∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) → 𝑦 ∈ 𝐵) ∧ (𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥))))) |
28 | 16, 27 | bitr4id 290 |
. . . . . 6
⊢ (𝐹:𝐴⟶𝐵 → ((∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) ↔ 𝑦 ∈ 𝐵) ↔ (𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)))) |
29 | 28 | albidv 1919 |
. . . . 5
⊢ (𝐹:𝐴⟶𝐵 → (∀𝑦(∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) ↔ 𝑦 ∈ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)))) |
30 | | eqabcb 2886 |
. . . . 5
⊢ ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} = 𝐵 ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) ↔ 𝑦 ∈ 𝐵)) |
31 | | df-ral 3068 |
. . . . 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→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥))) |