Proof of Theorem funcnvmpt
Step | Hyp | Ref
| Expression |
1 | | relcnv 5503 |
. . . 4
⊢ Rel ◡𝐹 |
2 | | nfcv 2764 |
. . . . 5
⊢
Ⅎ𝑦◡𝐹 |
3 | | funcnvmpt.2 |
. . . . . 6
⊢
Ⅎ𝑥𝐹 |
4 | 3 | nfcnv 5301 |
. . . . 5
⊢
Ⅎ𝑥◡𝐹 |
5 | 2, 4 | dffun6f 5902 |
. . . 4
⊢ (Fun
◡𝐹 ↔ (Rel ◡𝐹 ∧ ∀𝑦∃*𝑥 𝑦◡𝐹𝑥)) |
6 | 1, 5 | mpbiran 953 |
. . 3
⊢ (Fun
◡𝐹 ↔ ∀𝑦∃*𝑥 𝑦◡𝐹𝑥) |
7 | | vex 3203 |
. . . . . 6
⊢ 𝑦 ∈ V |
8 | | vex 3203 |
. . . . . 6
⊢ 𝑥 ∈ V |
9 | 7, 8 | brcnv 5305 |
. . . . 5
⊢ (𝑦◡𝐹𝑥 ↔ 𝑥𝐹𝑦) |
10 | 9 | mobii 2493 |
. . . 4
⊢
(∃*𝑥 𝑦◡𝐹𝑥 ↔ ∃*𝑥 𝑥𝐹𝑦) |
11 | 10 | albii 1747 |
. . 3
⊢
(∀𝑦∃*𝑥 𝑦◡𝐹𝑥 ↔ ∀𝑦∃*𝑥 𝑥𝐹𝑦) |
12 | 6, 11 | bitri 264 |
. 2
⊢ (Fun
◡𝐹 ↔ ∀𝑦∃*𝑥 𝑥𝐹𝑦) |
13 | | funcnvmpt.0 |
. . . . 5
⊢
Ⅎ𝑥𝜑 |
14 | | funcnvmpt.3 |
. . . . . . . . . 10
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) |
15 | 14 | funmpt2 5927 |
. . . . . . . . 9
⊢ Fun 𝐹 |
16 | | funbrfv2b 6240 |
. . . . . . . . 9
⊢ (Fun
𝐹 → (𝑥𝐹𝑦 ↔ (𝑥 ∈ dom 𝐹 ∧ (𝐹‘𝑥) = 𝑦))) |
17 | 15, 16 | ax-mp 5 |
. . . . . . . 8
⊢ (𝑥𝐹𝑦 ↔ (𝑥 ∈ dom 𝐹 ∧ (𝐹‘𝑥) = 𝑦)) |
18 | | funcnvmpt.4 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) |
19 | | elex 3212 |
. . . . . . . . . . . . . . 15
⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ V) |
20 | 18, 19 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ V) |
21 | 20 | ex 450 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝐵 ∈ V)) |
22 | 13, 21 | ralrimi 2957 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ∈ V) |
23 | | funcnvmpt.1 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥𝐴 |
24 | 23 | rabid2f 3119 |
. . . . . . . . . . . 12
⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V} ↔ ∀𝑥 ∈ 𝐴 𝐵 ∈ V) |
25 | 22, 24 | sylibr 224 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V}) |
26 | 14 | dmmpt 5630 |
. . . . . . . . . . 11
⊢ dom 𝐹 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V} |
27 | 25, 26 | syl6reqr 2675 |
. . . . . . . . . 10
⊢ (𝜑 → dom 𝐹 = 𝐴) |
28 | 27 | eleq2d 2687 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ dom 𝐹 ↔ 𝑥 ∈ 𝐴)) |
29 | 28 | anbi1d 741 |
. . . . . . . 8
⊢ (𝜑 → ((𝑥 ∈ dom 𝐹 ∧ (𝐹‘𝑥) = 𝑦) ↔ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 𝑦))) |
30 | 17, 29 | syl5bb 272 |
. . . . . . 7
⊢ (𝜑 → (𝑥𝐹𝑦 ↔ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 𝑦))) |
31 | 30 | bian1d 29306 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ↔ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 𝑦))) |
32 | | simpr 477 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
33 | 14 | fveq1i 6192 |
. . . . . . . . . . 11
⊢ (𝐹‘𝑥) = ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) |
34 | 23 | fvmpt2f 6283 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵) |
35 | 33, 34 | syl5eq 2668 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → (𝐹‘𝑥) = 𝐵) |
36 | 32, 18, 35 | syl2anc 693 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐵) |
37 | 36 | eqeq2d 2632 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑦 = (𝐹‘𝑥) ↔ 𝑦 = 𝐵)) |
38 | | eqcom 2629 |
. . . . . . . . 9
⊢ ((𝐹‘𝑥) = 𝑦 ↔ 𝑦 = (𝐹‘𝑥)) |
39 | 28 | biimpar 502 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ dom 𝐹) |
40 | | funbrfvb 6238 |
. . . . . . . . . 10
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ dom 𝐹) → ((𝐹‘𝑥) = 𝑦 ↔ 𝑥𝐹𝑦)) |
41 | 15, 39, 40 | sylancr 695 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐹‘𝑥) = 𝑦 ↔ 𝑥𝐹𝑦)) |
42 | 38, 41 | syl5bbr 274 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑦 = (𝐹‘𝑥) ↔ 𝑥𝐹𝑦)) |
43 | 37, 42 | bitr3d 270 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑦 = 𝐵 ↔ 𝑥𝐹𝑦)) |
44 | 43 | pm5.32da 673 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦))) |
45 | 31, 44, 30 | 3bitr4rd 301 |
. . . . 5
⊢ (𝜑 → (𝑥𝐹𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))) |
46 | 13, 45 | mobid 2489 |
. . . 4
⊢ (𝜑 → (∃*𝑥 𝑥𝐹𝑦 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))) |
47 | | df-rmo 2920 |
. . . 4
⊢
(∃*𝑥 ∈
𝐴 𝑦 = 𝐵 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)) |
48 | 46, 47 | syl6bbr 278 |
. . 3
⊢ (𝜑 → (∃*𝑥 𝑥𝐹𝑦 ↔ ∃*𝑥 ∈ 𝐴 𝑦 = 𝐵)) |
49 | 48 | albidv 1849 |
. 2
⊢ (𝜑 → (∀𝑦∃*𝑥 𝑥𝐹𝑦 ↔ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 = 𝐵)) |
50 | 12, 49 | syl5bb 272 |
1
⊢ (𝜑 → (Fun ◡𝐹 ↔ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 = 𝐵)) |