This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem isstruct

Description: The property of being a structure with components in M ... N . (Contributed by Mario Carneiro, 29-Aug-2015)

Ref Expression
Assertion isstruct ( 𝐹 Struct ⟨ 𝑀 , 𝑁 ⟩ ↔ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁 ) ∧ Fun ( 𝐹 ∖ { ∅ } ) ∧ dom 𝐹 ⊆ ( 𝑀 ... 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 isstruct2 ⊢ ( 𝐹 Struct ⟨ 𝑀 , 𝑁 ⟩ ↔ ( ⟨ 𝑀 , 𝑁 ⟩ ∈ ( ≤ ∩ ( ℕ × ℕ ) ) ∧ Fun ( 𝐹 ∖ { ∅ } ) ∧ dom 𝐹 ⊆ ( ... ‘ ⟨ 𝑀 , 𝑁 ⟩ ) ) )
2 df-3an ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁 ) ↔ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ 𝑀 ≤ 𝑁 ) )
3 brinxp2 ⊢ ( 𝑀 ( ≤ ∩ ( ℕ × ℕ ) ) 𝑁 ↔ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ) ∧ 𝑀 ≤ 𝑁 ) )
4 df-br ⊢ ( 𝑀 ( ≤ ∩ ( ℕ × ℕ ) ) 𝑁 ↔ ⟨ 𝑀 , 𝑁 ⟩ ∈ ( ≤ ∩ ( ℕ × ℕ ) ) )
5 2 3 4 3bitr2i ⊢ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁 ) ↔ ⟨ 𝑀 , 𝑁 ⟩ ∈ ( ≤ ∩ ( ℕ × ℕ ) ) )
6 biid ⊢ ( Fun ( 𝐹 ∖ { ∅ } ) ↔ Fun ( 𝐹 ∖ { ∅ } ) )
7 df-ov ⊢ ( 𝑀 ... 𝑁 ) = ( ... ‘ ⟨ 𝑀 , 𝑁 ⟩ )
8 7 sseq2i ⊢ ( dom 𝐹 ⊆ ( 𝑀 ... 𝑁 ) ↔ dom 𝐹 ⊆ ( ... ‘ ⟨ 𝑀 , 𝑁 ⟩ ) )
9 5 6 8 3anbi123i ⊢ ( ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁 ) ∧ Fun ( 𝐹 ∖ { ∅ } ) ∧ dom 𝐹 ⊆ ( 𝑀 ... 𝑁 ) ) ↔ ( ⟨ 𝑀 , 𝑁 ⟩ ∈ ( ≤ ∩ ( ℕ × ℕ ) ) ∧ Fun ( 𝐹 ∖ { ∅ } ) ∧ dom 𝐹 ⊆ ( ... ‘ ⟨ 𝑀 , 𝑁 ⟩ ) ) )
10 1 9 bitr4i ⊢ ( 𝐹 Struct ⟨ 𝑀 , 𝑁 ⟩ ↔ ( ( 𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑀 ≤ 𝑁 ) ∧ Fun ( 𝐹 ∖ { ∅ } ) ∧ dom 𝐹 ⊆ ( 𝑀 ... 𝑁 ) ) )