Step | Hyp | Ref
| Expression |
1 | | fvelimad.c |
. . . 4
⊢ (𝜑 → 𝐶 ∈ (𝐹 “ 𝐵)) |
2 | | elimag 5470 |
. . . . 5
⊢ (𝐶 ∈ (𝐹 “ 𝐵) → (𝐶 ∈ (𝐹 “ 𝐵) ↔ ∃𝑦 ∈ 𝐵 𝑦𝐹𝐶)) |
3 | 2 | ibi 256 |
. . . 4
⊢ (𝐶 ∈ (𝐹 “ 𝐵) → ∃𝑦 ∈ 𝐵 𝑦𝐹𝐶) |
4 | 1, 3 | syl 17 |
. . 3
⊢ (𝜑 → ∃𝑦 ∈ 𝐵 𝑦𝐹𝐶) |
5 | | nfv 1843 |
. . . 4
⊢
Ⅎ𝑦𝜑 |
6 | | nfre1 3005 |
. . . 4
⊢
Ⅎ𝑦∃𝑦 ∈ (𝐴 ∩ 𝐵)(𝐹‘𝑦) = 𝐶 |
7 | | vex 3203 |
. . . . . . . . . . 11
⊢ 𝑦 ∈ V |
8 | 7 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦𝐹𝐶) → 𝑦 ∈ V) |
9 | 1 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦𝐹𝐶) → 𝐶 ∈ (𝐹 “ 𝐵)) |
10 | | simpr 477 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦𝐹𝐶) → 𝑦𝐹𝐶) |
11 | | breldmg 5330 |
. . . . . . . . . 10
⊢ ((𝑦 ∈ V ∧ 𝐶 ∈ (𝐹 “ 𝐵) ∧ 𝑦𝐹𝐶) → 𝑦 ∈ dom 𝐹) |
12 | 8, 9, 10, 11 | syl3anc 1326 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦𝐹𝐶) → 𝑦 ∈ dom 𝐹) |
13 | | fvelimad.f |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 Fn 𝐴) |
14 | 13 | fndmd 39441 |
. . . . . . . . . 10
⊢ (𝜑 → dom 𝐹 = 𝐴) |
15 | 14 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦𝐹𝐶) → dom 𝐹 = 𝐴) |
16 | 12, 15 | eleqtrd 2703 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦𝐹𝐶) → 𝑦 ∈ 𝐴) |
17 | 16 | 3adant2 1080 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦𝐹𝐶) → 𝑦 ∈ 𝐴) |
18 | | simp2 1062 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦𝐹𝐶) → 𝑦 ∈ 𝐵) |
19 | 17, 18 | elind 3798 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦𝐹𝐶) → 𝑦 ∈ (𝐴 ∩ 𝐵)) |
20 | | fnfun 5988 |
. . . . . . . . 9
⊢ (𝐹 Fn 𝐴 → Fun 𝐹) |
21 | 13, 20 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → Fun 𝐹) |
22 | 21 | 3ad2ant1 1082 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦𝐹𝐶) → Fun 𝐹) |
23 | | simp3 1063 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦𝐹𝐶) → 𝑦𝐹𝐶) |
24 | | funbrfv 6234 |
. . . . . . 7
⊢ (Fun
𝐹 → (𝑦𝐹𝐶 → (𝐹‘𝑦) = 𝐶)) |
25 | 22, 23, 24 | sylc 65 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦𝐹𝐶) → (𝐹‘𝑦) = 𝐶) |
26 | | rspe 3003 |
. . . . . 6
⊢ ((𝑦 ∈ (𝐴 ∩ 𝐵) ∧ (𝐹‘𝑦) = 𝐶) → ∃𝑦 ∈ (𝐴 ∩ 𝐵)(𝐹‘𝑦) = 𝐶) |
27 | 19, 25, 26 | syl2anc 693 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐵 ∧ 𝑦𝐹𝐶) → ∃𝑦 ∈ (𝐴 ∩ 𝐵)(𝐹‘𝑦) = 𝐶) |
28 | 27 | 3exp 1264 |
. . . 4
⊢ (𝜑 → (𝑦 ∈ 𝐵 → (𝑦𝐹𝐶 → ∃𝑦 ∈ (𝐴 ∩ 𝐵)(𝐹‘𝑦) = 𝐶))) |
29 | 5, 6, 28 | rexlimd 3026 |
. . 3
⊢ (𝜑 → (∃𝑦 ∈ 𝐵 𝑦𝐹𝐶 → ∃𝑦 ∈ (𝐴 ∩ 𝐵)(𝐹‘𝑦) = 𝐶)) |
30 | 4, 29 | mpd 15 |
. 2
⊢ (𝜑 → ∃𝑦 ∈ (𝐴 ∩ 𝐵)(𝐹‘𝑦) = 𝐶) |
31 | | nfv 1843 |
. . 3
⊢
Ⅎ𝑦(𝐹‘𝑥) = 𝐶 |
32 | | fvelimad.x |
. . . . 5
⊢
Ⅎ𝑥𝐹 |
33 | | nfcv 2764 |
. . . . 5
⊢
Ⅎ𝑥𝑦 |
34 | 32, 33 | nffv 6198 |
. . . 4
⊢
Ⅎ𝑥(𝐹‘𝑦) |
35 | | nfcv 2764 |
. . . 4
⊢
Ⅎ𝑥𝐶 |
36 | 34, 35 | nfeq 2776 |
. . 3
⊢
Ⅎ𝑥(𝐹‘𝑦) = 𝐶 |
37 | | fveq2 6191 |
. . . 4
⊢ (𝑥 = 𝑦 → (𝐹‘𝑥) = (𝐹‘𝑦)) |
38 | 37 | eqeq1d 2624 |
. . 3
⊢ (𝑥 = 𝑦 → ((𝐹‘𝑥) = 𝐶 ↔ (𝐹‘𝑦) = 𝐶)) |
39 | 31, 36, 38 | cbvrex 3168 |
. 2
⊢
(∃𝑥 ∈
(𝐴 ∩ 𝐵)(𝐹‘𝑥) = 𝐶 ↔ ∃𝑦 ∈ (𝐴 ∩ 𝐵)(𝐹‘𝑦) = 𝐶) |
40 | 30, 39 | sylibr 224 |
1
⊢ (𝜑 → ∃𝑥 ∈ (𝐴 ∩ 𝐵)(𝐹‘𝑥) = 𝐶) |