Step | Hyp | Ref
| Expression |
1 | | ffn 4989 |
. . 3
⊢ (𝐹:A⟶{B}
→ 𝐹 Fn A) |
2 | | fvconst 5294 |
. . . 4
⊢ ((𝐹:A⟶{B}
∧ x ∈ A) →
(𝐹‘x) = B) |
3 | 2 | ralrimiva 2386 |
. . 3
⊢ (𝐹:A⟶{B}
→ ∀x ∈ A (𝐹‘x) = B) |
4 | 1, 3 | jca 290 |
. 2
⊢ (𝐹:A⟶{B}
→ (𝐹 Fn A ∧ ∀x ∈ A (𝐹‘x) = B)) |
5 | | fvelrnb 5164 |
. . . . . . . . 9
⊢ (𝐹 Fn A → (w
∈ ran 𝐹 ↔ ∃z ∈ A (𝐹‘z) = w)) |
6 | | fveq2 5121 |
. . . . . . . . . . . . . 14
⊢ (x = z →
(𝐹‘x) = (𝐹‘z)) |
7 | 6 | eqeq1d 2045 |
. . . . . . . . . . . . 13
⊢ (x = z →
((𝐹‘x) = B ↔
(𝐹‘z) = B)) |
8 | 7 | rspccva 2649 |
. . . . . . . . . . . 12
⊢ ((∀x ∈ A (𝐹‘x) = B ∧ z ∈ A) →
(𝐹‘z) = B) |
9 | 8 | eqeq1d 2045 |
. . . . . . . . . . 11
⊢ ((∀x ∈ A (𝐹‘x) = B ∧ z ∈ A) →
((𝐹‘z) = w ↔
B = w)) |
10 | 9 | rexbidva 2317 |
. . . . . . . . . 10
⊢ (∀x ∈ A (𝐹‘x) = B →
(∃z
∈ A
(𝐹‘z) = w ↔
∃z ∈ A B = w)) |
11 | | r19.9rmv 3307 |
. . . . . . . . . . 11
⊢ (∃y y ∈ A → (B =
w ↔ ∃z ∈ A B = w)) |
12 | 11 | bicomd 129 |
. . . . . . . . . 10
⊢ (∃y y ∈ A → (∃z ∈ A B = w ↔
B = w)) |
13 | 10, 12 | sylan9bbr 436 |
. . . . . . . . 9
⊢ ((∃y y ∈ A ∧ ∀x ∈ A (𝐹‘x) = B) →
(∃z
∈ A
(𝐹‘z) = w ↔
B = w)) |
14 | 5, 13 | sylan9bbr 436 |
. . . . . . . 8
⊢ (((∃y y ∈ A ∧ ∀x ∈ A (𝐹‘x) = B) ∧ 𝐹 Fn A)
→ (w ∈ ran 𝐹 ↔ B = w)) |
15 | | elsn 3382 |
. . . . . . . . 9
⊢ (w ∈ {B} ↔ w =
B) |
16 | | eqcom 2039 |
. . . . . . . . 9
⊢ (w = B ↔
B = w) |
17 | 15, 16 | bitr2i 174 |
. . . . . . . 8
⊢ (B = w ↔
w ∈
{B}) |
18 | 14, 17 | syl6bb 185 |
. . . . . . 7
⊢ (((∃y y ∈ A ∧ ∀x ∈ A (𝐹‘x) = B) ∧ 𝐹 Fn A)
→ (w ∈ ran 𝐹 ↔ w ∈ {B})) |
19 | 18 | eqrdv 2035 |
. . . . . 6
⊢ (((∃y y ∈ A ∧ ∀x ∈ A (𝐹‘x) = B) ∧ 𝐹 Fn A)
→ ran 𝐹 = {B}) |
20 | 19 | an32s 502 |
. . . . 5
⊢ (((∃y y ∈ A ∧ 𝐹 Fn A) ∧ ∀x ∈ A (𝐹‘x) = B) →
ran 𝐹 = {B}) |
21 | 20 | exp31 346 |
. . . 4
⊢ (∃y y ∈ A → (𝐹 Fn A
→ (∀x ∈ A (𝐹‘x) = B →
ran 𝐹 = {B}))) |
22 | 21 | imdistand 421 |
. . 3
⊢ (∃y y ∈ A → ((𝐹 Fn A
∧ ∀x ∈ A (𝐹‘x) = B) →
(𝐹 Fn A ∧ ran 𝐹 = {B}))) |
23 | | df-fo 4851 |
. . . 4
⊢ (𝐹:A–onto→{B} ↔
(𝐹 Fn A ∧ ran 𝐹 = {B})) |
24 | | fof 5049 |
. . . 4
⊢ (𝐹:A–onto→{B} →
𝐹:A⟶{B}) |
25 | 23, 24 | sylbir 125 |
. . 3
⊢ ((𝐹 Fn A ∧ ran 𝐹 = {B}) → 𝐹:A⟶{B}) |
26 | 22, 25 | syl6 29 |
. 2
⊢ (∃y y ∈ A → ((𝐹 Fn A
∧ ∀x ∈ A (𝐹‘x) = B) →
𝐹:A⟶{B})) |
27 | 4, 26 | impbid2 131 |
1
⊢ (∃y y ∈ A → (𝐹:A⟶{B}
↔ (𝐹 Fn A ∧ ∀x ∈ A (𝐹‘x) = B))) |