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 ⊢ 𝐹 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 ... 𝑁 ) )