Metamath Proof Explorer

Theorem ltexprlem1

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 ltexprlem1 
|- ( B e. P. -> ( A C. B -> C =/= (/) ) )

Proof

Step Hyp Ref Expression
1 ltexprlem.1 
 |-  C = { x | E. y ( -. y e. A /\ ( y +Q x ) e. B ) }
2 pssnel 
 |-  ( A C. B -> E. y ( y e. B /\ -. y e. A ) )
3 prnmadd 
 |-  ( ( B e. P. /\ y e. B ) -> E. x ( y +Q x ) e. B )
4 3 anim2i 
 |-  ( ( -. y e. A /\ ( B e. P. /\ y e. B ) ) -> ( -. y e. A /\ E. x ( y +Q x ) e. B ) )
5 19.42v 
 |-  ( E. x ( -. y e. A /\ ( y +Q x ) e. B ) <-> ( -. y e. A /\ E. x ( y +Q x ) e. B ) )
6 4 5 sylibr 
 |-  ( ( -. y e. A /\ ( B e. P. /\ y e. B ) ) -> E. x ( -. y e. A /\ ( y +Q x ) e. B ) )
7 6 exp32 
 |-  ( -. y e. A -> ( B e. P. -> ( y e. B -> E. x ( -. y e. A /\ ( y +Q x ) e. B ) ) ) )
8 7 com3l 
 |-  ( B e. P. -> ( y e. B -> ( -. y e. A -> E. x ( -. y e. A /\ ( y +Q x ) e. B ) ) ) )
9 8 impd 
 |-  ( B e. P. -> ( ( y e. B /\ -. y e. A ) -> E. x ( -. y e. A /\ ( y +Q x ) e. B ) ) )
10 9 eximdv 
 |-  ( B e. P. -> ( E. y ( y e. B /\ -. y e. A ) -> E. y E. x ( -. y e. A /\ ( y +Q x ) e. B ) ) )
11 2 10 syl5 
 |-  ( B e. P. -> ( A C. B -> E. y E. x ( -. y e. A /\ ( y +Q x ) e. B ) ) )
12 1 eqabri 
 |-  ( x e. C <-> E. y ( -. y e. A /\ ( y +Q x ) e. B ) )
13 12 exbii 
 |-  ( E. x x e. C <-> E. x E. y ( -. y e. A /\ ( y +Q x ) e. B ) )
14 n0 
 |-  ( C =/= (/) <-> E. x x e. C )
15 excom 
 |-  ( E. y E. x ( -. y e. A /\ ( y +Q x ) e. B ) <-> E. x E. y ( -. y e. A /\ ( y +Q x ) e. B ) )
16 13 14 15 3bitr4i 
 |-  ( C =/= (/) <-> E. y E. x ( -. y e. A /\ ( y +Q x ) e. B ) )
17 11 16 imbitrrdi 
 |-  ( B e. P. -> ( A C. B -> C =/= (/) ) )