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

Metamath Proof Explorer

Theorem ltexprlem5

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

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

Proof

Step Hyp Ref Expression
1 ltexprlem.1 
 |-  C = { x | E. y ( -. y e. A /\ ( y +Q x ) e. B ) }
2 1 ltexprlem1 
 |-  ( B e. P. -> ( A C. B -> C =/= (/) ) )
3 0pss 
 |-  ( (/) C. C <-> C =/= (/) )
4 2 3 imbitrrdi 
 |-  ( B e. P. -> ( A C. B -> (/) C. C ) )
5 4 imp 
 |-  ( ( B e. P. /\ A C. B ) -> (/) C. C )
6 1 ltexprlem2 
 |-  ( B e. P. -> C C. Q. )
7 6 adantr 
 |-  ( ( B e. P. /\ A C. B ) -> C C. Q. )
8 1 ltexprlem3 
 |-  ( B e. P. -> ( x e. C -> A. z ( z  z e. C ) ) )
9 1 ltexprlem4 
 |-  ( B e. P. -> ( x e. C -> E. z ( z e. C /\ x
10 df-rex 
 |-  ( E. z e. C x  E. z ( z e. C /\ x
11 9 10 imbitrrdi 
 |-  ( B e. P. -> ( x e. C -> E. z e. C x
12 8 11 jcad 
 |-  ( B e. P. -> ( x e. C -> ( A. z ( z  z e. C ) /\ E. z e. C x
13 12 ralrimiv 
 |-  ( B e. P. -> A. x e. C ( A. z ( z  z e. C ) /\ E. z e. C x
14 13 adantr 
 |-  ( ( B e. P. /\ A C. B ) -> A. x e. C ( A. z ( z  z e. C ) /\ E. z e. C x
15 elnp 
 |-  ( C e. P. <-> ( ( (/) C. C /\ C C. Q. ) /\ A. x e. C ( A. z ( z  z e. C ) /\ E. z e. C x
16 5 7 14 15 syl21anbrc 
 |-  ( ( B e. P. /\ A C. B ) -> C e. P. )