Metamath Proof Explorer

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 Struct X -> dom F C_ NN )

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 isstruct 
 |-  ( F Struct <. m , n >. <-> ( ( m e. NN /\ n e. NN /\ m <_ n ) /\ Fun ( F \ { (/) } ) /\ dom F C_ ( m ... n ) ) )
12 11 simp3bi 
 |-  ( F Struct <. m , n >. -> dom F C_ ( m ... n ) )
13 simp11 
 |-  ( ( ( m e. NN /\ n e. NN /\ m <_ n ) /\ Fun ( F \ { (/) } ) /\ dom F C_ ( m ... n ) ) -> m e. NN )
14 11 13 sylbi 
 |-  ( F Struct <. m , n >. -> m e. NN )
15 fzssnn 
 |-  ( m e. NN -> ( m ... n ) C_ NN )
16 14 15 syl 
 |-  ( F Struct <. m , n >. -> ( m ... n ) C_ NN )
17 12 16 sstrd 
 |-  ( F Struct <. m , n >. -> dom F C_ NN )
18 10 17 syl6 
 |-  ( F Struct X -> ( X = <. m , n >. -> dom F C_ NN ) )
19 18 rexlimdvw 
 |-  ( F Struct X -> ( E. n e. NN X = <. m , n >. -> dom F C_ NN ) )
20 19 rexlimdvw 
 |-  ( F Struct X -> ( E. m e. NN E. n e. NN X = <. m , n >. -> dom F C_ NN ) )
21 8 20 mpd 
 |-  ( F Struct X -> dom F C_ NN )