Metamath Proof Explorer

Theorem kmlem2

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

Ref Expression
Assertion kmlem2 
|- ( E. y A. z e. x ( ph -> E! w w e. ( z i^i y ) ) <-> E. y ( -. y e. x /\ A. z e. x ( ph -> E! w w e. ( z i^i y ) ) ) )

Proof

Step Hyp Ref Expression
1 ineq2 
 |-  ( y = v -> ( z i^i y ) = ( z i^i v ) )
2 1 eleq2d 
 |-  ( y = v -> ( w e. ( z i^i y ) <-> w e. ( z i^i v ) ) )
3 2 eubidv 
 |-  ( y = v -> ( E! w w e. ( z i^i y ) <-> E! w w e. ( z i^i v ) ) )
4 3 imbi2d 
 |-  ( y = v -> ( ( ph -> E! w w e. ( z i^i y ) ) <-> ( ph -> E! w w e. ( z i^i v ) ) ) )
5 4 ralbidv 
 |-  ( y = v -> ( A. z e. x ( ph -> E! w w e. ( z i^i y ) ) <-> A. z e. x ( ph -> E! w w e. ( z i^i v ) ) ) )
6 5 cbvexvw 
 |-  ( E. y A. z e. x ( ph -> E! w w e. ( z i^i y ) ) <-> E. v A. z e. x ( ph -> E! w w e. ( z i^i v ) ) )
7 indi 
 |-  ( z i^i ( v u. { u } ) ) = ( ( z i^i v ) u. ( z i^i { u } ) )
8 elssuni 
 |-  ( z e. x -> z C_ U. x )
9 8 ssneld 
 |-  ( z e. x -> ( -. u e. U. x -> -. u e. z ) )
10 disjsn 
 |-  ( ( z i^i { u } ) = (/) <-> -. u e. z )
11 9 10 syl6ibr 
 |-  ( z e. x -> ( -. u e. U. x -> ( z i^i { u } ) = (/) ) )
12 11 impcom 
 |-  ( ( -. u e. U. x /\ z e. x ) -> ( z i^i { u } ) = (/) )
13 12 uneq2d 
 |-  ( ( -. u e. U. x /\ z e. x ) -> ( ( z i^i v ) u. ( z i^i { u } ) ) = ( ( z i^i v ) u. (/) ) )
14 un0 
 |-  ( ( z i^i v ) u. (/) ) = ( z i^i v )
15 13 14 eqtrdi 
 |-  ( ( -. u e. U. x /\ z e. x ) -> ( ( z i^i v ) u. ( z i^i { u } ) ) = ( z i^i v ) )
16 7 15 eqtr2id 
 |-  ( ( -. u e. U. x /\ z e. x ) -> ( z i^i v ) = ( z i^i ( v u. { u } ) ) )
17 16 eleq2d 
 |-  ( ( -. u e. U. x /\ z e. x ) -> ( w e. ( z i^i v ) <-> w e. ( z i^i ( v u. { u } ) ) ) )
18 17 eubidv 
 |-  ( ( -. u e. U. x /\ z e. x ) -> ( E! w w e. ( z i^i v ) <-> E! w w e. ( z i^i ( v u. { u } ) ) ) )
19 18 imbi2d 
 |-  ( ( -. u e. U. x /\ z e. x ) -> ( ( ph -> E! w w e. ( z i^i v ) ) <-> ( ph -> E! w w e. ( z i^i ( v u. { u } ) ) ) ) )
20 19 ralbidva 
 |-  ( -. u e. U. x -> ( A. z e. x ( ph -> E! w w e. ( z i^i v ) ) <-> A. z e. x ( ph -> E! w w e. ( z i^i ( v u. { u } ) ) ) ) )
21 vsnid 
 |-  u e. { u }
22 21 olci 
 |-  ( u e. v \/ u e. { u } )
23 elun 
 |-  ( u e. ( v u. { u } ) <-> ( u e. v \/ u e. { u } ) )
24 22 23 mpbir 
 |-  u e. ( v u. { u } )
25 elssuni 
 |-  ( ( v u. { u } ) e. x -> ( v u. { u } ) C_ U. x )
26 25 sseld 
 |-  ( ( v u. { u } ) e. x -> ( u e. ( v u. { u } ) -> u e. U. x ) )
27 24 26 mpi 
 |-  ( ( v u. { u } ) e. x -> u e. U. x )
28 27 con3i 
 |-  ( -. u e. U. x -> -. ( v u. { u } ) e. x )
29 28 biantrurd 
 |-  ( -. u e. U. x -> ( A. z e. x ( ph -> E! w w e. ( z i^i ( v u. { u } ) ) ) <-> ( -. ( v u. { u } ) e. x /\ A. z e. x ( ph -> E! w w e. ( z i^i ( v u. { u } ) ) ) ) ) )
30 20 29 bitrd 
 |-  ( -. u e. U. x -> ( A. z e. x ( ph -> E! w w e. ( z i^i v ) ) <-> ( -. ( v u. { u } ) e. x /\ A. z e. x ( ph -> E! w w e. ( z i^i ( v u. { u } ) ) ) ) ) )
31 vex 
 |-  v e. _V
32 snex 
 |-  { u } e. _V
33 31 32 unex 
 |-  ( v u. { u } ) e. _V
34 eleq1 
 |-  ( y = ( v u. { u } ) -> ( y e. x <-> ( v u. { u } ) e. x ) )
35 34 notbid 
 |-  ( y = ( v u. { u } ) -> ( -. y e. x <-> -. ( v u. { u } ) e. x ) )
36 ineq2 
 |-  ( y = ( v u. { u } ) -> ( z i^i y ) = ( z i^i ( v u. { u } ) ) )
37 36 eleq2d 
 |-  ( y = ( v u. { u } ) -> ( w e. ( z i^i y ) <-> w e. ( z i^i ( v u. { u } ) ) ) )
38 37 eubidv 
 |-  ( y = ( v u. { u } ) -> ( E! w w e. ( z i^i y ) <-> E! w w e. ( z i^i ( v u. { u } ) ) ) )
39 38 imbi2d 
 |-  ( y = ( v u. { u } ) -> ( ( ph -> E! w w e. ( z i^i y ) ) <-> ( ph -> E! w w e. ( z i^i ( v u. { u } ) ) ) ) )
40 39 ralbidv 
 |-  ( y = ( v u. { u } ) -> ( A. z e. x ( ph -> E! w w e. ( z i^i y ) ) <-> A. z e. x ( ph -> E! w w e. ( z i^i ( v u. { u } ) ) ) ) )
41 35 40 anbi12d 
 |-  ( y = ( v u. { u } ) -> ( ( -. y e. x /\ A. z e. x ( ph -> E! w w e. ( z i^i y ) ) ) <-> ( -. ( v u. { u } ) e. x /\ A. z e. x ( ph -> E! w w e. ( z i^i ( v u. { u } ) ) ) ) ) )
42 33 41 spcev 
 |-  ( ( -. ( v u. { u } ) e. x /\ A. z e. x ( ph -> E! w w e. ( z i^i ( v u. { u } ) ) ) ) -> E. y ( -. y e. x /\ A. z e. x ( ph -> E! w w e. ( z i^i y ) ) ) )
43 30 42 syl6bi 
 |-  ( -. u e. U. x -> ( A. z e. x ( ph -> E! w w e. ( z i^i v ) ) -> E. y ( -. y e. x /\ A. z e. x ( ph -> E! w w e. ( z i^i y ) ) ) ) )
44 vuniex 
 |-  U. x e. _V
45 eleq2 
 |-  ( y = U. x -> ( u e. y <-> u e. U. x ) )
46 45 notbid 
 |-  ( y = U. x -> ( -. u e. y <-> -. u e. U. x ) )
47 46 exbidv 
 |-  ( y = U. x -> ( E. u -. u e. y <-> E. u -. u e. U. x ) )
48 nalset 
 |-  -. E. y A. u u e. y
49 alexn 
 |-  ( A. y E. u -. u e. y <-> -. E. y A. u u e. y )
50 48 49 mpbir 
 |-  A. y E. u -. u e. y
51 50 spi 
 |-  E. u -. u e. y
52 44 47 51 vtocl 
 |-  E. u -. u e. U. x
53 43 52 exlimiiv 
 |-  ( A. z e. x ( ph -> E! w w e. ( z i^i v ) ) -> E. y ( -. y e. x /\ A. z e. x ( ph -> E! w w e. ( z i^i y ) ) ) )
54 53 exlimiv 
 |-  ( E. v A. z e. x ( ph -> E! w w e. ( z i^i v ) ) -> E. y ( -. y e. x /\ A. z e. x ( ph -> E! w w e. ( z i^i y ) ) ) )
55 6 54 sylbi 
 |-  ( E. y A. z e. x ( ph -> E! w w e. ( z i^i y ) ) -> E. y ( -. y e. x /\ A. z e. x ( ph -> E! w w e. ( z i^i y ) ) ) )
56 exsimpr 
 |-  ( E. y ( -. y e. x /\ A. z e. x ( ph -> E! w w e. ( z i^i y ) ) ) -> E. y A. z e. x ( ph -> E! w w e. ( z i^i y ) ) )
57 55 56 impbii 
 |-  ( E. y A. z e. x ( ph -> E! w w e. ( z i^i y ) ) <-> E. y ( -. y e. x /\ A. z e. x ( ph -> E! w w e. ( z i^i y ) ) ) )