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

Metamath Proof Explorer

Theorem ltexprlem3

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 ltexprlem3 
|- ( B e. P. -> ( x e. C -> A. z ( z  z e. C ) ) )

Proof

Step Hyp Ref Expression
1 ltexprlem.1 
 |-  C = { x | E. y ( -. y e. A /\ ( y +Q x ) e. B ) }
2 elprnq 
 |-  ( ( B e. P. /\ ( y +Q x ) e. B ) -> ( y +Q x ) e. Q. )
3 addnqf 
 |-  +Q : ( Q. X. Q. ) --> Q.
4 3 fdmi 
 |-  dom +Q = ( Q. X. Q. )
5 0nnq 
 |-  -. (/) e. Q.
6 4 5 ndmovrcl 
 |-  ( ( y +Q x ) e. Q. -> ( y e. Q. /\ x e. Q. ) )
7 6 simpld 
 |-  ( ( y +Q x ) e. Q. -> y e. Q. )
8 ltanq 
 |-  ( y e. Q. -> ( z  ( y +Q z )
9 2 7 8 3syl 
 |-  ( ( B e. P. /\ ( y +Q x ) e. B ) -> ( z  ( y +Q z )
10 prcdnq 
 |-  ( ( B e. P. /\ ( y +Q x ) e. B ) -> ( ( y +Q z )  ( y +Q z ) e. B ) )
11 9 10 sylbid 
 |-  ( ( B e. P. /\ ( y +Q x ) e. B ) -> ( z  ( y +Q z ) e. B ) )
12 11 impancom 
 |-  ( ( B e. P. /\ z  ( ( y +Q x ) e. B -> ( y +Q z ) e. B ) )
13 12 anim2d 
 |-  ( ( B e. P. /\ z  ( ( -. y e. A /\ ( y +Q x ) e. B ) -> ( -. y e. A /\ ( y +Q z ) e. B ) ) )
14 13 eximdv 
 |-  ( ( B e. P. /\ z  ( E. y ( -. y e. A /\ ( y +Q x ) e. B ) -> E. y ( -. y e. A /\ ( y +Q z ) e. B ) ) )
15 1 eqabri 
 |-  ( x e. C <-> E. y ( -. y e. A /\ ( y +Q x ) e. B ) )
16 vex 
 |-  z e. _V
17 oveq2 
 |-  ( x = z -> ( y +Q x ) = ( y +Q z ) )
18 17 eleq1d 
 |-  ( x = z -> ( ( y +Q x ) e. B <-> ( y +Q z ) e. B ) )
19 18 anbi2d 
 |-  ( x = z -> ( ( -. y e. A /\ ( y +Q x ) e. B ) <-> ( -. y e. A /\ ( y +Q z ) e. B ) ) )
20 19 exbidv 
 |-  ( x = z -> ( E. y ( -. y e. A /\ ( y +Q x ) e. B ) <-> E. y ( -. y e. A /\ ( y +Q z ) e. B ) ) )
21 16 20 1 elab2 
 |-  ( z e. C <-> E. y ( -. y e. A /\ ( y +Q z ) e. B ) )
22 14 15 21 3imtr4g 
 |-  ( ( B e. P. /\ z  ( x e. C -> z e. C ) )
23 22 ex 
 |-  ( B e. P. -> ( z  ( x e. C -> z e. C ) ) )
24 23 com23 
 |-  ( B e. P. -> ( x e. C -> ( z  z e. C ) ) )
25 24 alrimdv 
 |-  ( B e. P. -> ( x e. C -> A. z ( z  z e. C ) ) )