Metamath Proof Explorer

Theorem mclsval

Description: The function mapping variables to variable expressions is one-to-one. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses mclsval.d 
|- D = ( mDV ` T )
mclsval.e 
|- E = ( mEx ` T )
mclsval.c 
|- C = ( mCls ` T )
mclsval.1 
|- ( ph -> T e. mFS )
mclsval.2 
|- ( ph -> K C_ D )
mclsval.3 
|- ( ph -> B C_ E )
mclsval.h 
|- H = ( mVH ` T )
mclsval.a 
|- A = ( mAx ` T )
mclsval.s 
|- S = ( mSubst ` T )
mclsval.v 
|- V = ( mVars ` T )
Assertion mclsval 
|- ( ph -> ( K C B ) = |^| { c | ( ( B u. ran H ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. A -> A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) ) } )

Proof

Step Hyp Ref Expression
1 mclsval.d 
 |-  D = ( mDV ` T )
2 mclsval.e 
 |-  E = ( mEx ` T )
3 mclsval.c 
 |-  C = ( mCls ` T )
4 mclsval.1 
 |-  ( ph -> T e. mFS )
5 mclsval.2 
 |-  ( ph -> K C_ D )
6 mclsval.3 
 |-  ( ph -> B C_ E )
7 mclsval.h 
 |-  H = ( mVH ` T )
8 mclsval.a 
 |-  A = ( mAx ` T )
9 mclsval.s 
 |-  S = ( mSubst ` T )
10 mclsval.v 
 |-  V = ( mVars ` T )
11 elex 
 |-  ( T e. mFS -> T e. _V )
12 fveq2 
 |-  ( t = T -> ( mDV ` t ) = ( mDV ` T ) )
13 12 1 eqtr4di 
 |-  ( t = T -> ( mDV ` t ) = D )
14 13 pweqd 
 |-  ( t = T -> ~P ( mDV ` t ) = ~P D )
15 fveq2 
 |-  ( t = T -> ( mEx ` t ) = ( mEx ` T ) )
16 15 2 eqtr4di 
 |-  ( t = T -> ( mEx ` t ) = E )
17 16 pweqd 
 |-  ( t = T -> ~P ( mEx ` t ) = ~P E )
18 fveq2 
 |-  ( t = T -> ( mVH ` t ) = ( mVH ` T ) )
19 18 7 eqtr4di 
 |-  ( t = T -> ( mVH ` t ) = H )
20 19 rneqd 
 |-  ( t = T -> ran ( mVH ` t ) = ran H )
21 20 uneq2d 
 |-  ( t = T -> ( h u. ran ( mVH ` t ) ) = ( h u. ran H ) )
22 21 sseq1d 
 |-  ( t = T -> ( ( h u. ran ( mVH ` t ) ) C_ c <-> ( h u. ran H ) C_ c ) )
23 fveq2 
 |-  ( t = T -> ( mAx ` t ) = ( mAx ` T ) )
24 23 8 eqtr4di 
 |-  ( t = T -> ( mAx ` t ) = A )
25 24 eleq2d 
 |-  ( t = T -> ( <. m , o , p >. e. ( mAx ` t ) <-> <. m , o , p >. e. A ) )
26 fveq2 
 |-  ( t = T -> ( mSubst ` t ) = ( mSubst ` T ) )
27 26 9 eqtr4di 
 |-  ( t = T -> ( mSubst ` t ) = S )
28 27 rneqd 
 |-  ( t = T -> ran ( mSubst ` t ) = ran S )
29 20 uneq2d 
 |-  ( t = T -> ( o u. ran ( mVH ` t ) ) = ( o u. ran H ) )
30 29 imaeq2d 
 |-  ( t = T -> ( s " ( o u. ran ( mVH ` t ) ) ) = ( s " ( o u. ran H ) ) )
31 30 sseq1d 
 |-  ( t = T -> ( ( s " ( o u. ran ( mVH ` t ) ) ) C_ c <-> ( s " ( o u. ran H ) ) C_ c ) )
32 fveq2 
 |-  ( t = T -> ( mVars ` t ) = ( mVars ` T ) )
33 32 10 eqtr4di 
 |-  ( t = T -> ( mVars ` t ) = V )
34 19 fveq1d 
 |-  ( t = T -> ( ( mVH ` t ) ` x ) = ( H ` x ) )
35 34 fveq2d 
 |-  ( t = T -> ( s ` ( ( mVH ` t ) ` x ) ) = ( s ` ( H ` x ) ) )
36 33 35 fveq12d 
 |-  ( t = T -> ( ( mVars ` t ) ` ( s ` ( ( mVH ` t ) ` x ) ) ) = ( V ` ( s ` ( H ` x ) ) ) )
37 19 fveq1d 
 |-  ( t = T -> ( ( mVH ` t ) ` y ) = ( H ` y ) )
38 37 fveq2d 
 |-  ( t = T -> ( s ` ( ( mVH ` t ) ` y ) ) = ( s ` ( H ` y ) ) )
39 33 38 fveq12d 
 |-  ( t = T -> ( ( mVars ` t ) ` ( s ` ( ( mVH ` t ) ` y ) ) ) = ( V ` ( s ` ( H ` y ) ) ) )
40 36 39 xpeq12d 
 |-  ( t = T -> ( ( ( mVars ` t ) ` ( s ` ( ( mVH ` t ) ` x ) ) ) X. ( ( mVars ` t ) ` ( s ` ( ( mVH ` t ) ` y ) ) ) ) = ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) )
41 40 sseq1d 
 |-  ( t = T -> ( ( ( ( mVars ` t ) ` ( s ` ( ( mVH ` t ) ` x ) ) ) X. ( ( mVars ` t ) ` ( s ` ( ( mVH ` t ) ` y ) ) ) ) C_ d <-> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ d ) )
42 41 imbi2d 
 |-  ( t = T -> ( ( x m y -> ( ( ( mVars ` t ) ` ( s ` ( ( mVH ` t ) ` x ) ) ) X. ( ( mVars ` t ) ` ( s ` ( ( mVH ` t ) ` y ) ) ) ) C_ d ) <-> ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ d ) ) )
43 42 2albidv 
 |-  ( t = T -> ( A. x A. y ( x m y -> ( ( ( mVars ` t ) ` ( s ` ( ( mVH ` t ) ` x ) ) ) X. ( ( mVars ` t ) ` ( s ` ( ( mVH ` t ) ` y ) ) ) ) C_ d ) <-> A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ d ) ) )
44 31 43 anbi12d 
 |-  ( t = 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 " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ d ) ) ) )
45 44 imbi1d 
 |-  ( t = 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 ) <-> ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ d ) ) -> ( s ` p ) e. c ) ) )
46 28 45 raleqbidv 
 |-  ( t = 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 ) <-> A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ d ) ) -> ( s ` p ) e. c ) ) )
47 25 46 imbi12d 
 |-  ( t = T -> ( ( <. 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 ) ) <-> ( <. m , o , p >. e. A -> A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ d ) ) -> ( s ` p ) e. c ) ) ) )
48 47 albidv 
 |-  ( t = T -> ( 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 ) ) <-> A. p ( <. m , o , p >. e. A -> A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ d ) ) -> ( s ` p ) e. c ) ) ) )
49 48 2albidv 
 |-  ( t = T -> ( 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 ) ) <-> A. m A. o A. p ( <. m , o , p >. e. A -> A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ d ) ) -> ( s ` p ) e. c ) ) ) )
50 22 49 anbi12d 
 |-  ( t = T -> ( ( ( 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 ) ) ) <-> ( ( h u. ran H ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. A -> A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ d ) ) -> ( s ` p ) e. c ) ) ) ) )
51 50 abbidv 
 |-  ( t = 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 ) ) ) } = { c | ( ( h u. ran H ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. A -> A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ d ) ) -> ( s ` p ) e. c ) ) ) } )
52 51 inteqd 
 |-  ( t = 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 ) ) ) } = |^| { c | ( ( h u. ran H ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. A -> A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ d ) ) -> ( s ` p ) e. c ) ) ) } )
53 14 17 52 mpoeq123dv 
 |-  ( t = 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 ) ) ) } ) = ( d e. ~P D , h e. ~P E |-> |^| { c | ( ( h u. ran H ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. A -> A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ d ) ) -> ( s ` p ) e. c ) ) ) } ) )
54 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 ) ) ) } ) )
55 1 fvexi 
 |-  D e. _V
56 55 pwex 
 |-  ~P D e. _V
57 2 fvexi 
 |-  E e. _V
58 57 pwex 
 |-  ~P E e. _V
59 56 58 mpoex 
 |-  ( d e. ~P D , h e. ~P E |-> |^| { c | ( ( h u. ran H ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. A -> A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ d ) ) -> ( s ` p ) e. c ) ) ) } ) e. _V
60 53 54 59 fvmpt 
 |-  ( T e. _V -> ( mCls ` T ) = ( d e. ~P D , h e. ~P E |-> |^| { c | ( ( h u. ran H ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. A -> A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ d ) ) -> ( s ` p ) e. c ) ) ) } ) )
61 4 11 60 3syl 
 |-  ( ph -> ( mCls ` T ) = ( d e. ~P D , h e. ~P E |-> |^| { c | ( ( h u. ran H ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. A -> A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ d ) ) -> ( s ` p ) e. c ) ) ) } ) )
62 3 61 eqtrid 
 |-  ( ph -> C = ( d e. ~P D , h e. ~P E |-> |^| { c | ( ( h u. ran H ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. A -> A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ d ) ) -> ( s ` p ) e. c ) ) ) } ) )
63 simprr 
 |-  ( ( ph /\ ( d = K /\ h = B ) ) -> h = B )
64 63 uneq1d 
 |-  ( ( ph /\ ( d = K /\ h = B ) ) -> ( h u. ran H ) = ( B u. ran H ) )
65 64 sseq1d 
 |-  ( ( ph /\ ( d = K /\ h = B ) ) -> ( ( h u. ran H ) C_ c <-> ( B u. ran H ) C_ c ) )
66 simprl 
 |-  ( ( ph /\ ( d = K /\ h = B ) ) -> d = K )
67 66 sseq2d 
 |-  ( ( ph /\ ( d = K /\ h = B ) ) -> ( ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ d <-> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ K ) )
68 67 imbi2d 
 |-  ( ( ph /\ ( d = K /\ h = B ) ) -> ( ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ d ) <-> ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ K ) ) )
69 68 2albidv 
 |-  ( ( ph /\ ( d = K /\ h = B ) ) -> ( A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ d ) <-> A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ K ) ) )
70 69 anbi2d 
 |-  ( ( ph /\ ( d = K /\ h = B ) ) -> ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ d ) ) <-> ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ K ) ) ) )
71 70 imbi1d 
 |-  ( ( ph /\ ( d = K /\ h = B ) ) -> ( ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ d ) ) -> ( s ` p ) e. c ) <-> ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) )
72 71 ralbidv 
 |-  ( ( ph /\ ( d = K /\ h = B ) ) -> ( A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ d ) ) -> ( s ` p ) e. c ) <-> A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) )
73 72 imbi2d 
 |-  ( ( ph /\ ( d = K /\ h = B ) ) -> ( ( <. m , o , p >. e. A -> A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ d ) ) -> ( s ` p ) e. c ) ) <-> ( <. m , o , p >. e. A -> A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) ) )
74 73 albidv 
 |-  ( ( ph /\ ( d = K /\ h = B ) ) -> ( A. p ( <. m , o , p >. e. A -> A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ d ) ) -> ( s ` p ) e. c ) ) <-> A. p ( <. m , o , p >. e. A -> A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) ) )
75 74 2albidv 
 |-  ( ( ph /\ ( d = K /\ h = B ) ) -> ( A. m A. o A. p ( <. m , o , p >. e. A -> A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ d ) ) -> ( s ` p ) e. c ) ) <-> A. m A. o A. p ( <. m , o , p >. e. A -> A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) ) )
76 65 75 anbi12d 
 |-  ( ( ph /\ ( d = K /\ h = B ) ) -> ( ( ( h u. ran H ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. A -> A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ d ) ) -> ( s ` p ) e. c ) ) ) <-> ( ( B u. ran H ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. A -> A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) ) ) )
77 76 abbidv 
 |-  ( ( ph /\ ( d = K /\ h = B ) ) -> { c | ( ( h u. ran H ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. A -> A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ d ) ) -> ( s ` p ) e. c ) ) ) } = { c | ( ( B u. ran H ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. A -> A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) ) } )
78 77 inteqd 
 |-  ( ( ph /\ ( d = K /\ h = B ) ) -> |^| { c | ( ( h u. ran H ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. A -> A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ d ) ) -> ( s ` p ) e. c ) ) ) } = |^| { c | ( ( B u. ran H ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. A -> A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) ) } )
79 55 elpw2 
 |-  ( K e. ~P D <-> K C_ D )
80 5 79 sylibr 
 |-  ( ph -> K e. ~P D )
81 57 elpw2 
 |-  ( B e. ~P E <-> B C_ E )
82 6 81 sylibr 
 |-  ( ph -> B e. ~P E )
83 1 2 3 4 5 6 7 8 9 10 mclsssvlem 
 |-  ( ph -> |^| { c | ( ( B u. ran H ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. A -> A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) ) } C_ E )
84 57 ssex 
 |-  ( |^| { c | ( ( B u. ran H ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. A -> A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) ) } C_ E -> |^| { c | ( ( B u. ran H ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. A -> A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) ) } e. _V )
85 83 84 syl 
 |-  ( ph -> |^| { c | ( ( B u. ran H ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. A -> A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) ) } e. _V )
86 62 78 80 82 85 ovmpod 
 |-  ( ph -> ( K C B ) = |^| { c | ( ( B u. ran H ) C_ c /\ A. m A. o A. p ( <. m , o , p >. e. A -> A. s e. ran S ( ( ( s " ( o u. ran H ) ) C_ c /\ A. x A. y ( x m y -> ( ( V ` ( s ` ( H ` x ) ) ) X. ( V ` ( s ` ( H ` y ) ) ) ) C_ K ) ) -> ( s ` p ) e. c ) ) ) } )