Metamath Proof Explorer

Theorem omsshf

Description: The class of finite ordinals is included in the class of hereditarily finite sets. (Contributed by Eric Schmidt, 26-Sep-2026)

Ref Expression
Assertion omsshf 
|- _om C_ HF

Proof

Step Hyp Ref Expression
1 omhf 
 |-  ( x e. _om -> x e. HF )
2 1 ssriv 
 |-  _om C_ HF