Proof of Theorem f1ocnv
Step | Hyp | Ref
| Expression |
1 | | fnrel 6450 |
. . . 4
⊢ (𝐹 Fn 𝐴 → Rel 𝐹) |
2 | | dfrel2 6031 |
. . . . 5
⊢ (Rel
𝐹 ↔ ◡◡𝐹 = 𝐹) |
3 | | fneq1 6440 |
. . . . . 6
⊢ (◡◡𝐹 = 𝐹 → (◡◡𝐹 Fn 𝐴 ↔ 𝐹 Fn 𝐴)) |
4 | 3 | biimprd 251 |
. . . . 5
⊢ (◡◡𝐹 = 𝐹 → (𝐹 Fn 𝐴 → ◡◡𝐹 Fn 𝐴)) |
5 | 2, 4 | sylbi 220 |
. . . 4
⊢ (Rel
𝐹 → (𝐹 Fn 𝐴 → ◡◡𝐹 Fn 𝐴)) |
6 | 1, 5 | mpcom 38 |
. . 3
⊢ (𝐹 Fn 𝐴 → ◡◡𝐹 Fn 𝐴) |
7 | 6 | anim1ci 619 |
. 2
⊢ ((𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵) → (◡𝐹 Fn 𝐵 ∧ ◡◡𝐹 Fn 𝐴)) |
8 | | dff1o4 6639 |
. 2
⊢ (𝐹:𝐴–1-1-onto→𝐵 ↔ (𝐹 Fn 𝐴 ∧ ◡𝐹 Fn 𝐵)) |
9 | | dff1o4 6639 |
. 2
⊢ (◡𝐹:𝐵–1-1-onto→𝐴 ↔ (◡𝐹 Fn 𝐵 ∧ ◡◡𝐹 Fn 𝐴)) |
10 | 7, 8, 9 | 3imtr4i 295 |
1
⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴) |