![]() |
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 6857 | . . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝐹 ∘ ◡𝐹) = ( I ↾ 𝐵)) | |
2 | 1 | fveq1d 6890 | . . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶)) |
3 | 2 | adantr 482 | . 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶)) |
4 | f1ocnv 6842 | . . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴) | |
5 | f1of 6830 | . . . 4 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 → ◡𝐹:𝐵⟶𝐴) | |
6 | 4, 5 | syl 17 | . . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵⟶𝐴) |
7 | fvco3 6986 | . . 3 ⊢ ((◡𝐹:𝐵⟶𝐴 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶))) | |
8 | 6, 7 | sylan 581 | . 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶))) |
9 | fvresi 7166 | . . 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 5572 ◡ccnv 5674 ↾ cres 5677 ∘ ccom 5679 ⟶wf 6536 –1-1-onto→wf1o 6539 ‘cfv 6540 |
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 5298 ax-nul 5305 ax-pr 5426 |
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 3950 df-un 3952 df-in 3954 df-ss 3964 df-nul 4322 df-if 4528 df-sn 4628 df-pr 4630 df-op 4634 df-uni 4908 df-br 5148 df-opab 5210 df-id 5573 df-xp 5681 df-rel 5682 df-cnv 5683 df-co 5684 df-dm 5685 df-rn 5686 df-res 5687 df-ima 5688 df-iota 6492 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 |
This theorem is referenced by: f1ocnvfvb 7272 fveqf1o 7296 isocnv 7322 f1oiso2 7344 weniso 7346 dif1enlem 9152 dif1enlemOLD 9153 dif1en 9156 dif1enOLD 9158 ordiso2 9506 cantnfle 9662 cantnfp1lem3 9671 cantnflem1b 9677 cantnflem1d 9679 cantnflem1 9680 cnfcom2lem 9692 cnfcom2 9693 cnfcom3lem 9694 acndom2 10045 iunfictbso 10105 ttukeylem7 10506 fpwwe2lem5 10626 fpwwe2lem6 10627 uzrdglem 13918 uzrdgsuci 13921 fzennn 13929 axdc4uzlem 13944 seqf1olem1 14003 seqf1olem2 14004 hashfz1 14302 seqcoll 14421 seqcoll2 14422 summolem3 15656 summolem2a 15657 ackbijnn 15770 prodmolem3 15873 prodmolem2a 15874 sadcaddlem 16394 sadaddlem 16403 sadasslem 16407 sadeq 16409 phimullem 16708 eulerthlem2 16711 catcisolem 18056 mhmf1o 18678 ghmf1o 19116 f1omvdconj 19307 gsumval3eu 19764 gsumval3 19767 lmhmf1o 20645 fidomndrnglem 20910 basqtop 23197 tgqtop 23198 ordthmeolem 23287 symgtgp 23592 imasf1obl 23979 xrhmeo 24444 ovoliunlem2 25002 vitalilem2 25108 dvcnvlem 25475 dvcnv 25476 dvcnvre 25518 efif1olem4 26036 eff1olem 26039 eflog 26067 dvrelog 26127 dvlog 26141 asinrebnd 26386 sqff1o 26666 lgsqrlem4 26832 cnvmot 27772 f1otrg 28102 f1otrge 28103 axcontlem10 28211 usgrnbcnvfv 28602 wlkiswwlks2lem4 29106 clwlkclwwlklem2a4 29230 cnvunop 31149 unopadj 31150 bracnvbra 31344 abliso 32175 cycpmco2lem4 32266 cycpmco2lem5 32267 cycpmco2lem6 32268 cycpmco2lem7 32269 cycpmco2 32270 mndpluscn 32844 cvmfolem 34208 cvmliftlem6 34219 f1ocan1fv 36532 ismtycnv 36608 ismtyima 36609 ismtybndlem 36612 rngoisocnv 36787 lautcnvle 38898 lautcvr 38901 lautj 38902 lautm 38903 ltrncnvatb 38947 ltrncnvel 38951 ltrncnv 38955 ltrneq2 38957 cdlemg17h 39477 diainN 39866 diasslssN 39868 doca3N 39936 dihcnvid2 40082 dochocss 40175 mapdcnvid2 40466 sticksstones19 40919 rmxyval 41587 isomgrsym 46439 mgmhmf1o 46492 rngisom1 46652 |
Copyright terms: Public domain | W3C validator |