Theorem dmstructfi

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

	Ref	Expression
Assertion	dmstructfi	⊢ ( 𝐹 Struct 𝑋 → dom 𝐹 ∈ Fin )

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		fzfi	⊢ ( 𝑚 ... 𝑛 ) ∈ Fin
12		isstruct	⊢ ( 𝐹 Struct ⟨ 𝑚 , 𝑛 ⟩ ↔ ( ( 𝑚 ∈ ℕ ∧ 𝑛 ∈ ℕ ∧ 𝑚 ≤ 𝑛 ) ∧ Fun ( 𝐹 ∖ { ∅ } ) ∧ dom 𝐹 ⊆ ( 𝑚 ... 𝑛 ) ) )
13	12	simp3bi	⊢ ( 𝐹 Struct ⟨ 𝑚 , 𝑛 ⟩ → dom 𝐹 ⊆ ( 𝑚 ... 𝑛 ) )
14		ssfi	⊢ ( ( ( 𝑚 ... 𝑛 ) ∈ Fin ∧ dom 𝐹 ⊆ ( 𝑚 ... 𝑛 ) ) → dom 𝐹 ∈ Fin )
15	11 13 14	sylancr	⊢ ( 𝐹 Struct ⟨ 𝑚 , 𝑛 ⟩ → dom 𝐹 ∈ Fin )
16	10 15	syl6	⊢ ( 𝐹 Struct 𝑋 → ( 𝑋 = ⟨ 𝑚 , 𝑛 ⟩ → dom 𝐹 ∈ Fin ) )
17	16	rexlimdvw	⊢ ( 𝐹 Struct 𝑋 → ( ∃ 𝑛 ∈ ℕ 𝑋 = ⟨ 𝑚 , 𝑛 ⟩ → dom 𝐹 ∈ Fin ) )
18	17	rexlimdvw	⊢ ( 𝐹 Struct 𝑋 → ( ∃ 𝑚 ∈ ℕ ∃ 𝑛 ∈ ℕ 𝑋 = ⟨ 𝑚 , 𝑛 ⟩ → dom 𝐹 ∈ Fin ) )
19	8 18	mpd	⊢ ( 𝐹 Struct 𝑋 → dom 𝐹 ∈ Fin )