Theorem mptpreima 5328

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

Hypothesis

Ref	Expression
dmmpt2.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		dmmpt2.1	. . . . . 6 |- F = ( x e. A |-> B )
2		df-mpt 4349	. . . . . 6 |- ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }
3	1, 2	eqtri 2461	. . . . 5 |- F = { <. x , y >. | ( x e. A /\ y = B ) }
4	3	cnveqi 5010	. . . 4 |- `' F = `' { <. x , y >. | ( x e. A /\ y = B ) }
5		cnvopab 5235	. . . 4 |- `' { <. x , y >. | ( x e. A /\ y = B ) } = { <. y , x >. | ( x e. A /\ y = B ) }
6	4, 5	eqtri 2461	. . 3 |- `' F = { <. y , x >. | ( x e. A /\ y = B ) }
7	6	imaeq1i 5163	. 2 |- ( `' F " C ) = ( { <. y , x >. | ( x e. A /\ y = B ) } " C )
8		df-ima 4849	. . 3 |- ( { <. y , x >. | ( x e. A /\ y = B ) } " C ) = ran ( { <. y , x >. | ( x e. A /\ y = B ) } |` C )
9		resopab 5150	. . . . 5 |- ( { <. y , x >. | ( x e. A /\ y = B ) } |` C ) = { <. y , x >. | ( y e. C /\ ( x e. A /\ y = B ) ) }
10	9	rneqi 5062	. . . 4 |- ran ( { <. y , x >. | ( x e. A /\ y = B ) } |` C ) = ran { <. y , x >. | ( y e. C /\ ( x e. A /\ y = B ) ) }
11		ancom 448	. . . . . . . . 9 |- ( ( y e. C /\ ( x e. A /\ y = B ) ) <-> ( ( x e. A /\ y = B ) /\ y e. C ) )
12		anass 644	. . . . . . . . 9 |- ( ( ( x e. A /\ y = B ) /\ y e. C ) <-> ( x e. A /\ ( y = B /\ y e. C ) ) )
13	11, 12	bitri 249	. . . . . . . 8 |- ( ( y e. C /\ ( x e. A /\ y = B ) ) <-> ( x e. A /\ ( y = B /\ y e. C ) ) )
14	13	exbii 1639	. . . . . . 7 |- ( E. y ( y e. C /\ ( x e. A /\ y = B ) ) <-> E. y ( x e. A /\ ( y = B /\ y e. C ) ) )
15		19.42v 1928	. . . . . . . 8 |- ( E. y ( x e. A /\ ( y = B /\ y e. C ) ) <-> ( x e. A /\ E. y ( y = B /\ y e. C ) ) )
16		df-clel 2437	. . . . . . . . . 10 |- ( B e. C <-> E. y ( y = B /\ y e. C ) )
17	16	bicomi 202	. . . . . . . . 9 |- ( E. y ( y = B /\ y e. C ) <-> B e. C )
18	17	anbi2i 689	. . . . . . . 8 |- ( ( x e. A /\ E. y ( y = B /\ y e. C ) ) <-> ( x e. A /\ B e. C ) )
19	15, 18	bitri 249	. . . . . . 7 |- ( E. y ( x e. A /\ ( y = B /\ y e. C ) ) <-> ( x e. A /\ B e. C ) )
20	14, 19	bitri 249	. . . . . 6 |- ( E. y ( y e. C /\ ( x e. A /\ y = B ) ) <-> ( x e. A /\ B e. C ) )
21	20	abbii 2553	. . . . 5 |- { x | E. y ( y e. C /\ ( x e. A /\ y = B ) ) } = { x | ( x e. A /\ B e. C ) }
22		rnopab 5080	. . . . 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 2722	. . . . 5 |- { x e. A | B e. C } = { x | ( x e. A /\ B e. C ) }
24	21, 22, 23	3eqtr4i 2471	. . . 4 |- ran { <. y , x >. | ( y e. C /\ ( x e. A /\ y = B ) ) } = { x e. A | B e. C }
25	10, 24	eqtri 2461	. . 3 |- ran ( { <. y , x >. | ( x e. A /\ y = B ) } |` C ) = { x e. A | B e. C }
26	8, 25	eqtri 2461	. 2 |- ( { <. y , x >. | ( x e. A /\ y = B ) } " C ) = { x e. A | B e. C }
27	7, 26	eqtri 2461	1 |- ( `' F " C ) = { x e. A | B e. C }

Syntax hints:   /\ wa 369   = wceq 1364   E.wex 1591   e. wcel 1761   {cab 2427   {crab 2717   {copab 4346   e. cmpt 4347   `'ccnv 4835   ran crn 4837   |` cres 4838   "cima 4839

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-sep 4410  ax-nul 4418  ax-pr 4528

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2263  df-mo 2264  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-rab 2722  df-v 2972  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-nul 3635  df-if 3789  df-sn 3875  df-pr 3877  df-op 3881  df-br 4290  df-opab 4348  df-mpt 4349  df-xp 4842  df-rel 4843  df-cnv 4844  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849

This theorem is referenced by:  mptiniseg  5329  dmmpt  5330  fmpt  5861  f1oresrab  5872  suppss2OLD  6314  suppssfvOLD  6315  suppssov1OLD  6316  mptsuppdifd  6710  cantnflem1OLD  7916  cantnfOLD  7919  r0weon  8175  compss  8541  infmsup  10304  eqglact  15725  odngen  16069  rrgsuppOLD  17341  psrbagsn  17565  coe1mul2lem2  17676  pjdm  18032  xkoccn  19092  txcnmpt  19097  txdis1cn  19108  pthaus  19111  txkgen  19125  xkoco1cn  19130  xkoco2cn  19131  xkoinjcn  19160  txcon  19162  imasnopn  19163  imasncld  19164  imasncls  19165  ptcmplem1  19524  ptcmplem3  19526  ptcmplem4  19527  tmdgsum2  19567  symgtgp  19572  tgpconcompeqg  19582  ghmcnp  19585  tgpt0  19589  divstgpopn  19590  divstgphaus  19593  eltsms  19603  prdsxmslem2  20004  efopn  22046  atansopn  22270  xrlimcnp  22305  suppss2f  25873  fpwrelmapffslem  25951  ptrest  28334  mbfposadd  28348  cnambfre  28349  itg2addnclem2  28353  iblabsnclem  28364  ftc1anclem1  28376  ftc1anclem6  28381  pwfi2f1o  29360