Step | Hyp | Ref
| Expression |
1 | | eluni 3574 |
. 2
⊢ (A ∈ ∪ ran 𝐹 ↔ ∃y(A ∈ y ∧ y ∈ ran 𝐹)) |
2 | | funfn 4874 |
. . . . . . . 8
⊢ (Fun
𝐹 ↔ 𝐹 Fn dom 𝐹) |
3 | | fvelrnb 5164 |
. . . . . . . 8
⊢ (𝐹 Fn dom 𝐹 → (y ∈ ran 𝐹 ↔ ∃x ∈ dom 𝐹(𝐹‘x) = y)) |
4 | 2, 3 | sylbi 114 |
. . . . . . 7
⊢ (Fun
𝐹 → (y ∈ ran 𝐹 ↔ ∃x ∈ dom 𝐹(𝐹‘x) = y)) |
5 | 4 | anbi2d 437 |
. . . . . 6
⊢ (Fun
𝐹 → ((A ∈ y ∧ y ∈ ran 𝐹) ↔ (A ∈ y ∧ ∃x ∈ dom 𝐹(𝐹‘x) = y))) |
6 | | r19.42v 2461 |
. . . . . 6
⊢ (∃x ∈ dom 𝐹(A ∈ y ∧ (𝐹‘x) = y) ↔
(A ∈
y ∧ ∃x ∈ dom 𝐹(𝐹‘x) = y)) |
7 | 5, 6 | syl6bbr 187 |
. . . . 5
⊢ (Fun
𝐹 → ((A ∈ y ∧ y ∈ ran 𝐹) ↔ ∃x ∈ dom 𝐹(A ∈ y ∧ (𝐹‘x) = y))) |
8 | | eleq2 2098 |
. . . . . . 7
⊢ ((𝐹‘x) = y →
(A ∈
(𝐹‘x) ↔ A
∈ y)) |
9 | 8 | biimparc 283 |
. . . . . 6
⊢
((A ∈ y ∧ (𝐹‘x) = y) →
A ∈
(𝐹‘x)) |
10 | 9 | reximi 2410 |
. . . . 5
⊢ (∃x ∈ dom 𝐹(A ∈ y ∧ (𝐹‘x) = y) →
∃x ∈ dom 𝐹 A ∈ (𝐹‘x)) |
11 | 7, 10 | syl6bi 152 |
. . . 4
⊢ (Fun
𝐹 → ((A ∈ y ∧ y ∈ ran 𝐹) → ∃x ∈ dom 𝐹 A ∈ (𝐹‘x))) |
12 | 11 | exlimdv 1697 |
. . 3
⊢ (Fun
𝐹 → (∃y(A ∈ y ∧ y ∈ ran 𝐹) → ∃x ∈ dom 𝐹 A ∈ (𝐹‘x))) |
13 | | fvelrn 5241 |
. . . . 5
⊢ ((Fun
𝐹 ∧ x ∈ dom 𝐹) → (𝐹‘x) ∈ ran 𝐹) |
14 | | funfvex 5135 |
. . . . . 6
⊢ ((Fun
𝐹 ∧ x ∈ dom 𝐹) → (𝐹‘x) ∈
V) |
15 | | eleq2 2098 |
. . . . . . . 8
⊢ (y = (𝐹‘x) → (A
∈ y
↔ A ∈ (𝐹‘x))) |
16 | | eleq1 2097 |
. . . . . . . 8
⊢ (y = (𝐹‘x) → (y
∈ ran 𝐹 ↔ (𝐹‘x) ∈ ran 𝐹)) |
17 | 15, 16 | anbi12d 442 |
. . . . . . 7
⊢ (y = (𝐹‘x) → ((A
∈ y ∧ y ∈ ran 𝐹) ↔ (A ∈ (𝐹‘x) ∧ (𝐹‘x) ∈ ran 𝐹))) |
18 | 17 | spcegv 2635 |
. . . . . 6
⊢ ((𝐹‘x) ∈ V →
((A ∈
(𝐹‘x) ∧ (𝐹‘x) ∈ ran 𝐹) → ∃y(A ∈ y ∧ y ∈ ran 𝐹))) |
19 | 14, 18 | syl 14 |
. . . . 5
⊢ ((Fun
𝐹 ∧ x ∈ dom 𝐹) → ((A ∈ (𝐹‘x) ∧ (𝐹‘x) ∈ ran 𝐹) → ∃y(A ∈ y ∧ y ∈ ran 𝐹))) |
20 | 13, 19 | mpan2d 404 |
. . . 4
⊢ ((Fun
𝐹 ∧ x ∈ dom 𝐹) → (A ∈ (𝐹‘x) → ∃y(A ∈ y ∧ y ∈ ran 𝐹))) |
21 | 20 | rexlimdva 2427 |
. . 3
⊢ (Fun
𝐹 → (∃x ∈ dom 𝐹 A ∈ (𝐹‘x) → ∃y(A ∈ y ∧ y ∈ ran 𝐹))) |
22 | 12, 21 | impbid 120 |
. 2
⊢ (Fun
𝐹 → (∃y(A ∈ y ∧ y ∈ ran 𝐹) ↔ ∃x ∈ dom 𝐹 A ∈ (𝐹‘x))) |
23 | 1, 22 | syl5bb 181 |
1
⊢ (Fun
𝐹 → (A ∈ ∪ ran 𝐹 ↔ ∃x ∈ dom 𝐹 A ∈ (𝐹‘x))) |