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	abeq2i	|- ( 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	syl5bi	|- ( 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. )