Metamath Proof Explorer


Theorem hfelhf

Description: Any member of an HF set is itself an HF set. (Contributed by Scott Fenton, 16-Jul-2015)

Ref Expression
Assertion hfelhf ABBHfAHf

Proof

Step Hyp Ref Expression
1 rankelg BHfABrankArankB
2 1 ancoms ABBHfrankArankB
3 elhf2g BHfBHfrankBω
4 3 ibi BHfrankBω
5 elnn rankArankBrankBωrankAω
6 elhf2g ABAHfrankAω
7 5 6 syl5ibr ABrankArankBrankBωAHf
8 7 expcomd ABrankBωrankArankBAHf
9 8 imp ABrankBωrankArankBAHf
10 4 9 sylan2 ABBHfrankArankBAHf
11 2 10 mpd ABBHfAHf