| Step |
Hyp |
Ref |
Expression |
| 1 |
|
xpeq1 |
|- ( A = (/) -> ( A X. A ) = ( (/) X. A ) ) |
| 2 |
|
0xp |
|- ( (/) X. A ) = (/) |
| 3 |
1 2
|
eqtrdi |
|- ( A = (/) -> ( A X. A ) = (/) ) |
| 4 |
|
unieq |
|- ( ( A X. A ) = (/) -> U. ( A X. A ) = U. (/) ) |
| 5 |
4
|
unieqd |
|- ( ( A X. A ) = (/) -> U. U. ( A X. A ) = U. U. (/) ) |
| 6 |
|
uni0 |
|- U. (/) = (/) |
| 7 |
6
|
unieqi |
|- U. U. (/) = U. (/) |
| 8 |
7 6
|
eqtri |
|- U. U. (/) = (/) |
| 9 |
|
eqtr |
|- ( ( U. U. ( A X. A ) = U. U. (/) /\ U. U. (/) = (/) ) -> U. U. ( A X. A ) = (/) ) |
| 10 |
|
eqtr |
|- ( ( U. U. ( A X. A ) = (/) /\ (/) = A ) -> U. U. ( A X. A ) = A ) |
| 11 |
10
|
expcom |
|- ( (/) = A -> ( U. U. ( A X. A ) = (/) -> U. U. ( A X. A ) = A ) ) |
| 12 |
11
|
eqcoms |
|- ( A = (/) -> ( U. U. ( A X. A ) = (/) -> U. U. ( A X. A ) = A ) ) |
| 13 |
9 12
|
syl5com |
|- ( ( U. U. ( A X. A ) = U. U. (/) /\ U. U. (/) = (/) ) -> ( A = (/) -> U. U. ( A X. A ) = A ) ) |
| 14 |
5 8 13
|
sylancl |
|- ( ( A X. A ) = (/) -> ( A = (/) -> U. U. ( A X. A ) = A ) ) |
| 15 |
3 14
|
mpcom |
|- ( A = (/) -> U. U. ( A X. A ) = A ) |
| 16 |
|
df-ne |
|- ( A =/= (/) <-> -. A = (/) ) |
| 17 |
|
xpnz |
|- ( ( A =/= (/) /\ A =/= (/) ) <-> ( A X. A ) =/= (/) ) |
| 18 |
|
unixp |
|- ( ( A X. A ) =/= (/) -> U. U. ( A X. A ) = ( A u. A ) ) |
| 19 |
|
unidm |
|- ( A u. A ) = A |
| 20 |
18 19
|
eqtrdi |
|- ( ( A X. A ) =/= (/) -> U. U. ( A X. A ) = A ) |
| 21 |
17 20
|
sylbi |
|- ( ( A =/= (/) /\ A =/= (/) ) -> U. U. ( A X. A ) = A ) |
| 22 |
16 16 21
|
sylancbr |
|- ( -. A = (/) -> U. U. ( A X. A ) = A ) |
| 23 |
15 22
|
pm2.61i |
|- U. U. ( A X. A ) = A |