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