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

Metamath Proof Explorer

Theorem ltexprlem4

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 ltexprlem4 
|- ( B e. P. -> ( x e. C -> E. z ( z e. C /\ x

Proof

Step Hyp Ref Expression
1 ltexprlem.1 
 |-  C = { x | E. y ( -. y e. A /\ ( y +Q x ) e. B ) }
2 prnmax 
 |-  ( ( B e. P. /\ ( y +Q x ) e. B ) -> E. w e. B ( y +Q x )
3 df-rex 
 |-  ( E. w e. B ( y +Q x )  E. w ( w e. B /\ ( y +Q x )
4 2 3 sylib 
 |-  ( ( B e. P. /\ ( y +Q x ) e. B ) -> E. w ( w e. B /\ ( y +Q x )
5 ltrelnq 
 |-
6 5 brel 
 |-  ( ( y +Q x )  ( ( y +Q x ) e. Q. /\ w e. Q. ) )
7 6 simpld 
 |-  ( ( y +Q x )  ( y +Q x ) e. Q. )
8 addnqf 
 |-  +Q : ( Q. X. Q. ) --> Q.
9 8 fdmi 
 |-  dom +Q = ( Q. X. Q. )
10 0nnq 
 |-  -. (/) e. Q.
11 9 10 ndmovrcl 
 |-  ( ( y +Q x ) e. Q. -> ( y e. Q. /\ x e. Q. ) )
12 7 11 syl 
 |-  ( ( y +Q x )  ( y e. Q. /\ x e. Q. ) )
13 ltaddnq 
 |-  ( ( y e. Q. /\ x e. Q. ) -> y
14 ltsonq 
 |-
15 14 5 sotri 
 |-  ( ( y  y
16 13 15 sylan 
 |-  ( ( ( y e. Q. /\ x e. Q. ) /\ ( y +Q x )  y
17 12 16 mpancom 
 |-  ( ( y +Q x )  y
18 5 brel 
 |-  ( y  ( y e. Q. /\ w e. Q. ) )
19 18 simprd 
 |-  ( y  w e. Q. )
20 ltexnq 
 |-  ( w e. Q. -> ( y  E. z ( y +Q z ) = w ) )
21 20 biimpd 
 |-  ( w e. Q. -> ( y  E. z ( y +Q z ) = w ) )
22 19 21 mpcom 
 |-  ( y  E. z ( y +Q z ) = w )
23 17 22 syl 
 |-  ( ( y +Q x )  E. z ( y +Q z ) = w )
24 eqcom 
 |-  ( w = ( y +Q z ) <-> ( y +Q z ) = w )
25 24 exbii 
 |-  ( E. z w = ( y +Q z ) <-> E. z ( y +Q z ) = w )
26 23 25 sylibr 
 |-  ( ( y +Q x )  E. z w = ( y +Q z ) )
27 26 ancri 
 |-  ( ( y +Q x )  ( E. z w = ( y +Q z ) /\ ( y +Q x )
28 27 anim2i 
 |-  ( ( w e. B /\ ( y +Q x )  ( w e. B /\ ( E. z w = ( y +Q z ) /\ ( y +Q x )
29 an12 
 |-  ( ( E. z w = ( y +Q z ) /\ ( w e. B /\ ( y +Q x )  ( w e. B /\ ( E. z w = ( y +Q z ) /\ ( y +Q x )
30 28 29 sylibr 
 |-  ( ( w e. B /\ ( y +Q x )  ( E. z w = ( y +Q z ) /\ ( w e. B /\ ( y +Q x )
31 19.41v 
 |-  ( E. z ( w = ( y +Q z ) /\ ( w e. B /\ ( y +Q x )  ( E. z w = ( y +Q z ) /\ ( w e. B /\ ( y +Q x )
32 30 31 sylibr 
 |-  ( ( w e. B /\ ( y +Q x )  E. z ( w = ( y +Q z ) /\ ( w e. B /\ ( y +Q x )
33 32 eximi 
 |-  ( E. w ( w e. B /\ ( y +Q x )  E. w E. z ( w = ( y +Q z ) /\ ( w e. B /\ ( y +Q x )
34 excom 
 |-  ( E. z E. w ( w = ( y +Q z ) /\ ( w e. B /\ ( y +Q x )  E. w E. z ( w = ( y +Q z ) /\ ( w e. B /\ ( y +Q x )
35 33 34 sylibr 
 |-  ( E. w ( w e. B /\ ( y +Q x )  E. z E. w ( w = ( y +Q z ) /\ ( w e. B /\ ( y +Q x )
36 ovex 
 |-  ( y +Q z ) e. _V
37 eleq1 
 |-  ( w = ( y +Q z ) -> ( w e. B <-> ( y +Q z ) e. B ) )
38 breq2 
 |-  ( w = ( y +Q z ) -> ( ( y +Q x )  ( y +Q x )
39 37 38 anbi12d 
 |-  ( w = ( y +Q z ) -> ( ( w e. B /\ ( y +Q x )  ( ( y +Q z ) e. B /\ ( y +Q x )
40 36 39 ceqsexv 
 |-  ( E. w ( w = ( y +Q z ) /\ ( w e. B /\ ( y +Q x )  ( ( y +Q z ) e. B /\ ( y +Q x )
41 ltanq 
 |-  ( y e. Q. -> ( x  ( y +Q x )
42 9 5 10 41 ndmovordi 
 |-  ( ( y +Q x )  x
43 42 anim2i 
 |-  ( ( ( y +Q z ) e. B /\ ( y +Q x )  ( ( y +Q z ) e. B /\ x
44 40 43 sylbi 
 |-  ( E. w ( w = ( y +Q z ) /\ ( w e. B /\ ( y +Q x )  ( ( y +Q z ) e. B /\ x
45 44 eximi 
 |-  ( E. z E. w ( w = ( y +Q z ) /\ ( w e. B /\ ( y +Q x )  E. z ( ( y +Q z ) e. B /\ x
46 4 35 45 3syl 
 |-  ( ( B e. P. /\ ( y +Q x ) e. B ) -> E. z ( ( y +Q z ) e. B /\ x
47 46 anim2i 
 |-  ( ( -. y e. A /\ ( B e. P. /\ ( y +Q x ) e. B ) ) -> ( -. y e. A /\ E. z ( ( y +Q z ) e. B /\ x
48 47 an12s 
 |-  ( ( B e. P. /\ ( -. y e. A /\ ( y +Q x ) e. B ) ) -> ( -. y e. A /\ E. z ( ( y +Q z ) e. B /\ x
49 19.42v 
 |-  ( E. z ( -. y e. A /\ ( ( y +Q z ) e. B /\ x  ( -. y e. A /\ E. z ( ( y +Q z ) e. B /\ x
50 48 49 sylibr 
 |-  ( ( B e. P. /\ ( -. y e. A /\ ( y +Q x ) e. B ) ) -> E. z ( -. y e. A /\ ( ( y +Q z ) e. B /\ x
51 50 ex 
 |-  ( B e. P. -> ( ( -. y e. A /\ ( y +Q x ) e. B ) -> E. z ( -. y e. A /\ ( ( y +Q z ) e. B /\ x
52 51 eximdv 
 |-  ( B e. P. -> ( E. y ( -. y e. A /\ ( y +Q x ) e. B ) -> E. y E. z ( -. y e. A /\ ( ( y +Q z ) e. B /\ x
53 1 eqabri 
 |-  ( x e. C <-> E. y ( -. y e. A /\ ( y +Q x ) e. B ) )
54 vex 
 |-  z e. _V
55 oveq2 
 |-  ( x = z -> ( y +Q x ) = ( y +Q z ) )
56 55 eleq1d 
 |-  ( x = z -> ( ( y +Q x ) e. B <-> ( y +Q z ) e. B ) )
57 56 anbi2d 
 |-  ( x = z -> ( ( -. y e. A /\ ( y +Q x ) e. B ) <-> ( -. y e. A /\ ( y +Q z ) e. B ) ) )
58 57 exbidv 
 |-  ( x = z -> ( E. y ( -. y e. A /\ ( y +Q x ) e. B ) <-> E. y ( -. y e. A /\ ( y +Q z ) e. B ) ) )
59 54 58 1 elab2 
 |-  ( z e. C <-> E. y ( -. y e. A /\ ( y +Q z ) e. B ) )
60 59 anbi1i 
 |-  ( ( z e. C /\ x  ( E. y ( -. y e. A /\ ( y +Q z ) e. B ) /\ x
61 19.41v 
 |-  ( E. y ( ( -. y e. A /\ ( y +Q z ) e. B ) /\ x  ( E. y ( -. y e. A /\ ( y +Q z ) e. B ) /\ x
62 anass 
 |-  ( ( ( -. y e. A /\ ( y +Q z ) e. B ) /\ x  ( -. y e. A /\ ( ( y +Q z ) e. B /\ x
63 62 exbii 
 |-  ( E. y ( ( -. y e. A /\ ( y +Q z ) e. B ) /\ x  E. y ( -. y e. A /\ ( ( y +Q z ) e. B /\ x
64 60 61 63 3bitr2i 
 |-  ( ( z e. C /\ x  E. y ( -. y e. A /\ ( ( y +Q z ) e. B /\ x
65 64 exbii 
 |-  ( E. z ( z e. C /\ x  E. z E. y ( -. y e. A /\ ( ( y +Q z ) e. B /\ x
66 excom 
 |-  ( E. y E. z ( -. y e. A /\ ( ( y +Q z ) e. B /\ x  E. z E. y ( -. y e. A /\ ( ( y +Q z ) e. B /\ x
67 65 66 bitr4i 
 |-  ( E. z ( z e. C /\ x  E. y E. z ( -. y e. A /\ ( ( y +Q z ) e. B /\ x
68 52 53 67 3imtr4g 
 |-  ( B e. P. -> ( x e. C -> E. z ( z e. C /\ x