Metamath Proof Explorer

Theorem kmlem13

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

Ref Expression
Hypothesis kmlem9.1 
|- A = { u | E. t e. x u = ( t \ U. ( x \ { t } ) ) }
Assertion kmlem13 
|- ( A. x ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> E. y A. z e. x E! v v e. ( z i^i y ) ) <-> A. x ( -. E. z e. x A. v e. z E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) -> E. y A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) )

Proof

Step Hyp Ref Expression
1 kmlem9.1 
 |-  A = { u | E. t e. x u = ( t \ U. ( x \ { t } ) ) }
2 kmlem1 
 |-  ( A. x ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> E. y A. z e. x E! v v e. ( z i^i y ) ) -> A. x ( A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) -> E. y A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) )
3 raleq 
 |-  ( x = h -> ( A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) <-> A. w e. h ( z =/= w -> ( z i^i w ) = (/) ) ) )
4 3 raleqbi1dv 
 |-  ( x = h -> ( A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) <-> A. z e. h A. w e. h ( z =/= w -> ( z i^i w ) = (/) ) ) )
5 raleq 
 |-  ( x = h -> ( A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) <-> A. z e. h ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) )
6 5 exbidv 
 |-  ( x = h -> ( E. y A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) <-> E. y A. z e. h ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) )
7 4 6 imbi12d 
 |-  ( x = h -> ( ( A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) -> E. y A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) <-> ( A. z e. h A. w e. h ( z =/= w -> ( z i^i w ) = (/) ) -> E. y A. z e. h ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) ) )
8 7 cbvalvw 
 |-  ( A. x ( A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) -> E. y A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) <-> A. h ( A. z e. h A. w e. h ( z =/= w -> ( z i^i w ) = (/) ) -> E. y A. z e. h ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) )
9 1 kmlem10 
 |-  ( A. h ( A. z e. h A. w e. h ( z =/= w -> ( z i^i w ) = (/) ) -> E. y A. z e. h ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) -> E. y A. z e. A ( z =/= (/) -> E! v v e. ( z i^i y ) ) )
10 ineq2 
 |-  ( y = g -> ( z i^i y ) = ( z i^i g ) )
11 10 eleq2d 
 |-  ( y = g -> ( v e. ( z i^i y ) <-> v e. ( z i^i g ) ) )
12 11 eubidv 
 |-  ( y = g -> ( E! v v e. ( z i^i y ) <-> E! v v e. ( z i^i g ) ) )
13 12 imbi2d 
 |-  ( y = g -> ( ( z =/= (/) -> E! v v e. ( z i^i y ) ) <-> ( z =/= (/) -> E! v v e. ( z i^i g ) ) ) )
14 13 ralbidv 
 |-  ( y = g -> ( A. z e. A ( z =/= (/) -> E! v v e. ( z i^i y ) ) <-> A. z e. A ( z =/= (/) -> E! v v e. ( z i^i g ) ) ) )
15 14 cbvexvw 
 |-  ( E. y A. z e. A ( z =/= (/) -> E! v v e. ( z i^i y ) ) <-> E. g A. z e. A ( z =/= (/) -> E! v v e. ( z i^i g ) ) )
16 kmlem3 
 |-  ( ( z \ U. ( x \ { z } ) ) =/= (/) <-> E. v e. z A. w e. x ( z =/= w -> -. v e. ( z i^i w ) ) )
17 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 ) ) )
18 17 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 ) ) )
19 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 ) ) )
20 16 18 19 3bitri 
 |-  ( ( z \ U. ( x \ { z } ) ) =/= (/) <-> -. A. v e. z E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) )
21 20 ralbii 
 |-  ( A. z e. x ( z \ U. ( x \ { z } ) ) =/= (/) <-> A. z e. x -. A. v e. z E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) )
22 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 ) ) )
23 21 22 bitri 
 |-  ( A. z e. x ( z \ U. ( x \ { z } ) ) =/= (/) <-> -. E. z e. x A. v e. z E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) )
24 1 kmlem12 
 |-  ( A. z e. x ( z \ U. ( x \ { z } ) ) =/= (/) -> ( A. z e. A ( z =/= (/) -> E! v v e. ( z i^i g ) ) -> A. z e. x ( z =/= (/) -> E! v v e. ( z i^i ( g i^i U. A ) ) ) ) )
25 vex 
 |-  g e. _V
26 25 inex1 
 |-  ( g i^i U. A ) e. _V
27 ineq2 
 |-  ( y = ( g i^i U. A ) -> ( z i^i y ) = ( z i^i ( g i^i U. A ) ) )
28 27 eleq2d 
 |-  ( y = ( g i^i U. A ) -> ( v e. ( z i^i y ) <-> v e. ( z i^i ( g i^i U. A ) ) ) )
29 28 eubidv 
 |-  ( y = ( g i^i U. A ) -> ( E! v v e. ( z i^i y ) <-> E! v v e. ( z i^i ( g i^i U. A ) ) ) )
30 29 imbi2d 
 |-  ( y = ( g i^i U. A ) -> ( ( z =/= (/) -> E! v v e. ( z i^i y ) ) <-> ( z =/= (/) -> E! v v e. ( z i^i ( g i^i U. A ) ) ) ) )
31 30 ralbidv 
 |-  ( y = ( g i^i U. A ) -> ( A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) <-> A. z e. x ( z =/= (/) -> E! v v e. ( z i^i ( g i^i U. A ) ) ) ) )
32 26 31 spcev 
 |-  ( A. z e. x ( z =/= (/) -> E! v v e. ( z i^i ( g i^i U. A ) ) ) -> E. y A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) )
33 24 32 syl6 
 |-  ( A. z e. x ( z \ U. ( x \ { z } ) ) =/= (/) -> ( A. z e. A ( z =/= (/) -> E! v v e. ( z i^i g ) ) -> E. y A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) )
34 33 exlimdv 
 |-  ( A. z e. x ( z \ U. ( x \ { z } ) ) =/= (/) -> ( E. g A. z e. A ( z =/= (/) -> E! v v e. ( z i^i g ) ) -> E. y A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) )
35 34 com12 
 |-  ( E. g A. z e. A ( z =/= (/) -> E! v v e. ( z i^i g ) ) -> ( A. z e. x ( z \ U. ( x \ { z } ) ) =/= (/) -> E. y A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) )
36 23 35 syl5bir 
 |-  ( E. g A. z e. A ( z =/= (/) -> E! v v e. ( z i^i g ) ) -> ( -. E. z e. x A. v e. z E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) -> E. y A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) )
37 15 36 sylbi 
 |-  ( E. y A. z e. A ( z =/= (/) -> E! v v e. ( z i^i y ) ) -> ( -. E. z e. x A. v e. z E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) -> E. y A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) )
38 9 37 syl 
 |-  ( A. h ( A. z e. h A. w e. h ( z =/= w -> ( z i^i w ) = (/) ) -> E. y A. z e. h ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) -> ( -. E. z e. x A. v e. z E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) -> E. y A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) )
39 38 alrimiv 
 |-  ( A. h ( A. z e. h A. w e. h ( z =/= w -> ( z i^i w ) = (/) ) -> E. y A. z e. h ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) -> A. x ( -. E. z e. x A. v e. z E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) -> E. y A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) )
40 8 39 sylbi 
 |-  ( A. x ( A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) -> E. y A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) -> A. x ( -. E. z e. x A. v e. z E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) -> E. y A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) )
41 2 40 syl 
 |-  ( A. x ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> E. y A. z e. x E! v v e. ( z i^i y ) ) -> A. x ( -. E. z e. x A. v e. z E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) -> E. y A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) )
42 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 ) ) )
43 42 imim1i 
 |-  ( ( -. E. z e. x A. v e. z E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) -> E. y A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) -> ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> E. y A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) )
44 biimt 
 |-  ( z =/= (/) -> ( E! v v e. ( z i^i y ) <-> ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) )
45 44 ralimi 
 |-  ( A. z e. x z =/= (/) -> A. z e. x ( E! v v e. ( z i^i y ) <-> ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) )
46 ralbi 
 |-  ( A. z e. x ( E! v v e. ( z i^i y ) <-> ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) -> ( A. z e. x E! v v e. ( z i^i y ) <-> A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) )
47 45 46 syl 
 |-  ( A. z e. x z =/= (/) -> ( A. z e. x E! v v e. ( z i^i y ) <-> A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) )
48 47 exbidv 
 |-  ( A. z e. x z =/= (/) -> ( E. y A. z e. x E! v v e. ( z i^i y ) <-> E. y A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) )
49 48 adantr 
 |-  ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> ( E. y A. z e. x E! v v e. ( z i^i y ) <-> E. y A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) )
50 49 pm5.74i 
 |-  ( ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> E. y A. z e. x E! v v e. ( z i^i y ) ) <-> ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> E. y A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) )
51 43 50 sylibr 
 |-  ( ( -. E. z e. x A. v e. z E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) -> E. y A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) -> ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> E. y A. z e. x E! v v e. ( z i^i y ) ) )
52 51 alimi 
 |-  ( A. x ( -. E. z e. x A. v e. z E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) -> E. y A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) -> A. x ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> E. y A. z e. x E! v v e. ( z i^i y ) ) )
53 41 52 impbii 
 |-  ( A. x ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> E. y A. z e. x E! v v e. ( z i^i y ) ) <-> A. x ( -. E. z e. x A. v e. z E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) -> E. y A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) )