Proof of Theorem funcnvmpt
| Step | Hyp | Ref
| Expression |
| 1 | | relcnv 6122 |
. . . 4
⊢ Rel ◡𝐹 |
| 2 | | nfcv 2905 |
. . . . 5
⊢
Ⅎ𝑦◡𝐹 |
| 3 | | funcnvmpt.2 |
. . . . . 6
⊢
Ⅎ𝑥𝐹 |
| 4 | 3 | nfcnv 5889 |
. . . . 5
⊢
Ⅎ𝑥◡𝐹 |
| 5 | 2, 4 | dffun6f 6579 |
. . . 4
⊢ (Fun
◡𝐹 ↔ (Rel ◡𝐹 ∧ ∀𝑦∃*𝑥 𝑦◡𝐹𝑥)) |
| 6 | 1, 5 | mpbiran 709 |
. . 3
⊢ (Fun
◡𝐹 ↔ ∀𝑦∃*𝑥 𝑦◡𝐹𝑥) |
| 7 | | vex 3484 |
. . . . . 6
⊢ 𝑦 ∈ V |
| 8 | | vex 3484 |
. . . . . 6
⊢ 𝑥 ∈ V |
| 9 | 7, 8 | brcnv 5893 |
. . . . 5
⊢ (𝑦◡𝐹𝑥 ↔ 𝑥𝐹𝑦) |
| 10 | 9 | mobii 2548 |
. . . 4
⊢
(∃*𝑥 𝑦◡𝐹𝑥 ↔ ∃*𝑥 𝑥𝐹𝑦) |
| 11 | 10 | albii 1819 |
. . 3
⊢
(∀𝑦∃*𝑥 𝑦◡𝐹𝑥 ↔ ∀𝑦∃*𝑥 𝑥𝐹𝑦) |
| 12 | 6, 11 | bitri 275 |
. 2
⊢ (Fun
◡𝐹 ↔ ∀𝑦∃*𝑥 𝑥𝐹𝑦) |
| 13 | | funcnvmpt.0 |
. . . . 5
⊢
Ⅎ𝑥𝜑 |
| 14 | | funcnvmpt.3 |
. . . . . . . . . 10
⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵) |
| 15 | 14 | funmpt2 6605 |
. . . . . . . . 9
⊢ Fun 𝐹 |
| 16 | | funbrfv2b 6966 |
. . . . . . . . 9
⊢ (Fun
𝐹 → (𝑥𝐹𝑦 ↔ (𝑥 ∈ dom 𝐹 ∧ (𝐹‘𝑥) = 𝑦))) |
| 17 | 15, 16 | ax-mp 5 |
. . . . . . . 8
⊢ (𝑥𝐹𝑦 ↔ (𝑥 ∈ dom 𝐹 ∧ (𝐹‘𝑥) = 𝑦)) |
| 18 | 14 | dmmpt 6260 |
. . . . . . . . . . 11
⊢ dom 𝐹 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V} |
| 19 | | funcnvmpt.4 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ 𝑉) |
| 20 | 19 | elexd 3504 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ V) |
| 21 | 20 | ex 412 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑥 ∈ 𝐴 → 𝐵 ∈ V)) |
| 22 | 13, 21 | ralrimi 3257 |
. . . . . . . . . . . 12
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 𝐵 ∈ V) |
| 23 | | funcnvmpt.1 |
. . . . . . . . . . . . 13
⊢
Ⅎ𝑥𝐴 |
| 24 | 23 | rabid2f 3468 |
. . . . . . . . . . . 12
⊢ (𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V} ↔ ∀𝑥 ∈ 𝐴 𝐵 ∈ V) |
| 25 | 22, 24 | sylibr 234 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ V}) |
| 26 | 18, 25 | eqtr4id 2796 |
. . . . . . . . . 10
⊢ (𝜑 → dom 𝐹 = 𝐴) |
| 27 | 26 | eleq2d 2827 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ dom 𝐹 ↔ 𝑥 ∈ 𝐴)) |
| 28 | 27 | anbi1d 631 |
. . . . . . . 8
⊢ (𝜑 → ((𝑥 ∈ dom 𝐹 ∧ (𝐹‘𝑥) = 𝑦) ↔ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 𝑦))) |
| 29 | 17, 28 | bitrid 283 |
. . . . . . 7
⊢ (𝜑 → (𝑥𝐹𝑦 ↔ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 𝑦))) |
| 30 | 29 | bian1d 32475 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦) ↔ (𝑥 ∈ 𝐴 ∧ (𝐹‘𝑥) = 𝑦))) |
| 31 | | simpr 484 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
| 32 | 14 | fveq1i 6907 |
. . . . . . . . . . 11
⊢ (𝐹‘𝑥) = ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) |
| 33 | 23 | fvmpt2f 7017 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵) |
| 34 | 32, 33 | eqtrid 2789 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝑉) → (𝐹‘𝑥) = 𝐵) |
| 35 | 31, 19, 34 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = 𝐵) |
| 36 | 35 | eqeq2d 2748 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑦 = (𝐹‘𝑥) ↔ 𝑦 = 𝐵)) |
| 37 | | eqcom 2744 |
. . . . . . . . 9
⊢ ((𝐹‘𝑥) = 𝑦 ↔ 𝑦 = (𝐹‘𝑥)) |
| 38 | 27 | biimpar 477 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ dom 𝐹) |
| 39 | | funbrfvb 6962 |
. . . . . . . . . 10
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ dom 𝐹) → ((𝐹‘𝑥) = 𝑦 ↔ 𝑥𝐹𝑦)) |
| 40 | 15, 38, 39 | sylancr 587 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ((𝐹‘𝑥) = 𝑦 ↔ 𝑥𝐹𝑦)) |
| 41 | 37, 40 | bitr3id 285 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑦 = (𝐹‘𝑥) ↔ 𝑥𝐹𝑦)) |
| 42 | 36, 41 | bitr3d 281 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝑦 = 𝐵 ↔ 𝑥𝐹𝑦)) |
| 43 | 42 | pm5.32da 579 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ 𝑥𝐹𝑦))) |
| 44 | 30, 43, 29 | 3bitr4rd 312 |
. . . . 5
⊢ (𝜑 → (𝑥𝐹𝑦 ↔ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))) |
| 45 | 13, 44 | mobid 2550 |
. . . 4
⊢ (𝜑 → (∃*𝑥 𝑥𝐹𝑦 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))) |
| 46 | | df-rmo 3380 |
. . . 4
⊢
(∃*𝑥 ∈
𝐴 𝑦 = 𝐵 ↔ ∃*𝑥(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)) |
| 47 | 45, 46 | bitr4di 289 |
. . 3
⊢ (𝜑 → (∃*𝑥 𝑥𝐹𝑦 ↔ ∃*𝑥 ∈ 𝐴 𝑦 = 𝐵)) |
| 48 | 47 | albidv 1920 |
. 2
⊢ (𝜑 → (∀𝑦∃*𝑥 𝑥𝐹𝑦 ↔ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 = 𝐵)) |
| 49 | 12, 48 | bitrid 283 |
1
⊢ (𝜑 → (Fun ◡𝐹 ↔ ∀𝑦∃*𝑥 ∈ 𝐴 𝑦 = 𝐵)) |