Step |
Hyp |
Ref |
Expression |
1 |
|
mnupwd.1 |
|- M = { k | A. l e. k ( ~P l C_ k /\ A. m E. n e. k ( ~P l C_ n /\ A. p e. l ( E. q e. k ( p e. q /\ q e. m ) -> E. r e. m ( p e. r /\ U. r C_ n ) ) ) ) } |
2 |
|
mnupwd.2 |
|- ( ph -> U e. M ) |
3 |
|
mnupwd.3 |
|- ( ph -> A e. U ) |
4 |
|
0ex |
|- (/) e. _V |
5 |
4
|
a1i |
|- ( ph -> (/) e. _V ) |
6 |
1 2 3 5
|
mnuop23d |
|- ( ph -> E. w e. U ( ~P A C_ w /\ A. i e. A ( E. v e. U ( i e. v /\ v e. (/) ) -> E. u e. (/) ( i e. u /\ U. u C_ w ) ) ) ) |
7 |
|
simpl |
|- ( ( ~P A C_ w /\ A. i e. A ( E. v e. U ( i e. v /\ v e. (/) ) -> E. u e. (/) ( i e. u /\ U. u C_ w ) ) ) -> ~P A C_ w ) |
8 |
7
|
reximi |
|- ( E. w e. U ( ~P A C_ w /\ A. i e. A ( E. v e. U ( i e. v /\ v e. (/) ) -> E. u e. (/) ( i e. u /\ U. u C_ w ) ) ) -> E. w e. U ~P A C_ w ) |
9 |
6 8
|
syl |
|- ( ph -> E. w e. U ~P A C_ w ) |
10 |
1 2 9
|
mnuss2d |
|- ( ph -> ~P A e. U ) |