Step |
Hyp |
Ref |
Expression |
1 |
|
xpcomeng |
โข ( ( ๐ด โ On โง ๐ต โ On ) โ ( ๐ด ร ๐ต ) โ ( ๐ต ร ๐ด ) ) |
2 |
|
xpexg |
โข ( ( ๐ต โ On โง ๐ด โ On ) โ ( ๐ต ร ๐ด ) โ V ) |
3 |
2
|
ancoms |
โข ( ( ๐ด โ On โง ๐ต โ On ) โ ( ๐ต ร ๐ด ) โ V ) |
4 |
|
omcl |
โข ( ( ๐ด โ On โง ๐ต โ On ) โ ( ๐ด ยทo ๐ต ) โ On ) |
5 |
|
eqid |
โข ( ๐ฅ โ ๐ต , ๐ฆ โ ๐ด โฆ ( ( ๐ด ยทo ๐ฅ ) +o ๐ฆ ) ) = ( ๐ฅ โ ๐ต , ๐ฆ โ ๐ด โฆ ( ( ๐ด ยทo ๐ฅ ) +o ๐ฆ ) ) |
6 |
5
|
omxpenlem |
โข ( ( ๐ด โ On โง ๐ต โ On ) โ ( ๐ฅ โ ๐ต , ๐ฆ โ ๐ด โฆ ( ( ๐ด ยทo ๐ฅ ) +o ๐ฆ ) ) : ( ๐ต ร ๐ด ) โ1-1-ontoโ ( ๐ด ยทo ๐ต ) ) |
7 |
|
f1oen2g |
โข ( ( ( ๐ต ร ๐ด ) โ V โง ( ๐ด ยทo ๐ต ) โ On โง ( ๐ฅ โ ๐ต , ๐ฆ โ ๐ด โฆ ( ( ๐ด ยทo ๐ฅ ) +o ๐ฆ ) ) : ( ๐ต ร ๐ด ) โ1-1-ontoโ ( ๐ด ยทo ๐ต ) ) โ ( ๐ต ร ๐ด ) โ ( ๐ด ยทo ๐ต ) ) |
8 |
3 4 6 7
|
syl3anc |
โข ( ( ๐ด โ On โง ๐ต โ On ) โ ( ๐ต ร ๐ด ) โ ( ๐ด ยทo ๐ต ) ) |
9 |
|
entr |
โข ( ( ( ๐ด ร ๐ต ) โ ( ๐ต ร ๐ด ) โง ( ๐ต ร ๐ด ) โ ( ๐ด ยทo ๐ต ) ) โ ( ๐ด ร ๐ต ) โ ( ๐ด ยทo ๐ต ) ) |
10 |
1 8 9
|
syl2anc |
โข ( ( ๐ด โ On โง ๐ต โ On ) โ ( ๐ด ร ๐ต ) โ ( ๐ด ยทo ๐ต ) ) |
11 |
10
|
ensymd |
โข ( ( ๐ด โ On โง ๐ต โ On ) โ ( ๐ด ยทo ๐ต ) โ ( ๐ด ร ๐ต ) ) |