Metamath Proof Explorer


Theorem structfn

Description: Convert between two kinds of structure closure. (Contributed by Mario Carneiro, 29-Aug-2015)

Ref Expression
Hypothesis structfn.1
|- F Struct <. M , N >.
Assertion structfn
|- ( Fun `' `' F /\ dom F C_ ( 1 ... N ) )

Proof

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 ) )