Theorem f1ocnvfv2 7252

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 6827	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → (𝐹 ∘ ◡𝐹) = ( I ↾ 𝐵))
2	1	fveq1d 6860	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶))
3	2	adantr 480	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (( I ↾ 𝐵)‘𝐶))
4		f1ocnv 6812	. . . 4 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵–1-1-onto→𝐴)
5		f1of 6800	. . . 4 ⊢ (◡𝐹:𝐵–1-1-onto→𝐴 → ◡𝐹:𝐵⟶𝐴)
6	4, 5	syl 17	. . 3 ⊢ (𝐹:𝐴–1-1-onto→𝐵 → ◡𝐹:𝐵⟶𝐴)
7		fvco3 6960	. . 3 ⊢ ((◡𝐹:𝐵⟶𝐴 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶)))
8	6, 7	sylan 580	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → ((𝐹 ∘ ◡𝐹)‘𝐶) = (𝐹‘(◡𝐹‘𝐶)))
9		fvresi 7147	. . 3 ⊢ (𝐶 ∈ 𝐵 → (( I ↾ 𝐵)‘𝐶) = 𝐶)
10	9	adantl 481	. 2 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (( I ↾ 𝐵)‘𝐶) = 𝐶)
11	3, 8, 10	3eqtr3d 2772	1 ⊢ ((𝐹:𝐴–1-1-onto→𝐵 ∧ 𝐶 ∈ 𝐵) → (𝐹‘(◡𝐹‘𝐶)) = 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109   I cid 5532  ^◡ccnv 5637   ↾ cres 5640   ∘ ccom 5642  ⟶wf 6507  –1-1-onto→wf1o 6510  ‘cfv 6511

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rex 3054  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-br 5108  df-opab 5170  df-id 5533  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519

This theorem is referenced by:  f1ocnvfvb  7254  fveqf1o  7277  isocnv  7305  f1oiso2  7327  weniso  7329  dif1enlem  9120  dif1enlemOLD  9121  dif1en  9124  dif1enOLD  9126  ordiso2  9468  cantnfle  9624  cantnfp1lem3  9633  cantnflem1b  9639  cantnflem1d  9641  cantnflem1  9642  cnfcom2lem  9654  cnfcom2  9655  cnfcom3lem  9656  acndom2  10007  iunfictbso  10067  ttukeylem7  10468  fpwwe2lem5  10588  fpwwe2lem6  10589  uzrdglem  13922  uzrdgsuci  13925  fzennn  13933  axdc4uzlem  13948  seqf1olem1  14006  seqf1olem2  14007  hashfz1  14311  seqcoll  14429  seqcoll2  14430  summolem3  15680  summolem2a  15681  ackbijnn  15794  prodmolem3  15899  prodmolem2a  15900  sadcaddlem  16427  sadaddlem  16436  sadasslem  16440  sadeq  16442  phimullem  16749  eulerthlem2  16752  catcisolem  18072  mgmhmf1o  18627  mhmf1o  18723  ghmf1o  19180  f1omvdconj  19376  gsumval3eu  19834  gsumval3  19837  rngisom1  20375  fidomndrnglem  20681  lmhmf1o  20953  basqtop  23598  tgqtop  23599  ordthmeolem  23688  symgtgp  23993  imasf1obl  24376  xrhmeo  24844  ovoliunlem2  25404  vitalilem2  25510  dvcnvlem  25880  dvcnv  25881  dvcnvre  25924  efif1olem4  26454  eff1olem  26457  eflog  26485  dvrelog  26546  dvlog  26560  asinrebnd  26811  sqff1o  27092  lgsqrlem4  27260  noseqrdglem  28199  noseqrdgsuc  28202  cnvmot  28468  f1otrg  28798  f1otrge  28799  axcontlem10  28900  usgrnbcnvfv  29292  wlkiswwlks2lem4  29802  clwlkclwwlklem2a4  29926  cnvunop  31847  unopadj  31848  bracnvbra  32042  ccatws1f1o  32873  mndlactf1o  32971  mndractf1o  32972  abliso  32977  cycpmco2lem4  33086  cycpmco2lem5  33087  cycpmco2lem6  33088  cycpmco2lem7  33089  cycpmco2  33090  mndpluscn  33916  cvmfolem  35266  cvmliftlem6  35277  f1ocan1fv  37720  ismtycnv  37796  ismtyima  37797  ismtybndlem  37800  rngoisocnv  37975  lautcnvle  40083  lautcvr  40086  lautj  40087  lautm  40088  ltrncnvatb  40132  ltrncnvel  40136  ltrncnv  40140  ltrneq2  40142  cdlemg17h  40662  diainN  41051  diasslssN  41053  doca3N  41121  dihcnvid2  41267  dochocss  41360  mapdcnvid2  41651  sticksstones19  42153  rmxyval  42904  brpermmodelcnv  44994  permaxrep  44996  isuspgrim0lem  47893  isuspgrim0  47894  upgrimwlklem3  47899  uhgrimisgrgriclem  47930  clnbgrgrimlem  47933  uspgrlimlem1  47987  uspgrlimlem2  47988  uspgrlimlem3  47989  uspgrlimlem4  47990  grlicsym  48005  imaf1homlem  49096  uptrar  49205