Step |
Hyp |
Ref |
Expression |
1 |
|
hsmexlem.f |
|- F = OrdIso ( _E , B ) |
2 |
|
hsmexlem.g |
|- G = OrdIso ( _E , U_ a e. A B ) |
3 |
|
wdomref |
|- ( C e. On -> C ~<_* C ) |
4 |
|
xpwdomg |
|- ( ( A ~<_* D /\ C ~<_* C ) -> ( A X. C ) ~<_* ( D X. C ) ) |
5 |
3 4
|
sylan2 |
|- ( ( A ~<_* D /\ C e. On ) -> ( A X. C ) ~<_* ( D X. C ) ) |
6 |
|
wdompwdom |
|- ( ( A X. C ) ~<_* ( D X. C ) -> ~P ( A X. C ) ~<_ ~P ( D X. C ) ) |
7 |
|
harword |
|- ( ~P ( A X. C ) ~<_ ~P ( D X. C ) -> ( har ` ~P ( A X. C ) ) C_ ( har ` ~P ( D X. C ) ) ) |
8 |
5 6 7
|
3syl |
|- ( ( A ~<_* D /\ C e. On ) -> ( har ` ~P ( A X. C ) ) C_ ( har ` ~P ( D X. C ) ) ) |
9 |
8
|
adantr |
|- ( ( ( A ~<_* D /\ C e. On ) /\ A. a e. A ( B e. ~P On /\ dom F e. C ) ) -> ( har ` ~P ( A X. C ) ) C_ ( har ` ~P ( D X. C ) ) ) |
10 |
|
relwdom |
|- Rel ~<_* |
11 |
10
|
brrelex1i |
|- ( A ~<_* D -> A e. _V ) |
12 |
11
|
adantr |
|- ( ( A ~<_* D /\ C e. On ) -> A e. _V ) |
13 |
12
|
adantr |
|- ( ( ( A ~<_* D /\ C e. On ) /\ A. a e. A ( B e. ~P On /\ dom F e. C ) ) -> A e. _V ) |
14 |
|
simplr |
|- ( ( ( A ~<_* D /\ C e. On ) /\ A. a e. A ( B e. ~P On /\ dom F e. C ) ) -> C e. On ) |
15 |
|
simpr |
|- ( ( ( A ~<_* D /\ C e. On ) /\ A. a e. A ( B e. ~P On /\ dom F e. C ) ) -> A. a e. A ( B e. ~P On /\ dom F e. C ) ) |
16 |
1 2
|
hsmexlem2 |
|- ( ( A e. _V /\ C e. On /\ A. a e. A ( B e. ~P On /\ dom F e. C ) ) -> dom G e. ( har ` ~P ( A X. C ) ) ) |
17 |
13 14 15 16
|
syl3anc |
|- ( ( ( A ~<_* D /\ C e. On ) /\ A. a e. A ( B e. ~P On /\ dom F e. C ) ) -> dom G e. ( har ` ~P ( A X. C ) ) ) |
18 |
9 17
|
sseldd |
|- ( ( ( A ~<_* D /\ C e. On ) /\ A. a e. A ( B e. ~P On /\ dom F e. C ) ) -> dom G e. ( har ` ~P ( D X. C ) ) ) |