Theorem mptpreima 6141

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 5158	. . . . . 6 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
3	1, 2	eqtri 2766	. . . . 5 ⊢ 𝐹 = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
4	3	cnveqi 5783	. . . 4 ⊢ ◡𝐹 = ◡{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
5		cnvopab 6042	. . . 4 ⊢ ◡{⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {⟨𝑦, 𝑥⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
6	4, 5	eqtri 2766	. . 3 ⊢ ◡𝐹 = {⟨𝑦, 𝑥⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
7	6	imaeq1i 5966	. 2 ⊢ (◡𝐹 “ 𝐶) = ({⟨𝑦, 𝑥⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} “ 𝐶)
8		df-ima 5602	. . 3 ⊢ ({⟨𝑦, 𝑥⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} “ 𝐶) = ran ({⟨𝑦, 𝑥⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} ↾ 𝐶)
9		resopab 5942	. . . . 5 ⊢ ({⟨𝑦, 𝑥⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} ↾ 𝐶) = {⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))}
10	9	rneqi 5846	. . . 4 ⊢ ran ({⟨𝑦, 𝑥⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} ↾ 𝐶) = ran {⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))}
11		ancom 461	. . . . . . . . 9 ⊢ ((𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)) ↔ ((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) ∧ 𝑦 ∈ 𝐶))
12		anass 469	. . . . . . . . 9 ⊢ (((𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) ∧ 𝑦 ∈ 𝐶) ↔ (𝑥 ∈ 𝐴 ∧ (𝑦 = 𝐵 ∧ 𝑦 ∈ 𝐶)))
13	11, 12	bitri 274	. . . . . . . 8 ⊢ ((𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)) ↔ (𝑥 ∈ 𝐴 ∧ (𝑦 = 𝐵 ∧ 𝑦 ∈ 𝐶)))
14	13	exbii 1850	. . . . . . 7 ⊢ (∃𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)) ↔ ∃𝑦(𝑥 ∈ 𝐴 ∧ (𝑦 = 𝐵 ∧ 𝑦 ∈ 𝐶)))
15		19.42v 1957	. . . . . . . 8 ⊢ (∃𝑦(𝑥 ∈ 𝐴 ∧ (𝑦 = 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∧ ∃𝑦(𝑦 = 𝐵 ∧ 𝑦 ∈ 𝐶)))
16		dfclel 2817	. . . . . . . . . 10 ⊢ (𝐵 ∈ 𝐶 ↔ ∃𝑦(𝑦 = 𝐵 ∧ 𝑦 ∈ 𝐶))
17	16	bicomi 223	. . . . . . . . 9 ⊢ (∃𝑦(𝑦 = 𝐵 ∧ 𝑦 ∈ 𝐶) ↔ 𝐵 ∈ 𝐶)
18	17	anbi2i 623	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐴 ∧ ∃𝑦(𝑦 = 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶))
19	15, 18	bitri 274	. . . . . . 7 ⊢ (∃𝑦(𝑥 ∈ 𝐴 ∧ (𝑦 = 𝐵 ∧ 𝑦 ∈ 𝐶)) ↔ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶))
20	14, 19	bitri 274	. . . . . 6 ⊢ (∃𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)) ↔ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶))
21	20	abbii 2808	. . . . 5 ⊢ {𝑥 ∣ ∃𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶)}
22		rnopab 5863	. . . . 5 ⊢ ran {⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))} = {𝑥 ∣ ∃𝑦(𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))}
23		df-rab 3073	. . . . 5 ⊢ {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ 𝐶} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ 𝐵 ∈ 𝐶)}
24	21, 22, 23	3eqtr4i 2776	. . . 4 ⊢ ran {⟨𝑦, 𝑥⟩ ∣ (𝑦 ∈ 𝐶 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))} = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ 𝐶}
25	10, 24	eqtri 2766	. . 3 ⊢ ran ({⟨𝑦, 𝑥⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} ↾ 𝐶) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ 𝐶}
26	8, 25	eqtri 2766	. 2 ⊢ ({⟨𝑦, 𝑥⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} “ 𝐶) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ 𝐶}
27	7, 26	eqtri 2766	1 ⊢ (◡𝐹 “ 𝐶) = {𝑥 ∈ 𝐴 ∣ 𝐵 ∈ 𝐶}

Syntax hints:   ∧ wa 396   = wceq 1539  ∃wex 1782   ∈ wcel 2106  {cab 2715  {crab 3068  {copab 5136   ↦ cmpt 5157  ^◡ccnv 5588  ran crn 5590   ↾ cres 5591   “ cima 5592

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-br 5075  df-opab 5137  df-mpt 5158  df-xp 5595  df-rel 5596  df-cnv 5597  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602

This theorem is referenced by:  mptiniseg  6142  dmmpt  6143  fmpt  6984  f1oresrab  6999  mptsuppdifd  8002  r0weon  9768  compss  10132  infrenegsup  11958  eqglact  18807  odngen  19182  pjdm  20914  psrbagsn  21271  coe1mul2lem2  21439  xkoccn  22770  txcnmpt  22775  txdis1cn  22786  pthaus  22789  txkgen  22803  xkoco1cn  22808  xkoco2cn  22809  xkoinjcn  22838  txconn  22840  imasnopn  22841  imasncld  22842  imasncls  22843  ptcmplem1  23203  ptcmplem3  23205  ptcmplem4  23206  tmdgsum2  23247  symgtgp  23257  tgpconncompeqg  23263  ghmcnp  23266  tgpt0  23270  qustgpopn  23271  qustgphaus  23274  eltsms  23284  prdsxmslem2  23685  efopn  25813  atansopn  26082  xrlimcnp  26118  fpwrelmapffslem  31067  ptrest  35776  mbfposadd  35824  cnambfre  35825  itg2addnclem2  35829  iblabsnclem  35840  ftc1anclem1  35850  ftc1anclem6  35855  pwfi2f1o  40921  smfpimioo  44321