Theorem mptpreima 6182

Description: The preimage of a function in maps-to notation. (Contributed by Stefan O'Rear, 25-Jan-2015.)

Hypothesis

Ref	Expression
dmmpt.1	⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)

Assertion

Ref	Expression
mptpreima	⊢ (◡𝐹 “ 𝐶) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ 𝐶}

Distinct variable group:   𝑥,𝐶

Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)   𝐹(𝑥)

Proof of Theorem mptpreima

Dummy variable 𝑦 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dmmpt.1	. . . . . 6 ⊢ 𝐹 = (𝑥 ∈ 𝐴 ↦ 𝐵)
2		df-mpt 5171	. . . . . 6 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
3	1, 2	eqtri 2753	. . . . 5 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
4	3	cnveqi 5812	. . . 4 ⊢ ◡𝐹 = ◡{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
5		cnvopab 6081	. . . 4 ⊢ ◡{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {⟨𝑦, 𝑥⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
6	4, 5	eqtri 2753	. . 3 ⊢ ◡𝐹 = {⟨𝑦, 𝑥⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
7	6	imaeq1i 6003	. 2 ⊢ (◡𝐹 “ 𝐶) = ({⟨𝑦, 𝑥⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} “ 𝐶)
8		df-ima 5627	. . 3 ⊢ ({⟨𝑦, 𝑥⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} “ 𝐶) = ran ({⟨𝑦, 𝑥⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} ↾ 𝐶)
9		resopab 5980	. . . . 5 ⊢ ({⟨𝑦, 𝑥⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} ↾ 𝐶) = {⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))}
10	9	rneqi 5874	. . . 4 ⊢ ran ({⟨𝑦, 𝑥⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} ↾ 𝐶) = ran {⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))}
11		ancom 460	. . . . . . . . 9 ⊢ ((𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) ∧ 𝑦 ∈ 𝐶))
12		anass 468	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) ∧ 𝑦 ∈ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ (𝑦 = 𝐵 ∧ 𝑦 ∈ 𝐶)))
13	11, 12	bitri 275	. . . . . . . 8 ⊢ ((𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)) ↔ (𝑥 ∈ 𝐴 ∧ (𝑦 = 𝐵 ∧ 𝑦 ∈ 𝐶)))
14	13	exbii 1849	. . . . . . 7 ⊢ (∃𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)) ↔ ∃𝑦(𝑥 ∈ 𝐴 ∧ (𝑦 = 𝐵 ∧ 𝑦 ∈ 𝐶)))
15		19.42v 1954	. . . . . . . 8 ⊢ (∃𝑦(𝑥 ∈ 𝐴 ∧ (𝑦 = 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∧ ∃𝑦(𝑦 = 𝐵 ∧ 𝑦 ∈ 𝐶)))
16		dfclel 2805	. . . . . . . . . 10 ⊢ (𝐵 ∈ 𝐶 ↔ ∃𝑦(𝑦 = 𝐵 ∧ 𝑦 ∈ 𝐶))
17	16	bicomi 224	. . . . . . . . 9 ⊢ (∃𝑦(𝑦 = 𝐵 ∧ 𝑦 ∈ 𝐶) ↔ 𝐵 ∈ 𝐶)
18	17	anbi2i 623	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐴 ∧ ∃𝑦(𝑦 = 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶))
19	15, 18	bitri 275	. . . . . . 7 ⊢ (∃𝑦(𝑥 ∈ 𝐴 ∧ (𝑦 = 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶))
20	14, 19	bitri 275	. . . . . 6 ⊢ (∃𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)) ↔ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶))
21	20	abbii 2797	. . . . 5 ⊢ {𝑥 ∣ ∃𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶)}
22		rnopab 5891	. . . . 5 ⊢ ran {⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))} = {𝑥 ∣ ∃𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))}
23		df-rab 3394	. . . . 5 ⊢ {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ 𝐶} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶)}
24	21, 22, 23	3eqtr4i 2763	. . . 4 ⊢ ran {⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))} = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ 𝐶}
25	10, 24	eqtri 2753	. . 3 ⊢ ran ({⟨𝑦, 𝑥⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} ↾ 𝐶) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ 𝐶}
26	8, 25	eqtri 2753	. 2 ⊢ ({⟨𝑦, 𝑥⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} “ 𝐶) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ 𝐶}
27	7, 26	eqtri 2753	1 ⊢ (◡𝐹 “ 𝐶) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ 𝐶}

Syntax hints:   ∧ wa 395   = wceq 1541  ∃wex 1780   ∈ wcel 2110  {cab 2708  {crab 3393  {copab 5151   ↦ cmpt 5170  ^◡ccnv 5613  ran crn 5615   ↾ cres 5616   “ cima 5617

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2112  ax-9 2120  ax-10 2143  ax-11 2159  ax-12 2179  ax-ext 2702  ax-sep 5232  ax-nul 5242  ax-pr 5368

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-rab 3394  df-v 3436  df-dif 3903  df-un 3905  df-in 3907  df-ss 3917  df-nul 4282  df-if 4474  df-sn 4575  df-pr 4577  df-op 4581  df-br 5090  df-opab 5152  df-mpt 5171  df-xp 5620  df-rel 5621  df-cnv 5622  df-dm 5624  df-rn 5625  df-res 5626  df-ima 5627

This theorem is referenced by:  mptiniseg  6183  dmmpt  6184  fmpt  7038  f1oresrab  7055  mptsuppdifd  8111  r0weon  9895  compss  10259  infrenegsup  12097  eqglact  19084  odngen  19482  pjdm  21637  psrbagsn  21991  coe1mul2lem2  22175  xkoccn  23527  txcnmpt  23532  txdis1cn  23543  pthaus  23546  txkgen  23560  xkoco1cn  23565  xkoco2cn  23566  xkoinjcn  23595  txconn  23597  imasnopn  23598  imasncld  23599  imasncls  23600  ptcmplem1  23960  ptcmplem3  23962  ptcmplem4  23963  tmdgsum2  24004  symgtgp  24014  tgpconncompeqg  24020  ghmcnp  24023  tgpt0  24027  qustgpopn  24028  qustgphaus  24031  eltsms  24041  prdsxmslem2  24437  efopn  26587  atansopn  26862  xrlimcnp  26898  fpwrelmapffslem  32705  ptrest  37638  mbfposadd  37686  cnambfre  37687  itg2addnclem2  37691  iblabsnclem  37702  ftc1anclem1  37712  ftc1anclem6  37717  resuppsinopn  42375  pwfi2f1o  43108  smfpimioo  46804