This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem shftlem

Description: Two ways to write a shifted set ( B + A ) . (Contributed by Mario Carneiro, 3-Nov-2013)

Ref Expression
Assertion shftlem 
|- ( ( A e. CC /\ B C_ CC ) -> { x e. CC | ( x - A ) e. B } = { x | E. y e. B x = ( y + A ) } )

Proof

Step Hyp Ref Expression
1 df-rab 
 |-  { x e. CC | ( x - A ) e. B } = { x | ( x e. CC /\ ( x - A ) e. B ) }
2 npcan 
 |-  ( ( x e. CC /\ A e. CC ) -> ( ( x - A ) + A ) = x )
3 2 ancoms 
 |-  ( ( A e. CC /\ x e. CC ) -> ( ( x - A ) + A ) = x )
4 3 eqcomd 
 |-  ( ( A e. CC /\ x e. CC ) -> x = ( ( x - A ) + A ) )
5 oveq1 
 |-  ( y = ( x - A ) -> ( y + A ) = ( ( x - A ) + A ) )
6 5 rspceeqv 
 |-  ( ( ( x - A ) e. B /\ x = ( ( x - A ) + A ) ) -> E. y e. B x = ( y + A ) )
7 6 expcom 
 |-  ( x = ( ( x - A ) + A ) -> ( ( x - A ) e. B -> E. y e. B x = ( y + A ) ) )
8 4 7 syl 
 |-  ( ( A e. CC /\ x e. CC ) -> ( ( x - A ) e. B -> E. y e. B x = ( y + A ) ) )
9 8 expimpd 
 |-  ( A e. CC -> ( ( x e. CC /\ ( x - A ) e. B ) -> E. y e. B x = ( y + A ) ) )
10 9 adantr 
 |-  ( ( A e. CC /\ B C_ CC ) -> ( ( x e. CC /\ ( x - A ) e. B ) -> E. y e. B x = ( y + A ) ) )
11 ssel2 
 |-  ( ( B C_ CC /\ y e. B ) -> y e. CC )
12 addcl 
 |-  ( ( y e. CC /\ A e. CC ) -> ( y + A ) e. CC )
13 11 12 sylan 
 |-  ( ( ( B C_ CC /\ y e. B ) /\ A e. CC ) -> ( y + A ) e. CC )
14 pncan 
 |-  ( ( y e. CC /\ A e. CC ) -> ( ( y + A ) - A ) = y )
15 11 14 sylan 
 |-  ( ( ( B C_ CC /\ y e. B ) /\ A e. CC ) -> ( ( y + A ) - A ) = y )
16 simplr 
 |-  ( ( ( B C_ CC /\ y e. B ) /\ A e. CC ) -> y e. B )
17 15 16 eqeltrd 
 |-  ( ( ( B C_ CC /\ y e. B ) /\ A e. CC ) -> ( ( y + A ) - A ) e. B )
18 13 17 jca 
 |-  ( ( ( B C_ CC /\ y e. B ) /\ A e. CC ) -> ( ( y + A ) e. CC /\ ( ( y + A ) - A ) e. B ) )
19 18 ancoms 
 |-  ( ( A e. CC /\ ( B C_ CC /\ y e. B ) ) -> ( ( y + A ) e. CC /\ ( ( y + A ) - A ) e. B ) )
20 19 anassrs 
 |-  ( ( ( A e. CC /\ B C_ CC ) /\ y e. B ) -> ( ( y + A ) e. CC /\ ( ( y + A ) - A ) e. B ) )
21 eleq1 
 |-  ( x = ( y + A ) -> ( x e. CC <-> ( y + A ) e. CC ) )
22 oveq1 
 |-  ( x = ( y + A ) -> ( x - A ) = ( ( y + A ) - A ) )
23 22 eleq1d 
 |-  ( x = ( y + A ) -> ( ( x - A ) e. B <-> ( ( y + A ) - A ) e. B ) )
24 21 23 anbi12d 
 |-  ( x = ( y + A ) -> ( ( x e. CC /\ ( x - A ) e. B ) <-> ( ( y + A ) e. CC /\ ( ( y + A ) - A ) e. B ) ) )
25 20 24 syl5ibrcom 
 |-  ( ( ( A e. CC /\ B C_ CC ) /\ y e. B ) -> ( x = ( y + A ) -> ( x e. CC /\ ( x - A ) e. B ) ) )
26 25 rexlimdva 
 |-  ( ( A e. CC /\ B C_ CC ) -> ( E. y e. B x = ( y + A ) -> ( x e. CC /\ ( x - A ) e. B ) ) )
27 10 26 impbid 
 |-  ( ( A e. CC /\ B C_ CC ) -> ( ( x e. CC /\ ( x - A ) e. B ) <-> E. y e. B x = ( y + A ) ) )
28 27 abbidv 
 |-  ( ( A e. CC /\ B C_ CC ) -> { x | ( x e. CC /\ ( x - A ) e. B ) } = { x | E. y e. B x = ( y + A ) } )
29 1 28 eqtrid 
 |-  ( ( A e. CC /\ B C_ CC ) -> { x e. CC | ( x - A ) e. B } = { x | E. y e. B x = ( y + A ) } )