# 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 ${⊢}{F}\mathrm{Struct}⟨{M},{N}⟩↔\left(\left({M}\in ℕ\wedge {N}\in ℕ\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)$

### Proof

Step Hyp Ref Expression
1 isstruct2 ${⊢}{F}\mathrm{Struct}⟨{M},{N}⟩↔\left(⟨{M},{N}⟩\in \left(\le \cap \left(ℕ×ℕ\right)\right)\wedge \mathrm{Fun}\left({F}\setminus \left\{\varnothing \right\}\right)\wedge \mathrm{dom}{F}\subseteq \dots \left(⟨{M},{N}⟩\right)\right)$
2 df-3an ${⊢}\left({M}\in ℕ\wedge {N}\in ℕ\wedge {M}\le {N}\right)↔\left(\left({M}\in ℕ\wedge {N}\in ℕ\right)\wedge {M}\le {N}\right)$
3 brinxp2 ${⊢}{M}\left(\le \cap \left(ℕ×ℕ\right)\right){N}↔\left(\left({M}\in ℕ\wedge {N}\in ℕ\right)\wedge {M}\le {N}\right)$
4 df-br ${⊢}{M}\left(\le \cap \left(ℕ×ℕ\right)\right){N}↔⟨{M},{N}⟩\in \left(\le \cap \left(ℕ×ℕ\right)\right)$
5 2 3 4 3bitr2i ${⊢}\left({M}\in ℕ\wedge {N}\in ℕ\wedge {M}\le {N}\right)↔⟨{M},{N}⟩\in \left(\le \cap \left(ℕ×ℕ\right)\right)$
6 biid ${⊢}\mathrm{Fun}\left({F}\setminus \left\{\varnothing \right\}\right)↔\mathrm{Fun}\left({F}\setminus \left\{\varnothing \right\}\right)$
7 df-ov ${⊢}\left({M}\dots {N}\right)=\dots \left(⟨{M},{N}⟩\right)$
8 7 sseq2i ${⊢}\mathrm{dom}{F}\subseteq \left({M}\dots {N}\right)↔\mathrm{dom}{F}\subseteq \dots \left(⟨{M},{N}⟩\right)$
9 5 6 8 3anbi123i ${⊢}\left(\left({M}\in ℕ\wedge {N}\in ℕ\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)↔\left(⟨{M},{N}⟩\in \left(\le \cap \left(ℕ×ℕ\right)\right)\wedge \mathrm{Fun}\left({F}\setminus \left\{\varnothing \right\}\right)\wedge \mathrm{dom}{F}\subseteq \dots \left(⟨{M},{N}⟩\right)\right)$
10 1 9 bitr4i ${⊢}{F}\mathrm{Struct}⟨{M},{N}⟩↔\left(\left({M}\in ℕ\wedge {N}\in ℕ\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)$