Theorem f1ocnvfv2 7220

Description: The value of the converse value of a one-to-one onto function. (Contributed by NM, 20-May-2004.)

Assertion

Ref	Expression
f1ocnvfv2	⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (𝐹‘(◡𝐹‘𝐶)) = 𝐶)

Proof of Theorem f1ocnvfv2

Step	Hyp	Ref	Expression
1		f1ococnv2 6798	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝐹 ∘ ◡𝐹) = ( I ↾ 𝐵))
2	1	fveq1d 6833	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶))
3	2	adantr 480	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶))
4		f1ocnv 6783	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)
5		f1of 6771	. . . 4 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 → ◡𝐹:𝐵⟶𝐴)
6	4, 5	syl 17	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵⟶𝐴)
7		fvco3 6930	. . 3 ⊢ ((◡𝐹:𝐵⟶𝐴 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶)))
8	6, 7	sylan 580	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶)))
9		fvresi 7116	. . 3 ⊢ (𝐶 ∈ 𝐵 → (( I ↾ 𝐵)‘𝐶) = 𝐶)
10	9	adantl 481	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (( I ↾ 𝐵)‘𝐶) = 𝐶)
11	3, 8, 10	3eqtr3d 2776	1 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (𝐹‘(◡𝐹‘𝐶)) = 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1541   ∈ wcel 2113   I cid 5515  ^◡ccnv 5620   ↾ cres 5623   ∘ ccom 5625  ⟶wf 6485  –1-1-onto→wf1o 6488  ‘cfv 6489

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-ne 2930  df-ral 3049  df-rex 3058  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-br 5096  df-opab 5158  df-id 5516  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-iota 6445  df-fun 6491  df-fn 6492  df-f 6493  df-f1 6494  df-fo 6495  df-f1o 6496  df-fv 6497

This theorem is referenced by:  f1ocnvfvb  7222  fveqf1o  7245  isocnv  7273  f1oiso2  7295  weniso  7297  dif1enlem  9080  dif1en  9082  ordiso2  9412  cantnfle  9572  cantnfp1lem3  9581  cantnflem1b  9587  cantnflem1d  9589  cantnflem1  9590  cnfcom2lem  9602  cnfcom2  9603  cnfcom3lem  9604  acndom2  9956  iunfictbso  10016  ttukeylem7  10417  fpwwe2lem5  10537  fpwwe2lem6  10538  uzrdglem  13871  uzrdgsuci  13874  fzennn  13882  axdc4uzlem  13897  seqf1olem1  13955  seqf1olem2  13956  hashfz1  14260  seqcoll  14378  seqcoll2  14379  summolem3  15628  summolem2a  15629  ackbijnn  15742  prodmolem3  15847  prodmolem2a  15848  sadcaddlem  16375  sadaddlem  16384  sadasslem  16388  sadeq  16390  phimullem  16697  eulerthlem2  16700  catcisolem  18025  mgmhmf1o  18616  mhmf1o  18712  ghmf1o  19168  f1omvdconj  19366  gsumval3eu  19824  gsumval3  19827  rngisom1  20393  fidomndrnglem  20696  lmhmf1o  20989  basqtop  23646  tgqtop  23647  ordthmeolem  23736  symgtgp  24041  imasf1obl  24423  xrhmeo  24891  ovoliunlem2  25451  vitalilem2  25557  dvcnvlem  25927  dvcnv  25928  dvcnvre  25971  efif1olem4  26501  eff1olem  26504  eflog  26532  dvrelog  26593  dvlog  26607  asinrebnd  26858  sqff1o  27139  lgsqrlem4  27307  noseqrdglem  28255  noseqrdgsuc  28258  cnvmot  28539  f1otrg  28869  f1otrge  28870  axcontlem10  28972  usgrnbcnvfv  29364  wlkiswwlks2lem4  29871  clwlkclwwlklem2a4  29998  cnvunop  31919  unopadj  31920  bracnvbra  32114  ccatws1f1o  32961  mndlactf1o  33040  mndractf1o  33041  abliso  33046  cycpmco2lem4  33139  cycpmco2lem5  33140  cycpmco2lem6  33141  cycpmco2lem7  33142  cycpmco2  33143  mndpluscn  34011  cvmfolem  35395  cvmliftlem6  35406  f1ocan1fv  37839  ismtycnv  37915  ismtyima  37916  ismtybndlem  37919  rngoisocnv  38094  lautcnvle  40261  lautcvr  40264  lautj  40265  lautm  40266  ltrncnvatb  40310  ltrncnvel  40314  ltrncnv  40318  ltrneq2  40320  cdlemg17h  40840  diainN  41229  diasslssN  41231  doca3N  41299  dihcnvid2  41445  dochocss  41538  mapdcnvid2  41829  sticksstones19  42331  rmxyval  43072  brpermmodelcnv  45161  permaxrep  45163  isuspgrim0lem  48055  isuspgrim0  48056  upgrimwlklem3  48061  uhgrimisgrgriclem  48092  clnbgrgrimlem  48095  uspgrlimlem1  48150  uspgrlimlem2  48151  uspgrlimlem3  48152  uspgrlimlem4  48153  grlicsym  48175  imaf1homlem  49268  uptrar  49377