Theorem f1ocnvfv2 7316

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-1onto𝐵 ∧ 𝐶 ∈ 𝐵) → (𝐹‘(◡𝐹‘𝐶)) = 𝐶)

Proof of Theorem f1ocnvfv2

Step	Hyp	Ref	Expression
1		f1ococnv2 6883	. . . 4 ⊢ (𝐹:𝐴⟶1-1onto𝐵 → (𝐹 ∘ ◡𝐹) = ( I ↾ 𝐵))
2	1	fveq1d 6918	. . 3 ⊢ (𝐹:𝐴⟶1-1onto𝐵 → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶))
3	2	adantr 486	. 2 ⊢ ((𝐹:𝐴⟶1-1onto𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶))
4		f1ocnv 6867	. . . 4 ⊢ (𝐹:𝐴⟶1-1onto𝐵 → ◡𝐹:𝐵⟶1-1onto𝐴)
5		f1of 6854	. . . 4 ⊢ (◡𝐹:𝐵⟶1-1onto𝐴 → ◡𝐹:𝐵⟶𝐴)
6	4, 5	syl 18	. . 3 ⊢ (𝐹:𝐴⟶1-1onto𝐵 → ◡𝐹:𝐵⟶𝐴)
7		fvco3 7016	. . 3 ⊢ ((◡𝐹:𝐵⟶𝐴 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶)))
8	6, 7	sylan 592	. 2 ⊢ ((𝐹:𝐴⟶1-1onto𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶)))
9		fvresi 7209	. . 3 ⊢ (𝐶 ∈ 𝐵 → (( I ↾ 𝐵)‘𝐶) = 𝐶)
10	9	adantl 487	. 2 ⊢ ((𝐹:𝐴⟶1-1onto𝐵 ∧ 𝐶 ∈ 𝐵) → (( I ↾ 𝐵)‘𝐶) = 𝐶)
11	3, 8, 10	3eqtr3d 2806	1 ⊢ ((𝐹:𝐴⟶1-1onto𝐵 ∧ 𝐶 ∈ 𝐵) → (𝐹‘(◡𝐹‘𝐶)) = 𝐶)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2147   I cid 5552  ^◡ccnv 5657   ↾ cres 5660   ∘ ccom 5662  ⟶wf 6562  ⟶1-1ontowf1o 6565  ‘cfv 6566

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-br 5109  df-opab 5174  df-id 5553  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574

This theorem is used by:  f1ocnvfvb  7318  fveqf1o  7341  isocnv  7369  f1oiso2  7391  weniso  7395  dif1enlem  9213  dif1en  9215  ordiso2  9546  cantnfle  9709  cantnfp1lem3  9718  cantnflem1b  9724  cantnflem1d  9726  cantnflem1  9727  cnfcom2lem  9739  cnfcom2  9740  cnfcom3lem  9741  acndom2  10172  iunfictbso  10232  ttukeylem7  10632  fpwwe2lem5  10759  fpwwe2lem6  10760  uzrdglem  14140  uzrdgsuci  14143  fzennn  14151  axdc4uzlem  14166  seqf1olem1  14224  seqf1olem2  14225  hashfz1  14531  seqcoll  14650  seqcoll2  14651  summolem3  15924  summolem2a  15925  ackbijnn  16041  prodmolem3  16144  prodmolem2a  16145  sadcaddlem  16671  sadaddlem  16680  sadasslem  16684  sadeq  16686  phimullem  17000  eulerthlem2  17003  catcisolem  18335  mgmhmf1o  18939  mhmf1o  19041  ghmf1o  19512  f1omvdconj  19711  gsumval3eu  20169  gsumval3  20172  rngisom1  20747  fidomndrnglem  21081  lmhmf1o  21372  basqtop  24085  tgqtop  24086  ordthmeolem  24175  symgtgp  24480  imasf1obl  24862  xrhmeo  25322  ovoliunlem2  25879  vitalilem2  25985  dvcnvlem  26351  dvcnv  26352  dvcnvre  26394  efif1olem4  26930  eff1olem  26933  eflog  26961  dvrelog  27022  dvlog  27036  asinrebnd  27286  sqff1o  27566  lgsqrlem4  27733  addonbday  28722  noseqrdglem  28748  noseqrdgsuc  28751  bdayfinlem  28929  cnvmot  29061  f1otrg  29505  f1otrge  29506  axcontlem10  29608  usgrnbcnvfv  30003  wlkiswwlks2lem4  30518  clwlkclwwlklem2a4  30645  cnvunop  32577  unopadj  32578  bracnvbra  32772  ccatws1f1o  33610  mndlactf1o  33690  mndractf1o  33691  abliso  33695  cycpmco2lem4  33789  cycpmco2lem5  33790  cycpmco2lem6  33791  cycpmco2lem7  33792  cycpmco2  33793  mndpluscn  34669  vonf1oonfo  36090  cvmfolem  36252  cvmliftlem6  36263  f1ocan1fv  38928  ismtycnv  39002  ismtyima  39003  ismtybndlem  39006  rngoisocnv  39181  lautcnvle  41412  lautcvr  41415  lautj  41416  lautm  41417  ltrncnvatb  41461  ltrncnvel  41465  ltrncnv  41469  ltrneq2  41471  cdlemg17h  41991  diainN  42380  diasslssN  42382  doca3N  42450  dihcnvid2  42596  dochocss  42689  mapdcnvid2  42980  sticksstones19  43481  rmxyval  44188  brpermmodelcnv  46258  permaxrep  46260  isuspgrim0lem  49264  isuspgrim0  49265  upgrimwlklem3  49270  uhgrimisgrgriclem  49301  clnbgrgrimlem  49304  uspgrlimlem1  49359  uspgrlimlem2  49360  uspgrlimlem3  49361  uspgrlimlem4  49362  grlicsym  49384  imaf1homlem  50554  uptrar  50663