Step |
Hyp |
Ref |
Expression |
1 |
|
rankelg |
|- ( ( B e. Hf /\ A e. B ) -> ( rank ` A ) e. ( rank ` B ) ) |
2 |
1
|
ancoms |
|- ( ( A e. B /\ B e. Hf ) -> ( rank ` A ) e. ( rank ` B ) ) |
3 |
|
elhf2g |
|- ( B e. Hf -> ( B e. Hf <-> ( rank ` B ) e. _om ) ) |
4 |
3
|
ibi |
|- ( B e. Hf -> ( rank ` B ) e. _om ) |
5 |
|
elnn |
|- ( ( ( rank ` A ) e. ( rank ` B ) /\ ( rank ` B ) e. _om ) -> ( rank ` A ) e. _om ) |
6 |
|
elhf2g |
|- ( A e. B -> ( A e. Hf <-> ( rank ` A ) e. _om ) ) |
7 |
5 6
|
syl5ibr |
|- ( A e. B -> ( ( ( rank ` A ) e. ( rank ` B ) /\ ( rank ` B ) e. _om ) -> A e. Hf ) ) |
8 |
7
|
expcomd |
|- ( A e. B -> ( ( rank ` B ) e. _om -> ( ( rank ` A ) e. ( rank ` B ) -> A e. Hf ) ) ) |
9 |
8
|
imp |
|- ( ( A e. B /\ ( rank ` B ) e. _om ) -> ( ( rank ` A ) e. ( rank ` B ) -> A e. Hf ) ) |
10 |
4 9
|
sylan2 |
|- ( ( A e. B /\ B e. Hf ) -> ( ( rank ` A ) e. ( rank ` B ) -> A e. Hf ) ) |
11 |
2 10
|
mpd |
|- ( ( A e. B /\ B e. Hf ) -> A e. Hf ) |