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 -> dom F e. Fin )

Proof

Step	Hyp	Ref	Expression
1		isstruct2	|- ( F Struct X <-> ( X e. ( <_ i^i ( NN X. NN ) ) /\ Fun ( F \ { (/) } ) /\ dom F C_ ( ... ` X ) ) )
2	1	simp1bi	|- ( F Struct X -> X e. ( <_ i^i ( NN X. NN ) ) )
3		elinxp	|- ( X e. ( <_ i^i ( NN X. NN ) ) <-> E. m e. NN E. n e. NN ( X = <. m , n >. /\ <. m , n >. e. <_ ) )
4		simpl	|- ( ( X = <. m , n >. /\ <. m , n >. e. <_ ) -> X = <. m , n >. )
5	4	reximi	|- ( E. n e. NN ( X = <. m , n >. /\ <. m , n >. e. <_ ) -> E. n e. NN X = <. m , n >. )
6	5	reximi	|- ( E. m e. NN E. n e. NN ( X = <. m , n >. /\ <. m , n >. e. <_ ) -> E. m e. NN E. n e. NN X = <. m , n >. )
7	3 6	sylbi	|- ( X e. ( <_ i^i ( NN X. NN ) ) -> E. m e. NN E. n e. NN X = <. m , n >. )
8	2 7	syl	|- ( F Struct X -> E. m e. NN E. n e. NN X = <. m , n >. )
9		breq2	|- ( X = <. m , n >. -> ( F Struct X <-> F Struct <. m , n >. ) )
10	9	biimpcd	|- ( F Struct X -> ( X = <. m , n >. -> F Struct <. m , n >. ) )
11		fzfi	|- ( m ... n ) e. Fin
12		isstruct	|- ( F Struct <. m , n >. <-> ( ( m e. NN /\ n e. NN /\ m <_ n ) /\ Fun ( F \ { (/) } ) /\ dom F C_ ( m ... n ) ) )
13	12	simp3bi	|- ( F Struct <. m , n >. -> dom F C_ ( m ... n ) )
14		ssfi	|- ( ( ( m ... n ) e. Fin /\ dom F C_ ( m ... n ) ) -> dom F e. Fin )
15	11 13 14	sylancr	|- ( F Struct <. m , n >. -> dom F e. Fin )
16	10 15	syl6	|- ( F Struct X -> ( X = <. m , n >. -> dom F e. Fin ) )
17	16	rexlimdvw	|- ( F Struct X -> ( E. n e. NN X = <. m , n >. -> dom F e. Fin ) )
18	17	rexlimdvw	|- ( F Struct X -> ( E. m e. NN E. n e. NN X = <. m , n >. -> dom F e. Fin ) )
19	8 18	mpd	|- ( F Struct X -> dom F e. Fin )