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 ) ) ) )