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	⊢ ( 𝐹 Struct 𝑋 → dom 𝐹 ⊆ ℕ )

Proof

Step	Hyp	Ref	Expression
1		isstruct2	⊢ ( 𝐹 Struct 𝑋 ↔ ( 𝑋 ∈ ( ≤ ∩ ( ℕ × ℕ ) ) ∧ Fun ( 𝐹 ∖ { ∅ } ) ∧ dom 𝐹 ⊆ ( ... ‘ 𝑋 ) ) )
2	1	simp1bi	⊢ ( 𝐹 Struct 𝑋 → 𝑋 ∈ ( ≤ ∩ ( ℕ × ℕ ) ) )
3		elinxp	⊢ ( 𝑋 ∈ ( ≤ ∩ ( ℕ × ℕ ) ) ↔ ∃ 𝑚 ∈ ℕ ∃ 𝑛 ∈ ℕ ( 𝑋 = ⟨ 𝑚 , 𝑛 ⟩ ∧ ⟨ 𝑚 , 𝑛 ⟩ ∈ ≤ ) )
4		simpl	⊢ ( ( 𝑋 = ⟨ 𝑚 , 𝑛 ⟩ ∧ ⟨ 𝑚 , 𝑛 ⟩ ∈ ≤ ) → 𝑋 = ⟨ 𝑚 , 𝑛 ⟩ )
5	4	reximi	⊢ ( ∃ 𝑛 ∈ ℕ ( 𝑋 = ⟨ 𝑚 , 𝑛 ⟩ ∧ ⟨ 𝑚 , 𝑛 ⟩ ∈ ≤ ) → ∃ 𝑛 ∈ ℕ 𝑋 = ⟨ 𝑚 , 𝑛 ⟩ )
6	5	reximi	⊢ ( ∃ 𝑚 ∈ ℕ ∃ 𝑛 ∈ ℕ ( 𝑋 = ⟨ 𝑚 , 𝑛 ⟩ ∧ ⟨ 𝑚 , 𝑛 ⟩ ∈ ≤ ) → ∃ 𝑚 ∈ ℕ ∃ 𝑛 ∈ ℕ 𝑋 = ⟨ 𝑚 , 𝑛 ⟩ )
7	3 6	sylbi	⊢ ( 𝑋 ∈ ( ≤ ∩ ( ℕ × ℕ ) ) → ∃ 𝑚 ∈ ℕ ∃ 𝑛 ∈ ℕ 𝑋 = ⟨ 𝑚 , 𝑛 ⟩ )
8	2 7	syl	⊢ ( 𝐹 Struct 𝑋 → ∃ 𝑚 ∈ ℕ ∃ 𝑛 ∈ ℕ 𝑋 = ⟨ 𝑚 , 𝑛 ⟩ )
9		breq2	⊢ ( 𝑋 = ⟨ 𝑚 , 𝑛 ⟩ → ( 𝐹 Struct 𝑋 ↔ 𝐹 Struct ⟨ 𝑚 , 𝑛 ⟩ ) )
10	9	biimpcd	⊢ ( 𝐹 Struct 𝑋 → ( 𝑋 = ⟨ 𝑚 , 𝑛 ⟩ → 𝐹 Struct ⟨ 𝑚 , 𝑛 ⟩ ) )
11		isstruct	⊢ ( 𝐹 Struct ⟨ 𝑚 , 𝑛 ⟩ ↔ ( ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ∧ 𝑚 ≤ 𝑛 ) ∧ Fun ( 𝐹 ∖ { ∅ } ) ∧ dom 𝐹 ⊆ ( 𝑚 ... 𝑛 ) ) )
12	11	simp3bi	⊢ ( 𝐹 Struct ⟨ 𝑚 , 𝑛 ⟩ → dom 𝐹 ⊆ ( 𝑚 ... 𝑛 ) )
13		simp11	⊢ ( ( ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ∧ 𝑚 ≤ 𝑛 ) ∧ Fun ( 𝐹 ∖ { ∅ } ) ∧ dom 𝐹 ⊆ ( 𝑚 ... 𝑛 ) ) → 𝑚 ∈ ℕ )
14	11 13	sylbi	⊢ ( 𝐹 Struct ⟨ 𝑚 , 𝑛 ⟩ → 𝑚 ∈ ℕ )
15		fzssnn	⊢ ( 𝑚 ∈ ℕ → ( 𝑚 ... 𝑛 ) ⊆ ℕ )
16	14 15	syl	⊢ ( 𝐹 Struct ⟨ 𝑚 , 𝑛 ⟩ → ( 𝑚 ... 𝑛 ) ⊆ ℕ )
17	12 16	sstrd	⊢ ( 𝐹 Struct ⟨ 𝑚 , 𝑛 ⟩ → dom 𝐹 ⊆ ℕ )
18	10 17	syl6	⊢ ( 𝐹 Struct 𝑋 → ( 𝑋 = ⟨ 𝑚 , 𝑛 ⟩ → dom 𝐹 ⊆ ℕ ) )
19	18	rexlimdvw	⊢ ( 𝐹 Struct 𝑋 → ( ∃ 𝑛 ∈ ℕ 𝑋 = ⟨ 𝑚 , 𝑛 ⟩ → dom 𝐹 ⊆ ℕ ) )
20	19	rexlimdvw	⊢ ( 𝐹 Struct 𝑋 → ( ∃ 𝑚 ∈ ℕ ∃ 𝑛 ∈ ℕ 𝑋 = ⟨ 𝑚 , 𝑛 ⟩ → dom 𝐹 ⊆ ℕ ) )
21	8 20	mpd	⊢ ( 𝐹 Struct 𝑋 → dom 𝐹 ⊆ ℕ )