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 6687 | . . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝐹 ∘ ◡𝐹) = ( I ↾ 𝐵)) | |
2 | 1 | fveq1d 6719 | . . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶)) |
3 | 2 | adantr 484 | . 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶)) |
4 | f1ocnv 6673 | . . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴) | |
5 | f1of 6661 | . . . 4 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 → ◡𝐹:𝐵⟶𝐴) | |
6 | 4, 5 | syl 17 | . . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵⟶𝐴) |
7 | fvco3 6810 | . . 3 ⊢ ((◡𝐹:𝐵⟶𝐴 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶))) | |
8 | 6, 7 | sylan 583 | . 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶))) |
9 | fvresi 6988 | . . 3 ⊢ (𝐶 ∈ 𝐵 → (( I ↾ 𝐵)‘𝐶) = 𝐶) | |
10 | 9 | adantl 485 | . 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (( I ↾ 𝐵)‘𝐶) = 𝐶) |
11 | 3, 8, 10 | 3eqtr3d 2785 | 1 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (𝐹‘(◡𝐹‘𝐶)) = 𝐶) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 399 = wceq 1543 ∈ wcel 2110 I cid 5454 ◡ccnv 5550 ↾ cres 5553 ∘ ccom 5555 ⟶wf 6376 –1-1-onto→wf1o 6379 ‘cfv 6380 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-10 2141 ax-11 2158 ax-12 2175 ax-ext 2708 ax-sep 5192 ax-nul 5199 ax-pr 5322 |
This theorem depends on definitions: df-bi 210 df-an 400 df-or 848 df-3an 1091 df-tru 1546 df-fal 1556 df-ex 1788 df-nf 1792 df-sb 2071 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2886 df-ne 2941 df-ral 3066 df-rex 3067 df-rab 3070 df-v 3410 df-dif 3869 df-un 3871 df-in 3873 df-ss 3883 df-nul 4238 df-if 4440 df-sn 4542 df-pr 4544 df-op 4548 df-uni 4820 df-br 5054 df-opab 5116 df-id 5455 df-xp 5557 df-rel 5558 df-cnv 5559 df-co 5560 df-dm 5561 df-rn 5562 df-res 5563 df-ima 5564 df-iota 6338 df-fun 6382 df-fn 6383 df-f 6384 df-f1 6385 df-fo 6386 df-f1o 6387 df-fv 6388 |
This theorem is referenced by: f1ocnvfvb 7090 fveqf1o 7113 isocnv 7139 f1oiso2 7161 weniso 7163 dif1enlem 8838 dif1en 8840 ordiso2 9131 cantnfle 9286 cantnfp1lem3 9295 cantnflem1b 9301 cantnflem1d 9303 cantnflem1 9304 cnfcom2lem 9316 cnfcom2 9317 cnfcom3lem 9318 acndom2 9668 iunfictbso 9728 ttukeylem7 10129 fpwwe2lem5 10249 fpwwe2lem6 10250 uzrdglem 13530 uzrdgsuci 13533 fzennn 13541 axdc4uzlem 13556 seqf1olem1 13615 seqf1olem2 13616 hashfz1 13912 seqcoll 14030 seqcoll2 14031 summolem3 15278 summolem2a 15279 ackbijnn 15392 prodmolem3 15495 prodmolem2a 15496 sadcaddlem 16016 sadaddlem 16025 sadasslem 16029 sadeq 16031 phimullem 16332 eulerthlem2 16335 catcisolem 17616 mhmf1o 18228 ghmf1o 18652 f1omvdconj 18838 gsumval3eu 19289 gsumval3 19292 lmhmf1o 20083 fidomndrnglem 20344 basqtop 22608 tgqtop 22609 ordthmeolem 22698 symgtgp 23003 imasf1obl 23386 xrhmeo 23843 ovoliunlem2 24400 vitalilem2 24506 dvcnvlem 24873 dvcnv 24874 dvcnvre 24916 efif1olem4 25434 eff1olem 25437 eflog 25465 dvrelog 25525 dvlog 25539 asinrebnd 25784 sqff1o 26064 lgsqrlem4 26230 cnvmot 26632 f1otrg 26962 f1otrge 26963 axcontlem10 27064 usgrnbcnvfv 27453 wlkiswwlks2lem4 27956 clwlkclwwlklem2a4 28080 cnvunop 29999 unopadj 30000 bracnvbra 30194 abliso 31024 cycpmco2lem4 31115 cycpmco2lem5 31116 cycpmco2lem6 31117 cycpmco2lem7 31118 cycpmco2 31119 mndpluscn 31590 cvmfolem 32954 cvmliftlem6 32965 f1ocan1fv 35621 ismtycnv 35697 ismtyima 35698 ismtybndlem 35701 rngoisocnv 35876 lautcnvle 37840 lautcvr 37843 lautj 37844 lautm 37845 ltrncnvatb 37889 ltrncnvel 37893 ltrncnv 37897 ltrneq2 37899 cdlemg17h 38419 diainN 38808 diasslssN 38810 doca3N 38878 dihcnvid2 39024 dochocss 39117 mapdcnvid2 39408 sticksstones19 39843 rmxyval 40440 isomgrsym 44961 mgmhmf1o 45014 |
Copyright terms: Public domain | W3C validator |