Theorem f1ocnvfv2 7275

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 6848	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝐹 ∘ ◡𝐹) = ( I ↾ 𝐵))
2	1	fveq1d 6883	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶))
3	2	adantr 485	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶))
4		f1ocnv 6833	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)
5		f1of 6820	. . . 4 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 → ◡𝐹:𝐵⟶𝐴)
6	4, 5	syl 18	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵⟶𝐴)
7		fvco3 6981	. . 3 ⊢ ((◡𝐹:𝐵⟶𝐴 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶)))
8	6, 7	sylan 591	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶)))
9		fvresi 7171	. . 3 ⊢ (𝐶 ∈ 𝐵 → (( I ↾ 𝐵)‘𝐶) = 𝐶)
10	9	adantl 486	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (( I ↾ 𝐵)‘𝐶) = 𝐶)
11	3, 8, 10	3eqtr3d 2806	1 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (𝐹‘(◡𝐹‘𝐶)) = 𝐶)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1570   ∈ wcel 2143   I cid 5555  ^◡ccnv 5660   ↾ cres 5663   ∘ ccom 5665  ⟶wf 6532  –1-1-onto→wf1o 6535  ‘cfv 6536

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5257  ax-nul 5269  ax-pr 5404

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-nf 1814  df-sb 2097  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-ne 2959  df-ral 3080  df-rex 3090  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4873  df-br 5110  df-opab 5174  df-id 5556  df-xp 5667  df-rel 5668  df-cnv 5669  df-co 5670  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674  df-iota 6492  df-fun 6538  df-fn 6539  df-f 6540  df-f1 6541  df-fo 6542  df-f1o 6543  df-fv 6544

This theorem is referenced by:  f1ocnvfvb  7277  fveqf1o  7300  isocnv  7328  f1oiso2  7350  weniso  7352  dif1enlem  9140  dif1en  9142  ordiso2  9473  cantnfle  9636  cantnfp1lem3  9645  cantnflem1b  9651  cantnflem1d  9653  cantnflem1  9654  cnfcom2lem  9666  cnfcom2  9667  cnfcom3lem  9668  acndom2  10034  iunfictbso  10094  ttukeylem7  10494  fpwwe2lem5  10615  fpwwe2lem6  10616  uzrdglem  13989  uzrdgsuci  13992  fzennn  14000  axdc4uzlem  14015  seqf1olem1  14073  seqf1olem2  14074  hashfz1  14378  seqcoll  14497  seqcoll2  14498  summolem3  15761  summolem2a  15762  ackbijnn  15878  prodmolem3  15983  prodmolem2a  15984  sadcaddlem  16510  sadaddlem  16519  sadasslem  16523  sadeq  16525  phimullem  16833  eulerthlem2  16836  catcisolem  18162  mgmhmf1o  18753  mhmf1o  18849  ghmf1o  19313  f1omvdconj  19511  gsumval3eu  19969  gsumval3  19972  rngisom1  20544  fidomndrnglem  20876  lmhmf1o  21167  basqtop  23868  tgqtop  23869  ordthmeolem  23958  symgtgp  24263  imasf1obl  24645  xrhmeo  25105  ovoliunlem2  25662  vitalilem2  25768  dvcnvlem  26135  dvcnv  26136  dvcnvre  26178  efif1olem4  26710  eff1olem  26713  eflog  26741  dvrelog  26802  dvlog  26816  asinrebnd  27066  sqff1o  27346  lgsqrlem4  27513  addonbday  28472  noseqrdglem  28498  noseqrdgsuc  28501  bdayfinlem  28679  cnvmot  28810  f1otrg  29220  f1otrge  29221  axcontlem10  29323  usgrnbcnvfv  29715  wlkiswwlks2lem4  30221  clwlkclwwlklem2a4  30348  cnvunop  32270  unopadj  32271  bracnvbra  32465  ccatws1f1o  33271  mndlactf1o  33350  mndractf1o  33351  abliso  33355  cycpmco2lem4  33449  cycpmco2lem5  33450  cycpmco2lem6  33451  cycpmco2lem7  33452  cycpmco2  33453  mndpluscn  34316  vonf1oonfo  35599  cvmfolem  35771  cvmliftlem6  35782  f1ocan1fv  38377  ismtycnv  38453  ismtyima  38454  ismtybndlem  38457  rngoisocnv  38632  lautcnvle  40863  lautcvr  40866  lautj  40867  lautm  40868  ltrncnvatb  40912  ltrncnvel  40916  ltrncnv  40920  ltrneq2  40922  cdlemg17h  41442  diainN  41831  diasslssN  41833  doca3N  41901  dihcnvid2  42047  dochocss  42140  mapdcnvid2  42431  sticksstones19  42932  rmxyval  43642  brpermmodelcnv  45713  permaxrep  45715  isuspgrim0lem  48658  isuspgrim0  48659  upgrimwlklem3  48664  uhgrimisgrgriclem  48695  clnbgrgrimlem  48698  uspgrlimlem1  48753  uspgrlimlem2  48754  uspgrlimlem3  48755  uspgrlimlem4  48756  grlicsym  48778  imaf1homlem  49885  uptrar  49994