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 ∈ Fin

Proof

Step Hyp Ref Expression
1 imadmrn ⊢ F -1 -1 dom ⁡ F -1 -1 = ran ⁡ F -1 -1
2 rncnvcnv ⊢ ran ⁡ F -1 -1 = ran ⁡ F
3 1 2 eqtri ⊢ F -1 -1 dom ⁡ F -1 -1 = ran ⁡ F
4 structfung ⊢ F Struct X → Fun ⁡ F -1 -1
5 dmcnvcnv ⊢ dom ⁡ F -1 -1 = dom ⁡ F
6 dmstructfi ⊢ F Struct X → dom ⁡ F ∈ Fin
7 5 6 eqeltrid ⊢ F Struct X → dom ⁡ F -1 -1 ∈ Fin
8 imafi ⊢ Fun ⁡ F -1 -1 ∧ dom ⁡ F -1 -1 ∈ Fin → F -1 -1 dom ⁡ F -1 -1 ∈ Fin
9 4 7 8 syl2anc ⊢ F Struct X → F -1 -1 dom ⁡ F -1 -1 ∈ Fin
10 3 9 eqeltrrid ⊢ F Struct X → ran ⁡ F ∈ Fin