Metamath Proof Explorer

Theorem kmlem7

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

Ref Expression
Assertion kmlem7 
|- ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> -. E. z e. x A. v e. z E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) )

Proof

Step Hyp Ref Expression
1 kmlem6 
 |-  ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> A. z e. x E. v e. z A. w e. x ( z =/= w -> -. v e. ( z i^i w ) ) )
2 ralinexa 
 |-  ( A. w e. x ( z =/= w -> -. v e. ( z i^i w ) ) <-> -. E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) )
3 2 rexbii 
 |-  ( E. v e. z A. w e. x ( z =/= w -> -. v e. ( z i^i w ) ) <-> E. v e. z -. E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) )
4 rexnal 
 |-  ( E. v e. z -. E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) <-> -. A. v e. z E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) )
5 3 4 bitri 
 |-  ( E. v e. z A. w e. x ( z =/= w -> -. v e. ( z i^i w ) ) <-> -. A. v e. z E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) )
6 5 ralbii 
 |-  ( A. z e. x E. v e. z A. w e. x ( z =/= w -> -. v e. ( z i^i w ) ) <-> A. z e. x -. A. v e. z E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) )
7 ralnex 
 |-  ( A. z e. x -. A. v e. z E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) <-> -. E. z e. x A. v e. z E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) )
8 6 7 bitri 
 |-  ( A. z e. x E. v e. z A. w e. x ( z =/= w -> -. v e. ( z i^i w ) ) <-> -. E. z e. x A. v e. z E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) )
9 1 8 sylib 
 |-  ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> -. E. z e. x A. v e. z E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) )