Theorem f1ocnvfv2 7278

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 6845	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝐹 ∘ ◡𝐹) = ( I ↾ 𝐵))
2	1	fveq1d 6880	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶))
3	2	adantr 486	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶))
4		f1ocnv 6830	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)
5		f1of 6817	. . . 4 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 → ◡𝐹:𝐵⟶𝐴)
6	4, 5	syl 18	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵⟶𝐴)
7		fvco3 6978	. . 3 ⊢ ((◡𝐹:𝐵⟶𝐴 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶)))
8	6, 7	sylan 592	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶)))
9		fvresi 7171	. . 3 ⊢ (𝐶 ∈ 𝐵 → (( I ↾ 𝐵)‘𝐶) = 𝐶)
10	9	adantl 487	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (( I ↾ 𝐵)‘𝐶) = 𝐶)
11	3, 8, 10	3eqtr3d 2803	1 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (𝐹‘(◡𝐹‘𝐶)) = 𝐶)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2145   I cid 5549  ^◡ccnv 5654   ↾ cres 5657   ∘ ccom 5659  ⟶wf 6529  –1-1-onto→wf1o 6532  ‘cfv 6533

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5251  ax-nul 5263  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-iota 6489  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541

This theorem is used by:  f1ocnvfvb  7280  fveqf1o  7303  isocnv  7331  f1oiso2  7353  weniso  7357  dif1enlem  9154  dif1en  9156  ordiso2  9487  cantnfle  9650  cantnfp1lem3  9659  cantnflem1b  9665  cantnflem1d  9667  cantnflem1  9668  cnfcom2lem  9680  cnfcom2  9681  cnfcom3lem  9682  acndom2  10057  iunfictbso  10117  ttukeylem7  10517  fpwwe2lem5  10644  fpwwe2lem6  10645  uzrdglem  14021  uzrdgsuci  14024  fzennn  14032  axdc4uzlem  14047  seqf1olem1  14105  seqf1olem2  14106  hashfz1  14410  seqcoll  14529  seqcoll2  14530  summolem3  15800  summolem2a  15801  ackbijnn  15917  prodmolem3  16020  prodmolem2a  16021  sadcaddlem  16547  sadaddlem  16556  sadasslem  16560  sadeq  16562  phimullem  16870  eulerthlem2  16873  catcisolem  18199  mgmhmf1o  18802  mhmf1o  18904  ghmf1o  19375  f1omvdconj  19573  gsumval3eu  20031  gsumval3  20034  rngisom1  20607  fidomndrnglem  20939  lmhmf1o  21230  basqtop  23937  tgqtop  23938  ordthmeolem  24027  symgtgp  24332  imasf1obl  24714  xrhmeo  25174  ovoliunlem2  25731  vitalilem2  25837  dvcnvlem  26203  dvcnv  26204  dvcnvre  26246  efif1olem4  26782  eff1olem  26785  eflog  26813  dvrelog  26874  dvlog  26888  asinrebnd  27138  sqff1o  27418  lgsqrlem4  27585  addonbday  28544  noseqrdglem  28570  noseqrdgsuc  28573  bdayfinlem  28751  cnvmot  28883  f1otrg  29327  f1otrge  29328  axcontlem10  29430  usgrnbcnvfv  29825  wlkiswwlks2lem4  30340  clwlkclwwlklem2a4  30467  cnvunop  32399  unopadj  32400  bracnvbra  32594  ccatws1f1o  33393  mndlactf1o  33470  mndractf1o  33471  abliso  33475  cycpmco2lem4  33569  cycpmco2lem5  33570  cycpmco2lem6  33571  cycpmco2lem7  33572  cycpmco2  33573  mndpluscn  34436  vonf1oonfo  35712  cvmfolem  35858  cvmliftlem6  35869  f1ocan1fv  38476  ismtycnv  38552  ismtyima  38553  ismtybndlem  38556  rngoisocnv  38731  lautcnvle  40962  lautcvr  40965  lautj  40966  lautm  40967  ltrncnvatb  41011  ltrncnvel  41015  ltrncnv  41019  ltrneq2  41021  cdlemg17h  41541  diainN  41930  diasslssN  41932  doca3N  42000  dihcnvid2  42146  dochocss  42239  mapdcnvid2  42530  sticksstones19  43031  rmxyval  43756  brpermmodelcnv  45827  permaxrep  45829  isuspgrim0lem  48809  isuspgrim0  48810  upgrimwlklem3  48815  uhgrimisgrgriclem  48846  clnbgrgrimlem  48849  uspgrlimlem1  48904  uspgrlimlem2  48905  uspgrlimlem3  48906  uspgrlimlem4  48907  grlicsym  48929  imaf1homlem  50033  uptrar  50142