Theorem f1imacnv 6860

Description: Preimage of an image. (Contributed by NM, 30-Sep-2004.)

Assertion

Ref	Expression
f1imacnv	⊢ ((𝐹:𝐴⟶1-1𝐵 ∧ 𝐶 ⊆ 𝐴) → (◡𝐹 “ (𝐹 “ 𝐶)) = 𝐶)

Proof of Theorem f1imacnv

Step	Hyp	Ref	Expression
1		resima 6067	. 2 ⊢ ((◡𝐹 ↾ (𝐹 “ 𝐶)) “ (𝐹 “ 𝐶)) = (◡𝐹 “ (𝐹 “ 𝐶))
2		df-f1 6560	. . . . . . 7 ⊢ (𝐹:𝐴⟶1-1𝐵 ↔ (𝐹:𝐴⟶𝐵 ∧ Fun ◡𝐹))
3	2	simprbi 503	. . . . . 6 ⊢ (𝐹:𝐴⟶1-1𝐵 → Fun ◡𝐹)
4	3	adantr 486	. . . . 5 ⊢ ((𝐹:𝐴⟶1-1𝐵 ∧ 𝐶 ⊆ 𝐴) → Fun ◡𝐹)
5		funcnvres 6637	. . . . 5 ⊢ (Fun ◡𝐹 → ◡(𝐹 ↾ 𝐶) = (◡𝐹 ↾ (𝐹 “ 𝐶)))
6	4, 5	syl 18	. . . 4 ⊢ ((𝐹:𝐴⟶1-1𝐵 ∧ 𝐶 ⊆ 𝐴) → ◡(𝐹 ↾ 𝐶) = (◡𝐹 ↾ (𝐹 “ 𝐶)))
7	6	imaeq1d 6062	. . 3 ⊢ ((𝐹:𝐴⟶1-1𝐵 ∧ 𝐶 ⊆ 𝐴) → (◡(𝐹 ↾ 𝐶) “ (𝐹 “ 𝐶)) = ((◡𝐹 ↾ (𝐹 “ 𝐶)) “ (𝐹 “ 𝐶)))
8		f1ores 6858	. . . . 5 ⊢ ((𝐹:𝐴⟶1-1𝐵 ∧ 𝐶 ⊆ 𝐴) → (𝐹 ↾ 𝐶):𝐶⟶1-1onto(𝐹 “ 𝐶))
9		f1ocnv 6856	. . . . 5 ⊢ ((𝐹 ↾ 𝐶):𝐶⟶1-1onto(𝐹 “ 𝐶) → ◡(𝐹 ↾ 𝐶):(𝐹 “ 𝐶)⟶1-1onto𝐶)
10	8, 9	syl 18	. . . 4 ⊢ ((𝐹:𝐴⟶1-1𝐵 ∧ 𝐶 ⊆ 𝐴) → ◡(𝐹 ↾ 𝐶):(𝐹 “ 𝐶)⟶1-1onto𝐶)
11		imadmrn 6078	. . . . 5 ⊢ (◡(𝐹 ↾ 𝐶) “ dom ◡(𝐹 ↾ 𝐶)) = ran ◡(𝐹 ↾ 𝐶)
12		f1odm 6847	. . . . . 6 ⊢ (◡(𝐹 ↾ 𝐶):(𝐹 “ 𝐶)⟶1-1onto𝐶 → dom ◡(𝐹 ↾ 𝐶) = (𝐹 “ 𝐶))
13	12	imaeq2d 6063	. . . . 5 ⊢ (◡(𝐹 ↾ 𝐶):(𝐹 “ 𝐶)⟶1-1onto𝐶 → (◡(𝐹 ↾ 𝐶) “ dom ◡(𝐹 ↾ 𝐶)) = (◡(𝐹 ↾ 𝐶) “ (𝐹 “ 𝐶)))
14		f1ofo 6851	. . . . . 6 ⊢ (◡(𝐹 ↾ 𝐶):(𝐹 “ 𝐶)⟶1-1onto𝐶 → ◡(𝐹 ↾ 𝐶):(𝐹 “ 𝐶)⟶onto𝐶)
15		forn 6818	. . . . . 6 ⊢ (◡(𝐹 ↾ 𝐶):(𝐹 “ 𝐶)⟶onto𝐶 → ran ◡(𝐹 ↾ 𝐶) = 𝐶)
16	14, 15	syl 18	. . . . 5 ⊢ (◡(𝐹 ↾ 𝐶):(𝐹 “ 𝐶)⟶1-1onto𝐶 → ran ◡(𝐹 ↾ 𝐶) = 𝐶)
17	11, 13, 16	3eqtr3a 2822	. . . 4 ⊢ (◡(𝐹 ↾ 𝐶):(𝐹 “ 𝐶)⟶1-1onto𝐶 → (◡(𝐹 ↾ 𝐶) “ (𝐹 “ 𝐶)) = 𝐶)
18	10, 17	syl 18	. . 3 ⊢ ((𝐹:𝐴⟶1-1𝐵 ∧ 𝐶 ⊆ 𝐴) → (◡(𝐹 ↾ 𝐶) “ (𝐹 “ 𝐶)) = 𝐶)
19	7, 18	eqtr3d 2800	. 2 ⊢ ((𝐹:𝐴⟶1-1𝐵 ∧ 𝐶 ⊆ 𝐴) → ((◡𝐹 ↾ (𝐹 “ 𝐶)) “ (𝐹 “ 𝐶)) = 𝐶)
20	1, 19	eqtr3id 2812	1 ⊢ ((𝐹:𝐴⟶1-1𝐵 ∧ 𝐶 ⊆ 𝐴) → (◡𝐹 “ (𝐹 “ 𝐶)) = 𝐶)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ⊆ wss 3900  ^◡ccnv 5654  dom cdm 5655  ran crn 5656   ↾ cres 5657   “ cima 5658  Fun wfun 6549  ⟶wf 6551  ⟶1-1wf1 6552  ⟶ontowfo 6553  ⟶1-1ontowf1o 6554

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-pr 5395

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-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5171  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-fun 6557  df-fn 6558  df-f 6559  df-f1 6560  df-fo 6561  df-f1o 6562

This theorem is used by:  f1opw2  7697  mptcnfimad  8019  ssenen  9195  f1opwfi  9370  isf34lem3  10477  subggim  19506  gicsubgen  19520  cnt1  23695  basqtop  24057  tgqtop  24058  hmeoopn  24112  hmeocld  24113  hmeontr  24115  qtopf1  24162  f1otrg  29475  tpr2rico  34611  eulerpartlemmf  35074  ballotlemscr  35218  ballotlemrinv0  35232  f1preimaex  35782  cvmlift2lem9a  36234  grpokerinj  39018  grimcnv  49189  uhgrimedg  49192  isubgr3stgrlem8  49274