Metamath Proof Explorer

Theorem mptpreima

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

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

Proof

Step Hyp Ref Expression
1 dmmpt.1 
 |-  F = ( x e. A |-> B )
2 df-mpt 
 |-  ( x e. A |-> B ) = { <. x , y >. | ( x e. A /\ y = B ) }
3 1 2 eqtri 
 |-  F = { <. x , y >. | ( x e. A /\ y = B ) }
4 3 cnveqi 
 |-  `' F = `' { <. x , y >. | ( x e. A /\ y = B ) }
5 cnvopab 
 |-  `' { <. x , y >. | ( x e. A /\ y = B ) } = { <. y , x >. | ( x e. A /\ y = B ) }
6 4 5 eqtri 
 |-  `' F = { <. y , x >. | ( x e. A /\ y = B ) }
7 6 imaeq1i 
 |-  ( `' F " C ) = ( { <. y , x >. | ( x e. A /\ y = B ) } " C )
8 df-ima 
 |-  ( { <. y , x >. | ( x e. A /\ y = B ) } " C ) = ran ( { <. y , x >. | ( x e. A /\ y = B ) } |` C )
9 resopab 
 |-  ( { <. y , x >. | ( x e. A /\ y = B ) } |` C ) = { <. y , x >. | ( y e. C /\ ( x e. A /\ y = B ) ) }
10 9 rneqi 
 |-  ran ( { <. y , x >. | ( x e. A /\ y = B ) } |` C ) = ran { <. y , x >. | ( y e. C /\ ( x e. A /\ y = B ) ) }
11 ancom 
 |-  ( ( y e. C /\ ( x e. A /\ y = B ) ) <-> ( ( x e. A /\ y = B ) /\ y e. C ) )
12 anass 
 |-  ( ( ( x e. A /\ y = B ) /\ y e. C ) <-> ( x e. A /\ ( y = B /\ y e. C ) ) )
13 11 12 bitri 
 |-  ( ( y e. C /\ ( x e. A /\ y = B ) ) <-> ( x e. A /\ ( y = B /\ y e. C ) ) )
14 13 exbii 
 |-  ( E. y ( y e. C /\ ( x e. A /\ y = B ) ) <-> E. y ( x e. A /\ ( y = B /\ y e. C ) ) )
15 19.42v 
 |-  ( E. y ( x e. A /\ ( y = B /\ y e. C ) ) <-> ( x e. A /\ E. y ( y = B /\ y e. C ) ) )
16 dfclel 
 |-  ( B e. C <-> E. y ( y = B /\ y e. C ) )
17 16 bicomi 
 |-  ( E. y ( y = B /\ y e. C ) <-> B e. C )
18 17 anbi2i 
 |-  ( ( x e. A /\ E. y ( y = B /\ y e. C ) ) <-> ( x e. A /\ B e. C ) )
19 15 18 bitri 
 |-  ( E. y ( x e. A /\ ( y = B /\ y e. C ) ) <-> ( x e. A /\ B e. C ) )
20 14 19 bitri 
 |-  ( E. y ( y e. C /\ ( x e. A /\ y = B ) ) <-> ( x e. A /\ B e. C ) )
21 20 abbii 
 |-  { x | E. y ( y e. C /\ ( x e. A /\ y = B ) ) } = { x | ( x e. A /\ B e. C ) }
22 rnopab 
 |-  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 
 |-  { x e. A | B e. C } = { x | ( x e. A /\ B e. C ) }
24 21 22 23 3eqtr4i 
 |-  ran { <. y , x >. | ( y e. C /\ ( x e. A /\ y = B ) ) } = { x e. A | B e. C }
25 10 24 eqtri 
 |-  ran ( { <. y , x >. | ( x e. A /\ y = B ) } |` C ) = { x e. A | B e. C }
26 8 25 eqtri 
 |-  ( { <. y , x >. | ( x e. A /\ y = B ) } " C ) = { x e. A | B e. C }
27 7 26 eqtri 
 |-  ( `' F " C ) = { x e. A | B e. C }