Step | Hyp | Ref
| Expression |
1 | | eluni 3612 |
. 2
⊢ (𝐴 ∈ ∪ ran 𝐹 ↔ ∃𝑦(𝐴 ∈ 𝑦 ∧ 𝑦 ∈ ran 𝐹)) |
2 | | funfn 4961 |
. . . . . . . 8
⊢ (Fun
𝐹 ↔ 𝐹 Fn dom 𝐹) |
3 | | fvelrnb 5253 |
. . . . . . . 8
⊢ (𝐹 Fn dom 𝐹 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ dom 𝐹(𝐹‘𝑥) = 𝑦)) |
4 | 2, 3 | sylbi 119 |
. . . . . . 7
⊢ (Fun
𝐹 → (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ dom 𝐹(𝐹‘𝑥) = 𝑦)) |
5 | 4 | anbi2d 452 |
. . . . . 6
⊢ (Fun
𝐹 → ((𝐴 ∈ 𝑦 ∧ 𝑦 ∈ ran 𝐹) ↔ (𝐴 ∈ 𝑦 ∧ ∃𝑥 ∈ dom 𝐹(𝐹‘𝑥) = 𝑦))) |
6 | | r19.42v 2512 |
. . . . . 6
⊢
(∃𝑥 ∈ dom
𝐹(𝐴 ∈ 𝑦 ∧ (𝐹‘𝑥) = 𝑦) ↔ (𝐴 ∈ 𝑦 ∧ ∃𝑥 ∈ dom 𝐹(𝐹‘𝑥) = 𝑦)) |
7 | 5, 6 | syl6bbr 196 |
. . . . 5
⊢ (Fun
𝐹 → ((𝐴 ∈ 𝑦 ∧ 𝑦 ∈ ran 𝐹) ↔ ∃𝑥 ∈ dom 𝐹(𝐴 ∈ 𝑦 ∧ (𝐹‘𝑥) = 𝑦))) |
8 | | eleq2 2143 |
. . . . . . 7
⊢ ((𝐹‘𝑥) = 𝑦 → (𝐴 ∈ (𝐹‘𝑥) ↔ 𝐴 ∈ 𝑦)) |
9 | 8 | biimparc 293 |
. . . . . 6
⊢ ((𝐴 ∈ 𝑦 ∧ (𝐹‘𝑥) = 𝑦) → 𝐴 ∈ (𝐹‘𝑥)) |
10 | 9 | reximi 2459 |
. . . . 5
⊢
(∃𝑥 ∈ dom
𝐹(𝐴 ∈ 𝑦 ∧ (𝐹‘𝑥) = 𝑦) → ∃𝑥 ∈ dom 𝐹 𝐴 ∈ (𝐹‘𝑥)) |
11 | 7, 10 | syl6bi 161 |
. . . 4
⊢ (Fun
𝐹 → ((𝐴 ∈ 𝑦 ∧ 𝑦 ∈ ran 𝐹) → ∃𝑥 ∈ dom 𝐹 𝐴 ∈ (𝐹‘𝑥))) |
12 | 11 | exlimdv 1741 |
. . 3
⊢ (Fun
𝐹 → (∃𝑦(𝐴 ∈ 𝑦 ∧ 𝑦 ∈ ran 𝐹) → ∃𝑥 ∈ dom 𝐹 𝐴 ∈ (𝐹‘𝑥))) |
13 | | fvelrn 5330 |
. . . . 5
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ dom 𝐹) → (𝐹‘𝑥) ∈ ran 𝐹) |
14 | | funfvex 5223 |
. . . . . 6
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ dom 𝐹) → (𝐹‘𝑥) ∈ V) |
15 | | eleq2 2143 |
. . . . . . . 8
⊢ (𝑦 = (𝐹‘𝑥) → (𝐴 ∈ 𝑦 ↔ 𝐴 ∈ (𝐹‘𝑥))) |
16 | | eleq1 2142 |
. . . . . . . 8
⊢ (𝑦 = (𝐹‘𝑥) → (𝑦 ∈ ran 𝐹 ↔ (𝐹‘𝑥) ∈ ran 𝐹)) |
17 | 15, 16 | anbi12d 457 |
. . . . . . 7
⊢ (𝑦 = (𝐹‘𝑥) → ((𝐴 ∈ 𝑦 ∧ 𝑦 ∈ ran 𝐹) ↔ (𝐴 ∈ (𝐹‘𝑥) ∧ (𝐹‘𝑥) ∈ ran 𝐹))) |
18 | 17 | spcegv 2687 |
. . . . . 6
⊢ ((𝐹‘𝑥) ∈ V → ((𝐴 ∈ (𝐹‘𝑥) ∧ (𝐹‘𝑥) ∈ ran 𝐹) → ∃𝑦(𝐴 ∈ 𝑦 ∧ 𝑦 ∈ ran 𝐹))) |
19 | 14, 18 | syl 14 |
. . . . 5
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ dom 𝐹) → ((𝐴 ∈ (𝐹‘𝑥) ∧ (𝐹‘𝑥) ∈ ran 𝐹) → ∃𝑦(𝐴 ∈ 𝑦 ∧ 𝑦 ∈ ran 𝐹))) |
20 | 13, 19 | mpan2d 419 |
. . . 4
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ dom 𝐹) → (𝐴 ∈ (𝐹‘𝑥) → ∃𝑦(𝐴 ∈ 𝑦 ∧ 𝑦 ∈ ran 𝐹))) |
21 | 20 | rexlimdva 2478 |
. . 3
⊢ (Fun
𝐹 → (∃𝑥 ∈ dom 𝐹 𝐴 ∈ (𝐹‘𝑥) → ∃𝑦(𝐴 ∈ 𝑦 ∧ 𝑦 ∈ ran 𝐹))) |
22 | 12, 21 | impbid 127 |
. 2
⊢ (Fun
𝐹 → (∃𝑦(𝐴 ∈ 𝑦 ∧ 𝑦 ∈ ran 𝐹) ↔ ∃𝑥 ∈ dom 𝐹 𝐴 ∈ (𝐹‘𝑥))) |
23 | 1, 22 | syl5bb 190 |
1
⊢ (Fun
𝐹 → (𝐴 ∈ ∪ ran
𝐹 ↔ ∃𝑥 ∈ dom 𝐹 𝐴 ∈ (𝐹‘𝑥))) |