Metamath Proof Explorer

Theorem rnstructfi

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

Ref Expression
Assertion rnstructfi 
|- ( F Struct X -> ran F e. Fin )

Proof

Step Hyp Ref Expression
1 imadmrn 
 |-  ( `' `' F " dom `' `' F ) = ran `' `' F
2 rncnvcnv 
 |-  ran `' `' F = ran F
3 1 2 eqtri 
 |-  ( `' `' F " dom `' `' F ) = ran F
4 structfung 
 |-  ( F Struct X -> Fun `' `' F )
5 dmcnvcnv 
 |-  dom `' `' F = dom F
6 dmstructfi 
 |-  ( F Struct X -> dom F e. Fin )
7 5 6 eqeltrid 
 |-  ( F Struct X -> dom `' `' F e. Fin )
8 imafi 
 |-  ( ( Fun `' `' F /\ dom `' `' F e. Fin ) -> ( `' `' F " dom `' `' F ) e. Fin )
9 4 7 8 syl2anc 
 |-  ( F Struct X -> ( `' `' F " dom `' `' F ) e. Fin )
10 3 9 eqeltrrid 
 |-  ( F Struct X -> ran F e. Fin )