Step |
Hyp |
Ref |
Expression |
1 |
|
kmlem9.1 |
|- A = { u | E. t e. x u = ( t \ U. ( x \ { t } ) ) } |
2 |
|
kmlem1 |
|- ( A. x ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> E. y A. z e. x E! v v e. ( z i^i y ) ) -> A. x ( A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) -> E. y A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) ) |
3 |
|
raleq |
|- ( x = h -> ( A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) <-> A. w e. h ( z =/= w -> ( z i^i w ) = (/) ) ) ) |
4 |
3
|
raleqbi1dv |
|- ( x = h -> ( A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) <-> A. z e. h A. w e. h ( z =/= w -> ( z i^i w ) = (/) ) ) ) |
5 |
|
raleq |
|- ( x = h -> ( A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) <-> A. z e. h ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) ) |
6 |
5
|
exbidv |
|- ( x = h -> ( E. y A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) <-> E. y A. z e. h ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) ) |
7 |
4 6
|
imbi12d |
|- ( x = h -> ( ( A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) -> E. y A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) <-> ( A. z e. h A. w e. h ( z =/= w -> ( z i^i w ) = (/) ) -> E. y A. z e. h ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) ) ) |
8 |
7
|
cbvalvw |
|- ( A. x ( A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) -> E. y A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) <-> A. h ( A. z e. h A. w e. h ( z =/= w -> ( z i^i w ) = (/) ) -> E. y A. z e. h ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) ) |
9 |
1
|
kmlem10 |
|- ( A. h ( A. z e. h A. w e. h ( z =/= w -> ( z i^i w ) = (/) ) -> E. y A. z e. h ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) -> E. y A. z e. A ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) |
10 |
|
ineq2 |
|- ( y = g -> ( z i^i y ) = ( z i^i g ) ) |
11 |
10
|
eleq2d |
|- ( y = g -> ( v e. ( z i^i y ) <-> v e. ( z i^i g ) ) ) |
12 |
11
|
eubidv |
|- ( y = g -> ( E! v v e. ( z i^i y ) <-> E! v v e. ( z i^i g ) ) ) |
13 |
12
|
imbi2d |
|- ( y = g -> ( ( z =/= (/) -> E! v v e. ( z i^i y ) ) <-> ( z =/= (/) -> E! v v e. ( z i^i g ) ) ) ) |
14 |
13
|
ralbidv |
|- ( y = g -> ( A. z e. A ( z =/= (/) -> E! v v e. ( z i^i y ) ) <-> A. z e. A ( z =/= (/) -> E! v v e. ( z i^i g ) ) ) ) |
15 |
14
|
cbvexvw |
|- ( E. y A. z e. A ( z =/= (/) -> E! v v e. ( z i^i y ) ) <-> E. g A. z e. A ( z =/= (/) -> E! v v e. ( z i^i g ) ) ) |
16 |
|
kmlem3 |
|- ( ( z \ U. ( x \ { z } ) ) =/= (/) <-> E. v e. z A. w e. x ( z =/= w -> -. v e. ( z i^i w ) ) ) |
17 |
|
ralinexa |
|- ( A. w e. x ( z =/= w -> -. v e. ( z i^i w ) ) <-> -. E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) ) |
18 |
17
|
rexbii |
|- ( E. v e. z A. w e. x ( z =/= w -> -. v e. ( z i^i w ) ) <-> E. v e. z -. E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) ) |
19 |
|
rexnal |
|- ( E. v e. z -. E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) <-> -. A. v e. z E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) ) |
20 |
16 18 19
|
3bitri |
|- ( ( z \ U. ( x \ { z } ) ) =/= (/) <-> -. A. v e. z E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) ) |
21 |
20
|
ralbii |
|- ( A. z e. x ( z \ U. ( x \ { z } ) ) =/= (/) <-> A. z e. x -. A. v e. z E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) ) |
22 |
|
ralnex |
|- ( A. z e. x -. A. v e. z E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) <-> -. E. z e. x A. v e. z E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) ) |
23 |
21 22
|
bitri |
|- ( A. z e. x ( z \ U. ( x \ { z } ) ) =/= (/) <-> -. E. z e. x A. v e. z E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) ) |
24 |
1
|
kmlem12 |
|- ( A. z e. x ( z \ U. ( x \ { z } ) ) =/= (/) -> ( A. z e. A ( z =/= (/) -> E! v v e. ( z i^i g ) ) -> A. z e. x ( z =/= (/) -> E! v v e. ( z i^i ( g i^i U. A ) ) ) ) ) |
25 |
|
vex |
|- g e. _V |
26 |
25
|
inex1 |
|- ( g i^i U. A ) e. _V |
27 |
|
ineq2 |
|- ( y = ( g i^i U. A ) -> ( z i^i y ) = ( z i^i ( g i^i U. A ) ) ) |
28 |
27
|
eleq2d |
|- ( y = ( g i^i U. A ) -> ( v e. ( z i^i y ) <-> v e. ( z i^i ( g i^i U. A ) ) ) ) |
29 |
28
|
eubidv |
|- ( y = ( g i^i U. A ) -> ( E! v v e. ( z i^i y ) <-> E! v v e. ( z i^i ( g i^i U. A ) ) ) ) |
30 |
29
|
imbi2d |
|- ( y = ( g i^i U. A ) -> ( ( z =/= (/) -> E! v v e. ( z i^i y ) ) <-> ( z =/= (/) -> E! v v e. ( z i^i ( g i^i U. A ) ) ) ) ) |
31 |
30
|
ralbidv |
|- ( y = ( g i^i U. A ) -> ( A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) <-> A. z e. x ( z =/= (/) -> E! v v e. ( z i^i ( g i^i U. A ) ) ) ) ) |
32 |
26 31
|
spcev |
|- ( A. z e. x ( z =/= (/) -> E! v v e. ( z i^i ( g i^i U. A ) ) ) -> E. y A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) |
33 |
24 32
|
syl6 |
|- ( A. z e. x ( z \ U. ( x \ { z } ) ) =/= (/) -> ( A. z e. A ( z =/= (/) -> E! v v e. ( z i^i g ) ) -> E. y A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) ) |
34 |
33
|
exlimdv |
|- ( A. z e. x ( z \ U. ( x \ { z } ) ) =/= (/) -> ( E. g A. z e. A ( z =/= (/) -> E! v v e. ( z i^i g ) ) -> E. y A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) ) |
35 |
34
|
com12 |
|- ( E. g A. z e. A ( z =/= (/) -> E! v v e. ( z i^i g ) ) -> ( A. z e. x ( z \ U. ( x \ { z } ) ) =/= (/) -> E. y A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) ) |
36 |
23 35
|
syl5bir |
|- ( E. g A. z e. A ( z =/= (/) -> E! v v e. ( z i^i g ) ) -> ( -. E. z e. x A. v e. z E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) -> E. y A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) ) |
37 |
15 36
|
sylbi |
|- ( E. y A. z e. A ( z =/= (/) -> E! v v e. ( z i^i y ) ) -> ( -. E. z e. x A. v e. z E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) -> E. y A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) ) |
38 |
9 37
|
syl |
|- ( A. h ( A. z e. h A. w e. h ( z =/= w -> ( z i^i w ) = (/) ) -> E. y A. z e. h ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) -> ( -. E. z e. x A. v e. z E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) -> E. y A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) ) |
39 |
38
|
alrimiv |
|- ( A. h ( A. z e. h A. w e. h ( z =/= w -> ( z i^i w ) = (/) ) -> E. y A. z e. h ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) -> A. x ( -. E. z e. x A. v e. z E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) -> E. y A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) ) |
40 |
8 39
|
sylbi |
|- ( A. x ( A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) -> E. y A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) -> A. x ( -. E. z e. x A. v e. z E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) -> E. y A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) ) |
41 |
2 40
|
syl |
|- ( A. x ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> E. y A. z e. x E! v v e. ( z i^i y ) ) -> A. x ( -. E. z e. x A. v e. z E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) -> E. y A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) ) |
42 |
|
kmlem7 |
|- ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> -. E. z e. x A. v e. z E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) ) |
43 |
42
|
imim1i |
|- ( ( -. E. z e. x A. v e. z E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) -> E. y A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) -> ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> E. y A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) ) |
44 |
|
biimt |
|- ( z =/= (/) -> ( E! v v e. ( z i^i y ) <-> ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) ) |
45 |
44
|
ralimi |
|- ( A. z e. x z =/= (/) -> A. z e. x ( E! v v e. ( z i^i y ) <-> ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) ) |
46 |
|
ralbi |
|- ( A. z e. x ( E! v v e. ( z i^i y ) <-> ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) -> ( A. z e. x E! v v e. ( z i^i y ) <-> A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) ) |
47 |
45 46
|
syl |
|- ( A. z e. x z =/= (/) -> ( A. z e. x E! v v e. ( z i^i y ) <-> A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) ) |
48 |
47
|
exbidv |
|- ( A. z e. x z =/= (/) -> ( E. y A. z e. x E! v v e. ( z i^i y ) <-> E. y A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) ) |
49 |
48
|
adantr |
|- ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> ( E. y A. z e. x E! v v e. ( z i^i y ) <-> E. y A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) ) |
50 |
49
|
pm5.74i |
|- ( ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> E. y A. z e. x E! v v e. ( z i^i y ) ) <-> ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> E. y A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) ) |
51 |
43 50
|
sylibr |
|- ( ( -. E. z e. x A. v e. z E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) -> E. y A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) -> ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> E. y A. z e. x E! v v e. ( z i^i y ) ) ) |
52 |
51
|
alimi |
|- ( A. x ( -. E. z e. x A. v e. z E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) -> E. y A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) -> A. x ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> E. y A. z e. x E! v v e. ( z i^i y ) ) ) |
53 |
41 52
|
impbii |
|- ( A. x ( ( A. z e. x z =/= (/) /\ A. z e. x A. w e. x ( z =/= w -> ( z i^i w ) = (/) ) ) -> E. y A. z e. x E! v v e. ( z i^i y ) ) <-> A. x ( -. E. z e. x A. v e. z E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) -> E. y A. z e. x ( z =/= (/) -> E! v v e. ( z i^i y ) ) ) ) |