Metamath Proof Explorer

Theorem kmlem11

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

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

Proof

Step Hyp Ref Expression
1 kmlem9.1 
 |-  A = { u | E. t e. x u = ( t \ U. ( x \ { t } ) ) }
2 1 unieqi 
 |-  U. A = U. { u | E. t e. x u = ( t \ U. ( x \ { t } ) ) }
3 vex 
 |-  t e. _V
4 3 difexi 
 |-  ( t \ U. ( x \ { t } ) ) e. _V
5 4 dfiun2 
 |-  U_ t e. x ( t \ U. ( x \ { t } ) ) = U. { u | E. t e. x u = ( t \ U. ( x \ { t } ) ) }
6 2 5 eqtr4i 
 |-  U. A = U_ t e. x ( t \ U. ( x \ { t } ) )
7 6 ineq2i 
 |-  ( z i^i U. A ) = ( z i^i U_ t e. x ( t \ U. ( x \ { t } ) ) )
8 iunin2 
 |-  U_ t e. x ( z i^i ( t \ U. ( x \ { t } ) ) ) = ( z i^i U_ t e. x ( t \ U. ( x \ { t } ) ) )
9 7 8 eqtr4i 
 |-  ( z i^i U. A ) = U_ t e. x ( z i^i ( t \ U. ( x \ { t } ) ) )
10 undif2 
 |-  ( { z } u. ( x \ { z } ) ) = ( { z } u. x )
11 snssi 
 |-  ( z e. x -> { z } C_ x )
12 ssequn1 
 |-  ( { z } C_ x <-> ( { z } u. x ) = x )
13 11 12 sylib 
 |-  ( z e. x -> ( { z } u. x ) = x )
14 10 13 syl5req 
 |-  ( z e. x -> x = ( { z } u. ( x \ { z } ) ) )
15 14 iuneq1d 
 |-  ( z e. x -> U_ t e. x ( z i^i ( t \ U. ( x \ { t } ) ) ) = U_ t e. ( { z } u. ( x \ { z } ) ) ( z i^i ( t \ U. ( x \ { t } ) ) ) )
16 iunxun 
 |-  U_ t e. ( { z } u. ( x \ { z } ) ) ( z i^i ( t \ U. ( x \ { t } ) ) ) = ( U_ t e. { z } ( z i^i ( t \ U. ( x \ { t } ) ) ) u. U_ t e. ( x \ { z } ) ( z i^i ( t \ U. ( x \ { t } ) ) ) )
17 vex 
 |-  z e. _V
18 difeq1 
 |-  ( t = z -> ( t \ U. ( x \ { t } ) ) = ( z \ U. ( x \ { t } ) ) )
19 sneq 
 |-  ( t = z -> { t } = { z } )
20 19 difeq2d 
 |-  ( t = z -> ( x \ { t } ) = ( x \ { z } ) )
21 20 unieqd 
 |-  ( t = z -> U. ( x \ { t } ) = U. ( x \ { z } ) )
22 21 difeq2d 
 |-  ( t = z -> ( z \ U. ( x \ { t } ) ) = ( z \ U. ( x \ { z } ) ) )
23 18 22 eqtrd 
 |-  ( t = z -> ( t \ U. ( x \ { t } ) ) = ( z \ U. ( x \ { z } ) ) )
24 23 ineq2d 
 |-  ( t = z -> ( z i^i ( t \ U. ( x \ { t } ) ) ) = ( z i^i ( z \ U. ( x \ { z } ) ) ) )
25 17 24 iunxsn 
 |-  U_ t e. { z } ( z i^i ( t \ U. ( x \ { t } ) ) ) = ( z i^i ( z \ U. ( x \ { z } ) ) )
26 25 uneq1i 
 |-  ( U_ t e. { z } ( z i^i ( t \ U. ( x \ { t } ) ) ) u. U_ t e. ( x \ { z } ) ( z i^i ( t \ U. ( x \ { t } ) ) ) ) = ( ( z i^i ( z \ U. ( x \ { z } ) ) ) u. U_ t e. ( x \ { z } ) ( z i^i ( t \ U. ( x \ { t } ) ) ) )
27 16 26 eqtri 
 |-  U_ t e. ( { z } u. ( x \ { z } ) ) ( z i^i ( t \ U. ( x \ { t } ) ) ) = ( ( z i^i ( z \ U. ( x \ { z } ) ) ) u. U_ t e. ( x \ { z } ) ( z i^i ( t \ U. ( x \ { t } ) ) ) )
28 eldifsni 
 |-  ( t e. ( x \ { z } ) -> t =/= z )
29 incom 
 |-  ( z i^i ( t \ U. ( x \ { t } ) ) ) = ( ( t \ U. ( x \ { t } ) ) i^i z )
30 kmlem4 
 |-  ( ( z e. x /\ t =/= z ) -> ( ( t \ U. ( x \ { t } ) ) i^i z ) = (/) )
31 29 30 syl5eq 
 |-  ( ( z e. x /\ t =/= z ) -> ( z i^i ( t \ U. ( x \ { t } ) ) ) = (/) )
32 31 ex 
 |-  ( z e. x -> ( t =/= z -> ( z i^i ( t \ U. ( x \ { t } ) ) ) = (/) ) )
33 28 32 syl5 
 |-  ( z e. x -> ( t e. ( x \ { z } ) -> ( z i^i ( t \ U. ( x \ { t } ) ) ) = (/) ) )
34 33 ralrimiv 
 |-  ( z e. x -> A. t e. ( x \ { z } ) ( z i^i ( t \ U. ( x \ { t } ) ) ) = (/) )
35 iuneq2 
 |-  ( A. t e. ( x \ { z } ) ( z i^i ( t \ U. ( x \ { t } ) ) ) = (/) -> U_ t e. ( x \ { z } ) ( z i^i ( t \ U. ( x \ { t } ) ) ) = U_ t e. ( x \ { z } ) (/) )
36 34 35 syl 
 |-  ( z e. x -> U_ t e. ( x \ { z } ) ( z i^i ( t \ U. ( x \ { t } ) ) ) = U_ t e. ( x \ { z } ) (/) )
37 iun0 
 |-  U_ t e. ( x \ { z } ) (/) = (/)
38 36 37 eqtrdi 
 |-  ( z e. x -> U_ t e. ( x \ { z } ) ( z i^i ( t \ U. ( x \ { t } ) ) ) = (/) )
39 38 uneq2d 
 |-  ( z e. x -> ( ( z i^i ( z \ U. ( x \ { z } ) ) ) u. U_ t e. ( x \ { z } ) ( z i^i ( t \ U. ( x \ { t } ) ) ) ) = ( ( z i^i ( z \ U. ( x \ { z } ) ) ) u. (/) ) )
40 27 39 syl5eq 
 |-  ( z e. x -> U_ t e. ( { z } u. ( x \ { z } ) ) ( z i^i ( t \ U. ( x \ { t } ) ) ) = ( ( z i^i ( z \ U. ( x \ { z } ) ) ) u. (/) ) )
41 15 40 eqtrd 
 |-  ( z e. x -> U_ t e. x ( z i^i ( t \ U. ( x \ { t } ) ) ) = ( ( z i^i ( z \ U. ( x \ { z } ) ) ) u. (/) ) )
42 un0 
 |-  ( ( z i^i ( z \ U. ( x \ { z } ) ) ) u. (/) ) = ( z i^i ( z \ U. ( x \ { z } ) ) )
43 indif 
 |-  ( z i^i ( z \ U. ( x \ { z } ) ) ) = ( z \ U. ( x \ { z } ) )
44 42 43 eqtri 
 |-  ( ( z i^i ( z \ U. ( x \ { z } ) ) ) u. (/) ) = ( z \ U. ( x \ { z } ) )
45 41 44 eqtrdi 
 |-  ( z e. x -> U_ t e. x ( z i^i ( t \ U. ( x \ { t } ) ) ) = ( z \ U. ( x \ { z } ) ) )
46 9 45 syl5eq 
 |-  ( z e. x -> ( z i^i U. A ) = ( z \ U. ( x \ { z } ) ) )