Step | Hyp | Ref
| Expression |
1 | | elex 2560 |
. . . 4
⊢ (𝐶 ∈ (𝐹 “ B) → 𝐶 ∈
V) |
2 | 1 | anim2i 324 |
. . 3
⊢ (((𝐹 Fn A ∧ B ⊆ A)
∧ 𝐶 ∈ (𝐹 “ B)) → ((𝐹 Fn A
∧ B
⊆ A) ∧ 𝐶 ∈
V)) |
3 | | ssel2 2934 |
. . . . . . . 8
⊢
((B ⊆ A ∧ u ∈ B) → u
∈ A) |
4 | | funfvex 5135 |
. . . . . . . . 9
⊢ ((Fun
𝐹 ∧ u ∈ dom 𝐹) → (𝐹‘u) ∈
V) |
5 | 4 | funfni 4942 |
. . . . . . . 8
⊢ ((𝐹 Fn A ∧ u ∈ A) → (𝐹‘u) ∈
V) |
6 | 3, 5 | sylan2 270 |
. . . . . . 7
⊢ ((𝐹 Fn A ∧ (B ⊆ A
∧ u ∈ B)) →
(𝐹‘u) ∈
V) |
7 | 6 | anassrs 380 |
. . . . . 6
⊢ (((𝐹 Fn A ∧ B ⊆ A)
∧ u ∈ B) →
(𝐹‘u) ∈
V) |
8 | | eleq1 2097 |
. . . . . 6
⊢ ((𝐹‘u) = 𝐶 → ((𝐹‘u) ∈ V ↔
𝐶 ∈ V)) |
9 | 7, 8 | syl5ibcom 144 |
. . . . 5
⊢ (((𝐹 Fn A ∧ B ⊆ A)
∧ u ∈ B) →
((𝐹‘u) = 𝐶 → 𝐶 ∈
V)) |
10 | 9 | rexlimdva 2427 |
. . . 4
⊢ ((𝐹 Fn A ∧ B ⊆ A)
→ (∃u ∈ B (𝐹‘u) = 𝐶 → 𝐶 ∈
V)) |
11 | 10 | imdistani 419 |
. . 3
⊢ (((𝐹 Fn A ∧ B ⊆ A)
∧ ∃u ∈ B (𝐹‘u) = 𝐶) → ((𝐹 Fn A
∧ B
⊆ A) ∧ 𝐶 ∈
V)) |
12 | | eleq1 2097 |
. . . . . . 7
⊢ (v = 𝐶 → (v ∈ (𝐹 “ B) ↔ 𝐶 ∈ (𝐹 “ B))) |
13 | | eqeq2 2046 |
. . . . . . . 8
⊢ (v = 𝐶 → ((𝐹‘u) = v ↔
(𝐹‘u) = 𝐶)) |
14 | 13 | rexbidv 2321 |
. . . . . . 7
⊢ (v = 𝐶 → (∃u ∈ B (𝐹‘u) = v ↔
∃u ∈ B (𝐹‘u) = 𝐶)) |
15 | 12, 14 | bibi12d 224 |
. . . . . 6
⊢ (v = 𝐶 → ((v ∈ (𝐹 “ B) ↔ ∃u ∈ B (𝐹‘u) = v) ↔
(𝐶 ∈ (𝐹 “ B) ↔ ∃u ∈ B (𝐹‘u) = 𝐶))) |
16 | 15 | imbi2d 219 |
. . . . 5
⊢ (v = 𝐶 → (((𝐹 Fn A
∧ B
⊆ A) → (v ∈ (𝐹 “ B) ↔ ∃u ∈ B (𝐹‘u) = v)) ↔
((𝐹 Fn A ∧ B ⊆ A)
→ (𝐶 ∈ (𝐹 “ B) ↔ ∃u ∈ B (𝐹‘u) = 𝐶)))) |
17 | | fnfun 4939 |
. . . . . . . 8
⊢ (𝐹 Fn A → Fun 𝐹) |
18 | 17 | adantr 261 |
. . . . . . 7
⊢ ((𝐹 Fn A ∧ B ⊆ A)
→ Fun 𝐹) |
19 | | fndm 4941 |
. . . . . . . . 9
⊢ (𝐹 Fn A → dom 𝐹 = A) |
20 | 19 | sseq2d 2967 |
. . . . . . . 8
⊢ (𝐹 Fn A → (B
⊆ dom 𝐹 ↔
B ⊆ A)) |
21 | 20 | biimpar 281 |
. . . . . . 7
⊢ ((𝐹 Fn A ∧ B ⊆ A)
→ B ⊆ dom 𝐹) |
22 | | dfimafn 5165 |
. . . . . . 7
⊢ ((Fun
𝐹 ∧ B ⊆ dom
𝐹) → (𝐹 “ B) = {v ∣
∃u ∈ B (𝐹‘u) = v}) |
23 | 18, 21, 22 | syl2anc 391 |
. . . . . 6
⊢ ((𝐹 Fn A ∧ B ⊆ A)
→ (𝐹 “ B) = {v ∣
∃u ∈ B (𝐹‘u) = v}) |
24 | 23 | abeq2d 2147 |
. . . . 5
⊢ ((𝐹 Fn A ∧ B ⊆ A)
→ (v ∈ (𝐹 “ B) ↔ ∃u ∈ B (𝐹‘u) = v)) |
25 | 16, 24 | vtoclg 2607 |
. . . 4
⊢ (𝐶 ∈ V → ((𝐹 Fn A
∧ B
⊆ A) → (𝐶 ∈ (𝐹 “ B) ↔ ∃u ∈ B (𝐹‘u) = 𝐶))) |
26 | 25 | impcom 116 |
. . 3
⊢ (((𝐹 Fn A ∧ B ⊆ A)
∧ 𝐶 ∈ V)
→ (𝐶 ∈ (𝐹 “ B) ↔ ∃u ∈ B (𝐹‘u) = 𝐶)) |
27 | 2, 11, 26 | pm5.21nd 824 |
. 2
⊢ ((𝐹 Fn A ∧ B ⊆ A)
→ (𝐶 ∈ (𝐹 “ B) ↔ ∃u ∈ B (𝐹‘u) = 𝐶)) |
28 | | fveq2 5121 |
. . . 4
⊢ (u = x →
(𝐹‘u) = (𝐹‘x)) |
29 | 28 | eqeq1d 2045 |
. . 3
⊢ (u = x →
((𝐹‘u) = 𝐶 ↔ (𝐹‘x) = 𝐶)) |
30 | 29 | cbvrexv 2528 |
. 2
⊢ (∃u ∈ B (𝐹‘u) = 𝐶 ↔ ∃x ∈ B (𝐹‘x) = 𝐶) |
31 | 27, 30 | syl6bb 185 |
1
⊢ ((𝐹 Fn A ∧ B ⊆ A)
→ (𝐶 ∈ (𝐹 “ B) ↔ ∃x ∈ B (𝐹‘x) = 𝐶)) |