![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > f1ocnvfv2 | Structured version Visualization version GIF version |
Description: The value of the converse value of a one-to-one onto function. (Contributed by NM, 20-May-2004.) |
Ref | Expression |
---|---|
f1ocnvfv2 | ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (𝐹‘(◡𝐹‘𝐶)) = 𝐶) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | f1ococnv2 6812 | . . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝐹 ∘ ◡𝐹) = ( I ↾ 𝐵)) | |
2 | 1 | fveq1d 6845 | . . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶)) |
3 | 2 | adantr 482 | . 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶)) |
4 | f1ocnv 6797 | . . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴) | |
5 | f1of 6785 | . . . 4 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 → ◡𝐹:𝐵⟶𝐴) | |
6 | 4, 5 | syl 17 | . . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵⟶𝐴) |
7 | fvco3 6941 | . . 3 ⊢ ((◡𝐹:𝐵⟶𝐴 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶))) | |
8 | 6, 7 | sylan 581 | . 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶))) |
9 | fvresi 7120 | . . 3 ⊢ (𝐶 ∈ 𝐵 → (( I ↾ 𝐵)‘𝐶) = 𝐶) | |
10 | 9 | adantl 483 | . 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (( I ↾ 𝐵)‘𝐶) = 𝐶) |
11 | 3, 8, 10 | 3eqtr3d 2781 | 1 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (𝐹‘(◡𝐹‘𝐶)) = 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 397 = wceq 1542 ∈ wcel 2107 I cid 5531 ◡ccnv 5633 ↾ cres 5636 ∘ ccom 5638 ⟶wf 6493 –1-1-onto→wf1o 6496 ‘cfv 6497 |
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 1914 ax-6 1972 ax-7 2012 ax-8 2109 ax-9 2117 ax-10 2138 ax-11 2155 ax-12 2172 ax-ext 2704 ax-sep 5257 ax-nul 5264 ax-pr 5385 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 847 df-3an 1090 df-tru 1545 df-fal 1555 df-ex 1783 df-nf 1787 df-sb 2069 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-ne 2941 df-ral 3062 df-rex 3071 df-rab 3407 df-v 3446 df-dif 3914 df-un 3916 df-in 3918 df-ss 3928 df-nul 4284 df-if 4488 df-sn 4588 df-pr 4590 df-op 4594 df-uni 4867 df-br 5107 df-opab 5169 df-id 5532 df-xp 5640 df-rel 5641 df-cnv 5642 df-co 5643 df-dm 5644 df-rn 5645 df-res 5646 df-ima 5647 df-iota 6449 df-fun 6499 df-fn 6500 df-f 6501 df-f1 6502 df-fo 6503 df-f1o 6504 df-fv 6505 |
This theorem is referenced by: f1ocnvfvb 7226 fveqf1o 7250 isocnv 7276 f1oiso2 7298 weniso 7300 dif1enlem 9103 dif1enlemOLD 9104 dif1en 9107 dif1enOLD 9109 ordiso2 9456 cantnfle 9612 cantnfp1lem3 9621 cantnflem1b 9627 cantnflem1d 9629 cantnflem1 9630 cnfcom2lem 9642 cnfcom2 9643 cnfcom3lem 9644 acndom2 9995 iunfictbso 10055 ttukeylem7 10456 fpwwe2lem5 10576 fpwwe2lem6 10577 uzrdglem 13868 uzrdgsuci 13871 fzennn 13879 axdc4uzlem 13894 seqf1olem1 13953 seqf1olem2 13954 hashfz1 14252 seqcoll 14369 seqcoll2 14370 summolem3 15604 summolem2a 15605 ackbijnn 15718 prodmolem3 15821 prodmolem2a 15822 sadcaddlem 16342 sadaddlem 16351 sadasslem 16355 sadeq 16357 phimullem 16656 eulerthlem2 16659 catcisolem 18001 mhmf1o 18617 ghmf1o 19043 f1omvdconj 19233 gsumval3eu 19686 gsumval3 19689 lmhmf1o 20522 fidomndrnglem 20793 basqtop 23078 tgqtop 23079 ordthmeolem 23168 symgtgp 23473 imasf1obl 23860 xrhmeo 24325 ovoliunlem2 24883 vitalilem2 24989 dvcnvlem 25356 dvcnv 25357 dvcnvre 25399 efif1olem4 25917 eff1olem 25920 eflog 25948 dvrelog 26008 dvlog 26022 asinrebnd 26267 sqff1o 26547 lgsqrlem4 26713 cnvmot 27525 f1otrg 27855 f1otrge 27856 axcontlem10 27964 usgrnbcnvfv 28355 wlkiswwlks2lem4 28859 clwlkclwwlklem2a4 28983 cnvunop 30902 unopadj 30903 bracnvbra 31097 abliso 31936 cycpmco2lem4 32027 cycpmco2lem5 32028 cycpmco2lem6 32029 cycpmco2lem7 32030 cycpmco2 32031 mndpluscn 32564 cvmfolem 33930 cvmliftlem6 33941 f1ocan1fv 36231 ismtycnv 36307 ismtyima 36308 ismtybndlem 36311 rngoisocnv 36486 lautcnvle 38598 lautcvr 38601 lautj 38602 lautm 38603 ltrncnvatb 38647 ltrncnvel 38651 ltrncnv 38655 ltrneq2 38657 cdlemg17h 39177 diainN 39566 diasslssN 39568 doca3N 39636 dihcnvid2 39782 dochocss 39875 mapdcnvid2 40166 sticksstones19 40619 rmxyval 41282 isomgrsym 46114 mgmhmf1o 46167 |
Copyright terms: Public domain | W3C validator |