Step | Hyp | Ref
| Expression |
1 | | df-rex 2306 |
. . . 4
⊢ (∃x ∈ A (𝐹‘x) = B ↔
∃x(x ∈ A ∧ (𝐹‘x) = B)) |
2 | | 19.41v 1779 |
. . . . 5
⊢ (∃x((x ∈ A ∧ (𝐹‘x) = B) ∧ 𝐹 Fn A)
↔ (∃x(x ∈ A ∧ (𝐹‘x) = B) ∧ 𝐹 Fn A)) |
3 | | simpl 102 |
. . . . . . . . . 10
⊢
((x ∈ A ∧ (𝐹‘x) = B) →
x ∈
A) |
4 | 3 | anim1i 323 |
. . . . . . . . 9
⊢
(((x ∈ A ∧ (𝐹‘x) = B) ∧ 𝐹 Fn A)
→ (x ∈ A ∧ 𝐹 Fn A)) |
5 | 4 | ancomd 254 |
. . . . . . . 8
⊢
(((x ∈ A ∧ (𝐹‘x) = B) ∧ 𝐹 Fn A)
→ (𝐹 Fn A ∧ x ∈ A)) |
6 | | funfvex 5135 |
. . . . . . . . 9
⊢ ((Fun
𝐹 ∧ x ∈ dom 𝐹) → (𝐹‘x) ∈
V) |
7 | 6 | funfni 4942 |
. . . . . . . 8
⊢ ((𝐹 Fn A ∧ x ∈ A) → (𝐹‘x) ∈
V) |
8 | 5, 7 | syl 14 |
. . . . . . 7
⊢
(((x ∈ A ∧ (𝐹‘x) = B) ∧ 𝐹 Fn A)
→ (𝐹‘x) ∈
V) |
9 | | simpr 103 |
. . . . . . . . 9
⊢
((x ∈ A ∧ (𝐹‘x) = B) →
(𝐹‘x) = B) |
10 | 9 | eleq1d 2103 |
. . . . . . . 8
⊢
((x ∈ A ∧ (𝐹‘x) = B) →
((𝐹‘x) ∈ V ↔
B ∈
V)) |
11 | 10 | adantr 261 |
. . . . . . 7
⊢
(((x ∈ A ∧ (𝐹‘x) = B) ∧ 𝐹 Fn A)
→ ((𝐹‘x) ∈ V ↔
B ∈
V)) |
12 | 8, 11 | mpbid 135 |
. . . . . 6
⊢
(((x ∈ A ∧ (𝐹‘x) = B) ∧ 𝐹 Fn A)
→ B ∈ V) |
13 | 12 | exlimiv 1486 |
. . . . 5
⊢ (∃x((x ∈ A ∧ (𝐹‘x) = B) ∧ 𝐹 Fn A)
→ B ∈ V) |
14 | 2, 13 | sylbir 125 |
. . . 4
⊢ ((∃x(x ∈ A ∧ (𝐹‘x) = B) ∧ 𝐹 Fn A)
→ B ∈ V) |
15 | 1, 14 | sylanb 268 |
. . 3
⊢ ((∃x ∈ A (𝐹‘x) = B ∧ 𝐹 Fn A)
→ B ∈ V) |
16 | 15 | expcom 109 |
. 2
⊢ (𝐹 Fn A → (∃x ∈ A (𝐹‘x) = B →
B ∈
V)) |
17 | | fnrnfv 5163 |
. . . 4
⊢ (𝐹 Fn A → ran 𝐹 = {y
∣ ∃x ∈ A y = (𝐹‘x)}) |
18 | 17 | eleq2d 2104 |
. . 3
⊢ (𝐹 Fn A → (B
∈ ran 𝐹 ↔ B ∈ {y ∣ ∃x ∈ A y = (𝐹‘x)})) |
19 | | eqeq1 2043 |
. . . . . 6
⊢ (y = B →
(y = (𝐹‘x) ↔ B =
(𝐹‘x))) |
20 | | eqcom 2039 |
. . . . . 6
⊢ (B = (𝐹‘x) ↔ (𝐹‘x) = B) |
21 | 19, 20 | syl6bb 185 |
. . . . 5
⊢ (y = B →
(y = (𝐹‘x) ↔ (𝐹‘x) = B)) |
22 | 21 | rexbidv 2321 |
. . . 4
⊢ (y = B →
(∃x
∈ A
y = (𝐹‘x) ↔ ∃x ∈ A (𝐹‘x) = B)) |
23 | 22 | elab3g 2687 |
. . 3
⊢ ((∃x ∈ A (𝐹‘x) = B →
B ∈ V)
→ (B ∈ {y ∣
∃x ∈ A y = (𝐹‘x)} ↔ ∃x ∈ A (𝐹‘x) = B)) |
24 | 18, 23 | sylan9bbr 436 |
. 2
⊢ (((∃x ∈ A (𝐹‘x) = B →
B ∈ V)
∧ 𝐹 Fn A)
→ (B ∈ ran 𝐹 ↔ ∃x ∈ A (𝐹‘x) = B)) |
25 | 16, 24 | mpancom 399 |
1
⊢ (𝐹 Fn A → (B
∈ ran 𝐹 ↔ ∃x ∈ A (𝐹‘x) = B)) |