Metamath Proof Explorer


Theorem kmlem12

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

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

Proof

Step Hyp Ref Expression
1 kmlem9.1
 |-  A = { u | E. t e. x u = ( t \ U. ( x \ { t } ) ) }
2 difeq1
 |-  ( t = z -> ( t \ U. ( x \ { t } ) ) = ( z \ U. ( x \ { t } ) ) )
3 sneq
 |-  ( t = z -> { t } = { z } )
4 3 difeq2d
 |-  ( t = z -> ( x \ { t } ) = ( x \ { z } ) )
5 4 unieqd
 |-  ( t = z -> U. ( x \ { t } ) = U. ( x \ { z } ) )
6 5 difeq2d
 |-  ( t = z -> ( z \ U. ( x \ { t } ) ) = ( z \ U. ( x \ { z } ) ) )
7 2 6 eqtrd
 |-  ( t = z -> ( t \ U. ( x \ { t } ) ) = ( z \ U. ( x \ { z } ) ) )
8 7 neeq1d
 |-  ( t = z -> ( ( t \ U. ( x \ { t } ) ) =/= (/) <-> ( z \ U. ( x \ { z } ) ) =/= (/) ) )
9 8 cbvralvw
 |-  ( A. t e. x ( t \ U. ( x \ { t } ) ) =/= (/) <-> A. z e. x ( z \ U. ( x \ { z } ) ) =/= (/) )
10 7 ineq1d
 |-  ( t = z -> ( ( t \ U. ( x \ { t } ) ) i^i y ) = ( ( z \ U. ( x \ { z } ) ) i^i y ) )
11 10 eleq2d
 |-  ( t = z -> ( v e. ( ( t \ U. ( x \ { t } ) ) i^i y ) <-> v e. ( ( z \ U. ( x \ { z } ) ) i^i y ) ) )
12 11 eubidv
 |-  ( t = z -> ( E! v v e. ( ( t \ U. ( x \ { t } ) ) i^i y ) <-> E! v v e. ( ( z \ U. ( x \ { z } ) ) i^i y ) ) )
13 12 cbvralvw
 |-  ( A. t e. x E! v v e. ( ( t \ U. ( x \ { t } ) ) i^i y ) <-> A. z e. x E! v v e. ( ( z \ U. ( x \ { z } ) ) i^i y ) )
14 9 13 imbi12i
 |-  ( ( A. t e. x ( t \ U. ( x \ { t } ) ) =/= (/) -> A. t e. x E! v v e. ( ( t \ U. ( x \ { t } ) ) i^i y ) ) <-> ( A. z e. x ( z \ U. ( x \ { z } ) ) =/= (/) -> A. z e. x E! v v e. ( ( z \ U. ( x \ { z } ) ) i^i y ) ) )
15 in12
 |-  ( z i^i ( y i^i U. A ) ) = ( y i^i ( z i^i U. A ) )
16 incom
 |-  ( y i^i ( z i^i U. A ) ) = ( ( z i^i U. A ) i^i y )
17 15 16 eqtri
 |-  ( z i^i ( y i^i U. A ) ) = ( ( z i^i U. A ) i^i y )
18 1 kmlem11
 |-  ( z e. x -> ( z i^i U. A ) = ( z \ U. ( x \ { z } ) ) )
19 18 ineq1d
 |-  ( z e. x -> ( ( z i^i U. A ) i^i y ) = ( ( z \ U. ( x \ { z } ) ) i^i y ) )
20 17 19 eqtr2id
 |-  ( z e. x -> ( ( z \ U. ( x \ { z } ) ) i^i y ) = ( z i^i ( y i^i U. A ) ) )
21 20 eleq2d
 |-  ( z e. x -> ( v e. ( ( z \ U. ( x \ { z } ) ) i^i y ) <-> v e. ( z i^i ( y i^i U. A ) ) ) )
22 21 eubidv
 |-  ( z e. x -> ( E! v v e. ( ( z \ U. ( x \ { z } ) ) i^i y ) <-> E! v v e. ( z i^i ( y i^i U. A ) ) ) )
23 ax-1
 |-  ( E! v v e. ( z i^i ( y i^i U. A ) ) -> ( z =/= (/) -> E! v v e. ( z i^i ( y i^i U. A ) ) ) )
24 22 23 syl6bi
 |-  ( z e. x -> ( E! v v e. ( ( z \ U. ( x \ { z } ) ) i^i y ) -> ( z =/= (/) -> E! v v e. ( z i^i ( y i^i U. A ) ) ) ) )
25 24 ralimia
 |-  ( A. z e. x E! v v e. ( ( z \ U. ( x \ { z } ) ) i^i y ) -> A. z e. x ( z =/= (/) -> E! v v e. ( z i^i ( y i^i U. A ) ) ) )
26 25 imim2i
 |-  ( ( A. z e. x ( z \ U. ( x \ { z } ) ) =/= (/) -> A. z e. x E! v v e. ( ( z \ U. ( x \ { z } ) ) i^i y ) ) -> ( A. z e. x ( z \ U. ( x \ { z } ) ) =/= (/) -> A. z e. x ( z =/= (/) -> E! v v e. ( z i^i ( y i^i U. A ) ) ) ) )
27 14 26 sylbi
 |-  ( ( A. t e. x ( t \ U. ( x \ { t } ) ) =/= (/) -> A. t e. x E! v v e. ( ( t \ U. ( x \ { t } ) ) i^i y ) ) -> ( A. z e. x ( z \ U. ( x \ { z } ) ) =/= (/) -> A. z e. x ( z =/= (/) -> E! v v e. ( z i^i ( y i^i U. A ) ) ) ) )
28 1 raleqi
 |-  ( A. z e. A ( z =/= (/) -> E! v v e. ( z i^i y ) ) <-> A. z e. { u | E. t e. x u = ( t \ U. ( x \ { t } ) ) } ( z =/= (/) -> E! v v e. ( z i^i y ) ) )
29 df-ral
 |-  ( A. z e. { u | E. t e. x u = ( t \ U. ( x \ { t } ) ) } ( z =/= (/) -> E! v v e. ( z i^i y ) ) <-> A. z ( z e. { u | E. t e. x u = ( t \ U. ( x \ { t } ) ) } -> ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) )
30 vex
 |-  z e. _V
31 eqeq1
 |-  ( u = z -> ( u = ( t \ U. ( x \ { t } ) ) <-> z = ( t \ U. ( x \ { t } ) ) ) )
32 31 rexbidv
 |-  ( u = z -> ( E. t e. x u = ( t \ U. ( x \ { t } ) ) <-> E. t e. x z = ( t \ U. ( x \ { t } ) ) ) )
33 30 32 elab
 |-  ( z e. { u | E. t e. x u = ( t \ U. ( x \ { t } ) ) } <-> E. t e. x z = ( t \ U. ( x \ { t } ) ) )
34 33 imbi1i
 |-  ( ( z e. { u | E. t e. x u = ( t \ U. ( x \ { t } ) ) } -> ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) <-> ( E. t e. x z = ( t \ U. ( x \ { t } ) ) -> ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) )
35 r19.23v
 |-  ( A. t e. x ( z = ( t \ U. ( x \ { t } ) ) -> ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) <-> ( E. t e. x z = ( t \ U. ( x \ { t } ) ) -> ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) )
36 34 35 bitr4i
 |-  ( ( z e. { u | E. t e. x u = ( t \ U. ( x \ { t } ) ) } -> ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) <-> A. t e. x ( z = ( t \ U. ( x \ { t } ) ) -> ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) )
37 36 albii
 |-  ( A. z ( z e. { u | E. t e. x u = ( t \ U. ( x \ { t } ) ) } -> ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) <-> A. z A. t e. x ( z = ( t \ U. ( x \ { t } ) ) -> ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) )
38 ralcom4
 |-  ( A. t e. x A. z ( z = ( t \ U. ( x \ { t } ) ) -> ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) <-> A. z A. t e. x ( z = ( t \ U. ( x \ { t } ) ) -> ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) )
39 vex
 |-  t e. _V
40 39 difexi
 |-  ( t \ U. ( x \ { t } ) ) e. _V
41 neeq1
 |-  ( z = ( t \ U. ( x \ { t } ) ) -> ( z =/= (/) <-> ( t \ U. ( x \ { t } ) ) =/= (/) ) )
42 ineq1
 |-  ( z = ( t \ U. ( x \ { t } ) ) -> ( z i^i y ) = ( ( t \ U. ( x \ { t } ) ) i^i y ) )
43 42 eleq2d
 |-  ( z = ( t \ U. ( x \ { t } ) ) -> ( v e. ( z i^i y ) <-> v e. ( ( t \ U. ( x \ { t } ) ) i^i y ) ) )
44 43 eubidv
 |-  ( z = ( t \ U. ( x \ { t } ) ) -> ( E! v v e. ( z i^i y ) <-> E! v v e. ( ( t \ U. ( x \ { t } ) ) i^i y ) ) )
45 41 44 imbi12d
 |-  ( z = ( t \ U. ( x \ { t } ) ) -> ( ( z =/= (/) -> E! v v e. ( z i^i y ) ) <-> ( ( t \ U. ( x \ { t } ) ) =/= (/) -> E! v v e. ( ( t \ U. ( x \ { t } ) ) i^i y ) ) ) )
46 40 45 ceqsalv
 |-  ( A. z ( z = ( t \ U. ( x \ { t } ) ) -> ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) <-> ( ( t \ U. ( x \ { t } ) ) =/= (/) -> E! v v e. ( ( t \ U. ( x \ { t } ) ) i^i y ) ) )
47 46 ralbii
 |-  ( A. t e. x A. z ( z = ( t \ U. ( x \ { t } ) ) -> ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) <-> A. t e. x ( ( t \ U. ( x \ { t } ) ) =/= (/) -> E! v v e. ( ( t \ U. ( x \ { t } ) ) i^i y ) ) )
48 37 38 47 3bitr2i
 |-  ( A. z ( z e. { u | E. t e. x u = ( t \ U. ( x \ { t } ) ) } -> ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) <-> A. t e. x ( ( t \ U. ( x \ { t } ) ) =/= (/) -> E! v v e. ( ( t \ U. ( x \ { t } ) ) i^i y ) ) )
49 28 29 48 3bitri
 |-  ( A. z e. A ( z =/= (/) -> E! v v e. ( z i^i y ) ) <-> A. t e. x ( ( t \ U. ( x \ { t } ) ) =/= (/) -> E! v v e. ( ( t \ U. ( x \ { t } ) ) i^i y ) ) )
50 ralim
 |-  ( A. t e. x ( ( t \ U. ( x \ { t } ) ) =/= (/) -> E! v v e. ( ( t \ U. ( x \ { t } ) ) i^i y ) ) -> ( A. t e. x ( t \ U. ( x \ { t } ) ) =/= (/) -> A. t e. x E! v v e. ( ( t \ U. ( x \ { t } ) ) i^i y ) ) )
51 49 50 sylbi
 |-  ( A. z e. A ( z =/= (/) -> E! v v e. ( z i^i y ) ) -> ( A. t e. x ( t \ U. ( x \ { t } ) ) =/= (/) -> A. t e. x E! v v e. ( ( t \ U. ( x \ { t } ) ) i^i y ) ) )
52 27 51 syl11
 |-  ( A. z e. x ( z \ U. ( x \ { z } ) ) =/= (/) -> ( A. z e. A ( z =/= (/) -> E! v v e. ( z i^i y ) ) -> A. z e. x ( z =/= (/) -> E! v v e. ( z i^i ( y i^i U. A ) ) ) ) )