![]() |
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 6861 | . . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝐹 ∘ ◡𝐹) = ( I ↾ 𝐵)) | |
2 | 1 | fveq1d 6894 | . . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶)) |
3 | 2 | adantr 482 | . 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶)) |
4 | f1ocnv 6846 | . . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴) | |
5 | f1of 6834 | . . . 4 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 → ◡𝐹:𝐵⟶𝐴) | |
6 | 4, 5 | syl 17 | . . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵⟶𝐴) |
7 | fvco3 6991 | . . 3 ⊢ ((◡𝐹:𝐵⟶𝐴 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶))) | |
8 | 6, 7 | sylan 581 | . 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶))) |
9 | fvresi 7171 | . . 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 5574 ◡ccnv 5676 ↾ cres 5679 ∘ ccom 5681 ⟶wf 6540 –1-1-onto→wf1o 6543 ‘cfv 6544 |
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 5300 ax-nul 5307 ax-pr 5428 |
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 2942 df-ral 3063 df-rex 3072 df-rab 3434 df-v 3477 df-dif 3952 df-un 3954 df-in 3956 df-ss 3966 df-nul 4324 df-if 4530 df-sn 4630 df-pr 4632 df-op 4636 df-uni 4910 df-br 5150 df-opab 5212 df-id 5575 df-xp 5683 df-rel 5684 df-cnv 5685 df-co 5686 df-dm 5687 df-rn 5688 df-res 5689 df-ima 5690 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-fv 6552 |
This theorem is referenced by: f1ocnvfvb 7277 fveqf1o 7301 isocnv 7327 f1oiso2 7349 weniso 7351 dif1enlem 9156 dif1enlemOLD 9157 dif1en 9160 dif1enOLD 9162 ordiso2 9510 cantnfle 9666 cantnfp1lem3 9675 cantnflem1b 9681 cantnflem1d 9683 cantnflem1 9684 cnfcom2lem 9696 cnfcom2 9697 cnfcom3lem 9698 acndom2 10049 iunfictbso 10109 ttukeylem7 10510 fpwwe2lem5 10630 fpwwe2lem6 10631 uzrdglem 13922 uzrdgsuci 13925 fzennn 13933 axdc4uzlem 13948 seqf1olem1 14007 seqf1olem2 14008 hashfz1 14306 seqcoll 14425 seqcoll2 14426 summolem3 15660 summolem2a 15661 ackbijnn 15774 prodmolem3 15877 prodmolem2a 15878 sadcaddlem 16398 sadaddlem 16407 sadasslem 16411 sadeq 16413 phimullem 16712 eulerthlem2 16715 catcisolem 18060 mhmf1o 18682 ghmf1o 19122 f1omvdconj 19314 gsumval3eu 19772 gsumval3 19775 lmhmf1o 20657 fidomndrnglem 20925 basqtop 23215 tgqtop 23216 ordthmeolem 23305 symgtgp 23610 imasf1obl 23997 xrhmeo 24462 ovoliunlem2 25020 vitalilem2 25126 dvcnvlem 25493 dvcnv 25494 dvcnvre 25536 efif1olem4 26054 eff1olem 26057 eflog 26085 dvrelog 26145 dvlog 26159 asinrebnd 26406 sqff1o 26686 lgsqrlem4 26852 cnvmot 27792 f1otrg 28122 f1otrge 28123 axcontlem10 28231 usgrnbcnvfv 28622 wlkiswwlks2lem4 29126 clwlkclwwlklem2a4 29250 cnvunop 31171 unopadj 31172 bracnvbra 31366 abliso 32197 cycpmco2lem4 32288 cycpmco2lem5 32289 cycpmco2lem6 32290 cycpmco2lem7 32291 cycpmco2 32292 mndpluscn 32906 cvmfolem 34270 cvmliftlem6 34281 f1ocan1fv 36594 ismtycnv 36670 ismtyima 36671 ismtybndlem 36674 rngoisocnv 36849 lautcnvle 38960 lautcvr 38963 lautj 38964 lautm 38965 ltrncnvatb 39009 ltrncnvel 39013 ltrncnv 39017 ltrneq2 39019 cdlemg17h 39539 diainN 39928 diasslssN 39930 doca3N 39998 dihcnvid2 40144 dochocss 40237 mapdcnvid2 40528 sticksstones19 40981 rmxyval 41654 isomgrsym 46504 mgmhmf1o 46557 rngisom1 46718 |
Copyright terms: Public domain | W3C validator |