Step |
Hyp |
Ref |
Expression |
1 |
|
kmlem14.1 |
|- ( ph <-> ( z e. y -> ( ( v e. x /\ y =/= v ) /\ z e. v ) ) ) |
2 |
|
kmlem14.2 |
|- ( ps <-> ( z e. x -> ( ( v e. z /\ v e. y ) /\ ( ( u e. z /\ u e. y ) -> u = v ) ) ) ) |
3 |
|
kmlem14.3 |
|- ( ch <-> A. z e. x E! v v e. ( z i^i y ) ) |
4 |
1 2 3
|
kmlem14 |
|- ( 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. v A. u ( y e. x /\ ph ) ) |
5 |
1 2 3
|
kmlem15 |
|- ( ( -. y e. x /\ ch ) <-> A. z E. v A. u ( -. y e. x /\ ps ) ) |
6 |
5
|
exbii |
|- ( E. y ( -. y e. x /\ ch ) <-> E. y A. z E. v A. u ( -. y e. x /\ ps ) ) |
7 |
4 6
|
orbi12i |
|- ( ( E. z e. x A. v e. z E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) \/ E. y ( -. y e. x /\ ch ) ) <-> ( E. y A. z E. v A. u ( y e. x /\ ph ) \/ E. y A. z E. v A. u ( -. y e. x /\ ps ) ) ) |
8 |
|
19.43 |
|- ( E. y ( A. z E. v A. u ( y e. x /\ ph ) \/ A. z E. v A. u ( -. y e. x /\ ps ) ) <-> ( E. y A. z E. v A. u ( y e. x /\ ph ) \/ E. y A. z E. v A. u ( -. y e. x /\ ps ) ) ) |
9 |
|
pm3.24 |
|- -. ( y e. x /\ -. y e. x ) |
10 |
|
simpl |
|- ( ( y e. x /\ ph ) -> y e. x ) |
11 |
10
|
sps |
|- ( A. u ( y e. x /\ ph ) -> y e. x ) |
12 |
11
|
exlimivv |
|- ( E. z E. v A. u ( y e. x /\ ph ) -> y e. x ) |
13 |
|
simpl |
|- ( ( -. y e. x /\ ps ) -> -. y e. x ) |
14 |
13
|
sps |
|- ( A. u ( -. y e. x /\ ps ) -> -. y e. x ) |
15 |
14
|
exlimivv |
|- ( E. z E. v A. u ( -. y e. x /\ ps ) -> -. y e. x ) |
16 |
12 15
|
anim12i |
|- ( ( E. z E. v A. u ( y e. x /\ ph ) /\ E. z E. v A. u ( -. y e. x /\ ps ) ) -> ( y e. x /\ -. y e. x ) ) |
17 |
9 16
|
mto |
|- -. ( E. z E. v A. u ( y e. x /\ ph ) /\ E. z E. v A. u ( -. y e. x /\ ps ) ) |
18 |
|
19.33b |
|- ( -. ( E. z E. v A. u ( y e. x /\ ph ) /\ E. z E. v A. u ( -. y e. x /\ ps ) ) -> ( A. z ( E. v A. u ( y e. x /\ ph ) \/ E. v A. u ( -. y e. x /\ ps ) ) <-> ( A. z E. v A. u ( y e. x /\ ph ) \/ A. z E. v A. u ( -. y e. x /\ ps ) ) ) ) |
19 |
17 18
|
ax-mp |
|- ( A. z ( E. v A. u ( y e. x /\ ph ) \/ E. v A. u ( -. y e. x /\ ps ) ) <-> ( A. z E. v A. u ( y e. x /\ ph ) \/ A. z E. v A. u ( -. y e. x /\ ps ) ) ) |
20 |
10
|
exlimiv |
|- ( E. u ( y e. x /\ ph ) -> y e. x ) |
21 |
13
|
exlimiv |
|- ( E. u ( -. y e. x /\ ps ) -> -. y e. x ) |
22 |
20 21
|
anim12i |
|- ( ( E. u ( y e. x /\ ph ) /\ E. u ( -. y e. x /\ ps ) ) -> ( y e. x /\ -. y e. x ) ) |
23 |
9 22
|
mto |
|- -. ( E. u ( y e. x /\ ph ) /\ E. u ( -. y e. x /\ ps ) ) |
24 |
|
19.33b |
|- ( -. ( E. u ( y e. x /\ ph ) /\ E. u ( -. y e. x /\ ps ) ) -> ( A. u ( ( y e. x /\ ph ) \/ ( -. y e. x /\ ps ) ) <-> ( A. u ( y e. x /\ ph ) \/ A. u ( -. y e. x /\ ps ) ) ) ) |
25 |
23 24
|
ax-mp |
|- ( A. u ( ( y e. x /\ ph ) \/ ( -. y e. x /\ ps ) ) <-> ( A. u ( y e. x /\ ph ) \/ A. u ( -. y e. x /\ ps ) ) ) |
26 |
25
|
exbii |
|- ( E. v A. u ( ( y e. x /\ ph ) \/ ( -. y e. x /\ ps ) ) <-> E. v ( A. u ( y e. x /\ ph ) \/ A. u ( -. y e. x /\ ps ) ) ) |
27 |
|
19.43 |
|- ( E. v ( A. u ( y e. x /\ ph ) \/ A. u ( -. y e. x /\ ps ) ) <-> ( E. v A. u ( y e. x /\ ph ) \/ E. v A. u ( -. y e. x /\ ps ) ) ) |
28 |
26 27
|
bitr2i |
|- ( ( E. v A. u ( y e. x /\ ph ) \/ E. v A. u ( -. y e. x /\ ps ) ) <-> E. v A. u ( ( y e. x /\ ph ) \/ ( -. y e. x /\ ps ) ) ) |
29 |
28
|
albii |
|- ( A. z ( E. v A. u ( y e. x /\ ph ) \/ E. v A. u ( -. y e. x /\ ps ) ) <-> A. z E. v A. u ( ( y e. x /\ ph ) \/ ( -. y e. x /\ ps ) ) ) |
30 |
19 29
|
bitr3i |
|- ( ( A. z E. v A. u ( y e. x /\ ph ) \/ A. z E. v A. u ( -. y e. x /\ ps ) ) <-> A. z E. v A. u ( ( y e. x /\ ph ) \/ ( -. y e. x /\ ps ) ) ) |
31 |
30
|
exbii |
|- ( E. y ( A. z E. v A. u ( y e. x /\ ph ) \/ A. z E. v A. u ( -. y e. x /\ ps ) ) <-> E. y A. z E. v A. u ( ( y e. x /\ ph ) \/ ( -. y e. x /\ ps ) ) ) |
32 |
7 8 31
|
3bitr2i |
|- ( ( E. z e. x A. v e. z E. w e. x ( z =/= w /\ v e. ( z i^i w ) ) \/ E. y ( -. y e. x /\ ch ) ) <-> E. y A. z E. v A. u ( ( y e. x /\ ph ) \/ ( -. y e. x /\ ps ) ) ) |