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