Theorem f1ocnvfv2 7270

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 6857	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝐹 ∘ ◡𝐹) = ( I ↾ 𝐵))
2	1	fveq1d 6890	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶))
3	2	adantr 482	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶))
4		f1ocnv 6842	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)
5		f1of 6830	. . . 4 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 → ◡𝐹:𝐵⟶𝐴)
6	4, 5	syl 17	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵⟶𝐴)
7		fvco3 6986	. . 3 ⊢ ((◡𝐹:𝐵⟶𝐴 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶)))
8	6, 7	sylan 581	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶)))
9		fvresi 7166	. . 3 ⊢ (𝐶 ∈ 𝐵 → (( I ↾ 𝐵)‘𝐶) = 𝐶)
10	9	adantl 483	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (( I ↾ 𝐵)‘𝐶) = 𝐶)
11	3, 8, 10	3eqtr3d 2781	1 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (𝐹‘(◡𝐹‘𝐶)) = 𝐶)

Syntax hints:   → wi 4   ∧ wa 397   = wceq 1542   ∈ wcel 2107   I cid 5572  ^◡ccnv 5674   ↾ cres 5677   ∘ ccom 5679  ⟶wf 6536  –1-1-onto→wf1o 6539  ‘cfv 6540

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 2704  ax-sep 5298  ax-nul 5305  ax-pr 5426

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548

This theorem is referenced by:  f1ocnvfvb  7272  fveqf1o  7296  isocnv  7322  f1oiso2  7344  weniso  7346  dif1enlem  9152  dif1enlemOLD  9153  dif1en  9156  dif1enOLD  9158  ordiso2  9506  cantnfle  9662  cantnfp1lem3  9671  cantnflem1b  9677  cantnflem1d  9679  cantnflem1  9680  cnfcom2lem  9692  cnfcom2  9693  cnfcom3lem  9694  acndom2  10045  iunfictbso  10105  ttukeylem7  10506  fpwwe2lem5  10626  fpwwe2lem6  10627  uzrdglem  13918  uzrdgsuci  13921  fzennn  13929  axdc4uzlem  13944  seqf1olem1  14003  seqf1olem2  14004  hashfz1  14302  seqcoll  14421  seqcoll2  14422  summolem3  15656  summolem2a  15657  ackbijnn  15770  prodmolem3  15873  prodmolem2a  15874  sadcaddlem  16394  sadaddlem  16403  sadasslem  16407  sadeq  16409  phimullem  16708  eulerthlem2  16711  catcisolem  18056  mhmf1o  18678  ghmf1o  19116  f1omvdconj  19307  gsumval3eu  19764  gsumval3  19767  lmhmf1o  20645  fidomndrnglem  20910  basqtop  23197  tgqtop  23198  ordthmeolem  23287  symgtgp  23592  imasf1obl  23979  xrhmeo  24444  ovoliunlem2  25002  vitalilem2  25108  dvcnvlem  25475  dvcnv  25476  dvcnvre  25518  efif1olem4  26036  eff1olem  26039  eflog  26067  dvrelog  26127  dvlog  26141  asinrebnd  26386  sqff1o  26666  lgsqrlem4  26832  cnvmot  27772  f1otrg  28102  f1otrge  28103  axcontlem10  28211  usgrnbcnvfv  28602  wlkiswwlks2lem4  29106  clwlkclwwlklem2a4  29230  cnvunop  31149  unopadj  31150  bracnvbra  31344  abliso  32175  cycpmco2lem4  32266  cycpmco2lem5  32267  cycpmco2lem6  32268  cycpmco2lem7  32269  cycpmco2  32270  mndpluscn  32844  cvmfolem  34208  cvmliftlem6  34219  f1ocan1fv  36532  ismtycnv  36608  ismtyima  36609  ismtybndlem  36612  rngoisocnv  36787  lautcnvle  38898  lautcvr  38901  lautj  38902  lautm  38903  ltrncnvatb  38947  ltrncnvel  38951  ltrncnv  38955  ltrneq2  38957  cdlemg17h  39477  diainN  39866  diasslssN  39868  doca3N  39936  dihcnvid2  40082  dochocss  40175  mapdcnvid2  40466  sticksstones19  40919  rmxyval  41587  isomgrsym  46439  mgmhmf1o  46492  rngisom1  46652