Theorem structfn

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

	Ref	Expression
Hypothesis	structfn.1	⊢ 𝐹 Struct ⟨ 𝑀 , 𝑁 ⟩
Assertion	structfn	⊢ ( Fun ◡ ◡ 𝐹 ∧ dom 𝐹 ⊆ ( 1 ... 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		structfn.1	⊢ 𝐹 Struct ⟨ 𝑀 , 𝑁 ⟩
2	1	structfun	⊢ Fun ◡ ◡ 𝐹
3		isstruct	⊢ ( 𝐹 Struct ⟨ 𝑀 , 𝑁 ⟩ ↔ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁 ) ∧ Fun ( 𝐹 ∖ { ∅ } ) ∧ dom 𝐹 ⊆ ( 𝑀 ... 𝑁 ) ) )
4	1 3	mpbi	⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁 ) ∧ Fun ( 𝐹 ∖ { ∅ } ) ∧ dom 𝐹 ⊆ ( 𝑀 ... 𝑁 ) )
5	4	simp3i	⊢ dom 𝐹 ⊆ ( 𝑀 ... 𝑁 )
6	4	simp1i	⊢ ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁 )
7	6	simp1i	⊢ 𝑀 ∈ ℕ
8		elnnuz	⊢ ( 𝑀 ∈ ℕ ↔ 𝑀 ∈ ( ℤ≥ ‘ 1 ) )
9	7 8	mpbi	⊢ 𝑀 ∈ ( ℤ≥ ‘ 1 )
10		fzss1	⊢ ( 𝑀 ∈ ( ℤ≥ ‘ 1 ) → ( 𝑀 ... 𝑁 ) ⊆ ( 1 ... 𝑁 ) )
11	9 10	ax-mp	⊢ ( 𝑀 ... 𝑁 ) ⊆ ( 1 ... 𝑁 )
12	5 11	sstri	⊢ dom 𝐹 ⊆ ( 1 ... 𝑁 )
13	2 12	pm3.2i	⊢ ( Fun ◡ ◡ 𝐹 ∧ dom 𝐹 ⊆ ( 1 ... 𝑁 ) )