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