Proof of Theorem dffo4
Step | Hyp | Ref
| Expression |
1 | | dffo2 5053 |
. . 3
⊢ (𝐹:A–onto→B ↔
(𝐹:A⟶B ∧ ran 𝐹 = B)) |
2 | | simpl 102 |
. . . 4
⊢ ((𝐹:A⟶B ∧ ran 𝐹 = B)
→ 𝐹:A⟶B) |
3 | | vex 2554 |
. . . . . . . . . 10
⊢ y ∈
V |
4 | 3 | elrn 4520 |
. . . . . . . . 9
⊢ (y ∈ ran 𝐹 ↔ ∃x x𝐹y) |
5 | | eleq2 2098 |
. . . . . . . . 9
⊢ (ran
𝐹 = B → (y
∈ ran 𝐹 ↔ y ∈ B)) |
6 | 4, 5 | syl5bbr 183 |
. . . . . . . 8
⊢ (ran
𝐹 = B → (∃x x𝐹y ↔
y ∈
B)) |
7 | 6 | biimpar 281 |
. . . . . . 7
⊢ ((ran
𝐹 = B ∧ y ∈ B) → ∃x x𝐹y) |
8 | 7 | adantll 445 |
. . . . . 6
⊢ (((𝐹:A⟶B ∧ ran 𝐹 = B)
∧ y ∈ B) →
∃x
x𝐹y) |
9 | | ffn 4989 |
. . . . . . . . . . 11
⊢ (𝐹:A⟶B
→ 𝐹 Fn A) |
10 | | fnbr 4944 |
. . . . . . . . . . . 12
⊢ ((𝐹 Fn A ∧ x𝐹y)
→ x ∈ A) |
11 | 10 | ex 108 |
. . . . . . . . . . 11
⊢ (𝐹 Fn A → (x𝐹y → x ∈ A)) |
12 | 9, 11 | syl 14 |
. . . . . . . . . 10
⊢ (𝐹:A⟶B
→ (x𝐹y →
x ∈
A)) |
13 | 12 | ancrd 309 |
. . . . . . . . 9
⊢ (𝐹:A⟶B
→ (x𝐹y →
(x ∈
A ∧
x𝐹y))) |
14 | 13 | eximdv 1757 |
. . . . . . . 8
⊢ (𝐹:A⟶B
→ (∃x x𝐹y → ∃x(x ∈ A ∧ x𝐹y))) |
15 | | df-rex 2306 |
. . . . . . . 8
⊢ (∃x ∈ A x𝐹y ↔
∃x(x ∈ A ∧ x𝐹y)) |
16 | 14, 15 | syl6ibr 151 |
. . . . . . 7
⊢ (𝐹:A⟶B
→ (∃x x𝐹y → ∃x ∈ A x𝐹y)) |
17 | 16 | ad2antrr 457 |
. . . . . 6
⊢ (((𝐹:A⟶B ∧ ran 𝐹 = B)
∧ y ∈ B) →
(∃x
x𝐹y →
∃x ∈ A x𝐹y)) |
18 | 8, 17 | mpd 13 |
. . . . 5
⊢ (((𝐹:A⟶B ∧ ran 𝐹 = B)
∧ y ∈ B) →
∃x ∈ A x𝐹y) |
19 | 18 | ralrimiva 2386 |
. . . 4
⊢ ((𝐹:A⟶B ∧ ran 𝐹 = B)
→ ∀y ∈ B ∃x ∈ A x𝐹y) |
20 | 2, 19 | jca 290 |
. . 3
⊢ ((𝐹:A⟶B ∧ ran 𝐹 = B)
→ (𝐹:A⟶B ∧ ∀y ∈ B ∃x ∈ A x𝐹y)) |
21 | 1, 20 | sylbi 114 |
. 2
⊢ (𝐹:A–onto→B →
(𝐹:A⟶B ∧ ∀y ∈ B ∃x ∈ A x𝐹y)) |
22 | | fnbrfvb 5157 |
. . . . . . . . 9
⊢ ((𝐹 Fn A ∧ x ∈ A) → ((𝐹‘x) = y ↔
x𝐹y)) |
23 | 22 | biimprd 147 |
. . . . . . . 8
⊢ ((𝐹 Fn A ∧ x ∈ A) → (x𝐹y →
(𝐹‘x) = y)) |
24 | | eqcom 2039 |
. . . . . . . 8
⊢ ((𝐹‘x) = y ↔
y = (𝐹‘x)) |
25 | 23, 24 | syl6ib 150 |
. . . . . . 7
⊢ ((𝐹 Fn A ∧ x ∈ A) → (x𝐹y →
y = (𝐹‘x))) |
26 | 9, 25 | sylan 267 |
. . . . . 6
⊢ ((𝐹:A⟶B ∧ x ∈ A) →
(x𝐹y →
y = (𝐹‘x))) |
27 | 26 | reximdva 2415 |
. . . . 5
⊢ (𝐹:A⟶B
→ (∃x ∈ A x𝐹y → ∃x ∈ A y = (𝐹‘x))) |
28 | 27 | ralimdv 2382 |
. . . 4
⊢ (𝐹:A⟶B
→ (∀y ∈ B ∃x ∈ A x𝐹y → ∀y ∈ B ∃x ∈ A y = (𝐹‘x))) |
29 | 28 | imdistani 419 |
. . 3
⊢ ((𝐹:A⟶B ∧ ∀y ∈ B ∃x ∈ A x𝐹y) → (𝐹:A⟶B ∧ ∀y ∈ B ∃x ∈ A y = (𝐹‘x))) |
30 | | dffo3 5257 |
. . 3
⊢ (𝐹:A–onto→B ↔
(𝐹:A⟶B ∧ ∀y ∈ B ∃x ∈ A y = (𝐹‘x))) |
31 | 29, 30 | sylibr 137 |
. 2
⊢ ((𝐹:A⟶B ∧ ∀y ∈ B ∃x ∈ A x𝐹y) → 𝐹:A–onto→B) |
32 | 21, 31 | impbii 117 |
1
⊢ (𝐹:A–onto→B ↔
(𝐹:A⟶B ∧ ∀y ∈ B ∃x ∈ A x𝐹y)) |