Step |
Hyp |
Ref |
Expression |
1 |
|
xpcomeng |
|- ( ( A e. On /\ B e. On ) -> ( A X. B ) ~~ ( B X. A ) ) |
2 |
|
xpexg |
|- ( ( B e. On /\ A e. On ) -> ( B X. A ) e. _V ) |
3 |
2
|
ancoms |
|- ( ( A e. On /\ B e. On ) -> ( B X. A ) e. _V ) |
4 |
|
omcl |
|- ( ( A e. On /\ B e. On ) -> ( A .o B ) e. On ) |
5 |
|
eqid |
|- ( x e. B , y e. A |-> ( ( A .o x ) +o y ) ) = ( x e. B , y e. A |-> ( ( A .o x ) +o y ) ) |
6 |
5
|
omxpenlem |
|- ( ( A e. On /\ B e. On ) -> ( x e. B , y e. A |-> ( ( A .o x ) +o y ) ) : ( B X. A ) -1-1-onto-> ( A .o B ) ) |
7 |
|
f1oen2g |
|- ( ( ( B X. A ) e. _V /\ ( A .o B ) e. On /\ ( x e. B , y e. A |-> ( ( A .o x ) +o y ) ) : ( B X. A ) -1-1-onto-> ( A .o B ) ) -> ( B X. A ) ~~ ( A .o B ) ) |
8 |
3 4 6 7
|
syl3anc |
|- ( ( A e. On /\ B e. On ) -> ( B X. A ) ~~ ( A .o B ) ) |
9 |
|
entr |
|- ( ( ( A X. B ) ~~ ( B X. A ) /\ ( B X. A ) ~~ ( A .o B ) ) -> ( A X. B ) ~~ ( A .o B ) ) |
10 |
1 8 9
|
syl2anc |
|- ( ( A e. On /\ B e. On ) -> ( A X. B ) ~~ ( A .o B ) ) |
11 |
10
|
ensymd |
|- ( ( A e. On /\ B e. On ) -> ( A .o B ) ~~ ( A X. B ) ) |