Step |
Hyp |
Ref |
Expression |
1 |
|
axlowdimlem10.1 |
|- Q = ( { <. ( I + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) ) |
2 |
|
ovex |
|- ( I + 1 ) e. _V |
3 |
|
1ex |
|- 1 e. _V |
4 |
2 3
|
f1osn |
|- { <. ( I + 1 ) , 1 >. } : { ( I + 1 ) } -1-1-onto-> { 1 } |
5 |
|
f1of |
|- ( { <. ( I + 1 ) , 1 >. } : { ( I + 1 ) } -1-1-onto-> { 1 } -> { <. ( I + 1 ) , 1 >. } : { ( I + 1 ) } --> { 1 } ) |
6 |
4 5
|
ax-mp |
|- { <. ( I + 1 ) , 1 >. } : { ( I + 1 ) } --> { 1 } |
7 |
|
c0ex |
|- 0 e. _V |
8 |
7
|
fconst |
|- ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) : ( ( 1 ... N ) \ { ( I + 1 ) } ) --> { 0 } |
9 |
6 8
|
pm3.2i |
|- ( { <. ( I + 1 ) , 1 >. } : { ( I + 1 ) } --> { 1 } /\ ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) : ( ( 1 ... N ) \ { ( I + 1 ) } ) --> { 0 } ) |
10 |
|
disjdif |
|- ( { ( I + 1 ) } i^i ( ( 1 ... N ) \ { ( I + 1 ) } ) ) = (/) |
11 |
|
fun |
|- ( ( ( { <. ( I + 1 ) , 1 >. } : { ( I + 1 ) } --> { 1 } /\ ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) : ( ( 1 ... N ) \ { ( I + 1 ) } ) --> { 0 } ) /\ ( { ( I + 1 ) } i^i ( ( 1 ... N ) \ { ( I + 1 ) } ) ) = (/) ) -> ( { <. ( I + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) ) : ( { ( I + 1 ) } u. ( ( 1 ... N ) \ { ( I + 1 ) } ) ) --> ( { 1 } u. { 0 } ) ) |
12 |
9 10 11
|
mp2an |
|- ( { <. ( I + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) ) : ( { ( I + 1 ) } u. ( ( 1 ... N ) \ { ( I + 1 ) } ) ) --> ( { 1 } u. { 0 } ) |
13 |
1
|
feq1i |
|- ( Q : ( { ( I + 1 ) } u. ( ( 1 ... N ) \ { ( I + 1 ) } ) ) --> ( { 1 } u. { 0 } ) <-> ( { <. ( I + 1 ) , 1 >. } u. ( ( ( 1 ... N ) \ { ( I + 1 ) } ) X. { 0 } ) ) : ( { ( I + 1 ) } u. ( ( 1 ... N ) \ { ( I + 1 ) } ) ) --> ( { 1 } u. { 0 } ) ) |
14 |
12 13
|
mpbir |
|- Q : ( { ( I + 1 ) } u. ( ( 1 ... N ) \ { ( I + 1 ) } ) ) --> ( { 1 } u. { 0 } ) |
15 |
|
1re |
|- 1 e. RR |
16 |
|
snssi |
|- ( 1 e. RR -> { 1 } C_ RR ) |
17 |
15 16
|
ax-mp |
|- { 1 } C_ RR |
18 |
|
0re |
|- 0 e. RR |
19 |
|
snssi |
|- ( 0 e. RR -> { 0 } C_ RR ) |
20 |
18 19
|
ax-mp |
|- { 0 } C_ RR |
21 |
17 20
|
unssi |
|- ( { 1 } u. { 0 } ) C_ RR |
22 |
|
fss |
|- ( ( Q : ( { ( I + 1 ) } u. ( ( 1 ... N ) \ { ( I + 1 ) } ) ) --> ( { 1 } u. { 0 } ) /\ ( { 1 } u. { 0 } ) C_ RR ) -> Q : ( { ( I + 1 ) } u. ( ( 1 ... N ) \ { ( I + 1 ) } ) ) --> RR ) |
23 |
14 21 22
|
mp2an |
|- Q : ( { ( I + 1 ) } u. ( ( 1 ... N ) \ { ( I + 1 ) } ) ) --> RR |
24 |
|
fznatpl1 |
|- ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> ( I + 1 ) e. ( 1 ... N ) ) |
25 |
24
|
snssd |
|- ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> { ( I + 1 ) } C_ ( 1 ... N ) ) |
26 |
|
undif |
|- ( { ( I + 1 ) } C_ ( 1 ... N ) <-> ( { ( I + 1 ) } u. ( ( 1 ... N ) \ { ( I + 1 ) } ) ) = ( 1 ... N ) ) |
27 |
25 26
|
sylib |
|- ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> ( { ( I + 1 ) } u. ( ( 1 ... N ) \ { ( I + 1 ) } ) ) = ( 1 ... N ) ) |
28 |
27
|
feq2d |
|- ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> ( Q : ( { ( I + 1 ) } u. ( ( 1 ... N ) \ { ( I + 1 ) } ) ) --> RR <-> Q : ( 1 ... N ) --> RR ) ) |
29 |
23 28
|
mpbii |
|- ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> Q : ( 1 ... N ) --> RR ) |
30 |
|
elee |
|- ( N e. NN -> ( Q e. ( EE ` N ) <-> Q : ( 1 ... N ) --> RR ) ) |
31 |
30
|
adantr |
|- ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> ( Q e. ( EE ` N ) <-> Q : ( 1 ... N ) --> RR ) ) |
32 |
29 31
|
mpbird |
|- ( ( N e. NN /\ I e. ( 1 ... ( N - 1 ) ) ) -> Q e. ( EE ` N ) ) |