Theorem f1ocnvfv2 7130

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 6726	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝐹 ∘ ◡𝐹) = ( I ↾ 𝐵))
2	1	fveq1d 6758	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶))
3	2	adantr 480	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶))
4		f1ocnv 6712	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)
5		f1of 6700	. . . 4 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 → ◡𝐹:𝐵⟶𝐴)
6	4, 5	syl 17	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵⟶𝐴)
7		fvco3 6849	. . 3 ⊢ ((◡𝐹:𝐵⟶𝐴 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶)))
8	6, 7	sylan 579	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶)))
9		fvresi 7027	. . 3 ⊢ (𝐶 ∈ 𝐵 → (( I ↾ 𝐵)‘𝐶) = 𝐶)
10	9	adantl 481	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (( I ↾ 𝐵)‘𝐶) = 𝐶)
11	3, 8, 10	3eqtr3d 2786	1 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (𝐹‘(◡𝐹‘𝐶)) = 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539   ∈ wcel 2108   I cid 5479  ^◡ccnv 5579   ↾ cres 5582   ∘ ccom 5584  ⟶wf 6414  –1-1-onto→wf1o 6417  ‘cfv 6418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-opab 5133  df-id 5480  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426

This theorem is referenced by:  f1ocnvfvb  7132  fveqf1o  7155  isocnv  7181  f1oiso2  7203  weniso  7205  dif1enlem  8905  dif1en  8907  ordiso2  9204  cantnfle  9359  cantnfp1lem3  9368  cantnflem1b  9374  cantnflem1d  9376  cantnflem1  9377  cnfcom2lem  9389  cnfcom2  9390  cnfcom3lem  9391  acndom2  9741  iunfictbso  9801  ttukeylem7  10202  fpwwe2lem5  10322  fpwwe2lem6  10323  uzrdglem  13605  uzrdgsuci  13608  fzennn  13616  axdc4uzlem  13631  seqf1olem1  13690  seqf1olem2  13691  hashfz1  13988  seqcoll  14106  seqcoll2  14107  summolem3  15354  summolem2a  15355  ackbijnn  15468  prodmolem3  15571  prodmolem2a  15572  sadcaddlem  16092  sadaddlem  16101  sadasslem  16105  sadeq  16107  phimullem  16408  eulerthlem2  16411  catcisolem  17741  mhmf1o  18355  ghmf1o  18779  f1omvdconj  18969  gsumval3eu  19420  gsumval3  19423  lmhmf1o  20223  fidomndrnglem  20491  basqtop  22770  tgqtop  22771  ordthmeolem  22860  symgtgp  23165  imasf1obl  23550  xrhmeo  24015  ovoliunlem2  24572  vitalilem2  24678  dvcnvlem  25045  dvcnv  25046  dvcnvre  25088  efif1olem4  25606  eff1olem  25609  eflog  25637  dvrelog  25697  dvlog  25711  asinrebnd  25956  sqff1o  26236  lgsqrlem4  26402  cnvmot  26806  f1otrg  27136  f1otrge  27137  axcontlem10  27244  usgrnbcnvfv  27635  wlkiswwlks2lem4  28138  clwlkclwwlklem2a4  28262  cnvunop  30181  unopadj  30182  bracnvbra  30376  abliso  31207  cycpmco2lem4  31298  cycpmco2lem5  31299  cycpmco2lem6  31300  cycpmco2lem7  31301  cycpmco2  31302  mndpluscn  31778  cvmfolem  33141  cvmliftlem6  33152  f1ocan1fv  35811  ismtycnv  35887  ismtyima  35888  ismtybndlem  35891  rngoisocnv  36066  lautcnvle  38030  lautcvr  38033  lautj  38034  lautm  38035  ltrncnvatb  38079  ltrncnvel  38083  ltrncnv  38087  ltrneq2  38089  cdlemg17h  38609  diainN  38998  diasslssN  39000  doca3N  39068  dihcnvid2  39214  dochocss  39307  mapdcnvid2  39598  sticksstones19  40049  rmxyval  40653  isomgrsym  45176  mgmhmf1o  45229