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

Metamath Proof Explorer

Theorem kmlem6

Description: Lemma for 5-quantifier AC of Kurt Maes, Th. 4, part of 4 => 1. (Contributed by NM, 26-Mar-2004)

Ref Expression
Assertion kmlem6 
|- ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( ph -> A = (/) ) ) -> A. z e. x E. v e. z A. w e. x ( ph -> -. v e. A ) )

Proof

Step Hyp Ref Expression
1 r19.26 
 |-  ( A. z e. x ( z =/= (/) /\ A. w e. x ( ph -> A = (/) ) ) <-> ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( ph -> A = (/) ) ) )
2 n0 
 |-  ( z =/= (/) <-> E. v v e. z )
3 2 biimpi 
 |-  ( z =/= (/) -> E. v v e. z )
4 ne0i 
 |-  ( v e. A -> A =/= (/) )
5 4 necon2bi 
 |-  ( A = (/) -> -. v e. A )
6 5 imim2i 
 |-  ( ( ph -> A = (/) ) -> ( ph -> -. v e. A ) )
7 6 ralimi 
 |-  ( A. w e. x ( ph -> A = (/) ) -> A. w e. x ( ph -> -. v e. A ) )
8 7 alrimiv 
 |-  ( A. w e. x ( ph -> A = (/) ) -> A. v A. w e. x ( ph -> -. v e. A ) )
9 19.29r 
 |-  ( ( E. v v e. z /\ A. v A. w e. x ( ph -> -. v e. A ) ) -> E. v ( v e. z /\ A. w e. x ( ph -> -. v e. A ) ) )
10 df-rex 
 |-  ( E. v e. z A. w e. x ( ph -> -. v e. A ) <-> E. v ( v e. z /\ A. w e. x ( ph -> -. v e. A ) ) )
11 9 10 sylibr 
 |-  ( ( E. v v e. z /\ A. v A. w e. x ( ph -> -. v e. A ) ) -> E. v e. z A. w e. x ( ph -> -. v e. A ) )
12 3 8 11 syl2an 
 |-  ( ( z =/= (/) /\ A. w e. x ( ph -> A = (/) ) ) -> E. v e. z A. w e. x ( ph -> -. v e. A ) )
13 12 ralimi 
 |-  ( A. z e. x ( z =/= (/) /\ A. w e. x ( ph -> A = (/) ) ) -> A. z e. x E. v e. z A. w e. x ( ph -> -. v e. A ) )
14 1 13 sylbir 
 |-  ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( ph -> A = (/) ) ) -> A. z e. x E. v e. z A. w e. x ( ph -> -. v e. A ) )