This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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