Step |
Hyp |
Ref |
Expression |
1 |
|
structfn.1 |
|- F Struct <. M , N >. |
2 |
1
|
structfun |
|- Fun `' `' F |
3 |
|
isstruct |
|- ( F Struct <. M , N >. <-> ( ( M e. NN /\ N e. NN /\ M <_ N ) /\ Fun ( F \ { (/) } ) /\ dom F C_ ( M ... N ) ) ) |
4 |
1 3
|
mpbi |
|- ( ( M e. NN /\ N e. NN /\ M <_ N ) /\ Fun ( F \ { (/) } ) /\ dom F C_ ( M ... N ) ) |
5 |
4
|
simp3i |
|- dom F C_ ( M ... N ) |
6 |
4
|
simp1i |
|- ( M e. NN /\ N e. NN /\ M <_ N ) |
7 |
6
|
simp1i |
|- M e. NN |
8 |
|
elnnuz |
|- ( M e. NN <-> M e. ( ZZ>= ` 1 ) ) |
9 |
7 8
|
mpbi |
|- M e. ( ZZ>= ` 1 ) |
10 |
|
fzss1 |
|- ( M e. ( ZZ>= ` 1 ) -> ( M ... N ) C_ ( 1 ... N ) ) |
11 |
9 10
|
ax-mp |
|- ( M ... N ) C_ ( 1 ... N ) |
12 |
5 11
|
sstri |
|- dom F C_ ( 1 ... N ) |
13 |
2 12
|
pm3.2i |
|- ( Fun `' `' F /\ dom F C_ ( 1 ... N ) ) |