Theorem structfn

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

	Ref	Expression
Hypothesis	structfn.1	$$⊢F\mathrm{Struct}⟨M,N⟩$$
Assertion	structfn	$$⊢\left(\mathrm{Fun}{F^{-1}}^{-1}\wedge \mathrm{dom}F\subseteq \left(1\dots N\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		structfn.1	$$⊢F\mathrm{Struct}⟨M,N⟩$$
2	1	structfun	$$⊢\mathrm{Fun}{F^{-1}}^{-1}$$
3		isstruct	$$⊢F\mathrm{Struct}⟨M,N⟩\leftrightarrow \left(\left(M\in \mathbb{N}\wedge N\in \mathbb{N}\wedge M\le N\right)\wedge \mathrm{Fun}\left(F\setminus \left\{\varnothing \right\}\right)\wedge \mathrm{dom}F\subseteq \left(M\dots N\right)\right)$$
4	1 3	mpbi	$$⊢\left(\left(M\in \mathbb{N}\wedge N\in \mathbb{N}\wedge M\le N\right)\wedge \mathrm{Fun}\left(F\setminus \left\{\varnothing \right\}\right)\wedge \mathrm{dom}F\subseteq \left(M\dots N\right)\right)$$
5	4	simp3i	$$⊢\mathrm{dom}F\subseteq \left(M\dots N\right)$$
6	4	simp1i	$$⊢\left(M\in \mathbb{N}\wedge N\in \mathbb{N}\wedge M\le N\right)$$
7	6	simp1i	$$⊢M\in \mathbb{N}$$
8		elnnuz	$$⊢M\in \mathbb{N}\leftrightarrow M\in {\mathbb{Z}}_{\ge 1}$$
9	7 8	mpbi	$$⊢M\in {\mathbb{Z}}_{\ge 1}$$
10		fzss1	$$⊢M\in {\mathbb{Z}}_{\ge 1}\to \left(M\dots N\right)\subseteq \left(1\dots N\right)$$
11	9 10	ax-mp	$$⊢\left(M\dots N\right)\subseteq \left(1\dots N\right)$$
12	5 11	sstri	$$⊢\mathrm{dom}F\subseteq \left(1\dots N\right)$$
13	2 12	pm3.2i	$$⊢\left(\mathrm{Fun}{F^{-1}}^{-1}\wedge \mathrm{dom}F\subseteq \left(1\dots N\right)\right)$$