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 )