Theorem f1ocnvfv2 6433

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 6076	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝐹 ∘ ◡𝐹) = ( I ↾ 𝐵))
2	1	fveq1d 6105	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶))
3	2	adantr 480	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶))
4		f1ocnv 6062	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)
5		f1of 6050	. . . 4 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 → ◡𝐹:𝐵⟶𝐴)
6	4, 5	syl 17	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵⟶𝐴)
7		fvco3 6185	. . 3 ⊢ ((◡𝐹:𝐵⟶𝐴 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶)))
8	6, 7	sylan 487	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶)))
9		fvresi 6344	. . 3 ⊢ (𝐶 ∈ 𝐵 → (( I ↾ 𝐵)‘𝐶) = 𝐶)
10	9	adantl 481	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (( I ↾ 𝐵)‘𝐶) = 𝐶)
11	3, 8, 10	3eqtr3d 2652	1 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (𝐹‘(◡𝐹‘𝐶)) = 𝐶)

Syntax hints:   → wi 4   ∧ wa 383   = wceq 1475   ∈ wcel 1977   I cid 4948  ^◡ccnv 5037   ↾ cres 5040   ∘ ccom 5042  ⟶wf 5800  –1-1-onto→wf1o 5803  ‘cfv 5804

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-nul 3875  df-if 4037  df-sn 4126  df-pr 4128  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-id 4953  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812

This theorem is referenced by:  f1ocnvfvb  6435  fveqf1o  6457  isocnv  6480  f1oiso2  6502  weniso  6504  ordiso2  8303  cantnfle  8451  cantnfp1lem3  8460  cantnflem1b  8466  cantnflem1d  8468  cantnflem1  8469  cnfcom2lem  8481  cnfcom2  8482  cnfcom3lem  8483  acndom2  8760  iunfictbso  8820  ttukeylem7  9220  fpwwe2lem6  9336  fpwwe2lem7  9337  uzrdglem  12618  uzrdgsuci  12621  fzennn  12629  axdc4uzlem  12644  seqf1olem1  12702  seqf1olem2  12703  hashfz1  12996  seqcoll  13105  seqcoll2  13106  summolem3  14292  summolem2a  14293  ackbijnn  14399  prodmolem3  14502  prodmolem2a  14503  sadcaddlem  15017  sadaddlem  15026  sadasslem  15030  sadeq  15032  phimullem  15322  eulerthlem2  15325  catcisolem  16579  mhmf1o  17168  ghmf1o  17513  f1omvdconj  17689  gsumval3eu  18128  gsumval3  18131  lmhmf1o  18867  fidomndrnglem  19127  basqtop  21324  tgqtop  21325  ordthmeolem  21414  symgtgp  21715  imasf1obl  22103  xrhmeo  22553  ovoliunlem2  23078  vitalilem2  23184  dvcnvlem  23543  dvcnv  23544  dvcnvre  23586  efif1olem4  24095  eff1olem  24098  eflog  24127  dvrelog  24183  dvlog  24197  asinrebnd  24428  sqff1o  24708  lgsqrlem4  24874  cnvmot  25236  f1otrg  25551  f1otrge  25552  axcontlem10  25653  nbgracnvfv  25969  cusgrares  26001  usgra2adedgspthlem1  26139  constr3trllem5  26182  cusconngra  26204  wlkiswwlk2lem4  26222  clwlkisclwwlklem2a4  26312  2pthfrgra  26538  cnvunop  28161  unopadj  28162  bracnvbra  28356  abliso  29027  mndpluscn  29300  cvmfolem  30515  cvmliftlem6  30526  f1ocan1fv  32691  ismtycnv  32771  ismtyima  32772  ismtybndlem  32775  rngoisocnv  32950  lautcnvle  34393  lautcvr  34396  lautj  34397  lautm  34398  ltrncnvatb  34442  ltrncnvel  34446  ltrncnv  34450  ltrneq2  34452  cdlemg17h  34974  diainN  35364  diasslssN  35366  doca3N  35434  dihcnvid2  35580  dochocss  35673  mapdcnvid2  35964  rmxyval  36498  usgrnbcnvfv  40593  1wlkiswwlks2lem4  41069  clwlkclwwlklem2a4  41206  mgmhmf1o  41577