Theorem dmstructnn

Description: The domain of an extensible structure is a subset of NN . (Contributed by Eric Schmidt, 29-Sep-2026)

	Ref	Expression
Assertion	dmstructnn	$$⊢F\mathrm{Struct}X\to \mathrm{dom}F\subseteq \mathbb{N}$$

Proof

Step	Hyp	Ref	Expression
1		isstruct2	$$⊢F\mathrm{Struct}X\leftrightarrow \left(X\in \left(\le \cap \left(\mathbb{N}\times \mathbb{N}\right)\right)\wedge \mathrm{Fun}\left(F\setminus \left\{\varnothing \right\}\right)\wedge \mathrm{dom}F\subseteq \dots \left(X\right)\right)$$
2	1	simp1bi	$$⊢F\mathrm{Struct}X\to X\in \left(\le \cap \left(\mathbb{N}\times \mathbb{N}\right)\right)$$
3		elinxp	$$⊢X\in \left(\le \cap \left(\mathbb{N}\times \mathbb{N}\right)\right)\leftrightarrow \exists m\in \mathbb{N}\exists n\in \mathbb{N}\left(X=⟨m,n⟩\wedge ⟨m,n⟩\in \le \right)$$
4		simpl	$$⊢\left(X=⟨m,n⟩\wedge ⟨m,n⟩\in \le \right)\to X=⟨m,n⟩$$
5	4	reximi	$$⊢\exists n\in \mathbb{N}\left(X=⟨m,n⟩\wedge ⟨m,n⟩\in \le \right)\to \exists n\in \mathbb{N}X=⟨m,n⟩$$
6	5	reximi	$$⊢\exists m\in \mathbb{N}\exists n\in \mathbb{N}\left(X=⟨m,n⟩\wedge ⟨m,n⟩\in \le \right)\to \exists m\in \mathbb{N}\exists n\in \mathbb{N}X=⟨m,n⟩$$
7	3 6	sylbi	$$⊢X\in \left(\le \cap \left(\mathbb{N}\times \mathbb{N}\right)\right)\to \exists m\in \mathbb{N}\exists n\in \mathbb{N}X=⟨m,n⟩$$
8	2 7	syl	$$⊢F\mathrm{Struct}X\to \exists m\in \mathbb{N}\exists n\in \mathbb{N}X=⟨m,n⟩$$
9		breq2	$$⊢X=⟨m,n⟩\to \left(F\mathrm{Struct}X\leftrightarrow F\mathrm{Struct}⟨m,n⟩\right)$$
10	9	biimpcd	$$⊢F\mathrm{Struct}X\to \left(X=⟨m,n⟩\to F\mathrm{Struct}⟨m,n⟩\right)$$
11		isstruct	$$⊢F\mathrm{Struct}⟨m,n⟩\leftrightarrow \left(\left(m\in \mathbb{N}\wedge n\in \mathbb{N}\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)$$
12	11	simp3bi	$$⊢F\mathrm{Struct}⟨m,n⟩\to \mathrm{dom}F\subseteq \left(m\dots n\right)$$
13		simp11	$$⊢\left(\left(m\in \mathbb{N}\wedge n\in \mathbb{N}\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)\to m\in \mathbb{N}$$
14	11 13	sylbi	$$⊢F\mathrm{Struct}⟨m,n⟩\to m\in \mathbb{N}$$
15		fzssnn	$$⊢m\in \mathbb{N}\to \left(m\dots n\right)\subseteq \mathbb{N}$$
16	14 15	syl	$$⊢F\mathrm{Struct}⟨m,n⟩\to \left(m\dots n\right)\subseteq \mathbb{N}$$
17	12 16	sstrd	$$⊢F\mathrm{Struct}⟨m,n⟩\to \mathrm{dom}F\subseteq \mathbb{N}$$
18	10 17	syl6	$$⊢F\mathrm{Struct}X\to \left(X=⟨m,n⟩\to \mathrm{dom}F\subseteq \mathbb{N}\right)$$
19	18	rexlimdvw	$$⊢F\mathrm{Struct}X\to \left(\exists n\in \mathbb{N}X=⟨m,n⟩\to \mathrm{dom}F\subseteq \mathbb{N}\right)$$
20	19	rexlimdvw	$$⊢F\mathrm{Struct}X\to \left(\exists m\in \mathbb{N}\exists n\in \mathbb{N}X=⟨m,n⟩\to \mathrm{dom}F\subseteq \mathbb{N}\right)$$
21	8 20	mpd	$$⊢F\mathrm{Struct}X\to \mathrm{dom}F\subseteq \mathbb{N}$$