Step | Hyp | Ref
| Expression |
1 | | df-rex 2454 |
. . . 4
⊢
(∃𝑥 ∈
𝐴 (𝐹‘𝑥) = 𝐵 ↔ ∃𝑥(𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 𝐵)) |
2 | | 19.41v 1895 |
. . . . 5
⊢
(∃𝑥((𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 𝐵) ∧ 𝐹 Fn 𝐴) ↔ (∃𝑥(𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 𝐵) ∧ 𝐹 Fn 𝐴)) |
3 | | simpl 108 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 𝐵) → 𝑥 ∈ 𝐴) |
4 | 3 | anim1i 338 |
. . . . . . . . 9
⊢ (((𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 𝐵) ∧ 𝐹 Fn 𝐴) → (𝑥 ∈ 𝐴 ∧ 𝐹 Fn 𝐴)) |
5 | 4 | ancomd 265 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 𝐵) ∧ 𝐹 Fn 𝐴) → (𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴)) |
6 | | funfvex 5511 |
. . . . . . . . 9
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ dom 𝐹) → (𝐹‘𝑥) ∈ V) |
7 | 6 | funfni 5296 |
. . . . . . . 8
⊢ ((𝐹 Fn 𝐴 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ V) |
8 | 5, 7 | syl 14 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 𝐵) ∧ 𝐹 Fn 𝐴) → (𝐹‘𝑥) ∈ V) |
9 | | simpr 109 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 𝐵) → (𝐹‘𝑥) = 𝐵) |
10 | 9 | eleq1d 2239 |
. . . . . . . 8
⊢ ((𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 𝐵) → ((𝐹‘𝑥) ∈ V ↔ 𝐵 ∈ V)) |
11 | 10 | adantr 274 |
. . . . . . 7
⊢ (((𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 𝐵) ∧ 𝐹 Fn 𝐴) → ((𝐹‘𝑥) ∈ V ↔ 𝐵 ∈ V)) |
12 | 8, 11 | mpbid 146 |
. . . . . 6
⊢ (((𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 𝐵) ∧ 𝐹 Fn 𝐴) → 𝐵 ∈ V) |
13 | 12 | exlimiv 1591 |
. . . . 5
⊢
(∃𝑥((𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 𝐵) ∧ 𝐹 Fn 𝐴) → 𝐵 ∈ V) |
14 | 2, 13 | sylbir 134 |
. . . 4
⊢
((∃𝑥(𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 𝐵) ∧ 𝐹 Fn 𝐴) → 𝐵 ∈ V) |
15 | 1, 14 | sylanb 282 |
. . 3
⊢
((∃𝑥 ∈
𝐴 (𝐹‘𝑥) = 𝐵 ∧ 𝐹 Fn 𝐴) → 𝐵 ∈ V) |
16 | 15 | expcom 115 |
. 2
⊢ (𝐹 Fn 𝐴 → (∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V)) |
17 | | fnrnfv 5541 |
. . . 4
⊢ (𝐹 Fn 𝐴 → ran 𝐹 = {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)}) |
18 | 17 | eleq2d 2240 |
. . 3
⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ 𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)})) |
19 | | eqeq1 2177 |
. . . . . 6
⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ 𝐵 = (𝐹‘𝑥))) |
20 | | eqcom 2172 |
. . . . . 6
⊢ (𝐵 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵) |
21 | 19, 20 | bitrdi 195 |
. . . . 5
⊢ (𝑦 = 𝐵 → (𝑦 = (𝐹‘𝑥) ↔ (𝐹‘𝑥) = 𝐵)) |
22 | 21 | rexbidv 2471 |
. . . 4
⊢ (𝑦 = 𝐵 → (∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥) ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵)) |
23 | 22 | elab3g 2881 |
. . 3
⊢
((∃𝑥 ∈
𝐴 (𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V) → (𝐵 ∈ {𝑦 ∣ ∃𝑥 ∈ 𝐴 𝑦 = (𝐹‘𝑥)} ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵)) |
24 | 18, 23 | sylan9bbr 460 |
. 2
⊢
(((∃𝑥 ∈
𝐴 (𝐹‘𝑥) = 𝐵 → 𝐵 ∈ V) ∧ 𝐹 Fn 𝐴) → (𝐵 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵)) |
25 | 16, 24 | mpancom 420 |
1
⊢ (𝐹 Fn 𝐴 → (𝐵 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐴 (𝐹‘𝑥) = 𝐵)) |