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