Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  mclsval Structured version   Unicode version

Theorem mclsval 29190
Description: The function mapping variables to variable expressions is one-to-one. (Contributed by Mario Carneiro, 18-Jul-2016.)
Hypotheses
Ref Expression
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
Ref Expression
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 ) ) ) } )
Distinct variable groups:    m, c,
o, p, s, E   
x, c, H, m, o, p, s    y,
c, B, m, o, p, s, x    C, m, o, p, s, x    A, c, m, o, p, s    S, c, s, x, y    T, c, m, o, p, s, x, y    ph, c, m, o, p, s, x, y    V, c, x    K, c, m, o, p, s, x, y
Allowed substitution hints:    A( x, y)    C( y, c)    D( x, y, m, o, s, p, c)    S( m, o, p)    E( x, y)    H( y)    V( y, m, o, s, p)

Proof of Theorem mclsval
Dummy variables  h  d  t are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mclsval.c . . 3  |-  C  =  (mCls `  T )
2 mclsval.1 . . . 4  |-  ( ph  ->  T  e. mFS )
3 elex 3115 . . . 4  |-  ( T  e. mFS  ->  T  e.  _V )
4 fveq2 5848 . . . . . . . 8  |-  ( t  =  T  ->  (mDV `  t )  =  (mDV
`  T ) )
5 mclsval.d . . . . . . . 8  |-  D  =  (mDV `  T )
64, 5syl6eqr 2513 . . . . . . 7  |-  ( t  =  T  ->  (mDV `  t )  =  D )
76pweqd 4004 . . . . . 6  |-  ( t  =  T  ->  ~P (mDV `  t )  =  ~P D )
8 fveq2 5848 . . . . . . . 8  |-  ( t  =  T  ->  (mEx `  t )  =  (mEx
`  T ) )
9 mclsval.e . . . . . . . 8  |-  E  =  (mEx `  T )
108, 9syl6eqr 2513 . . . . . . 7  |-  ( t  =  T  ->  (mEx `  t )  =  E )
1110pweqd 4004 . . . . . 6  |-  ( t  =  T  ->  ~P (mEx `  t )  =  ~P E )
12 fveq2 5848 . . . . . . . . . . . . 13  |-  ( t  =  T  ->  (mVH `  t )  =  (mVH
`  T ) )
13 mclsval.h . . . . . . . . . . . . 13  |-  H  =  (mVH `  T )
1412, 13syl6eqr 2513 . . . . . . . . . . . 12  |-  ( t  =  T  ->  (mVH `  t )  =  H )
1514rneqd 5219 . . . . . . . . . . 11  |-  ( t  =  T  ->  ran  (mVH `  t )  =  ran  H )
1615uneq2d 3644 . . . . . . . . . 10  |-  ( t  =  T  ->  (
h  u.  ran  (mVH `  t ) )  =  ( h  u.  ran  H ) )
1716sseq1d 3516 . . . . . . . . 9  |-  ( t  =  T  ->  (
( h  u.  ran  (mVH `  t ) ) 
C_  c  <->  ( h  u.  ran  H )  C_  c ) )
18 fveq2 5848 . . . . . . . . . . . . . 14  |-  ( t  =  T  ->  (mAx `  t )  =  (mAx
`  T ) )
19 mclsval.a . . . . . . . . . . . . . 14  |-  A  =  (mAx `  T )
2018, 19syl6eqr 2513 . . . . . . . . . . . . 13  |-  ( t  =  T  ->  (mAx `  t )  =  A )
2120eleq2d 2524 . . . . . . . . . . . 12  |-  ( t  =  T  ->  ( <. m ,  o ,  p >.  e.  (mAx `  t )  <->  <. m ,  o ,  p >.  e.  A ) )
22 fveq2 5848 . . . . . . . . . . . . . . 15  |-  ( t  =  T  ->  (mSubst `  t )  =  (mSubst `  T ) )
23 mclsval.s . . . . . . . . . . . . . . 15  |-  S  =  (mSubst `  T )
2422, 23syl6eqr 2513 . . . . . . . . . . . . . 14  |-  ( t  =  T  ->  (mSubst `  t )  =  S )
2524rneqd 5219 . . . . . . . . . . . . 13  |-  ( t  =  T  ->  ran  (mSubst `  t )  =  ran  S )
2615uneq2d 3644 . . . . . . . . . . . . . . . . 17  |-  ( t  =  T  ->  (
o  u.  ran  (mVH `  t ) )  =  ( o  u.  ran  H ) )
2726imaeq2d 5325 . . . . . . . . . . . . . . . 16  |-  ( t  =  T  ->  (
s " ( o  u.  ran  (mVH `  t ) ) )  =  ( s "
( o  u.  ran  H ) ) )
2827sseq1d 3516 . . . . . . . . . . . . . . 15  |-  ( t  =  T  ->  (
( s " (
o  u.  ran  (mVH `  t ) ) ) 
C_  c  <->  ( s " ( o  u. 
ran  H ) ) 
C_  c ) )
29 fveq2 5848 . . . . . . . . . . . . . . . . . . . . 21  |-  ( t  =  T  ->  (mVars `  t )  =  (mVars `  T ) )
30 mclsval.v . . . . . . . . . . . . . . . . . . . . 21  |-  V  =  (mVars `  T )
3129, 30syl6eqr 2513 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  =  T  ->  (mVars `  t )  =  V )
3214fveq1d 5850 . . . . . . . . . . . . . . . . . . . . 21  |-  ( t  =  T  ->  (
(mVH `  t ) `  x )  =  ( H `  x ) )
3332fveq2d 5852 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  =  T  ->  (
s `  ( (mVH `  t ) `  x
) )  =  ( s `  ( H `
 x ) ) )
3431, 33fveq12d 5854 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  T  ->  (
(mVars `  t ) `  ( s `  (
(mVH `  t ) `  x ) ) )  =  ( V `  ( s `  ( H `  x )
) ) )
3514fveq1d 5850 . . . . . . . . . . . . . . . . . . . . 21  |-  ( t  =  T  ->  (
(mVH `  t ) `  y )  =  ( H `  y ) )
3635fveq2d 5852 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  =  T  ->  (
s `  ( (mVH `  t ) `  y
) )  =  ( s `  ( H `
 y ) ) )
3731, 36fveq12d 5854 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  T  ->  (
(mVars `  t ) `  ( s `  (
(mVH `  t ) `  y ) ) )  =  ( V `  ( s `  ( H `  y )
) ) )
3834, 37xpeq12d 5013 . . . . . . . . . . . . . . . . . 18  |-  ( t  =  T  ->  (
( (mVars `  t
) `  ( s `  ( (mVH `  t
) `  x )
) )  X.  (
(mVars `  t ) `  ( s `  (
(mVH `  t ) `  y ) ) ) )  =  ( ( V `  ( s `
 ( H `  x ) ) )  X.  ( V `  ( s `  ( H `  y )
) ) ) )
3938sseq1d 3516 . . . . . . . . . . . . . . . . 17  |-  ( 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 ) )
4039imbi2d 314 . . . . . . . . . . . . . . . 16  |-  ( 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 ) ) )
41402albidv 1720 . . . . . . . . . . . . . . 15  |-  ( 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 )
) )
4228, 41anbi12d 708 . . . . . . . . . . . . . 14  |-  ( 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 ) ) ) )
4342imbi1d 315 . . . . . . . . . . . . 13  |-  ( 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 ) ) )
4425, 43raleqbidv 3065 . . . . . . . . . . . 12  |-  ( 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 ) ) )
4521, 44imbi12d 318 . . . . . . . . . . 11  |-  ( 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 ) ) ) )
4645albidv 1718 . . . . . . . . . 10  |-  ( 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 ) ) ) )
47462albidv 1720 . . . . . . . . 9  |-  ( 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 ) ) ) )
4817, 47anbi12d 708 . . . . . . . 8  |-  ( 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 ) ) ) ) )
4948abbidv 2590 . . . . . . 7  |-  ( 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 ) ) ) } )
5049inteqd 4276 . . . . . 6  |-  ( 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 ) ) ) } )
517, 11, 50mpt2eq123dv 6332 . . . . 5  |-  ( 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 ) ) ) } ) )
52 df-mcls 29124 . . . . 5  |- 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 ) ) ) } ) )
53 fvex 5858 . . . . . . . 8  |-  (mDV `  T )  e.  _V
545, 53eqeltri 2538 . . . . . . 7  |-  D  e. 
_V
5554pwex 4620 . . . . . 6  |-  ~P D  e.  _V
56 fvex 5858 . . . . . . . 8  |-  (mEx `  T )  e.  _V
579, 56eqeltri 2538 . . . . . . 7  |-  E  e. 
_V
5857pwex 4620 . . . . . 6  |-  ~P E  e.  _V
5955, 58mpt2ex 6850 . . . . 5  |-  ( 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
6051, 52, 59fvmpt 5931 . . . 4  |-  ( 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 ) ) ) } ) )
612, 3, 603syl 20 . . 3  |-  ( 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 ) ) ) } ) )
621, 61syl5eq 2507 . 2  |-  ( 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 755 . . . . . . 7  |-  ( (
ph  /\  ( d  =  K  /\  h  =  B ) )  ->  h  =  B )
6463uneq1d 3643 . . . . . 6  |-  ( (
ph  /\  ( d  =  K  /\  h  =  B ) )  -> 
( h  u.  ran  H )  =  ( B  u.  ran  H ) )
6564sseq1d 3516 . . . . 5  |-  ( (
ph  /\  ( d  =  K  /\  h  =  B ) )  -> 
( ( h  u. 
ran  H )  C_  c 
<->  ( B  u.  ran  H )  C_  c )
)
66 simprl 754 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( d  =  K  /\  h  =  B ) )  -> 
d  =  K )
6766sseq2d 3517 . . . . . . . . . . . . 13  |-  ( (
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 )
)
6867imbi2d 314 . . . . . . . . . . . 12  |-  ( (
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 ) ) )
69682albidv 1720 . . . . . . . . . . 11  |-  ( (
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 ) ) )
7069anbi2d 701 . . . . . . . . . 10  |-  ( (
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 ) ) ) )
7170imbi1d 315 . . . . . . . . 9  |-  ( (
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 ) ) )
7271ralbidv 2893 . . . . . . . 8  |-  ( (
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 ) ) )
7372imbi2d 314 . . . . . . 7  |-  ( (
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 ) ) ) )
7473albidv 1718 . . . . . 6  |-  ( (
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 ) ) ) )
75742albidv 1720 . . . . 5  |-  ( (
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 ) ) ) )
7665, 75anbi12d 708 . . . 4  |-  ( (
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 ) ) ) ) )
7776abbidv 2590 . . 3  |-  ( (
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 ) ) ) } )
7877inteqd 4276 . 2  |-  ( (
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 mclsval.2 . . 3  |-  ( ph  ->  K  C_  D )
8054elpw2 4601 . . 3  |-  ( K  e.  ~P D  <->  K  C_  D
)
8179, 80sylibr 212 . 2  |-  ( ph  ->  K  e.  ~P D
)
82 mclsval.3 . . 3  |-  ( ph  ->  B  C_  E )
8357elpw2 4601 . . 3  |-  ( B  e.  ~P E  <->  B  C_  E
)
8482, 83sylibr 212 . 2  |-  ( ph  ->  B  e.  ~P E
)
855, 9, 1, 2, 79, 82, 13, 19, 23, 30mclsssvlem 29189 . . 3  |-  ( 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 )
8657ssex 4581 . . 3  |-  ( |^| { 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 )
8785, 86syl 16 . 2  |-  ( 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 )
8862, 78, 81, 84, 87ovmpt2d 6403 1  |-  ( 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 ) ) ) } )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367   A.wal 1396    = wceq 1398    e. wcel 1823   {cab 2439   A.wral 2804   _Vcvv 3106    u. cun 3459    C_ wss 3461   ~Pcpw 3999   <.cotp 4024   |^|cint 4271   class class class wbr 4439    X. cxp 4986   ran crn 4989   "cima 4991   ` cfv 5570  (class class class)co 6270    |-> cmpt2 6272  mAxcmax 29092  mExcmex 29094  mDVcmdv 29095  mVarscmvrs 29096  mSubstcmsub 29098  mVHcmvh 29099  mFScmfs 29103  mClscmcls 29104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-8 1825  ax-9 1827  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432  ax-rep 4550  ax-sep 4560  ax-nul 4568  ax-pow 4615  ax-pr 4676  ax-un 6565  ax-cnex 9537  ax-resscn 9538  ax-1cn 9539  ax-icn 9540  ax-addcl 9541  ax-addrcl 9542  ax-mulcl 9543  ax-mulrcl 9544  ax-mulcom 9545  ax-addass 9546  ax-mulass 9547  ax-distr 9548  ax-i2m1 9549  ax-1ne0 9550  ax-1rid 9551  ax-rnegex 9552  ax-rrecex 9553  ax-cnre 9554  ax-pre-lttri 9555  ax-pre-lttrn 9556  ax-pre-ltadd 9557  ax-pre-mulgt0 9558
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1401  df-fal 1404  df-ex 1618  df-nf 1622  df-sb 1745  df-eu 2288  df-mo 2289  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2651  df-nel 2652  df-ral 2809  df-rex 2810  df-reu 2811  df-rmo 2812  df-rab 2813  df-v 3108  df-sbc 3325  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3784  df-if 3930  df-pw 4001  df-sn 4017  df-pr 4019  df-tp 4021  df-op 4023  df-ot 4025  df-uni 4236  df-int 4272  df-iun 4317  df-br 4440  df-opab 4498  df-mpt 4499  df-tr 4533  df-eprel 4780  df-id 4784  df-po 4789  df-so 4790  df-fr 4827  df-we 4829  df-ord 4870  df-on 4871  df-lim 4872  df-suc 4873  df-xp 4994  df-rel 4995  df-cnv 4996  df-co 4997  df-dm 4998  df-rn 4999  df-res 5000  df-ima 5001  df-iota 5534  df-fun 5572  df-fn 5573  df-f 5574  df-f1 5575  df-fo 5576  df-f1o 5577  df-fv 5578  df-riota 6232  df-ov 6273  df-oprab 6274  df-mpt2 6275  df-om 6674  df-1st 6773  df-2nd 6774  df-recs 7034  df-rdg 7068  df-1o 7122  df-oadd 7126  df-er 7303  df-map 7414  df-pm 7415  df-en 7510  df-dom 7511  df-sdom 7512  df-fin 7513  df-card 8311  df-cda 8539  df-pnf 9619  df-mnf 9620  df-xr 9621  df-ltxr 9622  df-le 9623  df-sub 9798  df-neg 9799  df-nn 10532  df-2 10590  df-n0 10792  df-z 10861  df-uz 11083  df-fz 11676  df-fzo 11800  df-seq 12093  df-hash 12391  df-word 12529  df-concat 12531  df-s1 12532  df-struct 14721  df-ndx 14722  df-slot 14723  df-base 14724  df-sets 14725  df-ress 14726  df-plusg 14800  df-0g 14934  df-gsum 14935  df-mgm 16074  df-sgrp 16113  df-mnd 16123  df-submnd 16169  df-frmd 16219  df-mrex 29113  df-mex 29114  df-mrsub 29117  df-msub 29118  df-mvh 29119  df-mpst 29120  df-msr 29121  df-msta 29122  df-mfs 29123  df-mcls 29124
This theorem is referenced by:  mclsssv  29191  ssmclslem  29192  ss2mcls  29195  mclsax  29196  mclsind  29197
  Copyright terms: Public domain W3C validator