| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > f1ocnvb | Structured version Visualization version GIF version | ||
| Description: A relation is a one-to-one onto function iff its converse is a one-to-one onto function with domain and codomain/range interchanged. (Contributed by NM, 8-Dec-2003.) |
| Ref | Expression |
|---|---|
| f1ocnvb | ⊢ (Rel 𝐹 → (𝐹:𝐴–1-1-onto→𝐵 ↔ ◡𝐹:𝐵–1-1-onto→𝐴)) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | f1ocnv 6819 | . 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴) | |
| 2 | f1ocnv 6819 | . . 3 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 → ◡◡𝐹:𝐴–1-1-onto→𝐵) | |
| 3 | dfrel2 6175 | . . . 4 ⊢ (Rel 𝐹 ↔ ◡◡𝐹 = 𝐹) | |
| 4 | f1oeq1 6794 | . . . 4 ⊢ (◡◡𝐹 = 𝐹 → (◡◡𝐹:𝐴–1-1-onto→𝐵 ↔ 𝐹:𝐴–1-1-onto→𝐵)) | |
| 5 | 3, 4 | sylbi 219 | . . 3 ⊢ (Rel 𝐹 → (◡◡𝐹:𝐴–1-1-onto→𝐵 ↔ 𝐹:𝐴–1-1-onto→𝐵)) |
| 6 | 2, 5 | imbitrid 246 | . 2 ⊢ (Rel 𝐹 → (◡𝐹:𝐵–1-1-onto→𝐴 → 𝐹:𝐴–1-1-onto→𝐵)) |
| 7 | 1, 6 | impbid2 228 | 1 ⊢ (Rel 𝐹 → (𝐹:𝐴–1-1-onto→𝐵 ↔ ◡𝐹:𝐵–1-1-onto→𝐴)) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ↔ wb 208 = wceq 1560 ◡ccnv 5646 Rel wrel 5652 –1-1-onto→wf1o 6520 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1815 ax-4 1829 ax-5 1930 ax-6 1987 ax-7 2028 ax-8 2144 ax-9 2152 ax-ext 2734 ax-sep 5246 ax-pr 5390 |
| This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3an 1100 df-tru 1563 df-fal 1573 df-ex 1800 df-sb 2091 df-clab 2741 df-cleq 2754 df-clel 2837 df-rab 3415 df-v 3456 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-nul 4286 df-if 4481 df-sn 4583 df-pr 4585 df-op 4589 df-br 5101 df-opab 5163 df-xp 5653 df-rel 5654 df-cnv 5655 df-co 5656 df-dm 5657 df-rn 5658 df-fun 6523 df-fn 6524 df-f 6525 df-f1 6526 df-fo 6527 df-f1o 6528 |
| This theorem is referenced by: hasheqf1oi 14364 |
| Copyright terms: Public domain | W3C validator |