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

Metamath Proof Explorer

Theorem ltexprlem2

Description: Lemma for Proposition 9-3.5(iv) of Gleason p. 123. (Contributed by NM, 3-Apr-1996) (New usage is discouraged.)

Ref Expression
Hypothesis ltexprlem.1 
|- C = { x | E. y ( -. y e. A /\ ( y +Q x ) e. B ) }
Assertion ltexprlem2 
|- ( B e. P. -> C C. Q. )

Proof

Step Hyp Ref Expression
1 ltexprlem.1 
 |-  C = { x | E. y ( -. y e. A /\ ( y +Q x ) e. B ) }
2 1 eqabri 
 |-  ( x e. C <-> E. y ( -. y e. A /\ ( y +Q x ) e. B ) )
3 elprnq 
 |-  ( ( B e. P. /\ ( y +Q x ) e. B ) -> ( y +Q x ) e. Q. )
4 addnqf 
 |-  +Q : ( Q. X. Q. ) --> Q.
5 4 fdmi 
 |-  dom +Q = ( Q. X. Q. )
6 0nnq 
 |-  -. (/) e. Q.
7 5 6 ndmovrcl 
 |-  ( ( y +Q x ) e. Q. -> ( y e. Q. /\ x e. Q. ) )
8 3 7 syl 
 |-  ( ( B e. P. /\ ( y +Q x ) e. B ) -> ( y e. Q. /\ x e. Q. ) )
9 ltaddnq 
 |-  ( ( x e. Q. /\ y e. Q. ) -> x
10 9 ancoms 
 |-  ( ( y e. Q. /\ x e. Q. ) -> x
11 addcomnq 
 |-  ( x +Q y ) = ( y +Q x )
12 10 11 breqtrdi 
 |-  ( ( y e. Q. /\ x e. Q. ) -> x
13 prcdnq 
 |-  ( ( B e. P. /\ ( y +Q x ) e. B ) -> ( x  x e. B ) )
14 12 13 syl5 
 |-  ( ( B e. P. /\ ( y +Q x ) e. B ) -> ( ( y e. Q. /\ x e. Q. ) -> x e. B ) )
15 8 14 mpd 
 |-  ( ( B e. P. /\ ( y +Q x ) e. B ) -> x e. B )
16 15 ex 
 |-  ( B e. P. -> ( ( y +Q x ) e. B -> x e. B ) )
17 16 adantld 
 |-  ( B e. P. -> ( ( -. y e. A /\ ( y +Q x ) e. B ) -> x e. B ) )
18 17 exlimdv 
 |-  ( B e. P. -> ( E. y ( -. y e. A /\ ( y +Q x ) e. B ) -> x e. B ) )
19 2 18 biimtrid 
 |-  ( B e. P. -> ( x e. C -> x e. B ) )
20 19 ssrdv 
 |-  ( B e. P. -> C C_ B )
21 prpssnq 
 |-  ( B e. P. -> B C. Q. )
22 20 21 sspsstrd 
 |-  ( B e. P. -> C C. Q. )