Proof of Theorem funcnvmptOLD
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 | | nfv 1843 |
. . 3
⊢
Ⅎ𝑦𝜑 |
14 | | funcnvmpt.0 |
. . . 4
⊢
Ⅎ𝑥𝜑 |
15 | | funmpt 5926 |
. . . . . . . . 9
⊢ Fun
(𝑥 ∈ 𝐴 ↦ 𝐵) |
16 | | funcnvmpt.3 |
. . . . . . . . . 10
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) |
17 | 16 | funeqi 5909 |
. . . . . . . . 9
⊢ (Fun
𝐹 ↔ Fun (𝑥 ∈ 𝐴 ↦ 𝐵)) |
18 | 15, 17 | mpbir 221 |
. . . . . . . 8
⊢ Fun 𝐹 |
19 | | funbrfv2b 6240 |
. . . . . . . 8
⊢ (Fun
𝐹 → (𝑥𝐹𝑦 ↔ (𝑥 ∈ dom 𝐹 ∧ (𝐹‘𝑥) = 𝑦))) |
20 | 18, 19 | ax-mp 5 |
. . . . . . 7
⊢ (𝑥𝐹𝑦 ↔ (𝑥 ∈ dom 𝐹 ∧ (𝐹‘𝑥) = 𝑦)) |
21 | | funcnvmpt.4 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) |
22 | | elex 3212 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ V) |
23 | 21, 22 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ V) |
24 | 23 | ex 450 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝐵 ∈ V)) |
25 | 14, 24 | ralrimi 2957 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ∈ V) |
26 | | funcnvmpt.1 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥𝐴 |
27 | 26 | rabid2f 3119 |
. . . . . . . . . . 11
⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V} ↔ ∀𝑥 ∈ 𝐴 𝐵 ∈ V) |
28 | 25, 27 | sylibr 224 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V}) |
29 | 16 | dmmpt 5630 |
. . . . . . . . . 10
⊢ dom 𝐹 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V} |
30 | 28, 29 | syl6reqr 2675 |
. . . . . . . . 9
⊢ (𝜑 → dom 𝐹 = 𝐴) |
31 | 30 | eleq2d 2687 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ dom 𝐹 ↔ 𝑥 ∈ 𝐴)) |
32 | 31 | anbi1d 741 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ dom 𝐹 ∧ (𝐹‘𝑥) = 𝑦) ↔ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 𝑦))) |
33 | 20, 32 | syl5bb 272 |
. . . . . 6
⊢ (𝜑 → (𝑥𝐹𝑦 ↔ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 𝑦))) |
34 | 33 | bian1d 29306 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ↔ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 𝑦))) |
35 | 16 | fveq1i 6192 |
. . . . . . . . . 10
⊢ (𝐹‘𝑥) = ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) |
36 | | simpr 477 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
37 | 26 | fvmpt2f 6283 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵) |
38 | 36, 21, 37 | syl2anc 693 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵) |
39 | 35, 38 | syl5eq 2668 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐵) |
40 | 39 | eqeq2d 2632 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑦 = (𝐹‘𝑥) ↔ 𝑦 = 𝐵)) |
41 | 31 | biimpar 502 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ dom 𝐹) |
42 | | funbrfvb 6238 |
. . . . . . . . . 10
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ dom 𝐹) → ((𝐹‘𝑥) = 𝑦 ↔ 𝑥𝐹𝑦)) |
43 | 18, 41, 42 | sylancr 695 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐹‘𝑥) = 𝑦 ↔ 𝑥𝐹𝑦)) |
44 | | eqcom 2629 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑥) = 𝑦 ↔ 𝑦 = (𝐹‘𝑥)) |
45 | 44 | bibi1i 328 |
. . . . . . . . . 10
⊢ (((𝐹‘𝑥) = 𝑦 ↔ 𝑥𝐹𝑦) ↔ (𝑦 = (𝐹‘𝑥) ↔ 𝑥𝐹𝑦)) |
46 | 45 | imbi2i 326 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐹‘𝑥) = 𝑦 ↔ 𝑥𝐹𝑦)) ↔ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑦 = (𝐹‘𝑥) ↔ 𝑥𝐹𝑦))) |
47 | 43, 46 | mpbi 220 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑦 = (𝐹‘𝑥) ↔ 𝑥𝐹𝑦)) |
48 | 40, 47 | bitr3d 270 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑦 = 𝐵 ↔ 𝑥𝐹𝑦)) |
49 | 48 | ex 450 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝑦 = 𝐵 ↔ 𝑥𝐹𝑦))) |
50 | 49 | pm5.32d 671 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦))) |
51 | 34, 50, 33 | 3bitr4rd 301 |
. . . 4
⊢ (𝜑 → (𝑥𝐹𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))) |
52 | 14, 51 | mobid 2489 |
. . 3
⊢ (𝜑 → (∃*𝑥 𝑥𝐹𝑦 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))) |
53 | 13, 52 | albid 2090 |
. 2
⊢ (𝜑 → (∀𝑦∃*𝑥 𝑥𝐹𝑦 ↔ ∀𝑦∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))) |
54 | 12, 53 | syl5bb 272 |
1
⊢ (𝜑 → (Fun ◡𝐹 ↔ ∀𝑦∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))) |