Description: Any member of an HF set is itself an HF set. (Contributed by Scott Fenton, 16-Jul-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | hfelhf | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | rankelg | |
|
2 | 1 | ancoms | |
3 | elhf2g | |
|
4 | 3 | ibi | |
5 | elnn | |
|
6 | elhf2g | |
|
7 | 5 6 | syl5ibr | |
8 | 7 | expcomd | |
9 | 8 | imp | |
10 | 4 9 | sylan2 | |
11 | 2 10 | mpd | |