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

Metamath Proof Explorer

Theorem lhpexle1lem

Description: Lemma for lhpexle1 and others that eliminates restrictions on X . (Contributed by NM, 24-Jul-2013)

Ref Expression
Hypotheses lhpexle1lem.1 
|- ( ph -> E. p e. A ( p .<_ W /\ ps ) )
lhpexle1lem.2 
|- ( ( ph /\ ( X e. A /\ X .<_ W ) ) -> E. p e. A ( p .<_ W /\ ps /\ p =/= X ) )
Assertion lhpexle1lem 
|- ( ph -> E. p e. A ( p .<_ W /\ ps /\ p =/= X ) )

Proof

Step Hyp Ref Expression
1 lhpexle1lem.1 
 |-  ( ph -> E. p e. A ( p .<_ W /\ ps ) )
2 lhpexle1lem.2 
 |-  ( ( ph /\ ( X e. A /\ X .<_ W ) ) -> E. p e. A ( p .<_ W /\ ps /\ p =/= X ) )
3 1 adantr 
 |-  ( ( ph /\ -. X e. A ) -> E. p e. A ( p .<_ W /\ ps ) )
4 simprl 
 |-  ( ( ( ( ph /\ -. X e. A ) /\ p e. A ) /\ ( p .<_ W /\ ps ) ) -> p .<_ W )
5 simprr 
 |-  ( ( ( ( ph /\ -. X e. A ) /\ p e. A ) /\ ( p .<_ W /\ ps ) ) -> ps )
6 simplr 
 |-  ( ( ( ( ph /\ -. X e. A ) /\ p e. A ) /\ ( p .<_ W /\ ps ) ) -> p e. A )
7 simpllr 
 |-  ( ( ( ( ph /\ -. X e. A ) /\ p e. A ) /\ ( p .<_ W /\ ps ) ) -> -. X e. A )
8 nelne2 
 |-  ( ( p e. A /\ -. X e. A ) -> p =/= X )
9 6 7 8 syl2anc 
 |-  ( ( ( ( ph /\ -. X e. A ) /\ p e. A ) /\ ( p .<_ W /\ ps ) ) -> p =/= X )
10 4 5 9 3jca 
 |-  ( ( ( ( ph /\ -. X e. A ) /\ p e. A ) /\ ( p .<_ W /\ ps ) ) -> ( p .<_ W /\ ps /\ p =/= X ) )
11 10 ex 
 |-  ( ( ( ph /\ -. X e. A ) /\ p e. A ) -> ( ( p .<_ W /\ ps ) -> ( p .<_ W /\ ps /\ p =/= X ) ) )
12 11 reximdva 
 |-  ( ( ph /\ -. X e. A ) -> ( E. p e. A ( p .<_ W /\ ps ) -> E. p e. A ( p .<_ W /\ ps /\ p =/= X ) ) )
13 3 12 mpd 
 |-  ( ( ph /\ -. X e. A ) -> E. p e. A ( p .<_ W /\ ps /\ p =/= X ) )
14 1 adantr 
 |-  ( ( ph /\ -. X .<_ W ) -> E. p e. A ( p .<_ W /\ ps ) )
15 simprl 
 |-  ( ( ( ph /\ -. X .<_ W ) /\ ( p .<_ W /\ ps ) ) -> p .<_ W )
16 simprr 
 |-  ( ( ( ph /\ -. X .<_ W ) /\ ( p .<_ W /\ ps ) ) -> ps )
17 simplr 
 |-  ( ( ( ph /\ -. X .<_ W ) /\ ( p .<_ W /\ ps ) ) -> -. X .<_ W )
18 nbrne2 
 |-  ( ( p .<_ W /\ -. X .<_ W ) -> p =/= X )
19 15 17 18 syl2anc 
 |-  ( ( ( ph /\ -. X .<_ W ) /\ ( p .<_ W /\ ps ) ) -> p =/= X )
20 15 16 19 3jca 
 |-  ( ( ( ph /\ -. X .<_ W ) /\ ( p .<_ W /\ ps ) ) -> ( p .<_ W /\ ps /\ p =/= X ) )
21 20 ex 
 |-  ( ( ph /\ -. X .<_ W ) -> ( ( p .<_ W /\ ps ) -> ( p .<_ W /\ ps /\ p =/= X ) ) )
22 21 reximdv 
 |-  ( ( ph /\ -. X .<_ W ) -> ( E. p e. A ( p .<_ W /\ ps ) -> E. p e. A ( p .<_ W /\ ps /\ p =/= X ) ) )
23 14 22 mpd 
 |-  ( ( ph /\ -. X .<_ W ) -> E. p e. A ( p .<_ W /\ ps /\ p =/= X ) )
24 13 23 2 pm2.61dda 
 |-  ( ph -> E. p e. A ( p .<_ W /\ ps /\ p =/= X ) )