![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > f1ocnvdm | Structured version Visualization version GIF version |
Description: The value of the converse of a one-to-one onto function belongs to its domain. (Contributed by NM, 26-May-2006.) |
Ref | Expression |
---|---|
f1ocnvdm | ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (◡𝐹‘𝐶) ∈ 𝐴) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | f1ocnv 6607 | . . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴) | |
2 | f1of 6595 | . . 3 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 → ◡𝐹:𝐵⟶𝐴) | |
3 | 1, 2 | syl 17 | . 2 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵⟶𝐴) |
4 | 3 | ffvelrnda 6835 | 1 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (◡𝐹‘𝐶) ∈ 𝐴) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 400 ∈ wcel 2112 ◡ccnv 5516 ⟶wf 6324 –1-1-onto→wf1o 6327 ‘cfv 6328 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1798 ax-4 1812 ax-5 1912 ax-6 1971 ax-7 2016 ax-8 2114 ax-9 2122 ax-10 2143 ax-11 2159 ax-12 2176 ax-ext 2730 ax-sep 5162 ax-nul 5169 ax-pr 5291 |
This theorem depends on definitions: df-bi 210 df-an 401 df-or 846 df-3an 1087 df-tru 1542 df-ex 1783 df-nf 1787 df-sb 2071 df-mo 2558 df-eu 2589 df-clab 2737 df-cleq 2751 df-clel 2831 df-nfc 2899 df-ral 3073 df-rex 3074 df-v 3409 df-sbc 3694 df-dif 3857 df-un 3859 df-in 3861 df-ss 3871 df-nul 4222 df-if 4414 df-sn 4516 df-pr 4518 df-op 4522 df-uni 4792 df-br 5026 df-opab 5088 df-id 5423 df-xp 5523 df-rel 5524 df-cnv 5525 df-co 5526 df-dm 5527 df-rn 5528 df-iota 6287 df-fun 6330 df-fn 6331 df-f 6332 df-f1 6333 df-fo 6334 df-f1o 6335 df-fv 6336 |
This theorem is referenced by: f1oiso2 7092 f1ocnvfv3 7139 dif1enlem 8765 rexdif1en 8766 dif1en 8767 uzrdglem 13359 uzrdgsuci 13362 fzennn 13370 cardfz 13372 fzfi 13374 iunmbl2 24242 f1otrg 26749 axcontlem10 26851 wlkiswwlks2lem5 27743 clwlkclwwlklem2a 27867 cnvbraval 29977 cnvbracl 29978 cycpmco2lem6 30909 cycpmco2 30911 mndpluscn 31382 ismtycnv 35505 rngoisocnv 35684 lautcnvclN 37649 lautcnvle 37650 lautcvr 37653 lautj 37654 lautm 37655 ltrncnvatb 37699 diacnvclN 38612 dihcnvcl 38832 dihlspsnat 38894 dihglblem6 38901 dochocss 38927 dochnoncon 38952 mapdcnvcl 39213 rmxyelxp 40211 isomuspgrlem1 44697 isomgrsym 44706 |
Copyright terms: Public domain | W3C validator |