Theorem f1ocnvfv2 7256

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 6829	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝐹 ∘ ◡𝐹) = ( I ↾ 𝐵))
2	1	fveq1d 6864	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶))
3	2	adantr 484	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶))
4		f1ocnv 6814	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)
5		f1of 6801	. . . 4 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 → ◡𝐹:𝐵⟶𝐴)
6	4, 5	syl 17	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵⟶𝐴)
7		fvco3 6962	. . 3 ⊢ ((◡𝐹:𝐵⟶𝐴 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶)))
8	6, 7	sylan 589	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶)))
9		fvresi 7152	. . 3 ⊢ (𝐶 ∈ 𝐵 → (( I ↾ 𝐵)‘𝐶) = 𝐶)
10	9	adantl 485	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (( I ↾ 𝐵)‘𝐶) = 𝐶)
11	3, 8, 10	3eqtr3d 2804	1 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (𝐹‘(◡𝐹‘𝐶)) = 𝐶)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1559   ∈ wcel 2141   I cid 5537  ^◡ccnv 5642   ↾ cres 5645   ∘ ccom 5647  ⟶wf 6512  –1-1-onto→wf1o 6515  ‘cfv 6516

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733  ax-sep 5243  ax-nul 5253  ax-pr 5387

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-ne 2957  df-ral 3076  df-rex 3086  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4863  df-br 5098  df-opab 5160  df-id 5538  df-xp 5649  df-rel 5650  df-cnv 5651  df-co 5652  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656  df-iota 6472  df-fun 6518  df-fn 6519  df-f 6520  df-f1 6521  df-fo 6522  df-f1o 6523  df-fv 6524

This theorem is referenced by:  f1ocnvfvb  7258  fveqf1o  7281  isocnv  7309  f1oiso2  7331  weniso  7333  dif1enlem  9122  dif1en  9124  ordiso2  9457  cantnfle  9620  cantnfp1lem3  9629  cantnflem1b  9635  cantnflem1d  9637  cantnflem1  9638  cnfcom2lem  9650  cnfcom2  9651  cnfcom3lem  9652  acndom2  10004  iunfictbso  10064  ttukeylem7  10466  fpwwe2lem5  10587  fpwwe2lem6  10588  uzrdglem  13964  uzrdgsuci  13967  fzennn  13975  axdc4uzlem  13990  seqf1olem1  14048  seqf1olem2  14049  hashfz1  14353  seqcoll  14471  seqcoll2  14472  summolem3  15732  summolem2a  15733  ackbijnn  15849  prodmolem3  15954  prodmolem2a  15955  sadcaddlem  16482  sadaddlem  16491  sadasslem  16495  sadeq  16497  phimullem  16805  eulerthlem2  16808  catcisolem  18134  mgmhmf1o  18725  mhmf1o  18821  ghmf1o  19279  f1omvdconj  19477  gsumval3eu  19935  gsumval3  19938  rngisom1  20502  fidomndrnglem  20809  lmhmf1o  21101  basqtop  23759  tgqtop  23760  ordthmeolem  23849  symgtgp  24154  imasf1obl  24536  xrhmeo  24996  ovoliunlem2  25553  vitalilem2  25659  dvcnvlem  26026  dvcnv  26027  dvcnvre  26069  efif1olem4  26598  eff1olem  26601  eflog  26629  dvrelog  26690  dvlog  26704  asinrebnd  26954  sqff1o  27234  lgsqrlem4  27401  addonbday  28360  noseqrdglem  28386  noseqrdgsuc  28389  bdayfinlem  28567  cnvmot  28698  f1otrg  29028  f1otrge  29029  axcontlem10  29131  usgrnbcnvfv  29523  wlkiswwlks2lem4  30029  clwlkclwwlklem2a4  30156  cnvunop  32078  unopadj  32079  bracnvbra  32273  ccatws1f1o  33090  mndlactf1o  33169  mndractf1o  33170  abliso  33175  cycpmco2lem4  33270  cycpmco2lem5  33271  cycpmco2lem6  33272  cycpmco2lem7  33273  cycpmco2  33274  mndpluscn  34184  vonf1oonfo  35419  cvmfolem  35590  cvmliftlem6  35601  f1ocan1fv  38186  ismtycnv  38262  ismtyima  38263  ismtybndlem  38266  rngoisocnv  38441  lautcnvle  40674  lautcvr  40677  lautj  40678  lautm  40679  ltrncnvatb  40723  ltrncnvel  40727  ltrncnv  40731  ltrneq2  40733  cdlemg17h  41253  diainN  41642  diasslssN  41644  doca3N  41712  dihcnvid2  41858  dochocss  41951  mapdcnvid2  42242  sticksstones19  42743  rmxyval  43453  brpermmodelcnv  45541  permaxrep  45543  isuspgrim0lem  48476  isuspgrim0  48477  upgrimwlklem3  48482  uhgrimisgrgriclem  48513  clnbgrgrimlem  48516  uspgrlimlem1  48571  uspgrlimlem2  48572  uspgrlimlem3  48573  uspgrlimlem4  48574  grlicsym  48596  imaf1homlem  49689  uptrar  49798