Theorem f1ocnvfv2 7277

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 6860	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝐹 ∘ ◡𝐹) = ( I ↾ 𝐵))
2	1	fveq1d 6893	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶))
3	2	adantr 481	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶))
4		f1ocnv 6845	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)
5		f1of 6833	. . . 4 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 → ◡𝐹:𝐵⟶𝐴)
6	4, 5	syl 17	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵⟶𝐴)
7		fvco3 6990	. . 3 ⊢ ((◡𝐹:𝐵⟶𝐴 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶)))
8	6, 7	sylan 580	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶)))
9		fvresi 7173	. . 3 ⊢ (𝐶 ∈ 𝐵 → (( I ↾ 𝐵)‘𝐶) = 𝐶)
10	9	adantl 482	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (( I ↾ 𝐵)‘𝐶) = 𝐶)
11	3, 8, 10	3eqtr3d 2780	1 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (𝐹‘(◡𝐹‘𝐶)) = 𝐶)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541   ∈ wcel 2106   I cid 5573  ^◡ccnv 5675   ↾ cres 5678   ∘ ccom 5680  ⟶wf 6539  –1-1-onto→wf1o 6542  ‘cfv 6543

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551

This theorem is referenced by:  f1ocnvfvb  7279  fveqf1o  7303  isocnv  7329  f1oiso2  7351  weniso  7353  dif1enlem  9158  dif1enlemOLD  9159  dif1en  9162  dif1enOLD  9164  ordiso2  9512  cantnfle  9668  cantnfp1lem3  9677  cantnflem1b  9683  cantnflem1d  9685  cantnflem1  9686  cnfcom2lem  9698  cnfcom2  9699  cnfcom3lem  9700  acndom2  10051  iunfictbso  10111  ttukeylem7  10512  fpwwe2lem5  10632  fpwwe2lem6  10633  uzrdglem  13924  uzrdgsuci  13927  fzennn  13935  axdc4uzlem  13950  seqf1olem1  14009  seqf1olem2  14010  hashfz1  14308  seqcoll  14427  seqcoll2  14428  summolem3  15662  summolem2a  15663  ackbijnn  15776  prodmolem3  15879  prodmolem2a  15880  sadcaddlem  16400  sadaddlem  16409  sadasslem  16413  sadeq  16415  phimullem  16714  eulerthlem2  16717  catcisolem  18062  mhmf1o  18684  ghmf1o  19124  f1omvdconj  19316  gsumval3eu  19774  gsumval3  19777  lmhmf1o  20662  fidomndrnglem  20931  basqtop  23222  tgqtop  23223  ordthmeolem  23312  symgtgp  23617  imasf1obl  24004  xrhmeo  24469  ovoliunlem2  25027  vitalilem2  25133  dvcnvlem  25500  dvcnv  25501  dvcnvre  25543  efif1olem4  26061  eff1olem  26064  eflog  26092  dvrelog  26152  dvlog  26166  asinrebnd  26413  sqff1o  26693  lgsqrlem4  26859  cnvmot  27830  f1otrg  28160  f1otrge  28161  axcontlem10  28269  usgrnbcnvfv  28660  wlkiswwlks2lem4  29164  clwlkclwwlklem2a4  29288  cnvunop  31209  unopadj  31210  bracnvbra  31404  abliso  32235  cycpmco2lem4  32329  cycpmco2lem5  32330  cycpmco2lem6  32331  cycpmco2lem7  32332  cycpmco2  32333  mndpluscn  32975  cvmfolem  34339  cvmliftlem6  34350  f1ocan1fv  36680  ismtycnv  36756  ismtyima  36757  ismtybndlem  36760  rngoisocnv  36935  lautcnvle  39046  lautcvr  39049  lautj  39050  lautm  39051  ltrncnvatb  39095  ltrncnvel  39099  ltrncnv  39103  ltrneq2  39105  cdlemg17h  39625  diainN  40014  diasslssN  40016  doca3N  40084  dihcnvid2  40230  dochocss  40323  mapdcnvid2  40614  sticksstones19  41067  rmxyval  41736  isomgrsym  46583  mgmhmf1o  46636  rngisom1  46797