Theorem f1ocnvfv2 7221

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 6794	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝐹 ∘ ◡𝐹) = ( I ↾ 𝐵))
2	1	fveq1d 6829	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶))
3	2	adantr 481	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶))
4		f1ocnv 6779	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)
5		f1of 6767	. . . 4 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 → ◡𝐹:𝐵⟶𝐴)
6	4, 5	syl 17	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵⟶𝐴)
7		fvco3 6927	. . 3 ⊢ ((◡𝐹:𝐵⟶𝐴 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶)))
8	6, 7	sylan 586	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶)))
9		fvresi 7117	. . 3 ⊢ (𝐶 ∈ 𝐵 → (( I ↾ 𝐵)‘𝐶) = 𝐶)
10	9	adantl 482	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (( I ↾ 𝐵)‘𝐶) = 𝐶)
11	3, 8, 10	3eqtr3d 2782	1 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (𝐹‘(◡𝐹‘𝐶)) = 𝐶)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1547   ∈ wcel 2119   I cid 5512  ^◡ccnv 5617   ↾ cres 5620   ∘ ccom 5622  ⟶wf 6481  –1-1-onto→wf1o 6484  ‘cfv 6485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-sep 5218  ax-nul 5228  ax-pr 5362

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-ne 2935  df-ral 3054  df-rex 3064  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-uni 4839  df-br 5073  df-opab 5135  df-id 5513  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493

This theorem is referenced by:  f1ocnvfvb  7223  fveqf1o  7246  isocnv  7274  f1oiso2  7296  weniso  7298  dif1enlem  9084  dif1en  9086  ordiso2  9420  cantnfle  9583  cantnfp1lem3  9592  cantnflem1b  9598  cantnflem1d  9600  cantnflem1  9601  cnfcom2lem  9613  cnfcom2  9614  cnfcom3lem  9615  acndom2  9967  iunfictbso  10027  ttukeylem7  10428  fpwwe2lem5  10549  fpwwe2lem6  10550  uzrdglem  13910  uzrdgsuci  13913  fzennn  13921  axdc4uzlem  13936  seqf1olem1  13994  seqf1olem2  13995  hashfz1  14299  seqcoll  14417  seqcoll2  14418  summolem3  15667  summolem2a  15668  ackbijnn  15784  prodmolem3  15889  prodmolem2a  15890  sadcaddlem  16417  sadaddlem  16426  sadasslem  16430  sadeq  16432  phimullem  16740  eulerthlem2  16743  catcisolem  18068  mgmhmf1o  18659  mhmf1o  18755  ghmf1o  19214  f1omvdconj  19412  gsumval3eu  19870  gsumval3  19873  rngisom1  20437  fidomndrnglem  20744  lmhmf1o  21036  basqtop  23694  tgqtop  23695  ordthmeolem  23784  symgtgp  24089  imasf1obl  24471  xrhmeo  24931  ovoliunlem2  25488  vitalilem2  25594  dvcnvlem  25961  dvcnv  25962  dvcnvre  26004  efif1olem4  26527  eff1olem  26530  eflog  26558  dvrelog  26619  dvlog  26633  asinrebnd  26883  sqff1o  27163  lgsqrlem4  27330  addonbday  28289  noseqrdglem  28315  noseqrdgsuc  28318  bdayfinlem  28496  cnvmot  28627  f1otrg  28957  f1otrge  28958  axcontlem10  29060  usgrnbcnvfv  29452  wlkiswwlks2lem4  29958  clwlkclwwlklem2a4  30085  cnvunop  32007  unopadj  32008  bracnvbra  32202  ccatws1f1o  33030  mndlactf1o  33109  mndractf1o  33110  abliso  33115  cycpmco2lem4  33210  cycpmco2lem5  33211  cycpmco2lem6  33212  cycpmco2lem7  33213  cycpmco2  33214  mndpluscn  34110  cvmfolem  35507  cvmliftlem6  35518  f1ocan1fv  38093  ismtycnv  38169  ismtyima  38170  ismtybndlem  38173  rngoisocnv  38348  lautcnvle  40581  lautcvr  40584  lautj  40585  lautm  40586  ltrncnvatb  40630  ltrncnvel  40634  ltrncnv  40638  ltrneq2  40640  cdlemg17h  41160  diainN  41549  diasslssN  41551  doca3N  41619  dihcnvid2  41765  dochocss  41858  mapdcnvid2  42149  sticksstones19  42650  rmxyval  43360  brpermmodelcnv  45448  permaxrep  45450  isuspgrim0lem  48384  isuspgrim0  48385  upgrimwlklem3  48390  uhgrimisgrgriclem  48421  clnbgrgrimlem  48424  uspgrlimlem1  48479  uspgrlimlem2  48480  uspgrlimlem3  48481  uspgrlimlem4  48482  grlicsym  48504  imaf1homlem  49597  uptrar  49706