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. )