Theorem f1ocnvfv2 7088

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 6687	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝐹 ∘ ◡𝐹) = ( I ↾ 𝐵))
2	1	fveq1d 6719	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶))
3	2	adantr 484	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶))
4		f1ocnv 6673	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)
5		f1of 6661	. . . 4 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 → ◡𝐹:𝐵⟶𝐴)
6	4, 5	syl 17	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵⟶𝐴)
7		fvco3 6810	. . 3 ⊢ ((◡𝐹:𝐵⟶𝐴 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶)))
8	6, 7	sylan 583	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶)))
9		fvresi 6988	. . 3 ⊢ (𝐶 ∈ 𝐵 → (( I ↾ 𝐵)‘𝐶) = 𝐶)
10	9	adantl 485	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (( I ↾ 𝐵)‘𝐶) = 𝐶)
11	3, 8, 10	3eqtr3d 2785	1 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (𝐹‘(◡𝐹‘𝐶)) = 𝐶)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1543   ∈ wcel 2110   I cid 5454  ^◡ccnv 5550   ↾ cres 5553   ∘ ccom 5555  ⟶wf 6376  –1-1-onto→wf1o 6379  ‘cfv 6380

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-sep 5192  ax-nul 5199  ax-pr 5322

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-ral 3066  df-rex 3067  df-rab 3070  df-v 3410  df-dif 3869  df-un 3871  df-in 3873  df-ss 3883  df-nul 4238  df-if 4440  df-sn 4542  df-pr 4544  df-op 4548  df-uni 4820  df-br 5054  df-opab 5116  df-id 5455  df-xp 5557  df-rel 5558  df-cnv 5559  df-co 5560  df-dm 5561  df-rn 5562  df-res 5563  df-ima 5564  df-iota 6338  df-fun 6382  df-fn 6383  df-f 6384  df-f1 6385  df-fo 6386  df-f1o 6387  df-fv 6388

This theorem is referenced by:  f1ocnvfvb  7090  fveqf1o  7113  isocnv  7139  f1oiso2  7161  weniso  7163  dif1enlem  8838  dif1en  8840  ordiso2  9131  cantnfle  9286  cantnfp1lem3  9295  cantnflem1b  9301  cantnflem1d  9303  cantnflem1  9304  cnfcom2lem  9316  cnfcom2  9317  cnfcom3lem  9318  acndom2  9668  iunfictbso  9728  ttukeylem7  10129  fpwwe2lem5  10249  fpwwe2lem6  10250  uzrdglem  13530  uzrdgsuci  13533  fzennn  13541  axdc4uzlem  13556  seqf1olem1  13615  seqf1olem2  13616  hashfz1  13912  seqcoll  14030  seqcoll2  14031  summolem3  15278  summolem2a  15279  ackbijnn  15392  prodmolem3  15495  prodmolem2a  15496  sadcaddlem  16016  sadaddlem  16025  sadasslem  16029  sadeq  16031  phimullem  16332  eulerthlem2  16335  catcisolem  17616  mhmf1o  18228  ghmf1o  18652  f1omvdconj  18838  gsumval3eu  19289  gsumval3  19292  lmhmf1o  20083  fidomndrnglem  20344  basqtop  22608  tgqtop  22609  ordthmeolem  22698  symgtgp  23003  imasf1obl  23386  xrhmeo  23843  ovoliunlem2  24400  vitalilem2  24506  dvcnvlem  24873  dvcnv  24874  dvcnvre  24916  efif1olem4  25434  eff1olem  25437  eflog  25465  dvrelog  25525  dvlog  25539  asinrebnd  25784  sqff1o  26064  lgsqrlem4  26230  cnvmot  26632  f1otrg  26962  f1otrge  26963  axcontlem10  27064  usgrnbcnvfv  27453  wlkiswwlks2lem4  27956  clwlkclwwlklem2a4  28080  cnvunop  29999  unopadj  30000  bracnvbra  30194  abliso  31024  cycpmco2lem4  31115  cycpmco2lem5  31116  cycpmco2lem6  31117  cycpmco2lem7  31118  cycpmco2  31119  mndpluscn  31590  cvmfolem  32954  cvmliftlem6  32965  f1ocan1fv  35621  ismtycnv  35697  ismtyima  35698  ismtybndlem  35701  rngoisocnv  35876  lautcnvle  37840  lautcvr  37843  lautj  37844  lautm  37845  ltrncnvatb  37889  ltrncnvel  37893  ltrncnv  37897  ltrneq2  37899  cdlemg17h  38419  diainN  38808  diasslssN  38810  doca3N  38878  dihcnvid2  39024  dochocss  39117  mapdcnvid2  39408  sticksstones19  39843  rmxyval  40440  isomgrsym  44961  mgmhmf1o  45014