Step |
Hyp |
Ref |
Expression |
0 |
|
cpadd |
|- +P |
1 |
|
vl |
|- l |
2 |
|
cvv |
|- _V |
3 |
|
vm |
|- m |
4 |
|
catm |
|- Atoms |
5 |
1
|
cv |
|- l |
6 |
5 4
|
cfv |
|- ( Atoms ` l ) |
7 |
6
|
cpw |
|- ~P ( Atoms ` l ) |
8 |
|
vn |
|- n |
9 |
3
|
cv |
|- m |
10 |
8
|
cv |
|- n |
11 |
9 10
|
cun |
|- ( m u. n ) |
12 |
|
vp |
|- p |
13 |
|
vq |
|- q |
14 |
|
vr |
|- r |
15 |
12
|
cv |
|- p |
16 |
|
cple |
|- le |
17 |
5 16
|
cfv |
|- ( le ` l ) |
18 |
13
|
cv |
|- q |
19 |
|
cjn |
|- join |
20 |
5 19
|
cfv |
|- ( join ` l ) |
21 |
14
|
cv |
|- r |
22 |
18 21 20
|
co |
|- ( q ( join ` l ) r ) |
23 |
15 22 17
|
wbr |
|- p ( le ` l ) ( q ( join ` l ) r ) |
24 |
23 14 10
|
wrex |
|- E. r e. n p ( le ` l ) ( q ( join ` l ) r ) |
25 |
24 13 9
|
wrex |
|- E. q e. m E. r e. n p ( le ` l ) ( q ( join ` l ) r ) |
26 |
25 12 6
|
crab |
|- { p e. ( Atoms ` l ) | E. q e. m E. r e. n p ( le ` l ) ( q ( join ` l ) r ) } |
27 |
11 26
|
cun |
|- ( ( m u. n ) u. { p e. ( Atoms ` l ) | E. q e. m E. r e. n p ( le ` l ) ( q ( join ` l ) r ) } ) |
28 |
3 8 7 7 27
|
cmpo |
|- ( m e. ~P ( Atoms ` l ) , n e. ~P ( Atoms ` l ) |-> ( ( m u. n ) u. { p e. ( Atoms ` l ) | E. q e. m E. r e. n p ( le ` l ) ( q ( join ` l ) r ) } ) ) |
29 |
1 2 28
|
cmpt |
|- ( l e. _V |-> ( m e. ~P ( Atoms ` l ) , n e. ~P ( Atoms ` l ) |-> ( ( m u. n ) u. { p e. ( Atoms ` l ) | E. q e. m E. r e. n p ( le ` l ) ( q ( join ` l ) r ) } ) ) ) |
30 |
0 29
|
wceq |
|- +P = ( l e. _V |-> ( m e. ~P ( Atoms ` l ) , n e. ~P ( Atoms ` l ) |-> ( ( m u. n ) u. { p e. ( Atoms ` l ) | E. q e. m E. r e. n p ( le ` l ) ( q ( join ` l ) r ) } ) ) ) |