Theorem f1ocnvfv2 7297

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 6876	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝐹 ∘ ◡𝐹) = ( I ↾ 𝐵))
2	1	fveq1d 6909	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶))
3	2	adantr 480	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶))
4		f1ocnv 6861	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)
5		f1of 6849	. . . 4 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 → ◡𝐹:𝐵⟶𝐴)
6	4, 5	syl 17	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵⟶𝐴)
7		fvco3 7008	. . 3 ⊢ ((◡𝐹:𝐵⟶𝐴 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶)))
8	6, 7	sylan 580	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶)))
9		fvresi 7193	. . 3 ⊢ (𝐶 ∈ 𝐵 → (( I ↾ 𝐵)‘𝐶) = 𝐶)
10	9	adantl 481	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (( I ↾ 𝐵)‘𝐶) = 𝐶)
11	3, 8, 10	3eqtr3d 2783	1 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (𝐹‘(◡𝐹‘𝐶)) = 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1537   ∈ wcel 2106   I cid 5582  ^◡ccnv 5688   ↾ cres 5691   ∘ ccom 5693  ⟶wf 6559  –1-1-onto→wf1o 6562  ‘cfv 6563

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-br 5149  df-opab 5211  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571

This theorem is referenced by:  f1ocnvfvb  7299  fveqf1o  7322  isocnv  7350  f1oiso2  7372  weniso  7374  dif1enlem  9195  dif1enlemOLD  9196  dif1en  9199  dif1enOLD  9201  ordiso2  9553  cantnfle  9709  cantnfp1lem3  9718  cantnflem1b  9724  cantnflem1d  9726  cantnflem1  9727  cnfcom2lem  9739  cnfcom2  9740  cnfcom3lem  9741  acndom2  10092  iunfictbso  10152  ttukeylem7  10553  fpwwe2lem5  10673  fpwwe2lem6  10674  uzrdglem  13995  uzrdgsuci  13998  fzennn  14006  axdc4uzlem  14021  seqf1olem1  14079  seqf1olem2  14080  hashfz1  14382  seqcoll  14500  seqcoll2  14501  summolem3  15747  summolem2a  15748  ackbijnn  15861  prodmolem3  15966  prodmolem2a  15967  sadcaddlem  16491  sadaddlem  16500  sadasslem  16504  sadeq  16506  phimullem  16813  eulerthlem2  16816  catcisolem  18164  mgmhmf1o  18726  mhmf1o  18822  ghmf1o  19279  f1omvdconj  19479  gsumval3eu  19937  gsumval3  19940  rngisom1  20483  fidomndrnglem  20790  lmhmf1o  21063  basqtop  23735  tgqtop  23736  ordthmeolem  23825  symgtgp  24130  imasf1obl  24517  xrhmeo  24991  ovoliunlem2  25552  vitalilem2  25658  dvcnvlem  26029  dvcnv  26030  dvcnvre  26073  efif1olem4  26602  eff1olem  26605  eflog  26633  dvrelog  26694  dvlog  26708  asinrebnd  26959  sqff1o  27240  lgsqrlem4  27408  noseqrdglem  28326  noseqrdgsuc  28329  cnvmot  28564  f1otrg  28894  f1otrge  28895  axcontlem10  29003  usgrnbcnvfv  29397  wlkiswwlks2lem4  29902  clwlkclwwlklem2a4  30026  cnvunop  31947  unopadj  31948  bracnvbra  32142  ccatws1f1o  32921  mndlactf1o  33018  mndractf1o  33019  abliso  33024  cycpmco2lem4  33132  cycpmco2lem5  33133  cycpmco2lem6  33134  cycpmco2lem7  33135  cycpmco2  33136  mndpluscn  33887  cvmfolem  35264  cvmliftlem6  35275  f1ocan1fv  37713  ismtycnv  37789  ismtyima  37790  ismtybndlem  37793  rngoisocnv  37968  lautcnvle  40072  lautcvr  40075  lautj  40076  lautm  40077  ltrncnvatb  40121  ltrncnvel  40125  ltrncnv  40129  ltrneq2  40131  cdlemg17h  40651  diainN  41040  diasslssN  41042  doca3N  41110  dihcnvid2  41256  dochocss  41349  mapdcnvid2  41640  sticksstones19  42147  rmxyval  42904  isuspgrim0lem  47809  isuspgrim0  47810  uhgrimisgrgriclem  47836  clnbgrgrimlem  47839  uspgrlimlem1  47891  uspgrlimlem2  47892  uspgrlimlem3  47893  uspgrlimlem4  47894  grlicsym  47909