Step |
Hyp |
Ref |
Expression |
1 |
|
clsnei.o |
|- O = ( i e. _V , j e. _V |-> ( k e. ( ~P j ^m i ) |-> ( l e. j |-> { m e. i | l e. ( k ` m ) } ) ) ) |
2 |
|
clsnei.p |
|- P = ( n e. _V |-> ( p e. ( ~P n ^m ~P n ) |-> ( o e. ~P n |-> ( n \ ( p ` ( n \ o ) ) ) ) ) ) |
3 |
|
clsnei.d |
|- D = ( P ` B ) |
4 |
|
clsnei.f |
|- F = ( ~P B O B ) |
5 |
|
clsnei.h |
|- H = ( F o. D ) |
6 |
|
clsnei.r |
|- ( ph -> K H N ) |
7 |
3 5 6
|
clsneibex |
|- ( ph -> B e. _V ) |
8 |
|
pwexg |
|- ( B e. _V -> ~P B e. _V ) |
9 |
8
|
adantl |
|- ( ( ph /\ B e. _V ) -> ~P B e. _V ) |
10 |
|
simpr |
|- ( ( ph /\ B e. _V ) -> B e. _V ) |
11 |
1 9 10 4
|
fsovf1od |
|- ( ( ph /\ B e. _V ) -> F : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P ~P B ^m B ) ) |
12 |
|
f1ofn |
|- ( F : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P ~P B ^m B ) -> F Fn ( ~P B ^m ~P B ) ) |
13 |
11 12
|
syl |
|- ( ( ph /\ B e. _V ) -> F Fn ( ~P B ^m ~P B ) ) |
14 |
2 3 10
|
dssmapf1od |
|- ( ( ph /\ B e. _V ) -> D : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P B ^m ~P B ) ) |
15 |
|
f1of |
|- ( D : ( ~P B ^m ~P B ) -1-1-onto-> ( ~P B ^m ~P B ) -> D : ( ~P B ^m ~P B ) --> ( ~P B ^m ~P B ) ) |
16 |
14 15
|
syl |
|- ( ( ph /\ B e. _V ) -> D : ( ~P B ^m ~P B ) --> ( ~P B ^m ~P B ) ) |
17 |
6
|
adantr |
|- ( ( ph /\ B e. _V ) -> K H N ) |
18 |
5
|
breqi |
|- ( K H N <-> K ( F o. D ) N ) |
19 |
17 18
|
sylib |
|- ( ( ph /\ B e. _V ) -> K ( F o. D ) N ) |
20 |
13 16 19
|
brcoffn |
|- ( ( ph /\ B e. _V ) -> ( K D ( D ` K ) /\ ( D ` K ) F N ) ) |
21 |
7 20
|
mpdan |
|- ( ph -> ( K D ( D ` K ) /\ ( D ` K ) F N ) ) |
22 |
21
|
simprd |
|- ( ph -> ( D ` K ) F N ) |
23 |
1 4 22
|
ntrneinex |
|- ( ph -> N e. ( ~P ~P B ^m B ) ) |