Proof of Theorem dffo4
Step | Hyp | Ref
| Expression |
1 | | dffo2 6119 |
. . 3
⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ran 𝐹 = 𝐵)) |
2 | | simpl 473 |
. . . 4
⊢ ((𝐹:𝐴⟶𝐵 ∧ ran 𝐹 = 𝐵) → 𝐹:𝐴⟶𝐵) |
3 | | vex 3203 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
4 | 3 | elrn 5366 |
. . . . . . . . 9
⊢ (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 𝑥𝐹𝑦) |
5 | | eleq2 2690 |
. . . . . . . . 9
⊢ (ran
𝐹 = 𝐵 → (𝑦 ∈ ran 𝐹 ↔ 𝑦 ∈ 𝐵)) |
6 | 4, 5 | syl5bbr 274 |
. . . . . . . 8
⊢ (ran
𝐹 = 𝐵 → (∃𝑥 𝑥𝐹𝑦 ↔ 𝑦 ∈ 𝐵)) |
7 | 6 | biimpar 502 |
. . . . . . 7
⊢ ((ran
𝐹 = 𝐵 ∧ 𝑦 ∈ 𝐵) → ∃𝑥 𝑥𝐹𝑦) |
8 | 7 | adantll 750 |
. . . . . 6
⊢ (((𝐹:𝐴⟶𝐵 ∧ ran 𝐹 = 𝐵) ∧ 𝑦 ∈ 𝐵) → ∃𝑥 𝑥𝐹𝑦) |
9 | | ffn 6045 |
. . . . . . . . . . 11
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) |
10 | | fnbr 5993 |
. . . . . . . . . . . 12
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥𝐹𝑦) → 𝑥 ∈ 𝐴) |
11 | 10 | ex 450 |
. . . . . . . . . . 11
⊢ (𝐹 Fn 𝐴 → (𝑥𝐹𝑦 → 𝑥 ∈ 𝐴)) |
12 | 9, 11 | syl 17 |
. . . . . . . . . 10
⊢ (𝐹:𝐴⟶𝐵 → (𝑥𝐹𝑦 → 𝑥 ∈ 𝐴)) |
13 | 12 | ancrd 577 |
. . . . . . . . 9
⊢ (𝐹:𝐴⟶𝐵 → (𝑥𝐹𝑦 → (𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦))) |
14 | 13 | eximdv 1846 |
. . . . . . . 8
⊢ (𝐹:𝐴⟶𝐵 → (∃𝑥 𝑥𝐹𝑦 → ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦))) |
15 | | df-rex 2918 |
. . . . . . . 8
⊢
(∃𝑥 ∈
𝐴 𝑥𝐹𝑦 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦)) |
16 | 14, 15 | syl6ibr 242 |
. . . . . . 7
⊢ (𝐹:𝐴⟶𝐵 → (∃𝑥 𝑥𝐹𝑦 → ∃𝑥 ∈ 𝐴 𝑥𝐹𝑦)) |
17 | 16 | ad2antrr 762 |
. . . . . 6
⊢ (((𝐹:𝐴⟶𝐵 ∧ ran 𝐹 = 𝐵) ∧ 𝑦 ∈ 𝐵) → (∃𝑥 𝑥𝐹𝑦 → ∃𝑥 ∈ 𝐴 𝑥𝐹𝑦)) |
18 | 8, 17 | mpd 15 |
. . . . 5
⊢ (((𝐹:𝐴⟶𝐵 ∧ ran 𝐹 = 𝐵) ∧ 𝑦 ∈ 𝐵) → ∃𝑥 ∈ 𝐴 𝑥𝐹𝑦) |
19 | 18 | ralrimiva 2966 |
. . . 4
⊢ ((𝐹:𝐴⟶𝐵 ∧ ran 𝐹 = 𝐵) → ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑥𝐹𝑦) |
20 | 2, 19 | jca 554 |
. . 3
⊢ ((𝐹:𝐴⟶𝐵 ∧ ran 𝐹 = 𝐵) → (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑥𝐹𝑦)) |
21 | 1, 20 | sylbi 207 |
. 2
⊢ (𝐹:𝐴–onto→𝐵 → (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑥𝐹𝑦)) |
22 | | fnbrfvb 6236 |
. . . . . . . . 9
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → ((𝐹‘𝑥) = 𝑦 ↔ 𝑥𝐹𝑦)) |
23 | 22 | biimprd 238 |
. . . . . . . 8
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑥𝐹𝑦 → (𝐹‘𝑥) = 𝑦)) |
24 | | eqcom 2629 |
. . . . . . . 8
⊢ ((𝐹‘𝑥) = 𝑦 ↔ 𝑦 = (𝐹‘𝑥)) |
25 | 23, 24 | syl6ib 241 |
. . . . . . 7
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝑥𝐹𝑦 → 𝑦 = (𝐹‘𝑥))) |
26 | 9, 25 | sylan 488 |
. . . . . 6
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝑥𝐹𝑦 → 𝑦 = (𝐹‘𝑥))) |
27 | 26 | reximdva 3017 |
. . . . 5
⊢ (𝐹:𝐴⟶𝐵 → (∃𝑥 ∈ 𝐴 𝑥𝐹𝑦 → ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥))) |
28 | 27 | ralimdv 2963 |
. . . 4
⊢ (𝐹:𝐴⟶𝐵 → (∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑥𝐹𝑦 → ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥))) |
29 | 28 | imdistani 726 |
. . 3
⊢ ((𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑥𝐹𝑦) → (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥))) |
30 | | dffo3 6374 |
. . 3
⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥))) |
31 | 29, 30 | sylibr 224 |
. 2
⊢ ((𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑥𝐹𝑦) → 𝐹:𝐴–onto→𝐵) |
32 | 21, 31 | impbii 199 |
1
⊢ (𝐹:𝐴–onto→𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ ∀𝑦 ∈ 𝐵 ∃𝑥 ∈ 𝐴 𝑥𝐹𝑦)) |