Theorem f1ocnvfv2 7158

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 6752	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝐹 ∘ ◡𝐹) = ( I ↾ 𝐵))
2	1	fveq1d 6785	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶))
3	2	adantr 481	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶))
4		f1ocnv 6737	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)
5		f1of 6725	. . . 4 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 → ◡𝐹:𝐵⟶𝐴)
6	4, 5	syl 17	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵⟶𝐴)
7		fvco3 6876	. . 3 ⊢ ((◡𝐹:𝐵⟶𝐴 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶)))
8	6, 7	sylan 580	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶)))
9		fvresi 7054	. . 3 ⊢ (𝐶 ∈ 𝐵 → (( I ↾ 𝐵)‘𝐶) = 𝐶)
10	9	adantl 482	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (( I ↾ 𝐵)‘𝐶) = 𝐶)
11	3, 8, 10	3eqtr3d 2787	1 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (𝐹‘(◡𝐹‘𝐶)) = 𝐶)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1539   ∈ wcel 2107   I cid 5489  ^◡ccnv 5589   ↾ cres 5592   ∘ ccom 5594  ⟶wf 6433  –1-1-onto→wf1o 6436  ‘cfv 6437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2710  ax-sep 5224  ax-nul 5231  ax-pr 5353

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2817  df-ral 3070  df-rex 3071  df-rab 3074  df-v 3435  df-dif 3891  df-un 3893  df-in 3895  df-ss 3905  df-nul 4258  df-if 4461  df-sn 4563  df-pr 4565  df-op 4569  df-uni 4841  df-br 5076  df-opab 5138  df-id 5490  df-xp 5596  df-rel 5597  df-cnv 5598  df-co 5599  df-dm 5600  df-rn 5601  df-res 5602  df-ima 5603  df-iota 6395  df-fun 6439  df-fn 6440  df-f 6441  df-f1 6442  df-fo 6443  df-f1o 6444  df-fv 6445

This theorem is referenced by:  f1ocnvfvb  7160  fveqf1o  7184  isocnv  7210  f1oiso2  7232  weniso  7234  dif1enlem  8952  dif1en  8954  ordiso2  9283  cantnfle  9438  cantnfp1lem3  9447  cantnflem1b  9453  cantnflem1d  9455  cantnflem1  9456  cnfcom2lem  9468  cnfcom2  9469  cnfcom3lem  9470  acndom2  9819  iunfictbso  9879  ttukeylem7  10280  fpwwe2lem5  10400  fpwwe2lem6  10401  uzrdglem  13686  uzrdgsuci  13689  fzennn  13697  axdc4uzlem  13712  seqf1olem1  13771  seqf1olem2  13772  hashfz1  14069  seqcoll  14187  seqcoll2  14188  summolem3  15435  summolem2a  15436  ackbijnn  15549  prodmolem3  15652  prodmolem2a  15653  sadcaddlem  16173  sadaddlem  16182  sadasslem  16186  sadeq  16188  phimullem  16489  eulerthlem2  16492  catcisolem  17834  mhmf1o  18449  ghmf1o  18873  f1omvdconj  19063  gsumval3eu  19514  gsumval3  19517  lmhmf1o  20317  fidomndrnglem  20587  basqtop  22871  tgqtop  22872  ordthmeolem  22961  symgtgp  23266  imasf1obl  23653  xrhmeo  24118  ovoliunlem2  24676  vitalilem2  24782  dvcnvlem  25149  dvcnv  25150  dvcnvre  25192  efif1olem4  25710  eff1olem  25713  eflog  25741  dvrelog  25801  dvlog  25815  asinrebnd  26060  sqff1o  26340  lgsqrlem4  26506  cnvmot  26911  f1otrg  27241  f1otrge  27242  axcontlem10  27350  usgrnbcnvfv  27741  wlkiswwlks2lem4  28246  clwlkclwwlklem2a4  28370  cnvunop  30289  unopadj  30290  bracnvbra  30484  abliso  31314  cycpmco2lem4  31405  cycpmco2lem5  31406  cycpmco2lem6  31407  cycpmco2lem7  31408  cycpmco2  31409  mndpluscn  31885  cvmfolem  33250  cvmliftlem6  33261  f1ocan1fv  35893  ismtycnv  35969  ismtyima  35970  ismtybndlem  35973  rngoisocnv  36148  lautcnvle  38110  lautcvr  38113  lautj  38114  lautm  38115  ltrncnvatb  38159  ltrncnvel  38163  ltrncnv  38167  ltrneq2  38169  cdlemg17h  38689  diainN  39078  diasslssN  39080  doca3N  39148  dihcnvid2  39294  dochocss  39387  mapdcnvid2  39678  sticksstones19  40128  rmxyval  40744  isomgrsym  45299  mgmhmf1o  45352