Step |
Hyp |
Ref |
Expression |
1 |
|
ctex |
|- ( B ~<_ _om -> B e. _V ) |
2 |
1
|
adantl |
|- ( ( A ~<_ _om /\ B ~<_ _om ) -> B e. _V ) |
3 |
|
simpl |
|- ( ( A ~<_ _om /\ B ~<_ _om ) -> A ~<_ _om ) |
4 |
|
xpdom1g |
|- ( ( B e. _V /\ A ~<_ _om ) -> ( A X. B ) ~<_ ( _om X. B ) ) |
5 |
2 3 4
|
syl2anc |
|- ( ( A ~<_ _om /\ B ~<_ _om ) -> ( A X. B ) ~<_ ( _om X. B ) ) |
6 |
|
omex |
|- _om e. _V |
7 |
6
|
xpdom2 |
|- ( B ~<_ _om -> ( _om X. B ) ~<_ ( _om X. _om ) ) |
8 |
7
|
adantl |
|- ( ( A ~<_ _om /\ B ~<_ _om ) -> ( _om X. B ) ~<_ ( _om X. _om ) ) |
9 |
|
domtr |
|- ( ( ( A X. B ) ~<_ ( _om X. B ) /\ ( _om X. B ) ~<_ ( _om X. _om ) ) -> ( A X. B ) ~<_ ( _om X. _om ) ) |
10 |
5 8 9
|
syl2anc |
|- ( ( A ~<_ _om /\ B ~<_ _om ) -> ( A X. B ) ~<_ ( _om X. _om ) ) |
11 |
|
xpomen |
|- ( _om X. _om ) ~~ _om |
12 |
|
domentr |
|- ( ( ( A X. B ) ~<_ ( _om X. _om ) /\ ( _om X. _om ) ~~ _om ) -> ( A X. B ) ~<_ _om ) |
13 |
10 11 12
|
sylancl |
|- ( ( A ~<_ _om /\ B ~<_ _om ) -> ( A X. B ) ~<_ _om ) |