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

Metamath Proof Explorer

Theorem kmlem8

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

Ref Expression
Assertion kmlem8 
|- ( ( -. E. z e. u A. w e. z ps -> E. y A. z e. u ( z =/= (/) -> E! w w e. ( z i^i y ) ) ) <-> ( E. z e. u A. w e. z ps \/ E. y ( -. y e. u /\ A. z e. u E! w w e. ( z i^i y ) ) ) )

Proof

Step Hyp Ref Expression
1 ralnex 
 |-  ( A. z e. u -. A. w e. z ps <-> -. E. z e. u A. w e. z ps )
2 df-rex 
 |-  ( E. w e. z -. ps <-> E. w ( w e. z /\ -. ps ) )
3 rexnal 
 |-  ( E. w e. z -. ps <-> -. A. w e. z ps )
4 2 3 bitr3i 
 |-  ( E. w ( w e. z /\ -. ps ) <-> -. A. w e. z ps )
5 exsimpl 
 |-  ( E. w ( w e. z /\ -. ps ) -> E. w w e. z )
6 n0 
 |-  ( z =/= (/) <-> E. w w e. z )
7 5 6 sylibr 
 |-  ( E. w ( w e. z /\ -. ps ) -> z =/= (/) )
8 4 7 sylbir 
 |-  ( -. A. w e. z ps -> z =/= (/) )
9 8 ralimi 
 |-  ( A. z e. u -. A. w e. z ps -> A. z e. u z =/= (/) )
10 1 9 sylbir 
 |-  ( -. E. z e. u A. w e. z ps -> A. z e. u z =/= (/) )
11 kmlem2 
 |-  ( E. y A. z e. u ( z =/= (/) -> E! w w e. ( z i^i y ) ) <-> E. y ( -. y e. u /\ A. z e. u ( z =/= (/) -> E! w w e. ( z i^i y ) ) ) )
12 biimt 
 |-  ( z =/= (/) -> ( E! w w e. ( z i^i y ) <-> ( z =/= (/) -> E! w w e. ( z i^i y ) ) ) )
13 12 ralimi 
 |-  ( A. z e. u z =/= (/) -> A. z e. u ( E! w w e. ( z i^i y ) <-> ( z =/= (/) -> E! w w e. ( z i^i y ) ) ) )
14 ralbi 
 |-  ( A. z e. u ( E! w w e. ( z i^i y ) <-> ( z =/= (/) -> E! w w e. ( z i^i y ) ) ) -> ( A. z e. u E! w w e. ( z i^i y ) <-> A. z e. u ( z =/= (/) -> E! w w e. ( z i^i y ) ) ) )
15 13 14 syl 
 |-  ( A. z e. u z =/= (/) -> ( A. z e. u E! w w e. ( z i^i y ) <-> A. z e. u ( z =/= (/) -> E! w w e. ( z i^i y ) ) ) )
16 15 anbi2d 
 |-  ( A. z e. u z =/= (/) -> ( ( -. y e. u /\ A. z e. u E! w w e. ( z i^i y ) ) <-> ( -. y e. u /\ A. z e. u ( z =/= (/) -> E! w w e. ( z i^i y ) ) ) ) )
17 16 exbidv 
 |-  ( A. z e. u z =/= (/) -> ( E. y ( -. y e. u /\ A. z e. u E! w w e. ( z i^i y ) ) <-> E. y ( -. y e. u /\ A. z e. u ( z =/= (/) -> E! w w e. ( z i^i y ) ) ) ) )
18 11 17 bitr4id 
 |-  ( A. z e. u z =/= (/) -> ( E. y A. z e. u ( z =/= (/) -> E! w w e. ( z i^i y ) ) <-> E. y ( -. y e. u /\ A. z e. u E! w w e. ( z i^i y ) ) ) )
19 10 18 syl 
 |-  ( -. E. z e. u A. w e. z ps -> ( E. y A. z e. u ( z =/= (/) -> E! w w e. ( z i^i y ) ) <-> E. y ( -. y e. u /\ A. z e. u E! w w e. ( z i^i y ) ) ) )
20 19 pm5.74i 
 |-  ( ( -. E. z e. u A. w e. z ps -> E. y A. z e. u ( z =/= (/) -> E! w w e. ( z i^i y ) ) ) <-> ( -. E. z e. u A. w e. z ps -> E. y ( -. y e. u /\ A. z e. u E! w w e. ( z i^i y ) ) ) )
21 pm4.64 
 |-  ( ( -. E. z e. u A. w e. z ps -> E. y ( -. y e. u /\ A. z e. u E! w w e. ( z i^i y ) ) ) <-> ( E. z e. u A. w e. z ps \/ E. y ( -. y e. u /\ A. z e. u E! w w e. ( z i^i y ) ) ) )
22 20 21 bitri 
 |-  ( ( -. E. z e. u A. w e. z ps -> E. y A. z e. u ( z =/= (/) -> E! w w e. ( z i^i y ) ) ) <-> ( E. z e. u A. w e. z ps \/ E. y ( -. y e. u /\ A. z e. u E! w w e. ( z i^i y ) ) ) )