Step |
Hyp |
Ref |
Expression |
1 |
|
ustund.1 |
|- ( ph -> ( A X. A ) C_ V ) |
2 |
|
ustund.2 |
|- ( ph -> ( B X. B ) C_ V ) |
3 |
|
ustund.3 |
|- ( ph -> ( A i^i B ) =/= (/) ) |
4 |
|
xpco |
|- ( ( A i^i B ) =/= (/) -> ( ( ( A i^i B ) X. ( A u. B ) ) o. ( ( A u. B ) X. ( A i^i B ) ) ) = ( ( A u. B ) X. ( A u. B ) ) ) |
5 |
3 4
|
syl |
|- ( ph -> ( ( ( A i^i B ) X. ( A u. B ) ) o. ( ( A u. B ) X. ( A i^i B ) ) ) = ( ( A u. B ) X. ( A u. B ) ) ) |
6 |
|
xpundi |
|- ( ( A i^i B ) X. ( A u. B ) ) = ( ( ( A i^i B ) X. A ) u. ( ( A i^i B ) X. B ) ) |
7 |
|
xpindir |
|- ( ( A i^i B ) X. A ) = ( ( A X. A ) i^i ( B X. A ) ) |
8 |
|
inss1 |
|- ( ( A X. A ) i^i ( B X. A ) ) C_ ( A X. A ) |
9 |
8 1
|
sstrid |
|- ( ph -> ( ( A X. A ) i^i ( B X. A ) ) C_ V ) |
10 |
7 9
|
eqsstrid |
|- ( ph -> ( ( A i^i B ) X. A ) C_ V ) |
11 |
|
xpindir |
|- ( ( A i^i B ) X. B ) = ( ( A X. B ) i^i ( B X. B ) ) |
12 |
|
inss2 |
|- ( ( A X. B ) i^i ( B X. B ) ) C_ ( B X. B ) |
13 |
12 2
|
sstrid |
|- ( ph -> ( ( A X. B ) i^i ( B X. B ) ) C_ V ) |
14 |
11 13
|
eqsstrid |
|- ( ph -> ( ( A i^i B ) X. B ) C_ V ) |
15 |
10 14
|
unssd |
|- ( ph -> ( ( ( A i^i B ) X. A ) u. ( ( A i^i B ) X. B ) ) C_ V ) |
16 |
6 15
|
eqsstrid |
|- ( ph -> ( ( A i^i B ) X. ( A u. B ) ) C_ V ) |
17 |
|
xpundir |
|- ( ( A u. B ) X. ( A i^i B ) ) = ( ( A X. ( A i^i B ) ) u. ( B X. ( A i^i B ) ) ) |
18 |
|
xpindi |
|- ( A X. ( A i^i B ) ) = ( ( A X. A ) i^i ( A X. B ) ) |
19 |
|
inss1 |
|- ( ( A X. A ) i^i ( A X. B ) ) C_ ( A X. A ) |
20 |
19 1
|
sstrid |
|- ( ph -> ( ( A X. A ) i^i ( A X. B ) ) C_ V ) |
21 |
18 20
|
eqsstrid |
|- ( ph -> ( A X. ( A i^i B ) ) C_ V ) |
22 |
|
xpindi |
|- ( B X. ( A i^i B ) ) = ( ( B X. A ) i^i ( B X. B ) ) |
23 |
|
inss2 |
|- ( ( B X. A ) i^i ( B X. B ) ) C_ ( B X. B ) |
24 |
23 2
|
sstrid |
|- ( ph -> ( ( B X. A ) i^i ( B X. B ) ) C_ V ) |
25 |
22 24
|
eqsstrid |
|- ( ph -> ( B X. ( A i^i B ) ) C_ V ) |
26 |
21 25
|
unssd |
|- ( ph -> ( ( A X. ( A i^i B ) ) u. ( B X. ( A i^i B ) ) ) C_ V ) |
27 |
17 26
|
eqsstrid |
|- ( ph -> ( ( A u. B ) X. ( A i^i B ) ) C_ V ) |
28 |
16 27
|
coss12d |
|- ( ph -> ( ( ( A i^i B ) X. ( A u. B ) ) o. ( ( A u. B ) X. ( A i^i B ) ) ) C_ ( V o. V ) ) |
29 |
5 28
|
eqsstrrd |
|- ( ph -> ( ( A u. B ) X. ( A u. B ) ) C_ ( V o. V ) ) |