Step |
Hyp |
Ref |
Expression |
1 |
|
hstr.1 |
|- A e. CH |
2 |
|
hstr.2 |
|- B e. CH |
3 |
1 2
|
hstri |
|- ( A. f e. CHStates ( ( normh ` ( f ` A ) ) = 1 -> ( normh ` ( f ` B ) ) = 1 ) -> A C_ B ) |
4 |
|
hstles |
|- ( ( ( f e. CHStates /\ A e. CH ) /\ ( B e. CH /\ A C_ B ) ) -> ( ( normh ` ( f ` A ) ) = 1 -> ( normh ` ( f ` B ) ) = 1 ) ) |
5 |
2 4
|
mpanr1 |
|- ( ( ( f e. CHStates /\ A e. CH ) /\ A C_ B ) -> ( ( normh ` ( f ` A ) ) = 1 -> ( normh ` ( f ` B ) ) = 1 ) ) |
6 |
1 5
|
mpanl2 |
|- ( ( f e. CHStates /\ A C_ B ) -> ( ( normh ` ( f ` A ) ) = 1 -> ( normh ` ( f ` B ) ) = 1 ) ) |
7 |
6
|
expcom |
|- ( A C_ B -> ( f e. CHStates -> ( ( normh ` ( f ` A ) ) = 1 -> ( normh ` ( f ` B ) ) = 1 ) ) ) |
8 |
7
|
ralrimiv |
|- ( A C_ B -> A. f e. CHStates ( ( normh ` ( f ` A ) ) = 1 -> ( normh ` ( f ` B ) ) = 1 ) ) |
9 |
3 8
|
impbii |
|- ( A. f e. CHStates ( ( normh ` ( f ` A ) ) = 1 -> ( normh ` ( f ` B ) ) = 1 ) <-> A C_ B ) |