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 eqtr2id
 |-  ( 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 eqtrid
 |-  ( ( 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 eqtrid
 |-  ( 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 eqtrid
 |-  ( z e. x -> ( z i^i U. A ) = ( z \ U. ( x \ { z } ) ) )