Step |
Hyp |
Ref |
Expression |
1 |
|
mclsval.d |
|- D = ( mDV ` T ) |
2 |
|
mclsval.e |
|- E = ( mEx ` T ) |
3 |
|
mclsval.c |
|- C = ( mCls ` T ) |
4 |
|
n0i |
|- ( A e. ( K C B ) -> -. ( K C B ) = (/) ) |
5 |
|
fvprc |
|- ( -. T e. _V -> ( mCls ` T ) = (/) ) |
6 |
3 5
|
syl5eq |
|- ( -. T e. _V -> C = (/) ) |
7 |
6
|
oveqd |
|- ( -. T e. _V -> ( K C B ) = ( K (/) B ) ) |
8 |
|
0ov |
|- ( K (/) B ) = (/) |
9 |
7 8
|
eqtrdi |
|- ( -. T e. _V -> ( K C B ) = (/) ) |
10 |
4 9
|
nsyl2 |
|- ( A e. ( K C B ) -> T e. _V ) |
11 |
|
fveq2 |
|- ( t = T -> ( mCls ` t ) = ( mCls ` T ) ) |
12 |
11 3
|
eqtr4di |
|- ( t = T -> ( mCls ` t ) = C ) |
13 |
12
|
oveqd |
|- ( t = T -> ( K ( mCls ` t ) B ) = ( K C B ) ) |
14 |
13
|
eleq2d |
|- ( t = T -> ( A e. ( K ( mCls ` t ) B ) <-> A e. ( K C B ) ) ) |
15 |
|
fvex |
|- ( mDV ` t ) e. _V |
16 |
15
|
elpw2 |
|- ( K e. ~P ( mDV ` t ) <-> K C_ ( mDV ` t ) ) |
17 |
|
fveq2 |
|- ( t = T -> ( mDV ` t ) = ( mDV ` T ) ) |
18 |
17 1
|
eqtr4di |
|- ( t = T -> ( mDV ` t ) = D ) |
19 |
18
|
sseq2d |
|- ( t = T -> ( K C_ ( mDV ` t ) <-> K C_ D ) ) |
20 |
16 19
|
syl5bb |
|- ( t = T -> ( K e. ~P ( mDV ` t ) <-> K C_ D ) ) |
21 |
|
fvex |
|- ( mEx ` t ) e. _V |
22 |
21
|
elpw2 |
|- ( B e. ~P ( mEx ` t ) <-> B C_ ( mEx ` t ) ) |
23 |
|
fveq2 |
|- ( t = T -> ( mEx ` t ) = ( mEx ` T ) ) |
24 |
23 2
|
eqtr4di |
|- ( t = T -> ( mEx ` t ) = E ) |
25 |
24
|
sseq2d |
|- ( t = T -> ( B C_ ( mEx ` t ) <-> B C_ E ) ) |
26 |
22 25
|
syl5bb |
|- ( t = T -> ( B e. ~P ( mEx ` t ) <-> B C_ E ) ) |
27 |
20 26
|
anbi12d |
|- ( t = T -> ( ( K e. ~P ( mDV ` t ) /\ B e. ~P ( mEx ` t ) ) <-> ( K C_ D /\ B C_ E ) ) ) |
28 |
14 27
|
imbi12d |
|- ( t = T -> ( ( A e. ( K ( mCls ` t ) B ) -> ( K e. ~P ( mDV ` t ) /\ B e. ~P ( mEx ` t ) ) ) <-> ( A e. ( K C B ) -> ( K C_ D /\ B C_ E ) ) ) ) |
29 |
|
vex |
|- t e. _V |
30 |
15
|
pwex |
|- ~P ( mDV ` t ) e. _V |
31 |
21
|
pwex |
|- ~P ( mEx ` t ) e. _V |
32 |
30 31
|
mpoex |
|- ( d e. ~P ( mDV ` t ) , h e. ~P ( mEx ` t ) |-> |^| { c | ( ( h u. ran ( mVH ` t ) ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. ( mAx ` t ) -> A. s e. ran ( mSubst ` t ) ( ( ( s " ( o u. ran ( mVH ` t ) ) ) C_ c /\ A. x A. y ( x m y -> ( ( ( mVars ` t ) ` ( s ` ( ( mVH ` t ) ` x ) ) ) X. ( ( mVars ` t ) ` ( s ` ( ( mVH ` t ) ` y ) ) ) ) C_ d ) ) -> ( s ` p ) e. c ) ) ) } ) e. _V |
33 |
|
df-mcls |
|- mCls = ( t e. _V |-> ( d e. ~P ( mDV ` t ) , h e. ~P ( mEx ` t ) |-> |^| { c | ( ( h u. ran ( mVH ` t ) ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. ( mAx ` t ) -> A. s e. ran ( mSubst ` t ) ( ( ( s " ( o u. ran ( mVH ` t ) ) ) C_ c /\ A. x A. y ( x m y -> ( ( ( mVars ` t ) ` ( s ` ( ( mVH ` t ) ` x ) ) ) X. ( ( mVars ` t ) ` ( s ` ( ( mVH ` t ) ` y ) ) ) ) C_ d ) ) -> ( s ` p ) e. c ) ) ) } ) ) |
34 |
33
|
fvmpt2 |
|- ( ( t e. _V /\ ( d e. ~P ( mDV ` t ) , h e. ~P ( mEx ` t ) |-> |^| { c | ( ( h u. ran ( mVH ` t ) ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. ( mAx ` t ) -> A. s e. ran ( mSubst ` t ) ( ( ( s " ( o u. ran ( mVH ` t ) ) ) C_ c /\ A. x A. y ( x m y -> ( ( ( mVars ` t ) ` ( s ` ( ( mVH ` t ) ` x ) ) ) X. ( ( mVars ` t ) ` ( s ` ( ( mVH ` t ) ` y ) ) ) ) C_ d ) ) -> ( s ` p ) e. c ) ) ) } ) e. _V ) -> ( mCls ` t ) = ( d e. ~P ( mDV ` t ) , h e. ~P ( mEx ` t ) |-> |^| { c | ( ( h u. ran ( mVH ` t ) ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. ( mAx ` t ) -> A. s e. ran ( mSubst ` t ) ( ( ( s " ( o u. ran ( mVH ` t ) ) ) C_ c /\ A. x A. y ( x m y -> ( ( ( mVars ` t ) ` ( s ` ( ( mVH ` t ) ` x ) ) ) X. ( ( mVars ` t ) ` ( s ` ( ( mVH ` t ) ` y ) ) ) ) C_ d ) ) -> ( s ` p ) e. c ) ) ) } ) ) |
35 |
29 32 34
|
mp2an |
|- ( mCls ` t ) = ( d e. ~P ( mDV ` t ) , h e. ~P ( mEx ` t ) |-> |^| { c | ( ( h u. ran ( mVH ` t ) ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. ( mAx ` t ) -> A. s e. ran ( mSubst ` t ) ( ( ( s " ( o u. ran ( mVH ` t ) ) ) C_ c /\ A. x A. y ( x m y -> ( ( ( mVars ` t ) ` ( s ` ( ( mVH ` t ) ` x ) ) ) X. ( ( mVars ` t ) ` ( s ` ( ( mVH ` t ) ` y ) ) ) ) C_ d ) ) -> ( s ` p ) e. c ) ) ) } ) |
36 |
35
|
elmpocl |
|- ( A e. ( K ( mCls ` t ) B ) -> ( K e. ~P ( mDV ` t ) /\ B e. ~P ( mEx ` t ) ) ) |
37 |
28 36
|
vtoclg |
|- ( T e. _V -> ( A e. ( K C B ) -> ( K C_ D /\ B C_ E ) ) ) |
38 |
10 37
|
mpcom |
|- ( A e. ( K C B ) -> ( K C_ D /\ B C_ E ) ) |
39 |
38
|
simpld |
|- ( A e. ( K C B ) -> K C_ D ) |
40 |
38
|
simprd |
|- ( A e. ( K C B ) -> B C_ E ) |
41 |
10 39 40
|
3jca |
|- ( A e. ( K C B ) -> ( T e. _V /\ K C_ D /\ B C_ E ) ) |