Metamath Proof Explorer

Theorem dmstructfi

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

		Ref	Expression
	Assertion	dmstructfi	$⊢ F Struct X \to dom F \in Fin$

Proof

Step	Hyp	Ref	Expression
1		isstruct2	$⊢ F Struct X \leftrightarrow (X \in (\leq \cap (ℕ \times ℕ)) \land Fun (F ∖ \{\emptyset\}) \land dom F \subseteq \dots (X))$
2	1	simp1bi	$⊢ F Struct X \to X \in (\leq \cap (ℕ \times ℕ))$
3		elinxp	$⊢ X \in (\leq \cap (ℕ \times ℕ)) \leftrightarrow \exists m \in ℕ \exists n \in ℕ (X = ⟨m, n⟩ \land ⟨m, n⟩ \in \leq)$
4		simpl	$⊢ (X = ⟨m, n⟩ \land ⟨m, n⟩ \in \leq) \to X = ⟨m, n⟩$
5	4	reximi	$⊢ \exists n \in ℕ (X = ⟨m, n⟩ \land ⟨m, n⟩ \in \leq) \to \exists n \in ℕ X = ⟨m, n⟩$
6	5	reximi	$⊢ \exists m \in ℕ \exists n \in ℕ (X = ⟨m, n⟩ \land ⟨m, n⟩ \in \leq) \to \exists m \in ℕ \exists n \in ℕ X = ⟨m, n⟩$
7	3 6	sylbi	$⊢ X \in (\leq \cap (ℕ \times ℕ)) \to \exists m \in ℕ \exists n \in ℕ X = ⟨m, n⟩$
8	2 7	syl	$⊢ F Struct X \to \exists m \in ℕ \exists n \in ℕ X = ⟨m, n⟩$
9		breq2	$⊢ X = ⟨m, n⟩ \to (F Struct X \leftrightarrow F Struct ⟨m, n⟩)$
10	9	biimpcd	$⊢ F Struct X \to (X = ⟨m, n⟩ \to F Struct ⟨m, n⟩)$
11		fzfi	$⊢ (m \dots n) \in Fin$
12		isstruct	$⊢ F Struct ⟨m, n⟩ \leftrightarrow ((m \in ℕ \land n \in ℕ \land m \leq n) \land Fun (F ∖ \{\emptyset\}) \land dom F \subseteq (m \dots n))$
13	12	simp3bi	$⊢ F Struct ⟨m, n⟩ \to dom F \subseteq (m \dots n)$
14		ssfi	$⊢ ((m \dots n) \in Fin \land dom F \subseteq (m \dots n)) \to dom F \in Fin$
15	11 13 14	sylancr	$⊢ F Struct ⟨m, n⟩ \to dom F \in Fin$
16	10 15	syl6	$⊢ F Struct X \to (X = ⟨m, n⟩ \to dom F \in Fin)$
17	16	rexlimdvw	$⊢ F Struct X \to (\exists n \in ℕ X = ⟨m, n⟩ \to dom F \in Fin)$
18	17	rexlimdvw	$⊢ F Struct X \to (\exists m \in ℕ \exists n \in ℕ X = ⟨m, n⟩ \to dom F \in Fin)$
19	8 18	mpd	$⊢ F Struct X \to dom F \in Fin$