Proof of Theorem funcnvmptOLD
Step | Hyp | Ref
| Expression |
1 | | relcnv 5422 |
. . . 4
⊢ Rel ◡𝐹 |
2 | | nfcv 2751 |
. . . . 5
⊢
Ⅎ𝑦◡𝐹 |
3 | | funcnvmpt.2 |
. . . . . 6
⊢
Ⅎ𝑥𝐹 |
4 | 3 | nfcnv 5223 |
. . . . 5
⊢
Ⅎ𝑥◡𝐹 |
5 | 2, 4 | dffun6f 5818 |
. . . 4
⊢ (Fun
◡𝐹 ↔ (Rel ◡𝐹 ∧ ∀𝑦∃*𝑥 𝑦◡𝐹𝑥)) |
6 | 1, 5 | mpbiran 955 |
. . 3
⊢ (Fun
◡𝐹 ↔ ∀𝑦∃*𝑥 𝑦◡𝐹𝑥) |
7 | | vex 3176 |
. . . . . 6
⊢ 𝑦 ∈ V |
8 | | vex 3176 |
. . . . . 6
⊢ 𝑥 ∈ V |
9 | 7, 8 | brcnv 5227 |
. . . . 5
⊢ (𝑦◡𝐹𝑥 ↔ 𝑥𝐹𝑦) |
10 | 9 | mobii 2481 |
. . . 4
⊢
(∃*𝑥 𝑦◡𝐹𝑥 ↔ ∃*𝑥 𝑥𝐹𝑦) |
11 | 10 | albii 1737 |
. . 3
⊢
(∀𝑦∃*𝑥 𝑦◡𝐹𝑥 ↔ ∀𝑦∃*𝑥 𝑥𝐹𝑦) |
12 | 6, 11 | bitri 263 |
. 2
⊢ (Fun
◡𝐹 ↔ ∀𝑦∃*𝑥 𝑥𝐹𝑦) |
13 | | nfv 1830 |
. . 3
⊢
Ⅎ𝑦𝜑 |
14 | | funcnvmpt.0 |
. . . 4
⊢
Ⅎ𝑥𝜑 |
15 | | funmpt 5840 |
. . . . . . . . 9
⊢ Fun
(𝑥 ∈ 𝐴 ↦ 𝐵) |
16 | | funcnvmpt.3 |
. . . . . . . . . 10
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) |
17 | 16 | funeqi 5824 |
. . . . . . . . 9
⊢ (Fun
𝐹 ↔ Fun (𝑥 ∈ 𝐴 ↦ 𝐵)) |
18 | 15, 17 | mpbir 220 |
. . . . . . . 8
⊢ Fun 𝐹 |
19 | | funbrfv2b 6150 |
. . . . . . . 8
⊢ (Fun
𝐹 → (𝑥𝐹𝑦 ↔ (𝑥 ∈ dom 𝐹 ∧ (𝐹‘𝑥) = 𝑦))) |
20 | 18, 19 | ax-mp 5 |
. . . . . . 7
⊢ (𝑥𝐹𝑦 ↔ (𝑥 ∈ dom 𝐹 ∧ (𝐹‘𝑥) = 𝑦)) |
21 | | funcnvmpt.4 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) |
22 | | elex 3185 |
. . . . . . . . . . . . . 14
⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ V) |
23 | 21, 22 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ V) |
24 | 23 | ex 449 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝐵 ∈ V)) |
25 | 14, 24 | ralrimi 2940 |
. . . . . . . . . . 11
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ∈ V) |
26 | | funcnvmpt.1 |
. . . . . . . . . . . 12
⊢
Ⅎ𝑥𝐴 |
27 | 26 | rabid2f 28724 |
. . . . . . . . . . 11
⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V} ↔ ∀𝑥 ∈ 𝐴 𝐵 ∈ V) |
28 | 25, 27 | sylibr 223 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V}) |
29 | 16 | dmmpt 5547 |
. . . . . . . . . 10
⊢ dom 𝐹 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V} |
30 | 28, 29 | syl6reqr 2663 |
. . . . . . . . 9
⊢ (𝜑 → dom 𝐹 = 𝐴) |
31 | 30 | eleq2d 2673 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ dom 𝐹 ↔ 𝑥 ∈ 𝐴)) |
32 | 31 | anbi1d 737 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ dom 𝐹 ∧ (𝐹‘𝑥) = 𝑦) ↔ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 𝑦))) |
33 | 20, 32 | syl5bb 271 |
. . . . . 6
⊢ (𝜑 → (𝑥𝐹𝑦 ↔ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 𝑦))) |
34 | 33 | bian1d 28690 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ↔ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 𝑦))) |
35 | 16 | fveq1i 6104 |
. . . . . . . . . 10
⊢ (𝐹‘𝑥) = ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) |
36 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
37 | 26 | fvmpt2f 6192 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵) |
38 | 36, 21, 37 | syl2anc 691 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵) |
39 | 35, 38 | syl5eq 2656 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐵) |
40 | 39 | eqeq2d 2620 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑦 = (𝐹‘𝑥) ↔ 𝑦 = 𝐵)) |
41 | 31 | biimpar 501 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ dom 𝐹) |
42 | | funbrfvb 6148 |
. . . . . . . . . 10
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ dom 𝐹) → ((𝐹‘𝑥) = 𝑦 ↔ 𝑥𝐹𝑦)) |
43 | 18, 41, 42 | sylancr 694 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐹‘𝑥) = 𝑦 ↔ 𝑥𝐹𝑦)) |
44 | | eqcom 2617 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑥) = 𝑦 ↔ 𝑦 = (𝐹‘𝑥)) |
45 | 44 | bibi1i 327 |
. . . . . . . . . 10
⊢ (((𝐹‘𝑥) = 𝑦 ↔ 𝑥𝐹𝑦) ↔ (𝑦 = (𝐹‘𝑥) ↔ 𝑥𝐹𝑦)) |
46 | 45 | imbi2i 325 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐹‘𝑥) = 𝑦 ↔ 𝑥𝐹𝑦)) ↔ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑦 = (𝐹‘𝑥) ↔ 𝑥𝐹𝑦))) |
47 | 43, 46 | mpbi 219 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑦 = (𝐹‘𝑥) ↔ 𝑥𝐹𝑦)) |
48 | 40, 47 | bitr3d 269 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑦 = 𝐵 ↔ 𝑥𝐹𝑦)) |
49 | 48 | ex 449 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐴 → (𝑦 = 𝐵 ↔ 𝑥𝐹𝑦))) |
50 | 49 | pm5.32d 669 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦))) |
51 | 34, 50, 33 | 3bitr4rd 300 |
. . . 4
⊢ (𝜑 → (𝑥𝐹𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))) |
52 | 14, 51 | mobid 2477 |
. . 3
⊢ (𝜑 → (∃*𝑥 𝑥𝐹𝑦 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))) |
53 | 13, 52 | albid 2077 |
. 2
⊢ (𝜑 → (∀𝑦∃*𝑥 𝑥𝐹𝑦 ↔ ∀𝑦∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))) |
54 | 12, 53 | syl5bb 271 |
1
⊢ (𝜑 → (Fun ◡𝐹 ↔ ∀𝑦∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))) |