Step |
Hyp |
Ref |
Expression |
1 |
|
sdomdom |
|- ( B ~< A -> B ~<_ A ) |
2 |
|
infxpabs |
|- ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( B =/= (/) /\ B ~<_ A ) ) -> ( A X. B ) ~~ A ) |
3 |
|
infunabs |
|- ( ( A e. dom card /\ _om ~<_ A /\ B ~<_ A ) -> ( A u. B ) ~~ A ) |
4 |
3
|
3expa |
|- ( ( ( A e. dom card /\ _om ~<_ A ) /\ B ~<_ A ) -> ( A u. B ) ~~ A ) |
5 |
4
|
adantrl |
|- ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( B =/= (/) /\ B ~<_ A ) ) -> ( A u. B ) ~~ A ) |
6 |
5
|
ensymd |
|- ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( B =/= (/) /\ B ~<_ A ) ) -> A ~~ ( A u. B ) ) |
7 |
|
entr |
|- ( ( ( A X. B ) ~~ A /\ A ~~ ( A u. B ) ) -> ( A X. B ) ~~ ( A u. B ) ) |
8 |
2 6 7
|
syl2anc |
|- ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( B =/= (/) /\ B ~<_ A ) ) -> ( A X. B ) ~~ ( A u. B ) ) |
9 |
8
|
expr |
|- ( ( ( A e. dom card /\ _om ~<_ A ) /\ B =/= (/) ) -> ( B ~<_ A -> ( A X. B ) ~~ ( A u. B ) ) ) |
10 |
9
|
adantrl |
|- ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( B e. dom card /\ B =/= (/) ) ) -> ( B ~<_ A -> ( A X. B ) ~~ ( A u. B ) ) ) |
11 |
1 10
|
syl5 |
|- ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( B e. dom card /\ B =/= (/) ) ) -> ( B ~< A -> ( A X. B ) ~~ ( A u. B ) ) ) |
12 |
|
domtri2 |
|- ( ( A e. dom card /\ B e. dom card ) -> ( A ~<_ B <-> -. B ~< A ) ) |
13 |
12
|
ad2ant2r |
|- ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( B e. dom card /\ B =/= (/) ) ) -> ( A ~<_ B <-> -. B ~< A ) ) |
14 |
|
xpcomeng |
|- ( ( A e. dom card /\ B e. dom card ) -> ( A X. B ) ~~ ( B X. A ) ) |
15 |
14
|
ad2ant2r |
|- ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( B e. dom card /\ B =/= (/) ) ) -> ( A X. B ) ~~ ( B X. A ) ) |
16 |
|
simplrl |
|- ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( B e. dom card /\ B =/= (/) ) ) /\ A ~<_ B ) -> B e. dom card ) |
17 |
|
domtr |
|- ( ( _om ~<_ A /\ A ~<_ B ) -> _om ~<_ B ) |
18 |
17
|
ad4ant24 |
|- ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( B e. dom card /\ B =/= (/) ) ) /\ A ~<_ B ) -> _om ~<_ B ) |
19 |
|
infn0 |
|- ( _om ~<_ A -> A =/= (/) ) |
20 |
19
|
ad3antlr |
|- ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( B e. dom card /\ B =/= (/) ) ) /\ A ~<_ B ) -> A =/= (/) ) |
21 |
|
simpr |
|- ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( B e. dom card /\ B =/= (/) ) ) /\ A ~<_ B ) -> A ~<_ B ) |
22 |
|
infxpabs |
|- ( ( ( B e. dom card /\ _om ~<_ B ) /\ ( A =/= (/) /\ A ~<_ B ) ) -> ( B X. A ) ~~ B ) |
23 |
16 18 20 21 22
|
syl22anc |
|- ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( B e. dom card /\ B =/= (/) ) ) /\ A ~<_ B ) -> ( B X. A ) ~~ B ) |
24 |
|
uncom |
|- ( A u. B ) = ( B u. A ) |
25 |
|
infunabs |
|- ( ( B e. dom card /\ _om ~<_ B /\ A ~<_ B ) -> ( B u. A ) ~~ B ) |
26 |
16 18 21 25
|
syl3anc |
|- ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( B e. dom card /\ B =/= (/) ) ) /\ A ~<_ B ) -> ( B u. A ) ~~ B ) |
27 |
24 26
|
eqbrtrid |
|- ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( B e. dom card /\ B =/= (/) ) ) /\ A ~<_ B ) -> ( A u. B ) ~~ B ) |
28 |
27
|
ensymd |
|- ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( B e. dom card /\ B =/= (/) ) ) /\ A ~<_ B ) -> B ~~ ( A u. B ) ) |
29 |
|
entr |
|- ( ( ( B X. A ) ~~ B /\ B ~~ ( A u. B ) ) -> ( B X. A ) ~~ ( A u. B ) ) |
30 |
23 28 29
|
syl2anc |
|- ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( B e. dom card /\ B =/= (/) ) ) /\ A ~<_ B ) -> ( B X. A ) ~~ ( A u. B ) ) |
31 |
|
entr |
|- ( ( ( A X. B ) ~~ ( B X. A ) /\ ( B X. A ) ~~ ( A u. B ) ) -> ( A X. B ) ~~ ( A u. B ) ) |
32 |
15 30 31
|
syl2an2r |
|- ( ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( B e. dom card /\ B =/= (/) ) ) /\ A ~<_ B ) -> ( A X. B ) ~~ ( A u. B ) ) |
33 |
32
|
ex |
|- ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( B e. dom card /\ B =/= (/) ) ) -> ( A ~<_ B -> ( A X. B ) ~~ ( A u. B ) ) ) |
34 |
13 33
|
sylbird |
|- ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( B e. dom card /\ B =/= (/) ) ) -> ( -. B ~< A -> ( A X. B ) ~~ ( A u. B ) ) ) |
35 |
11 34
|
pm2.61d |
|- ( ( ( A e. dom card /\ _om ~<_ A ) /\ ( B e. dom card /\ B =/= (/) ) ) -> ( A X. B ) ~~ ( A u. B ) ) |