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