Step | Hyp | Ref
| Expression |
1 | | dffo2 6589 |
. 2
⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ran 𝐹 = 𝐵)) |
2 | | ffn 6509 |
. . . . 5
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) |
3 | | fnrnfv 6720 |
. . . . . . 7
⊢ (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑤 ∈ 𝐴 𝑦 = (𝐹‘𝑤)}) |
4 | | dffo3f.1 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥𝐹 |
5 | | nfcv 2977 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥𝑤 |
6 | 4, 5 | nffv 6675 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝐹‘𝑤) |
7 | 6 | nfeq2 2995 |
. . . . . . . . 9
⊢
Ⅎ𝑥 𝑦 = (𝐹‘𝑤) |
8 | | nfv 1911 |
. . . . . . . . 9
⊢
Ⅎ𝑤 𝑦 = (𝐹‘𝑥) |
9 | | fveq2 6665 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑥 → (𝐹‘𝑤) = (𝐹‘𝑥)) |
10 | 9 | eqeq2d 2832 |
. . . . . . . . 9
⊢ (𝑤 = 𝑥 → (𝑦 = (𝐹‘𝑤) ↔ 𝑦 = (𝐹‘𝑥))) |
11 | 7, 8, 10 | cbvrexw 3443 |
. . . . . . . 8
⊢
(∃𝑤 ∈
𝐴 𝑦 = (𝐹‘𝑤) ↔ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)) |
12 | 11 | abbii 2886 |
. . . . . . 7
⊢ {𝑦 ∣ ∃𝑤 ∈ 𝐴 𝑦 = (𝐹‘𝑤)} = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} |
13 | 3, 12 | syl6eq 2872 |
. . . . . 6
⊢ (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)}) |
14 | 13 | eqeq1d 2823 |
. . . . 5
⊢ (𝐹 Fn 𝐴 → (ran 𝐹 = 𝐵 ↔ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} = 𝐵)) |
15 | 2, 14 | syl 17 |
. . . 4
⊢ (𝐹:𝐴⟶𝐵 → (ran 𝐹 = 𝐵 ↔ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} = 𝐵)) |
16 | | nfcv 2977 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝐴 |
17 | | nfcv 2977 |
. . . . . . . . . 10
⊢
Ⅎ𝑥𝐵 |
18 | 4, 16, 17 | nff 6505 |
. . . . . . . . 9
⊢
Ⅎ𝑥 𝐹:𝐴⟶𝐵 |
19 | | nfv 1911 |
. . . . . . . . 9
⊢
Ⅎ𝑥 𝑦 ∈ 𝐵 |
20 | | simpr 487 |
. . . . . . . . . 10
⊢ (((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 = (𝐹‘𝑥)) → 𝑦 = (𝐹‘𝑥)) |
21 | | ffvelrn 6844 |
. . . . . . . . . . 11
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵) |
22 | 21 | adantr 483 |
. . . . . . . . . 10
⊢ (((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 = (𝐹‘𝑥)) → (𝐹‘𝑥) ∈ 𝐵) |
23 | 20, 22 | eqeltrd 2913 |
. . . . . . . . 9
⊢ (((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 = (𝐹‘𝑥)) → 𝑦 ∈ 𝐵) |
24 | 18, 19, 23 | rexlimd3 41405 |
. . . . . . . 8
⊢ (𝐹:𝐴⟶𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) → 𝑦 ∈ 𝐵)) |
25 | 24 | biantrurd 535 |
. . . . . . 7
⊢ (𝐹:𝐴⟶𝐵 → ((𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)) ↔ ((∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) → 𝑦 ∈ 𝐵) ∧ (𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥))))) |
26 | | dfbi2 477 |
. . . . . . 7
⊢
((∃𝑥 ∈
𝐴 𝑦 = (𝐹‘𝑥) ↔ 𝑦 ∈ 𝐵) ↔ ((∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) → 𝑦 ∈ 𝐵) ∧ (𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)))) |
27 | 25, 26 | syl6rbbr 292 |
. . . . . 6
⊢ (𝐹:𝐴⟶𝐵 → ((∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) ↔ 𝑦 ∈ 𝐵) ↔ (𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)))) |
28 | 27 | albidv 1917 |
. . . . 5
⊢ (𝐹:𝐴⟶𝐵 → (∀𝑦(∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) ↔ 𝑦 ∈ 𝐵) ↔ ∀𝑦(𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)))) |
29 | | abeq1 2946 |
. . . . 5
⊢ ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} = 𝐵 ↔ ∀𝑦(∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) ↔ 𝑦 ∈ 𝐵)) |
30 | | df-ral 3143 |
. . . . 5
⊢
(∀𝑦 ∈
𝐵 ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) ↔ ∀𝑦(𝑦 ∈ 𝐵 → ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥))) |
31 | 28, 29, 30 | 3bitr4g 316 |
. . . 4
⊢ (𝐹:𝐴⟶𝐵 → ({𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} = 𝐵 ↔ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥))) |
32 | 15, 31 | bitrd 281 |
. . 3
⊢ (𝐹:𝐴⟶𝐵 → (ran 𝐹 = 𝐵 ↔ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥))) |
33 | 32 | pm5.32i 577 |
. 2
⊢ ((𝐹:𝐴⟶𝐵 ∧ ran 𝐹 = 𝐵) ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥))) |
34 | 1, 33 | bitri 277 |
1
⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥))) |