Theorem mptpreima 5328

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

Hypothesis

Ref	Expression
dmmpt.1	|- F = ( x e. A |-> B )

Assertion

Ref	Expression
mptpreima	|- ( `' F " C ) = { x e. A | B e. C }

Distinct variable group:   x, C

Allowed substitution hints:   A( x)   B( x)   F( x)

Proof of Theorem mptpreima

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		dmmpt.1	. . . . . 6 |- F = ( x e. A |-> B )
2		df-mpt 4463	. . . . . 6 |- ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }
3	1, 2	eqtri 2473	. . . . 5 |- F = { <. x , y >. | ( x e. A /\ y = B ) }
4	3	cnveqi 5009	. . . 4 |- `' F = `' { <. x , y >. | ( x e. A /\ y = B ) }
5		cnvopab 5237	. . . 4 |- `' { <. x , y >. | ( x e. A /\ y = B ) } = { <. y , x >. | ( x e. A /\ y = B ) }
6	4, 5	eqtri 2473	. . 3 |- `' F = { <. y , x >. | ( x e. A /\ y = B ) }
7	6	imaeq1i 5165	. 2 |- ( `' F " C ) = ( { <. y , x >. | ( x e. A /\ y = B ) } " C )
8		df-ima 4847	. . 3 |- ( { <. y , x >. | ( x e. A /\ y = B ) } " C ) = ran ( { <. y , x >. | ( x e. A /\ y = B ) } |` C )
9		resopab 5151	. . . . 5 |- ( { <. y , x >. | ( x e. A /\ y = B ) } |` C ) = { <. y , x >. | ( y e. C /\ ( x e. A /\ y = B ) ) }
10	9	rneqi 5061	. . . 4 |- ran ( { <. y , x >. | ( x e. A /\ y = B ) } |` C ) = ran { <. y , x >. | ( y e. C /\ ( x e. A /\ y = B ) ) }
11		ancom 452	. . . . . . . . 9 |- ( ( y e. C /\ ( x e. A /\ y = B ) ) <-> ( ( x e. A /\ y = B ) /\ y e. C ) )
12		anass 655	. . . . . . . . 9 |- ( ( ( x e. A /\ y = B ) /\ y e. C ) <-> ( x e. A /\ ( y = B /\ y e. C ) ) )
13	11, 12	bitri 253	. . . . . . . 8 |- ( ( y e. C /\ ( x e. A /\ y = B ) ) <-> ( x e. A /\ ( y = B /\ y e. C ) ) )
14	13	exbii 1718	. . . . . . 7 |- ( E. y ( y e. C /\ ( x e. A /\ y = B ) ) <-> E. y ( x e. A /\ ( y = B /\ y e. C ) ) )
15		19.42v 1834	. . . . . . . 8 |- ( E. y ( x e. A /\ ( y = B /\ y e. C ) ) <-> ( x e. A /\ E. y ( y = B /\ y e. C ) ) )
16		df-clel 2447	. . . . . . . . . 10 |- ( B e. C <-> E. y ( y = B /\ y e. C ) )
17	16	bicomi 206	. . . . . . . . 9 |- ( E. y ( y = B /\ y e. C ) <-> B e. C )
18	17	anbi2i 700	. . . . . . . 8 |- ( ( x e. A /\ E. y ( y = B /\ y e. C ) ) <-> ( x e. A /\ B e. C ) )
19	15, 18	bitri 253	. . . . . . 7 |- ( E. y ( x e. A /\ ( y = B /\ y e. C ) ) <-> ( x e. A /\ B e. C ) )
20	14, 19	bitri 253	. . . . . 6 |- ( E. y ( y e. C /\ ( x e. A /\ y = B ) ) <-> ( x e. A /\ B e. C ) )
21	20	abbii 2567	. . . . 5 |- { x | E. y ( y e. C /\ ( x e. A /\ y = B ) ) } = { x | ( x e. A /\ B e. C ) }
22		rnopab 5079	. . . . 5 |- ran { <. y , x >. | ( y e. C /\ ( x e. A /\ y = B ) ) } = { x | E. y ( y e. C /\ ( x e. A /\ y = B ) ) }
23		df-rab 2746	. . . . 5 |- { x e. A | B e. C } = { x | ( x e. A /\ B e. C ) }
24	21, 22, 23	3eqtr4i 2483	. . . 4 |- ran { <. y , x >. | ( y e. C /\ ( x e. A /\ y = B ) ) } = { x e. A | B e. C }
25	10, 24	eqtri 2473	. . 3 |- ran ( { <. y , x >. | ( x e. A /\ y = B ) } |` C ) = { x e. A | B e. C }
26	8, 25	eqtri 2473	. 2 |- ( { <. y , x >. | ( x e. A /\ y = B ) } " C ) = { x e. A | B e. C }
27	7, 26	eqtri 2473	1 |- ( `' F " C ) = { x e. A | B e. C }

Syntax hints:   /\ wa 371   = wceq 1444   E.wex 1663   e. wcel 1887   {cab 2437   {crab 2741   {copab 4460   |-> cmpt 4461   `'ccnv 4833   ran crn 4835   |` cres 4836   "cima 4837

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pr 4639

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3047  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-nul 3732  df-if 3882  df-sn 3969  df-pr 3971  df-op 3975  df-br 4403  df-opab 4462  df-mpt 4463  df-xp 4840  df-rel 4841  df-cnv 4842  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847

This theorem is referenced by:  mptiniseg  5329  dmmpt  5330  fmpt  6043  f1oresrab  6055  mptsuppdifd  6937  r0weon  8443  compss  8806  infrenegsup  10591  infmsupOLD  10592  eqglact  16868  odngen  17226  psrbagsn  18718  coe1mul2lem2  18861  pjdm  19270  xkoccn  20634  txcnmpt  20639  txdis1cn  20650  pthaus  20653  txkgen  20667  xkoco1cn  20672  xkoco2cn  20673  xkoinjcn  20702  txcon  20704  imasnopn  20705  imasncld  20706  imasncls  20707  ptcmplem1  21067  ptcmplem3  21069  ptcmplem4  21070  tmdgsum2  21111  symgtgp  21116  tgpconcompeqg  21126  ghmcnp  21129  tgpt0  21133  qustgpopn  21134  qustgphaus  21137  eltsms  21147  prdsxmslem2  21544  efopn  23603  atansopn  23858  xrlimcnp  23894  suppss2fOLD  28237  fpwrelmapffslem  28317  ptrest  31939  mbfposadd  31988  cnambfre  31989  itg2addnclem2  31994  iblabsnclem  32005  ftc1anclem1  32017  ftc1anclem6  32022  pwfi2f1o  35954