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^{-1}}^{-1} \land dom F \subseteq (1 \dots N))$

Step	Hyp	Ref	Expression
1		structfn.1	$⊢ F Struct ⟨M, N⟩$
2	1	structfun	$⊢ Fun {F^{-1}}^{-1}$
3		isstruct	$⊢ F Struct ⟨M, N⟩ \leftrightarrow ((M \in ℕ \land N \in ℕ \land M \leq N) \land Fun (F ∖ \{\emptyset\}) \land dom F \subseteq (M \dots N))$
4	1 3	mpbi	$⊢ ((M \in ℕ \land N \in ℕ \land M \leq N) \land Fun (F ∖ \{\emptyset\}) \land dom F \subseteq (M \dots N))$
5	4	simp3i	$⊢ dom F \subseteq (M \dots N)$
6	4	simp1i	$⊢ (M \in ℕ \land N \in ℕ \land M \leq N)$
7	6	simp1i	$⊢ M \in ℕ$
8		elnnuz	$⊢ M \in ℕ \leftrightarrow M \in ℤ_{\geq 1}$
9	7 8	mpbi	$⊢ M \in ℤ_{\geq 1}$
10		fzss1	$⊢ M \in ℤ_{\geq 1} \to (M \dots N) \subseteq (1 \dots N)$
11	9 10	ax-mp	$⊢ (M \dots N) \subseteq (1 \dots N)$
12	5 11	sstri	$⊢ dom F \subseteq (1 \dots N)$
13	2 12	pm3.2i	$⊢ (Fun {F^{-1}}^{-1} \land dom F \subseteq (1 \dots N))$

Metamath Proof Explorer