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

Theorem mclsax 30256
Description: The closure is closed under axiom application. (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 )
mclsax.a  |-  A  =  (mAx `  T )
mclsax.l  |-  L  =  (mSubst `  T )
mclsax.v  |-  V  =  (mVR `  T )
mclsax.h  |-  H  =  (mVH `  T )
mclsax.w  |-  W  =  (mVars `  T )
mclsax.4  |-  ( ph  -> 
<. M ,  O ,  P >.  e.  A )
mclsax.5  |-  ( ph  ->  S  e.  ran  L
)
mclsax.6  |-  ( (
ph  /\  x  e.  O )  ->  ( S `  x )  e.  ( K C B ) )
mclsax.7  |-  ( (
ph  /\  v  e.  V )  ->  ( S `  ( H `  v ) )  e.  ( K C B ) )
mclsax.8  |-  ( (
ph  /\  ( x M y  /\  a  e.  ( W `  ( S `  ( H `  x ) ) )  /\  b  e.  ( W `  ( S `
 ( H `  y ) ) ) ) )  ->  a K b )
Assertion
Ref Expression
mclsax  |-  ( ph  ->  ( S `  P
)  e.  ( K C B ) )
Distinct variable groups:    v, E    a, b, v, x, H   
y, v, B, x   
v, C, x    x, L, y    x, O, y   
y, a, S, b, v, x    M, a, b, x, y    x, P, y    x, T, y    ph, a, b, v, x, y    v, V, x    W, a, b, x    K, a, b, v, x, y
Allowed substitution hints:    A( x, y, v, a, b)    B( a, b)    C( y, a, b)    D( x, y, v, a, b)    P( v, a, b)    T( v, a, b)    E( x, y, a, b)    H( y)    L( v, a, b)    M( v)    O( v, a, b)    V( y, a, b)    W( y, v)

Proof of Theorem mclsax
Dummy variables  c  m  o  p  s 
z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 abid 2450 . . . . . . . 8  |-  ( c  e.  { c  |  ( ( B  u.  ran  H )  C_  c  /\  A. m A. o A. p ( <. m ,  o ,  p >.  e.  A  ->  A. s  e.  ran  L ( ( ( s " (
o  u.  ran  H
) )  C_  c  /\  A. x A. y
( x m y  ->  ( ( W `
 ( s `  ( H `  x ) ) )  X.  ( W `  ( s `  ( H `  y
) ) ) ) 
C_  K ) )  ->  ( 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  L ( ( ( s " (
o  u.  ran  H
) )  C_  c  /\  A. x A. y
( x m y  ->  ( ( W `
 ( s `  ( H `  x ) ) )  X.  ( W `  ( s `  ( H `  y
) ) ) ) 
C_  K ) )  ->  ( s `  p )  e.  c ) ) ) )
2 intss1 4263 . . . . . . . 8  |-  ( c  e.  { c  |  ( ( B  u.  ran  H )  C_  c  /\  A. m A. o A. p ( <. m ,  o ,  p >.  e.  A  ->  A. s  e.  ran  L ( ( ( s " (
o  u.  ran  H
) )  C_  c  /\  A. x A. y
( x m y  ->  ( ( W `
 ( s `  ( H `  x ) ) )  X.  ( W `  ( s `  ( H `  y
) ) ) ) 
C_  K ) )  ->  ( 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  L ( ( ( s " (
o  u.  ran  H
) )  C_  c  /\  A. x A. y
( x m y  ->  ( ( W `
 ( s `  ( H `  x ) ) )  X.  ( W `  ( s `  ( H `  y
) ) ) ) 
C_  K ) )  ->  ( s `  p )  e.  c ) ) ) } 
C_  c )
31, 2sylbir 218 . . . . . . 7  |-  ( ( ( B  u.  ran  H )  C_  c  /\  A. m A. o A. p ( <. m ,  o ,  p >.  e.  A  ->  A. s  e.  ran  L ( ( ( s " (
o  u.  ran  H
) )  C_  c  /\  A. x A. y
( x m y  ->  ( ( W `
 ( s `  ( H `  x ) ) )  X.  ( W `  ( s `  ( H `  y
) ) ) ) 
C_  K ) )  ->  ( 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  L ( ( ( s " (
o  u.  ran  H
) )  C_  c  /\  A. x A. y
( x m y  ->  ( ( W `
 ( s `  ( H `  x ) ) )  X.  ( W `  ( s `  ( H `  y
) ) ) ) 
C_  K ) )  ->  ( s `  p )  e.  c ) ) ) } 
C_  c )
4 mclsval.d . . . . . . . . 9  |-  D  =  (mDV `  T )
5 mclsval.e . . . . . . . . 9  |-  E  =  (mEx `  T )
6 mclsval.c . . . . . . . . 9  |-  C  =  (mCls `  T )
7 mclsval.1 . . . . . . . . 9  |-  ( ph  ->  T  e. mFS )
8 mclsval.2 . . . . . . . . 9  |-  ( ph  ->  K  C_  D )
9 mclsval.3 . . . . . . . . 9  |-  ( ph  ->  B  C_  E )
10 mclsax.h . . . . . . . . 9  |-  H  =  (mVH `  T )
11 mclsax.a . . . . . . . . 9  |-  A  =  (mAx `  T )
12 mclsax.l . . . . . . . . 9  |-  L  =  (mSubst `  T )
13 mclsax.w . . . . . . . . 9  |-  W  =  (mVars `  T )
144, 5, 6, 7, 8, 9, 10, 11, 12, 13mclsval 30250 . . . . . . . 8  |-  ( 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  L ( ( ( s
" ( o  u. 
ran  H ) ) 
C_  c  /\  A. x A. y ( x m y  ->  (
( W `  (
s `  ( H `  x ) ) )  X.  ( W `  ( s `  ( H `  y )
) ) )  C_  K ) )  -> 
( s `  p
)  e.  c ) ) ) } )
1514sseq1d 3471 . . . . . . 7  |-  ( ph  ->  ( ( K C B )  C_  c  <->  |^|
{ c  |  ( ( B  u.  ran  H )  C_  c  /\  A. m A. o A. p ( <. m ,  o ,  p >.  e.  A  ->  A. s  e.  ran  L ( ( ( s " (
o  u.  ran  H
) )  C_  c  /\  A. x A. y
( x m y  ->  ( ( W `
 ( s `  ( H `  x ) ) )  X.  ( W `  ( s `  ( H `  y
) ) ) ) 
C_  K ) )  ->  ( s `  p )  e.  c ) ) ) } 
C_  c ) )
163, 15syl5ibr 229 . . . . . 6  |-  ( ph  ->  ( ( ( B  u.  ran  H ) 
C_  c  /\  A. m A. o A. p
( <. m ,  o ,  p >.  e.  A  ->  A. s  e.  ran  L ( ( ( s
" ( o  u. 
ran  H ) ) 
C_  c  /\  A. x A. y ( x m y  ->  (
( W `  (
s `  ( H `  x ) ) )  X.  ( W `  ( s `  ( H `  y )
) ) )  C_  K ) )  -> 
( s `  p
)  e.  c ) ) )  ->  ( K C B )  C_  c ) )
17 sstr2 3451 . . . . . . . . . . . . . . 15  |-  ( ( s " ( o  u.  ran  H ) )  C_  ( K C B )  ->  (
( K C B )  C_  c  ->  ( s " ( o  u.  ran  H ) )  C_  c )
)
1817com12 32 . . . . . . . . . . . . . 14  |-  ( ( K C B ) 
C_  c  ->  (
( s " (
o  u.  ran  H
) )  C_  ( K C B )  -> 
( s " (
o  u.  ran  H
) )  C_  c
) )
1918anim1d 572 . . . . . . . . . . . . 13  |-  ( ( K C B ) 
C_  c  ->  (
( ( s "
( o  u.  ran  H ) )  C_  ( K C B )  /\  A. x A. y ( x m y  -> 
( ( W `  ( s `  ( H `  x )
) )  X.  ( W `  ( s `  ( H `  y
) ) ) ) 
C_  K ) )  ->  ( ( s
" ( o  u. 
ran  H ) ) 
C_  c  /\  A. x A. y ( x m y  ->  (
( W `  (
s `  ( H `  x ) ) )  X.  ( W `  ( s `  ( H `  y )
) ) )  C_  K ) ) ) )
2019imim1d 78 . . . . . . . . . . . 12  |-  ( ( K C B ) 
C_  c  ->  (
( ( ( s
" ( o  u. 
ran  H ) ) 
C_  c  /\  A. x A. y ( x m y  ->  (
( W `  (
s `  ( H `  x ) ) )  X.  ( W `  ( s `  ( H `  y )
) ) )  C_  K ) )  -> 
( s `  p
)  e.  c )  ->  ( ( ( s " ( o  u.  ran  H ) )  C_  ( K C B )  /\  A. x A. y ( x m y  ->  (
( W `  (
s `  ( H `  x ) ) )  X.  ( W `  ( s `  ( H `  y )
) ) )  C_  K ) )  -> 
( s `  p
)  e.  c ) ) )
2120ralimdv 2810 . . . . . . . . . . 11  |-  ( ( K C B ) 
C_  c  ->  ( A. s  e.  ran  L ( ( ( s
" ( o  u. 
ran  H ) ) 
C_  c  /\  A. x A. y ( x m y  ->  (
( W `  (
s `  ( H `  x ) ) )  X.  ( W `  ( s `  ( H `  y )
) ) )  C_  K ) )  -> 
( s `  p
)  e.  c )  ->  A. s  e.  ran  L ( ( ( s
" ( o  u. 
ran  H ) ) 
C_  ( K C B )  /\  A. x A. y ( x m y  ->  (
( W `  (
s `  ( H `  x ) ) )  X.  ( W `  ( s `  ( H `  y )
) ) )  C_  K ) )  -> 
( s `  p
)  e.  c ) ) )
2221imim2d 54 . . . . . . . . . 10  |-  ( ( K C B ) 
C_  c  ->  (
( <. m ,  o ,  p >.  e.  A  ->  A. s  e.  ran  L ( ( ( s
" ( o  u. 
ran  H ) ) 
C_  c  /\  A. x A. y ( x m y  ->  (
( W `  (
s `  ( H `  x ) ) )  X.  ( W `  ( s `  ( H `  y )
) ) )  C_  K ) )  -> 
( s `  p
)  e.  c ) )  ->  ( <. m ,  o ,  p >.  e.  A  ->  A. s  e.  ran  L ( ( ( s " (
o  u.  ran  H
) )  C_  ( K C B )  /\  A. x A. y ( x m y  -> 
( ( W `  ( s `  ( H `  x )
) )  X.  ( W `  ( s `  ( H `  y
) ) ) ) 
C_  K ) )  ->  ( s `  p )  e.  c ) ) ) )
2322alimdv 1774 . . . . . . . . 9  |-  ( ( K C B ) 
C_  c  ->  ( A. p ( <. m ,  o ,  p >.  e.  A  ->  A. s  e.  ran  L ( ( ( s " (
o  u.  ran  H
) )  C_  c  /\  A. x A. y
( x m y  ->  ( ( W `
 ( s `  ( H `  x ) ) )  X.  ( W `  ( s `  ( H `  y
) ) ) ) 
C_  K ) )  ->  ( s `  p )  e.  c ) )  ->  A. p
( <. m ,  o ,  p >.  e.  A  ->  A. s  e.  ran  L ( ( ( s
" ( o  u. 
ran  H ) ) 
C_  ( K C B )  /\  A. x A. y ( x m y  ->  (
( W `  (
s `  ( H `  x ) ) )  X.  ( W `  ( s `  ( H `  y )
) ) )  C_  K ) )  -> 
( s `  p
)  e.  c ) ) ) )
24232alimdv 1776 . . . . . . . 8  |-  ( ( K C B ) 
C_  c  ->  ( A. m A. o A. p ( <. m ,  o ,  p >.  e.  A  ->  A. s  e.  ran  L ( ( ( s " (
o  u.  ran  H
) )  C_  c  /\  A. x A. y
( x m y  ->  ( ( W `
 ( s `  ( H `  x ) ) )  X.  ( W `  ( s `  ( H `  y
) ) ) ) 
C_  K ) )  ->  ( s `  p )  e.  c ) )  ->  A. m A. o A. p (
<. m ,  o ,  p >.  e.  A  ->  A. s  e.  ran  L ( ( ( s
" ( o  u. 
ran  H ) ) 
C_  ( K C B )  /\  A. x A. y ( x m y  ->  (
( W `  (
s `  ( H `  x ) ) )  X.  ( W `  ( s `  ( H `  y )
) ) )  C_  K ) )  -> 
( s `  p
)  e.  c ) ) ) )
2524com12 32 . . . . . . 7  |-  ( A. m A. o A. p
( <. m ,  o ,  p >.  e.  A  ->  A. s  e.  ran  L ( ( ( s
" ( o  u. 
ran  H ) ) 
C_  c  /\  A. x A. y ( x m y  ->  (
( W `  (
s `  ( H `  x ) ) )  X.  ( W `  ( s `  ( H `  y )
) ) )  C_  K ) )  -> 
( s `  p
)  e.  c ) )  ->  ( ( K C B )  C_  c  ->  A. m A. o A. p ( <. m ,  o ,  p >.  e.  A  ->  A. s  e.  ran  L ( ( ( s " (
o  u.  ran  H
) )  C_  ( K C B )  /\  A. x A. y ( x m y  -> 
( ( W `  ( s `  ( H `  x )
) )  X.  ( W `  ( s `  ( H `  y
) ) ) ) 
C_  K ) )  ->  ( s `  p )  e.  c ) ) ) )
2625adantl 472 . . . . . 6  |-  ( ( ( B  u.  ran  H )  C_  c  /\  A. m A. o A. p ( <. m ,  o ,  p >.  e.  A  ->  A. s  e.  ran  L ( ( ( s " (
o  u.  ran  H
) )  C_  c  /\  A. x A. y
( x m y  ->  ( ( W `
 ( s `  ( H `  x ) ) )  X.  ( W `  ( s `  ( H `  y
) ) ) ) 
C_  K ) )  ->  ( s `  p )  e.  c ) ) )  -> 
( ( K C B )  C_  c  ->  A. m A. o A. p ( <. m ,  o ,  p >.  e.  A  ->  A. s  e.  ran  L ( ( ( s " (
o  u.  ran  H
) )  C_  ( K C B )  /\  A. x A. y ( x m y  -> 
( ( W `  ( s `  ( H `  x )
) )  X.  ( W `  ( s `  ( H `  y
) ) ) ) 
C_  K ) )  ->  ( s `  p )  e.  c ) ) ) )
2716, 26sylcom 30 . . . . 5  |-  ( ph  ->  ( ( ( B  u.  ran  H ) 
C_  c  /\  A. m A. o A. p
( <. m ,  o ,  p >.  e.  A  ->  A. s  e.  ran  L ( ( ( s
" ( o  u. 
ran  H ) ) 
C_  c  /\  A. x A. y ( x m y  ->  (
( W `  (
s `  ( H `  x ) ) )  X.  ( W `  ( s `  ( H `  y )
) ) )  C_  K ) )  -> 
( s `  p
)  e.  c ) ) )  ->  A. m A. o A. p (
<. m ,  o ,  p >.  e.  A  ->  A. s  e.  ran  L ( ( ( s
" ( o  u. 
ran  H ) ) 
C_  ( K C B )  /\  A. x A. y ( x m y  ->  (
( W `  (
s `  ( H `  x ) ) )  X.  ( W `  ( s `  ( H `  y )
) ) )  C_  K ) )  -> 
( s `  p
)  e.  c ) ) ) )
28 eqid 2462 . . . . . . . 8  |-  (mPreSt `  T )  =  (mPreSt `  T )
29 eqid 2462 . . . . . . . 8  |-  (mStat `  T )  =  (mStat `  T )
3028, 29mstapst 30234 . . . . . . 7  |-  (mStat `  T )  C_  (mPreSt `  T )
3111, 29maxsta 30241 . . . . . . . . 9  |-  ( T  e. mFS  ->  A  C_  (mStat `  T ) )
327, 31syl 17 . . . . . . . 8  |-  ( ph  ->  A  C_  (mStat `  T
) )
33 mclsax.4 . . . . . . . 8  |-  ( ph  -> 
<. M ,  O ,  P >.  e.  A )
3432, 33sseldd 3445 . . . . . . 7  |-  ( ph  -> 
<. M ,  O ,  P >.  e.  (mStat `  T ) )
3530, 34sseldi 3442 . . . . . 6  |-  ( ph  -> 
<. M ,  O ,  P >.  e.  (mPreSt `  T ) )
3628mpstrcl 30228 . . . . . 6  |-  ( <. M ,  O ,  P >.  e.  (mPreSt `  T )  ->  ( M  e.  _V  /\  O  e.  _V  /\  P  e. 
_V ) )
37 simp1 1014 . . . . . . . . . 10  |-  ( ( m  =  M  /\  o  =  O  /\  p  =  P )  ->  m  =  M )
38 simp2 1015 . . . . . . . . . 10  |-  ( ( m  =  M  /\  o  =  O  /\  p  =  P )  ->  o  =  O )
39 simp3 1016 . . . . . . . . . 10  |-  ( ( m  =  M  /\  o  =  O  /\  p  =  P )  ->  p  =  P )
4037, 38, 39oteq123d 4195 . . . . . . . . 9  |-  ( ( m  =  M  /\  o  =  O  /\  p  =  P )  -> 
<. m ,  o ,  p >.  =  <. M ,  O ,  P >. )
4140eleq1d 2524 . . . . . . . 8  |-  ( ( m  =  M  /\  o  =  O  /\  p  =  P )  ->  ( <. m ,  o ,  p >.  e.  A  <->  <. M ,  O ,  P >.  e.  A ) )
4238uneq1d 3599 . . . . . . . . . . . . 13  |-  ( ( m  =  M  /\  o  =  O  /\  p  =  P )  ->  ( o  u.  ran  H )  =  ( O  u.  ran  H ) )
4342imaeq2d 5187 . . . . . . . . . . . 12  |-  ( ( m  =  M  /\  o  =  O  /\  p  =  P )  ->  ( s " (
o  u.  ran  H
) )  =  ( s " ( O  u.  ran  H ) ) )
4443sseq1d 3471 . . . . . . . . . . 11  |-  ( ( m  =  M  /\  o  =  O  /\  p  =  P )  ->  ( ( s "
( o  u.  ran  H ) )  C_  ( K C B )  <->  ( s " ( O  u.  ran  H ) )  C_  ( K C B ) ) )
4537breqd 4427 . . . . . . . . . . . . 13  |-  ( ( m  =  M  /\  o  =  O  /\  p  =  P )  ->  ( x m y  <-> 
x M y ) )
4645imbi1d 323 . . . . . . . . . . . 12  |-  ( ( m  =  M  /\  o  =  O  /\  p  =  P )  ->  ( ( x m y  ->  ( ( W `  ( s `  ( H `  x
) ) )  X.  ( W `  (
s `  ( H `  y ) ) ) )  C_  K )  <->  ( x M y  -> 
( ( W `  ( s `  ( H `  x )
) )  X.  ( W `  ( s `  ( H `  y
) ) ) ) 
C_  K ) ) )
47462albidv 1780 . . . . . . . . . . 11  |-  ( ( m  =  M  /\  o  =  O  /\  p  =  P )  ->  ( A. x A. y ( x m y  ->  ( ( W `  ( s `  ( H `  x
) ) )  X.  ( W `  (
s `  ( H `  y ) ) ) )  C_  K )  <->  A. x A. y ( x M y  -> 
( ( W `  ( s `  ( H `  x )
) )  X.  ( W `  ( s `  ( H `  y
) ) ) ) 
C_  K ) ) )
4844, 47anbi12d 722 . . . . . . . . . 10  |-  ( ( m  =  M  /\  o  =  O  /\  p  =  P )  ->  ( ( ( s
" ( o  u. 
ran  H ) ) 
C_  ( K C B )  /\  A. x A. y ( x m y  ->  (
( W `  (
s `  ( H `  x ) ) )  X.  ( W `  ( s `  ( H `  y )
) ) )  C_  K ) )  <->  ( (
s " ( O  u.  ran  H ) )  C_  ( K C B )  /\  A. x A. y ( x M y  ->  (
( W `  (
s `  ( H `  x ) ) )  X.  ( W `  ( s `  ( H `  y )
) ) )  C_  K ) ) ) )
4939fveq2d 5892 . . . . . . . . . . 11  |-  ( ( m  =  M  /\  o  =  O  /\  p  =  P )  ->  ( s `  p
)  =  ( s `
 P ) )
5049eleq1d 2524 . . . . . . . . . 10  |-  ( ( m  =  M  /\  o  =  O  /\  p  =  P )  ->  ( ( s `  p )  e.  c  <-> 
( s `  P
)  e.  c ) )
5148, 50imbi12d 326 . . . . . . . . 9  |-  ( ( m  =  M  /\  o  =  O  /\  p  =  P )  ->  ( ( ( ( s " ( o  u.  ran  H ) )  C_  ( K C B )  /\  A. x A. y ( x m y  ->  (
( W `  (
s `  ( H `  x ) ) )  X.  ( W `  ( s `  ( H `  y )
) ) )  C_  K ) )  -> 
( s `  p
)  e.  c )  <-> 
( ( ( s
" ( O  u.  ran  H ) )  C_  ( K C B )  /\  A. x A. y ( x M y  ->  ( ( W `  ( s `  ( H `  x
) ) )  X.  ( W `  (
s `  ( H `  y ) ) ) )  C_  K )
)  ->  ( s `  P )  e.  c ) ) )
5251ralbidv 2839 . . . . . . . 8  |-  ( ( m  =  M  /\  o  =  O  /\  p  =  P )  ->  ( A. s  e. 
ran  L ( ( ( s " (
o  u.  ran  H
) )  C_  ( K C B )  /\  A. x A. y ( x m y  -> 
( ( W `  ( s `  ( H `  x )
) )  X.  ( W `  ( s `  ( H `  y
) ) ) ) 
C_  K ) )  ->  ( s `  p )  e.  c )  <->  A. s  e.  ran  L ( ( ( s
" ( O  u.  ran  H ) )  C_  ( K C B )  /\  A. x A. y ( x M y  ->  ( ( W `  ( s `  ( H `  x
) ) )  X.  ( W `  (
s `  ( H `  y ) ) ) )  C_  K )
)  ->  ( s `  P )  e.  c ) ) )
5341, 52imbi12d 326 . . . . . . 7  |-  ( ( m  =  M  /\  o  =  O  /\  p  =  P )  ->  ( ( <. m ,  o ,  p >.  e.  A  ->  A. s  e.  ran  L ( ( ( s " (
o  u.  ran  H
) )  C_  ( K C B )  /\  A. x A. y ( x m y  -> 
( ( W `  ( s `  ( H `  x )
) )  X.  ( W `  ( s `  ( H `  y
) ) ) ) 
C_  K ) )  ->  ( s `  p )  e.  c ) )  <->  ( <. M ,  O ,  P >.  e.  A  ->  A. s  e.  ran  L ( ( ( s " ( O  u.  ran  H ) )  C_  ( K C B )  /\  A. x A. y ( x M y  ->  (
( W `  (
s `  ( H `  x ) ) )  X.  ( W `  ( s `  ( H `  y )
) ) )  C_  K ) )  -> 
( s `  P
)  e.  c ) ) ) )
5453spc3gv 3151 . . . . . 6  |-  ( ( M  e.  _V  /\  O  e.  _V  /\  P  e.  _V )  ->  ( A. m A. o A. p ( <. m ,  o ,  p >.  e.  A  ->  A. s  e.  ran  L ( ( ( s " (
o  u.  ran  H
) )  C_  ( K C B )  /\  A. x A. y ( x m y  -> 
( ( W `  ( s `  ( H `  x )
) )  X.  ( W `  ( s `  ( H `  y
) ) ) ) 
C_  K ) )  ->  ( s `  p )  e.  c ) )  ->  ( <. M ,  O ,  P >.  e.  A  ->  A. s  e.  ran  L ( ( ( s
" ( O  u.  ran  H ) )  C_  ( K C B )  /\  A. x A. y ( x M y  ->  ( ( W `  ( s `  ( H `  x
) ) )  X.  ( W `  (
s `  ( H `  y ) ) ) )  C_  K )
)  ->  ( s `  P )  e.  c ) ) ) )
5535, 36, 543syl 18 . . . . 5  |-  ( ph  ->  ( A. m A. o A. p ( <.
m ,  o ,  p >.  e.  A  ->  A. s  e.  ran  L ( ( ( s
" ( o  u. 
ran  H ) ) 
C_  ( K C B )  /\  A. x A. y ( x m y  ->  (
( W `  (
s `  ( H `  x ) ) )  X.  ( W `  ( s `  ( H `  y )
) ) )  C_  K ) )  -> 
( s `  p
)  e.  c ) )  ->  ( <. M ,  O ,  P >.  e.  A  ->  A. s  e.  ran  L ( ( ( s " ( O  u.  ran  H ) )  C_  ( K C B )  /\  A. x A. y ( x M y  ->  (
( W `  (
s `  ( H `  x ) ) )  X.  ( W `  ( s `  ( H `  y )
) ) )  C_  K ) )  -> 
( s `  P
)  e.  c ) ) ) )
56 elun 3586 . . . . . . . . . . 11  |-  ( x  e.  ( O  u.  ran  H )  <->  ( x  e.  O  \/  x  e.  ran  H ) )
57 mclsax.6 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  O )  ->  ( S `  x )  e.  ( K C B ) )
58 mclsax.7 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  v  e.  V )  ->  ( S `  ( H `  v ) )  e.  ( K C B ) )
5958ralrimiva 2814 . . . . . . . . . . . . . 14  |-  ( ph  ->  A. v  e.  V  ( S `  ( H `
 v ) )  e.  ( K C B ) )
60 mclsax.v . . . . . . . . . . . . . . . . 17  |-  V  =  (mVR `  T )
6160, 5, 10mvhf 30245 . . . . . . . . . . . . . . . 16  |-  ( T  e. mFS  ->  H : V --> E )
627, 61syl 17 . . . . . . . . . . . . . . 15  |-  ( ph  ->  H : V --> E )
63 ffn 5751 . . . . . . . . . . . . . . 15  |-  ( H : V --> E  ->  H  Fn  V )
64 fveq2 5888 . . . . . . . . . . . . . . . . 17  |-  ( x  =  ( H `  v )  ->  ( S `  x )  =  ( S `  ( H `  v ) ) )
6564eleq1d 2524 . . . . . . . . . . . . . . . 16  |-  ( x  =  ( H `  v )  ->  (
( S `  x
)  e.  ( K C B )  <->  ( S `  ( H `  v
) )  e.  ( K C B ) ) )
6665ralrn 6048 . . . . . . . . . . . . . . 15  |-  ( H  Fn  V  ->  ( A. x  e.  ran  H ( S `  x
)  e.  ( K C B )  <->  A. v  e.  V  ( S `  ( H `  v
) )  e.  ( K C B ) ) )
6762, 63, 663syl 18 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( A. x  e. 
ran  H ( S `
 x )  e.  ( K C B )  <->  A. v  e.  V  ( S `  ( H `
 v ) )  e.  ( K C B ) ) )
6859, 67mpbird 240 . . . . . . . . . . . . 13  |-  ( ph  ->  A. x  e.  ran  H ( S `  x
)  e.  ( K C B ) )
6968r19.21bi 2769 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  ran  H )  ->  ( S `  x )  e.  ( K C B ) )
7057, 69jaodan 799 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  O  \/  x  e.  ran  H ) )  ->  ( S `  x )  e.  ( K C B ) )
7156, 70sylan2b 482 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  ( O  u.  ran  H ) )  ->  ( S `  x )  e.  ( K C B ) )
7271ralrimiva 2814 . . . . . . . . 9  |-  ( ph  ->  A. x  e.  ( O  u.  ran  H
) ( S `  x )  e.  ( K C B ) )
73 mclsax.5 . . . . . . . . . . . 12  |-  ( ph  ->  S  e.  ran  L
)
7412, 5msubf 30219 . . . . . . . . . . . 12  |-  ( S  e.  ran  L  ->  S : E --> E )
7573, 74syl 17 . . . . . . . . . . 11  |-  ( ph  ->  S : E --> E )
76 ffun 5754 . . . . . . . . . . 11  |-  ( S : E --> E  ->  Fun  S )
7775, 76syl 17 . . . . . . . . . 10  |-  ( ph  ->  Fun  S )
784, 5, 28elmpst 30223 . . . . . . . . . . . . . . 15  |-  ( <. M ,  O ,  P >.  e.  (mPreSt `  T )  <->  ( ( M  C_  D  /\  `' M  =  M )  /\  ( O  C_  E  /\  O  e.  Fin )  /\  P  e.  E
) )
7935, 78sylib 201 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( ( M  C_  D  /\  `' M  =  M )  /\  ( O  C_  E  /\  O  e.  Fin )  /\  P  e.  E ) )
8079simp2d 1027 . . . . . . . . . . . . 13  |-  ( ph  ->  ( O  C_  E  /\  O  e.  Fin ) )
8180simpld 465 . . . . . . . . . . . 12  |-  ( ph  ->  O  C_  E )
82 fdm 5756 . . . . . . . . . . . . 13  |-  ( S : E --> E  ->  dom  S  =  E )
8375, 82syl 17 . . . . . . . . . . . 12  |-  ( ph  ->  dom  S  =  E )
8481, 83sseqtr4d 3481 . . . . . . . . . . 11  |-  ( ph  ->  O  C_  dom  S )
85 frn 5758 . . . . . . . . . . . . 13  |-  ( H : V --> E  ->  ran  H  C_  E )
8662, 85syl 17 . . . . . . . . . . . 12  |-  ( ph  ->  ran  H  C_  E
)
8786, 83sseqtr4d 3481 . . . . . . . . . . 11  |-  ( ph  ->  ran  H  C_  dom  S )
8884, 87unssd 3622 . . . . . . . . . 10  |-  ( ph  ->  ( O  u.  ran  H )  C_  dom  S )
89 funimass4 5939 . . . . . . . . . 10  |-  ( ( Fun  S  /\  ( O  u.  ran  H ) 
C_  dom  S )  ->  ( ( S "
( O  u.  ran  H ) )  C_  ( K C B )  <->  A. x  e.  ( O  u.  ran  H ) ( S `  x )  e.  ( K C B ) ) )
9077, 88, 89syl2anc 671 . . . . . . . . 9  |-  ( ph  ->  ( ( S "
( O  u.  ran  H ) )  C_  ( K C B )  <->  A. x  e.  ( O  u.  ran  H ) ( S `  x )  e.  ( K C B ) ) )
9172, 90mpbird 240 . . . . . . . 8  |-  ( ph  ->  ( S " ( O  u.  ran  H ) )  C_  ( K C B ) )
92 mclsax.8 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( x M y  /\  a  e.  ( W `  ( S `  ( H `  x ) ) )  /\  b  e.  ( W `  ( S `
 ( H `  y ) ) ) ) )  ->  a K b )
93923exp2 1235 . . . . . . . . . . . . 13  |-  ( ph  ->  ( x M y  ->  ( a  e.  ( W `  ( S `  ( H `  x ) ) )  ->  ( b  e.  ( W `  ( S `  ( H `  y ) ) )  ->  a K b ) ) ) )
9493imp4b 599 . . . . . . . . . . . 12  |-  ( (
ph  /\  x M
y )  ->  (
( a  e.  ( W `  ( S `
 ( H `  x ) ) )  /\  b  e.  ( W `  ( S `
 ( H `  y ) ) ) )  ->  a K
b ) )
9594ralrimivv 2820 . . . . . . . . . . 11  |-  ( (
ph  /\  x M
y )  ->  A. a  e.  ( W `  ( S `  ( H `  x ) ) ) A. b  e.  ( W `  ( S `
 ( H `  y ) ) ) a K b )
96 dfss3 3434 . . . . . . . . . . . 12  |-  ( ( ( W `  ( S `  ( H `  x ) ) )  X.  ( W `  ( S `  ( H `
 y ) ) ) )  C_  K  <->  A. z  e.  ( ( W `  ( S `
 ( H `  x ) ) )  X.  ( W `  ( S `  ( H `
 y ) ) ) ) z  e.  K )
97 eleq1 2528 . . . . . . . . . . . . . 14  |-  ( z  =  <. a ,  b
>.  ->  ( z  e.  K  <->  <. a ,  b
>.  e.  K ) )
98 df-br 4417 . . . . . . . . . . . . . 14  |-  ( a K b  <->  <. a ,  b >.  e.  K
)
9997, 98syl6bbr 271 . . . . . . . . . . . . 13  |-  ( z  =  <. a ,  b
>.  ->  ( z  e.  K  <->  a K b ) )
10099ralxp 4995 . . . . . . . . . . . 12  |-  ( A. z  e.  ( ( W `  ( S `  ( H `  x
) ) )  X.  ( W `  ( S `  ( H `  y ) ) ) ) z  e.  K  <->  A. a  e.  ( W `
 ( S `  ( H `  x ) ) ) A. b  e.  ( W `  ( S `  ( H `  y ) ) ) a K b )
10196, 100bitri 257 . . . . . . . . . . 11  |-  ( ( ( W `  ( S `  ( H `  x ) ) )  X.  ( W `  ( S `  ( H `
 y ) ) ) )  C_  K  <->  A. a  e.  ( W `
 ( S `  ( H `  x ) ) ) A. b  e.  ( W `  ( S `  ( H `  y ) ) ) a K b )
10295, 101sylibr 217 . . . . . . . . . 10  |-  ( (
ph  /\  x M
y )  ->  (
( W `  ( S `  ( H `  x ) ) )  X.  ( W `  ( S `  ( H `
 y ) ) ) )  C_  K
)
103102ex 440 . . . . . . . . 9  |-  ( ph  ->  ( x M y  ->  ( ( W `
 ( S `  ( H `  x ) ) )  X.  ( W `  ( S `  ( H `  y
) ) ) ) 
C_  K ) )
104103alrimivv 1785 . . . . . . . 8  |-  ( ph  ->  A. x A. y
( x M y  ->  ( ( W `
 ( S `  ( H `  x ) ) )  X.  ( W `  ( S `  ( H `  y
) ) ) ) 
C_  K ) )
10591, 104jca 539 . . . . . . 7  |-  ( ph  ->  ( ( S "
( O  u.  ran  H ) )  C_  ( K C B )  /\  A. x A. y ( x M y  -> 
( ( W `  ( S `  ( H `
 x ) ) )  X.  ( W `
 ( S `  ( H `  y ) ) ) )  C_  K ) ) )
106 imaeq1 5182 . . . . . . . . . . . 12  |-  ( s  =  S  ->  (
s " ( O  u.  ran  H ) )  =  ( S
" ( O  u.  ran  H ) ) )
107106sseq1d 3471 . . . . . . . . . . 11  |-  ( s  =  S  ->  (
( s " ( O  u.  ran  H ) )  C_  ( K C B )  <->  ( S " ( O  u.  ran  H ) )  C_  ( K C B ) ) )
108 fveq1 5887 . . . . . . . . . . . . . . . 16  |-  ( s  =  S  ->  (
s `  ( H `  x ) )  =  ( S `  ( H `  x )
) )
109108fveq2d 5892 . . . . . . . . . . . . . . 15  |-  ( s  =  S  ->  ( W `  ( s `  ( H `  x
) ) )  =  ( W `  ( S `  ( H `  x ) ) ) )
110 fveq1 5887 . . . . . . . . . . . . . . . 16  |-  ( s  =  S  ->  (
s `  ( H `  y ) )  =  ( S `  ( H `  y )
) )
111110fveq2d 5892 . . . . . . . . . . . . . . 15  |-  ( s  =  S  ->  ( W `  ( s `  ( H `  y
) ) )  =  ( W `  ( S `  ( H `  y ) ) ) )
112109, 111xpeq12d 4878 . . . . . . . . . . . . . 14  |-  ( s  =  S  ->  (
( W `  (
s `  ( H `  x ) ) )  X.  ( W `  ( s `  ( H `  y )
) ) )  =  ( ( W `  ( S `  ( H `
 x ) ) )  X.  ( W `
 ( S `  ( H `  y ) ) ) ) )
113112sseq1d 3471 . . . . . . . . . . . . 13  |-  ( s  =  S  ->  (
( ( W `  ( s `  ( H `  x )
) )  X.  ( W `  ( s `  ( H `  y
) ) ) ) 
C_  K  <->  ( ( W `  ( S `  ( H `  x
) ) )  X.  ( W `  ( S `  ( H `  y ) ) ) )  C_  K )
)
114113imbi2d 322 . . . . . . . . . . . 12  |-  ( s  =  S  ->  (
( x M y  ->  ( ( W `
 ( s `  ( H `  x ) ) )  X.  ( W `  ( s `  ( H `  y
) ) ) ) 
C_  K )  <->  ( x M y  ->  (
( W `  ( S `  ( H `  x ) ) )  X.  ( W `  ( S `  ( H `
 y ) ) ) )  C_  K
) ) )
1151142albidv 1780 . . . . . . . . . . 11  |-  ( s  =  S  ->  ( A. x A. y ( x M y  -> 
( ( W `  ( s `  ( H `  x )
) )  X.  ( W `  ( s `  ( H `  y
) ) ) ) 
C_  K )  <->  A. x A. y ( x M y  ->  ( ( W `  ( S `  ( H `  x
) ) )  X.  ( W `  ( S `  ( H `  y ) ) ) )  C_  K )
) )
116107, 115anbi12d 722 . . . . . . . . . 10  |-  ( s  =  S  ->  (
( ( s "
( O  u.  ran  H ) )  C_  ( K C B )  /\  A. x A. y ( x M y  -> 
( ( W `  ( s `  ( H `  x )
) )  X.  ( W `  ( s `  ( H `  y
) ) ) ) 
C_  K ) )  <-> 
( ( S "
( O  u.  ran  H ) )  C_  ( K C B )  /\  A. x A. y ( x M y  -> 
( ( W `  ( S `  ( H `
 x ) ) )  X.  ( W `
 ( S `  ( H `  y ) ) ) )  C_  K ) ) ) )
117 fveq1 5887 . . . . . . . . . . 11  |-  ( s  =  S  ->  (
s `  P )  =  ( S `  P ) )
118117eleq1d 2524 . . . . . . . . . 10  |-  ( s  =  S  ->  (
( s `  P
)  e.  c  <->  ( S `  P )  e.  c ) )
119116, 118imbi12d 326 . . . . . . . . 9  |-  ( s  =  S  ->  (
( ( ( s
" ( O  u.  ran  H ) )  C_  ( K C B )  /\  A. x A. y ( x M y  ->  ( ( W `  ( s `  ( H `  x
) ) )  X.  ( W `  (
s `  ( H `  y ) ) ) )  C_  K )
)  ->  ( s `  P )  e.  c )  <->  ( ( ( S " ( O  u.  ran  H ) )  C_  ( K C B )  /\  A. x A. y ( x M y  ->  (
( W `  ( S `  ( H `  x ) ) )  X.  ( W `  ( S `  ( H `
 y ) ) ) )  C_  K
) )  ->  ( S `  P )  e.  c ) ) )
120119rspcv 3158 . . . . . . . 8  |-  ( S  e.  ran  L  -> 
( A. s  e. 
ran  L ( ( ( s " ( O  u.  ran  H ) )  C_  ( K C B )  /\  A. x A. y ( x M y  ->  (
( W `  (
s `  ( H `  x ) ) )  X.  ( W `  ( s `  ( H `  y )
) ) )  C_  K ) )  -> 
( s `  P
)  e.  c )  ->  ( ( ( S " ( O  u.  ran  H ) )  C_  ( K C B )  /\  A. x A. y ( x M y  ->  (
( W `  ( S `  ( H `  x ) ) )  X.  ( W `  ( S `  ( H `
 y ) ) ) )  C_  K
) )  ->  ( S `  P )  e.  c ) ) )
12173, 120syl 17 . . . . . . 7  |-  ( ph  ->  ( A. s  e. 
ran  L ( ( ( s " ( O  u.  ran  H ) )  C_  ( K C B )  /\  A. x A. y ( x M y  ->  (
( W `  (
s `  ( H `  x ) ) )  X.  ( W `  ( s `  ( H `  y )
) ) )  C_  K ) )  -> 
( s `  P
)  e.  c )  ->  ( ( ( S " ( O  u.  ran  H ) )  C_  ( K C B )  /\  A. x A. y ( x M y  ->  (
( W `  ( S `  ( H `  x ) ) )  X.  ( W `  ( S `  ( H `
 y ) ) ) )  C_  K
) )  ->  ( S `  P )  e.  c ) ) )
122105, 121mpid 42 . . . . . 6  |-  ( ph  ->  ( A. s  e. 
ran  L ( ( ( s " ( O  u.  ran  H ) )  C_  ( K C B )  /\  A. x A. y ( x M y  ->  (
( W `  (
s `  ( H `  x ) ) )  X.  ( W `  ( s `  ( H `  y )
) ) )  C_  K ) )  -> 
( s `  P
)  e.  c )  ->  ( S `  P )  e.  c ) )
12333, 122embantd 56 . . . . 5  |-  ( ph  ->  ( ( <. M ,  O ,  P >.  e.  A  ->  A. s  e.  ran  L ( ( ( s " ( O  u.  ran  H ) )  C_  ( K C B )  /\  A. x A. y ( x M y  ->  (
( W `  (
s `  ( H `  x ) ) )  X.  ( W `  ( s `  ( H `  y )
) ) )  C_  K ) )  -> 
( s `  P
)  e.  c ) )  ->  ( S `  P )  e.  c ) )
12427, 55, 1233syld 57 . . . 4  |-  ( ph  ->  ( ( ( B  u.  ran  H ) 
C_  c  /\  A. m A. o A. p
( <. m ,  o ,  p >.  e.  A  ->  A. s  e.  ran  L ( ( ( s
" ( o  u. 
ran  H ) ) 
C_  c  /\  A. x A. y ( x m y  ->  (
( W `  (
s `  ( H `  x ) ) )  X.  ( W `  ( s `  ( H `  y )
) ) )  C_  K ) )  -> 
( s `  p
)  e.  c ) ) )  ->  ( S `  P )  e.  c ) )
125124alrimiv 1784 . . 3  |-  ( ph  ->  A. c ( ( ( B  u.  ran  H )  C_  c  /\  A. m A. o A. p ( <. m ,  o ,  p >.  e.  A  ->  A. s  e.  ran  L ( ( ( s " (
o  u.  ran  H
) )  C_  c  /\  A. x A. y
( x m y  ->  ( ( W `
 ( s `  ( H `  x ) ) )  X.  ( W `  ( s `  ( H `  y
) ) ) ) 
C_  K ) )  ->  ( s `  p )  e.  c ) ) )  -> 
( S `  P
)  e.  c ) )
126 fvex 5898 . . . 4  |-  ( S `
 P )  e. 
_V
127126elintab 4259 . . 3  |-  ( ( 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  L ( ( ( s " (
o  u.  ran  H
) )  C_  c  /\  A. x A. y
( x m y  ->  ( ( W `
 ( s `  ( H `  x ) ) )  X.  ( W `  ( s `  ( H `  y
) ) ) ) 
C_  K ) )  ->  ( s `  p )  e.  c ) ) ) }  <->  A. c ( ( ( B  u.  ran  H
)  C_  c  /\  A. m A. o A. p ( <. m ,  o ,  p >.  e.  A  ->  A. s  e.  ran  L ( ( ( s " (
o  u.  ran  H
) )  C_  c  /\  A. x A. y
( x m y  ->  ( ( W `
 ( s `  ( H `  x ) ) )  X.  ( W `  ( s `  ( H `  y
) ) ) ) 
C_  K ) )  ->  ( s `  p )  e.  c ) ) )  -> 
( S `  P
)  e.  c ) )
128125, 127sylibr 217 . 2  |-  ( ph  ->  ( 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  L ( ( ( s
" ( o  u. 
ran  H ) ) 
C_  c  /\  A. x A. y ( x m y  ->  (
( W `  (
s `  ( H `  x ) ) )  X.  ( W `  ( s `  ( H `  y )
) ) )  C_  K ) )  -> 
( s `  p
)  e.  c ) ) ) } )
129128, 14eleqtrrd 2543 1  |-  ( ph  ->  ( S `  P
)  e.  ( K C B ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 189    \/ wo 374    /\ wa 375    /\ w3a 991   A.wal 1453    = wceq 1455    e. wcel 1898   {cab 2448   A.wral 2749   _Vcvv 3057    u. cun 3414    C_ wss 3416   <.cop 3986   <.cotp 3988   |^|cint 4248   class class class wbr 4416    X. cxp 4851   `'ccnv 4852   dom cdm 4853   ran crn 4854   "cima 4856   Fun wfun 5595    Fn wfn 5596   -->wf 5597   ` cfv 5601  (class class class)co 6315   Fincfn 7595  mVRcmvar 30148  mAxcmax 30152  mExcmex 30154  mDVcmdv 30155  mVarscmvrs 30156  mSubstcmsub 30158  mVHcmvh 30159  mPreStcmpst 30160  mStatcmsta 30162  mFScmfs 30163  mClscmcls 30164
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-rep 4529  ax-sep 4539  ax-nul 4548  ax-pow 4595  ax-pr 4653  ax-un 6610  ax-cnex 9621  ax-resscn 9622  ax-1cn 9623  ax-icn 9624  ax-addcl 9625  ax-addrcl 9626  ax-mulcl 9627  ax-mulrcl 9628  ax-mulcom 9629  ax-addass 9630  ax-mulass 9631  ax-distr 9632  ax-i2m1 9633  ax-1ne0 9634  ax-1rid 9635  ax-rnegex 9636  ax-rrecex 9637  ax-cnre 9638  ax-pre-lttri 9639  ax-pre-lttrn 9640  ax-pre-ltadd 9641  ax-pre-mulgt0 9642
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-fal 1461  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-nel 2636  df-ral 2754  df-rex 2755  df-reu 2756  df-rmo 2757  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-ot 3989  df-uni 4213  df-int 4249  df-iun 4294  df-br 4417  df-opab 4476  df-mpt 4477  df-tr 4512  df-eprel 4764  df-id 4768  df-po 4774  df-so 4775  df-fr 4812  df-we 4814  df-xp 4859  df-rel 4860  df-cnv 4861  df-co 4862  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-riota 6277  df-ov 6318  df-oprab 6319  df-mpt2 6320  df-om 6720  df-1st 6820  df-2nd 6821  df-wrecs 7054  df-recs 7116  df-rdg 7154  df-1o 7208  df-oadd 7212  df-er 7389  df-map 7500  df-pm 7501  df-en 7596  df-dom 7597  df-sdom 7598  df-fin 7599  df-card 8399  df-cda 8624  df-pnf 9703  df-mnf 9704  df-xr 9705  df-ltxr 9706  df-le 9707  df-sub 9888  df-neg 9889  df-nn 10638  df-2 10696  df-n0 10899  df-z 10967  df-uz 11189  df-fz 11814  df-fzo 11947  df-seq 12246  df-hash 12548  df-word 12697  df-concat 12699  df-s1 12700  df-struct 15172  df-ndx 15173  df-slot 15174  df-base 15175  df-sets 15176  df-ress 15177  df-plusg 15252  df-0g 15389  df-gsum 15390  df-mgm 16537  df-sgrp 16576  df-mnd 16586  df-submnd 16632  df-frmd 16682  df-mrex 30173  df-mex 30174  df-mrsub 30177  df-msub 30178  df-mvh 30179  df-mpst 30180  df-msr 30181  df-msta 30182  df-mfs 30183  df-mcls 30184
This theorem is referenced by:  mclsppslem  30270
  Copyright terms: Public domain W3C validator