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

Metamath Proof Explorer

Theorem ltexpri

Description: Proposition 9-3.5(iv) of Gleason p. 123. (Contributed by NM, 13-May-1996) (Revised by Mario Carneiro, 14-Jun-2013) (New usage is discouraged.)

Ref Expression
Assertion ltexpri 
|- ( A 
 E. x e. P. ( A +P. x ) = B )

Proof

Step Hyp Ref Expression
1 ltrelpr 
 |-
2 1 brel 
 |-  ( A 
 ( A e. P. /\ B e. P. ) )
3 ltprord 
 |-  ( ( A e. P. /\ B e. P. ) -> ( A 
 A C. B ) )
4 oveq2 
 |-  ( y = z -> ( w +Q y ) = ( w +Q z ) )
5 4 eleq1d 
 |-  ( y = z -> ( ( w +Q y ) e. B <-> ( w +Q z ) e. B ) )
6 5 anbi2d 
 |-  ( y = z -> ( ( -. w e. A /\ ( w +Q y ) e. B ) <-> ( -. w e. A /\ ( w +Q z ) e. B ) ) )
7 6 exbidv 
 |-  ( y = z -> ( E. w ( -. w e. A /\ ( w +Q y ) e. B ) <-> E. w ( -. w e. A /\ ( w +Q z ) e. B ) ) )
8 7 cbvabv 
 |-  { y | E. w ( -. w e. A /\ ( w +Q y ) e. B ) } = { z | E. w ( -. w e. A /\ ( w +Q z ) e. B ) }
9 8 ltexprlem5 
 |-  ( ( B e. P. /\ A C. B ) -> { y | E. w ( -. w e. A /\ ( w +Q y ) e. B ) } e. P. )
10 9 adantll 
 |-  ( ( ( A e. P. /\ B e. P. ) /\ A C. B ) -> { y | E. w ( -. w e. A /\ ( w +Q y ) e. B ) } e. P. )
11 8 ltexprlem6 
 |-  ( ( ( A e. P. /\ B e. P. ) /\ A C. B ) -> ( A +P. { y | E. w ( -. w e. A /\ ( w +Q y ) e. B ) } ) C_ B )
12 8 ltexprlem7 
 |-  ( ( ( A e. P. /\ B e. P. ) /\ A C. B ) -> B C_ ( A +P. { y | E. w ( -. w e. A /\ ( w +Q y ) e. B ) } ) )
13 11 12 eqssd 
 |-  ( ( ( A e. P. /\ B e. P. ) /\ A C. B ) -> ( A +P. { y | E. w ( -. w e. A /\ ( w +Q y ) e. B ) } ) = B )
14 oveq2 
 |-  ( x = { y | E. w ( -. w e. A /\ ( w +Q y ) e. B ) } -> ( A +P. x ) = ( A +P. { y | E. w ( -. w e. A /\ ( w +Q y ) e. B ) } ) )
15 14 eqeq1d 
 |-  ( x = { y | E. w ( -. w e. A /\ ( w +Q y ) e. B ) } -> ( ( A +P. x ) = B <-> ( A +P. { y | E. w ( -. w e. A /\ ( w +Q y ) e. B ) } ) = B ) )
16 15 rspcev 
 |-  ( ( { y | E. w ( -. w e. A /\ ( w +Q y ) e. B ) } e. P. /\ ( A +P. { y | E. w ( -. w e. A /\ ( w +Q y ) e. B ) } ) = B ) -> E. x e. P. ( A +P. x ) = B )
17 10 13 16 syl2anc 
 |-  ( ( ( A e. P. /\ B e. P. ) /\ A C. B ) -> E. x e. P. ( A +P. x ) = B )
18 17 ex 
 |-  ( ( A e. P. /\ B e. P. ) -> ( A C. B -> E. x e. P. ( A +P. x ) = B ) )
19 3 18 sylbid 
 |-  ( ( A e. P. /\ B e. P. ) -> ( A 
 E. x e. P. ( A +P. x ) = B ) )
20 2 19 mpcom 
 |-  ( A 
 E. x e. P. ( A +P. x ) = B )