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

Theorem mclsppslem 30173
Description: The closure is closed under application of provable pre-statements. (Compare mclsax 30159.) This theorem is what justifies the treatment of theorems as "equivalent" to axioms once they have been proven: the composition of one theorem in the proof of another yields a theorem. (Contributed by Mario Carneiro, 18-Jul-2016.)
Hypotheses
Ref Expression
mclspps.d  |-  D  =  (mDV `  T )
mclspps.e  |-  E  =  (mEx `  T )
mclspps.c  |-  C  =  (mCls `  T )
mclspps.1  |-  ( ph  ->  T  e. mFS )
mclspps.2  |-  ( ph  ->  K  C_  D )
mclspps.3  |-  ( ph  ->  B  C_  E )
mclspps.j  |-  J  =  (mPPSt `  T )
mclspps.l  |-  L  =  (mSubst `  T )
mclspps.v  |-  V  =  (mVR `  T )
mclspps.h  |-  H  =  (mVH `  T )
mclspps.w  |-  W  =  (mVars `  T )
mclspps.4  |-  ( ph  -> 
<. M ,  O ,  P >.  e.  J )
mclspps.5  |-  ( ph  ->  S  e.  ran  L
)
mclspps.6  |-  ( (
ph  /\  x  e.  O )  ->  ( S `  x )  e.  ( K C B ) )
mclspps.7  |-  ( (
ph  /\  v  e.  V )  ->  ( S `  ( H `  v ) )  e.  ( K C B ) )
mclspps.8  |-  ( (
ph  /\  ( x M y  /\  a  e.  ( W `  ( S `  ( H `  x ) ) )  /\  b  e.  ( W `  ( S `
 ( H `  y ) ) ) ) )  ->  a K b )
mclsppslem.9  |-  ( ph  -> 
<. m ,  o ,  p >.  e.  (mAx `  T ) )
mclsppslem.10  |-  ( ph  ->  s  e.  ran  L
)
mclsppslem.11  |-  ( ph  ->  ( s " (
o  u.  ran  H
) )  C_  ( `' S " ( K C B ) ) )
mclsppslem.12  |-  ( ph  ->  A. z A. w
( z m w  ->  ( ( W `
 ( s `  ( H `  z ) ) )  X.  ( W `  ( s `  ( H `  w
) ) ) ) 
C_  M ) )
Assertion
Ref Expression
mclsppslem  |-  ( ph  ->  ( s `  p
)  e.  ( `' S " ( K C B ) ) )
Distinct variable groups:    m, o, p, s, v, E    a,
b, m, o, p, s, v, w, x, y, z, H    v, V, z    K, a, b, m, o, p, s, v, x, y    T, a, b, m, o, p, s, v, w, x, y, z    L, a, b, m, o, p, s, v, w, x, y, z    S, a, b, m, o, p, s, v, x, y    B, a, b, m, o, p, s, v, x, y    W, a, b, m, o, p, s, v, w, x, y, z    C, a, b, m, o, p, s, v, x, y, z    M, a, b, m, o, p, s, v, w, x, y, z    m, O, o, p, s, v, w, x, z    ph, a,
b, v, x, y
Allowed substitution hints:    ph( z, w, m, o, s, p)    B( z, w)    C( w)    D( x, y, z, w, v, m, o, s, p, a, b)    P( x, y, z, w, v, m, o, s, p, a, b)    S( z, w)    E( x, y, z, w, a, b)    J( x, y, z, w, v, m, o, s, p, a, b)    K( z, w)    O( y, a, b)    V( x, y, w, m, o, s, p, a, b)

Proof of Theorem mclsppslem
Dummy variables  t  u  c  d are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mclsppslem.10 . . . 4  |-  ( ph  ->  s  e.  ran  L
)
2 mclspps.l . . . . 5  |-  L  =  (mSubst `  T )
3 mclspps.e . . . . 5  |-  E  =  (mEx `  T )
42, 3msubf 30122 . . . 4  |-  ( s  e.  ran  L  -> 
s : E --> E )
51, 4syl 17 . . 3  |-  ( ph  ->  s : E --> E )
6 mclspps.1 . . . . . . . 8  |-  ( ph  ->  T  e. mFS )
7 eqid 2428 . . . . . . . . 9  |-  (mAx `  T )  =  (mAx
`  T )
8 eqid 2428 . . . . . . . . 9  |-  (mStat `  T )  =  (mStat `  T )
97, 8maxsta 30144 . . . . . . . 8  |-  ( T  e. mFS  ->  (mAx `  T
)  C_  (mStat `  T
) )
106, 9syl 17 . . . . . . 7  |-  ( ph  ->  (mAx `  T )  C_  (mStat `  T )
)
11 eqid 2428 . . . . . . . 8  |-  (mPreSt `  T )  =  (mPreSt `  T )
1211, 8mstapst 30137 . . . . . . 7  |-  (mStat `  T )  C_  (mPreSt `  T )
1310, 12syl6ss 3419 . . . . . 6  |-  ( ph  ->  (mAx `  T )  C_  (mPreSt `  T )
)
14 mclsppslem.9 . . . . . 6  |-  ( ph  -> 
<. m ,  o ,  p >.  e.  (mAx `  T ) )
1513, 14sseldd 3408 . . . . 5  |-  ( ph  -> 
<. m ,  o ,  p >.  e.  (mPreSt `  T ) )
16 mclspps.d . . . . . 6  |-  D  =  (mDV `  T )
1716, 3, 11elmpst 30126 . . . . 5  |-  ( <.
m ,  o ,  p >.  e.  (mPreSt `  T )  <->  ( (
m  C_  D  /\  `' m  =  m
)  /\  ( o  C_  E  /\  o  e. 
Fin )  /\  p  e.  E ) )
1815, 17sylib 199 . . . 4  |-  ( ph  ->  ( ( m  C_  D  /\  `' m  =  m )  /\  (
o  C_  E  /\  o  e.  Fin )  /\  p  e.  E
) )
1918simp3d 1019 . . 3  |-  ( ph  ->  p  e.  E )
205, 19ffvelrnd 5982 . 2  |-  ( ph  ->  ( s `  p
)  e.  E )
21 fvco3 5902 . . . 4  |-  ( ( s : E --> E  /\  p  e.  E )  ->  ( ( S  o.  s ) `  p
)  =  ( S `
 ( s `  p ) ) )
225, 19, 21syl2anc 665 . . 3  |-  ( ph  ->  ( ( S  o.  s ) `  p
)  =  ( S `
 ( s `  p ) ) )
23 mclspps.c . . . 4  |-  C  =  (mCls `  T )
24 mclspps.2 . . . 4  |-  ( ph  ->  K  C_  D )
25 mclspps.3 . . . 4  |-  ( ph  ->  B  C_  E )
26 mclspps.v . . . 4  |-  V  =  (mVR `  T )
27 mclspps.h . . . 4  |-  H  =  (mVH `  T )
28 mclspps.w . . . 4  |-  W  =  (mVars `  T )
29 mclspps.5 . . . . 5  |-  ( ph  ->  S  e.  ran  L
)
302msubco 30121 . . . . 5  |-  ( ( S  e.  ran  L  /\  s  e.  ran  L )  ->  ( S  o.  s )  e.  ran  L )
3129, 1, 30syl2anc 665 . . . 4  |-  ( ph  ->  ( S  o.  s
)  e.  ran  L
)
322, 3msubf 30122 . . . . . . . . 9  |-  ( S  e.  ran  L  ->  S : E --> E )
3329, 32syl 17 . . . . . . . 8  |-  ( ph  ->  S : E --> E )
34 fco 5699 . . . . . . . 8  |-  ( ( S : E --> E  /\  s : E --> E )  ->  ( S  o.  s ) : E --> E )
3533, 5, 34syl2anc 665 . . . . . . 7  |-  ( ph  ->  ( S  o.  s
) : E --> E )
36 ffn 5689 . . . . . . 7  |-  ( ( S  o.  s ) : E --> E  -> 
( S  o.  s
)  Fn  E )
3735, 36syl 17 . . . . . 6  |-  ( ph  ->  ( S  o.  s
)  Fn  E )
3837adantr 466 . . . . 5  |-  ( (
ph  /\  c  e.  o )  ->  ( S  o.  s )  Fn  E )
39 mclsppslem.11 . . . . . . . . 9  |-  ( ph  ->  ( s " (
o  u.  ran  H
) )  C_  ( `' S " ( K C B ) ) )
40 ffun 5691 . . . . . . . . . . 11  |-  ( s : E --> E  ->  Fun  s )
415, 40syl 17 . . . . . . . . . 10  |-  ( ph  ->  Fun  s )
4217simp2bi 1021 . . . . . . . . . . . . . 14  |-  ( <.
m ,  o ,  p >.  e.  (mPreSt `  T )  ->  (
o  C_  E  /\  o  e.  Fin )
)
4315, 42syl 17 . . . . . . . . . . . . 13  |-  ( ph  ->  ( o  C_  E  /\  o  e.  Fin ) )
4443simpld 460 . . . . . . . . . . . 12  |-  ( ph  ->  o  C_  E )
4526, 3, 27mvhf 30148 . . . . . . . . . . . . 13  |-  ( T  e. mFS  ->  H : V --> E )
46 frn 5695 . . . . . . . . . . . . 13  |-  ( H : V --> E  ->  ran  H  C_  E )
476, 45, 463syl 18 . . . . . . . . . . . 12  |-  ( ph  ->  ran  H  C_  E
)
4844, 47unssd 3585 . . . . . . . . . . 11  |-  ( ph  ->  ( o  u.  ran  H )  C_  E )
49 fdm 5693 . . . . . . . . . . . 12  |-  ( s : E --> E  ->  dom  s  =  E
)
505, 49syl 17 . . . . . . . . . . 11  |-  ( ph  ->  dom  s  =  E )
5148, 50sseqtr4d 3444 . . . . . . . . . 10  |-  ( ph  ->  ( o  u.  ran  H )  C_  dom  s )
52 funimass3 5957 . . . . . . . . . 10  |-  ( ( Fun  s  /\  (
o  u.  ran  H
)  C_  dom  s )  ->  ( ( s
" ( o  u. 
ran  H ) ) 
C_  ( `' S " ( K C B ) )  <->  ( o  u.  ran  H )  C_  ( `' s " ( `' S " ( K C B ) ) ) ) )
5341, 51, 52syl2anc 665 . . . . . . . . 9  |-  ( ph  ->  ( ( s "
( o  u.  ran  H ) )  C_  ( `' S " ( K C B ) )  <-> 
( o  u.  ran  H )  C_  ( `' s " ( `' S " ( K C B ) ) ) ) )
5439, 53mpbid 213 . . . . . . . 8  |-  ( ph  ->  ( o  u.  ran  H )  C_  ( `' s " ( `' S " ( K C B ) ) ) )
55 cnvco 4982 . . . . . . . . . 10  |-  `' ( S  o.  s )  =  ( `' s  o.  `' S )
5655imaeq1i 5127 . . . . . . . . 9  |-  ( `' ( S  o.  s
) " ( K C B ) )  =  ( ( `' s  o.  `' S
) " ( K C B ) )
57 imaco 5302 . . . . . . . . 9  |-  ( ( `' s  o.  `' S ) " ( K C B ) )  =  ( `' s
" ( `' S " ( K C B ) ) )
5856, 57eqtri 2450 . . . . . . . 8  |-  ( `' ( S  o.  s
) " ( K C B ) )  =  ( `' s
" ( `' S " ( K C B ) ) )
5954, 58syl6sseqr 3454 . . . . . . 7  |-  ( ph  ->  ( o  u.  ran  H )  C_  ( `' ( S  o.  s
) " ( K C B ) ) )
6059unssad 3586 . . . . . 6  |-  ( ph  ->  o  C_  ( `' ( S  o.  s
) " ( K C B ) ) )
6160sselda 3407 . . . . 5  |-  ( (
ph  /\  c  e.  o )  ->  c  e.  ( `' ( S  o.  s ) "
( K C B ) ) )
62 elpreima 5961 . . . . . 6  |-  ( ( S  o.  s )  Fn  E  ->  (
c  e.  ( `' ( S  o.  s
) " ( K C B ) )  <-> 
( c  e.  E  /\  ( ( S  o.  s ) `  c
)  e.  ( K C B ) ) ) )
6362simplbda 628 . . . . 5  |-  ( ( ( S  o.  s
)  Fn  E  /\  c  e.  ( `' ( S  o.  s
) " ( K C B ) ) )  ->  ( ( S  o.  s ) `  c )  e.  ( K C B ) )
6438, 61, 63syl2anc 665 . . . 4  |-  ( (
ph  /\  c  e.  o )  ->  (
( S  o.  s
) `  c )  e.  ( K C B ) )
6537adantr 466 . . . . 5  |-  ( (
ph  /\  t  e.  V )  ->  ( S  o.  s )  Fn  E )
6659unssbd 3587 . . . . . . 7  |-  ( ph  ->  ran  H  C_  ( `' ( S  o.  s ) " ( K C B ) ) )
6766adantr 466 . . . . . 6  |-  ( (
ph  /\  t  e.  V )  ->  ran  H 
C_  ( `' ( S  o.  s )
" ( K C B ) ) )
68 ffn 5689 . . . . . . . 8  |-  ( H : V --> E  ->  H  Fn  V )
696, 45, 683syl 18 . . . . . . 7  |-  ( ph  ->  H  Fn  V )
70 fnfvelrn 5978 . . . . . . 7  |-  ( ( H  Fn  V  /\  t  e.  V )  ->  ( H `  t
)  e.  ran  H
)
7169, 70sylan 473 . . . . . 6  |-  ( (
ph  /\  t  e.  V )  ->  ( H `  t )  e.  ran  H )
7267, 71sseldd 3408 . . . . 5  |-  ( (
ph  /\  t  e.  V )  ->  ( H `  t )  e.  ( `' ( S  o.  s ) "
( K C B ) ) )
73 elpreima 5961 . . . . . 6  |-  ( ( S  o.  s )  Fn  E  ->  (
( H `  t
)  e.  ( `' ( S  o.  s
) " ( K C B ) )  <-> 
( ( H `  t )  e.  E  /\  ( ( S  o.  s ) `  ( H `  t )
)  e.  ( K C B ) ) ) )
7473simplbda 628 . . . . 5  |-  ( ( ( S  o.  s
)  Fn  E  /\  ( H `  t )  e.  ( `' ( S  o.  s )
" ( K C B ) ) )  ->  ( ( S  o.  s ) `  ( H `  t ) )  e.  ( K C B ) )
7565, 72, 74syl2anc 665 . . . 4  |-  ( (
ph  /\  t  e.  V )  ->  (
( S  o.  s
) `  ( H `  t ) )  e.  ( K C B ) )
765adantr 466 . . . . . . . . . . . . 13  |-  ( (
ph  /\  c m
d )  ->  s : E --> E )
776, 45syl 17 . . . . . . . . . . . . . . 15  |-  ( ph  ->  H : V --> E )
7877adantr 466 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  c m
d )  ->  H : V --> E )
7918simp1d 1017 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  ( m  C_  D  /\  `' m  =  m
) )
8079simpld 460 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  m  C_  D )
8126, 16mdvval 30094 . . . . . . . . . . . . . . . . . . . 20  |-  D  =  ( ( V  X.  V )  \  _I  )
82 difss 3535 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( V  X.  V ) 
\  _I  )  C_  ( V  X.  V
)
8381, 82eqsstri 3437 . . . . . . . . . . . . . . . . . . 19  |-  D  C_  ( V  X.  V
)
8480, 83syl6ss 3419 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  m  C_  ( V  X.  V ) )
8584ssbrd 4408 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( c m d  ->  c ( V  X.  V ) d ) )
8685imp 430 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  c m
d )  ->  c
( V  X.  V
) d )
87 brxp 4827 . . . . . . . . . . . . . . . 16  |-  ( c ( V  X.  V
) d  <->  ( c  e.  V  /\  d  e.  V ) )
8886, 87sylib 199 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  c m
d )  ->  (
c  e.  V  /\  d  e.  V )
)
8988simpld 460 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  c m
d )  ->  c  e.  V )
9078, 89ffvelrnd 5982 . . . . . . . . . . . . 13  |-  ( (
ph  /\  c m
d )  ->  ( H `  c )  e.  E )
91 fvco3 5902 . . . . . . . . . . . . 13  |-  ( ( s : E --> E  /\  ( H `  c )  e.  E )  -> 
( ( S  o.  s ) `  ( H `  c )
)  =  ( S `
 ( s `  ( H `  c ) ) ) )
9276, 90, 91syl2anc 665 . . . . . . . . . . . 12  |-  ( (
ph  /\  c m
d )  ->  (
( S  o.  s
) `  ( H `  c ) )  =  ( S `  (
s `  ( H `  c ) ) ) )
9392fveq2d 5829 . . . . . . . . . . 11  |-  ( (
ph  /\  c m
d )  ->  ( W `  ( ( S  o.  s ) `  ( H `  c
) ) )  =  ( W `  ( S `  ( s `  ( H `  c
) ) ) ) )
946adantr 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  c m
d )  ->  T  e. mFS )
9529adantr 466 . . . . . . . . . . . 12  |-  ( (
ph  /\  c m
d )  ->  S  e.  ran  L )
9676, 90ffvelrnd 5982 . . . . . . . . . . . 12  |-  ( (
ph  /\  c m
d )  ->  (
s `  ( H `  c ) )  e.  E )
972, 3, 28, 27msubvrs 30150 . . . . . . . . . . . 12  |-  ( ( T  e. mFS  /\  S  e.  ran  L  /\  (
s `  ( H `  c ) )  e.  E )  ->  ( W `  ( S `  ( s `  ( H `  c )
) ) )  = 
U_ u  e.  ( W `  ( s `
 ( H `  c ) ) ) ( W `  ( S `  ( H `  u ) ) ) )
9894, 95, 96, 97syl3anc 1264 . . . . . . . . . . 11  |-  ( (
ph  /\  c m
d )  ->  ( W `  ( S `  ( s `  ( H `  c )
) ) )  = 
U_ u  e.  ( W `  ( s `
 ( H `  c ) ) ) ( W `  ( S `  ( H `  u ) ) ) )
9993, 98eqtrd 2462 . . . . . . . . . 10  |-  ( (
ph  /\  c m
d )  ->  ( W `  ( ( S  o.  s ) `  ( H `  c
) ) )  = 
U_ u  e.  ( W `  ( s `
 ( H `  c ) ) ) ( W `  ( S `  ( H `  u ) ) ) )
10099eleq2d 2491 . . . . . . . . 9  |-  ( (
ph  /\  c m
d )  ->  (
a  e.  ( W `
 ( ( S  o.  s ) `  ( H `  c ) ) )  <->  a  e.  U_ u  e.  ( W `
 ( s `  ( H `  c ) ) ) ( W `
 ( S `  ( H `  u ) ) ) ) )
101 eliun 4247 . . . . . . . . 9  |-  ( a  e.  U_ u  e.  ( W `  (
s `  ( H `  c ) ) ) ( W `  ( S `  ( H `  u ) ) )  <->  E. u  e.  ( W `  ( s `  ( H `  c
) ) ) a  e.  ( W `  ( S `  ( H `
 u ) ) ) )
102100, 101syl6bb 264 . . . . . . . 8  |-  ( (
ph  /\  c m
d )  ->  (
a  e.  ( W `
 ( ( S  o.  s ) `  ( H `  c ) ) )  <->  E. u  e.  ( W `  (
s `  ( H `  c ) ) ) a  e.  ( W `
 ( S `  ( H `  u ) ) ) ) )
10388simprd 464 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  c m
d )  ->  d  e.  V )
10478, 103ffvelrnd 5982 . . . . . . . . . . . . 13  |-  ( (
ph  /\  c m
d )  ->  ( H `  d )  e.  E )
105 fvco3 5902 . . . . . . . . . . . . 13  |-  ( ( s : E --> E  /\  ( H `  d )  e.  E )  -> 
( ( S  o.  s ) `  ( H `  d )
)  =  ( S `
 ( s `  ( H `  d ) ) ) )
10676, 104, 105syl2anc 665 . . . . . . . . . . . 12  |-  ( (
ph  /\  c m
d )  ->  (
( S  o.  s
) `  ( H `  d ) )  =  ( S `  (
s `  ( H `  d ) ) ) )
107106fveq2d 5829 . . . . . . . . . . 11  |-  ( (
ph  /\  c m
d )  ->  ( W `  ( ( S  o.  s ) `  ( H `  d
) ) )  =  ( W `  ( S `  ( s `  ( H `  d
) ) ) ) )
10876, 104ffvelrnd 5982 . . . . . . . . . . . 12  |-  ( (
ph  /\  c m
d )  ->  (
s `  ( H `  d ) )  e.  E )
1092, 3, 28, 27msubvrs 30150 . . . . . . . . . . . 12  |-  ( ( T  e. mFS  /\  S  e.  ran  L  /\  (
s `  ( H `  d ) )  e.  E )  ->  ( W `  ( S `  ( s `  ( H `  d )
) ) )  = 
U_ v  e.  ( W `  ( s `
 ( H `  d ) ) ) ( W `  ( S `  ( H `  v ) ) ) )
11094, 95, 108, 109syl3anc 1264 . . . . . . . . . . 11  |-  ( (
ph  /\  c m
d )  ->  ( W `  ( S `  ( s `  ( H `  d )
) ) )  = 
U_ v  e.  ( W `  ( s `
 ( H `  d ) ) ) ( W `  ( S `  ( H `  v ) ) ) )
111107, 110eqtrd 2462 . . . . . . . . . 10  |-  ( (
ph  /\  c m
d )  ->  ( W `  ( ( S  o.  s ) `  ( H `  d
) ) )  = 
U_ v  e.  ( W `  ( s `
 ( H `  d ) ) ) ( W `  ( S `  ( H `  v ) ) ) )
112111eleq2d 2491 . . . . . . . . 9  |-  ( (
ph  /\  c m
d )  ->  (
b  e.  ( W `
 ( ( S  o.  s ) `  ( H `  d ) ) )  <->  b  e.  U_ v  e.  ( W `
 ( s `  ( H `  d ) ) ) ( W `
 ( S `  ( H `  v ) ) ) ) )
113 eliun 4247 . . . . . . . . 9  |-  ( b  e.  U_ v  e.  ( W `  (
s `  ( H `  d ) ) ) ( W `  ( S `  ( H `  v ) ) )  <->  E. v  e.  ( W `  ( s `  ( H `  d
) ) ) b  e.  ( W `  ( S `  ( H `
 v ) ) ) )
114112, 113syl6bb 264 . . . . . . . 8  |-  ( (
ph  /\  c m
d )  ->  (
b  e.  ( W `
 ( ( S  o.  s ) `  ( H `  d ) ) )  <->  E. v  e.  ( W `  (
s `  ( H `  d ) ) ) b  e.  ( W `
 ( S `  ( H `  v ) ) ) ) )
115102, 114anbi12d 715 . . . . . . 7  |-  ( (
ph  /\  c m
d )  ->  (
( a  e.  ( W `  ( ( S  o.  s ) `
 ( H `  c ) ) )  /\  b  e.  ( W `  ( ( S  o.  s ) `
 ( H `  d ) ) ) )  <->  ( E. u  e.  ( W `  (
s `  ( H `  c ) ) ) a  e.  ( W `
 ( S `  ( H `  u ) ) )  /\  E. v  e.  ( W `  ( s `  ( H `  d )
) ) b  e.  ( W `  ( S `  ( H `  v ) ) ) ) ) )
116 reeanv 2935 . . . . . . . 8  |-  ( E. u  e.  ( W `
 ( s `  ( H `  c ) ) ) E. v  e.  ( W `  (
s `  ( H `  d ) ) ) ( a  e.  ( W `  ( S `
 ( H `  u ) ) )  /\  b  e.  ( W `  ( S `
 ( H `  v ) ) ) )  <->  ( E. u  e.  ( W `  (
s `  ( H `  c ) ) ) a  e.  ( W `
 ( S `  ( H `  u ) ) )  /\  E. v  e.  ( W `  ( s `  ( H `  d )
) ) b  e.  ( W `  ( S `  ( H `  v ) ) ) ) )
117 simpll 758 . . . . . . . . . 10  |-  ( ( ( ph  /\  c
m d )  /\  ( u  e.  ( W `  ( s `  ( H `  c
) ) )  /\  v  e.  ( W `  ( s `  ( H `  d )
) ) ) )  ->  ph )
118 brxp 4827 . . . . . . . . . . . 12  |-  ( u ( ( W `  ( s `  ( H `  c )
) )  X.  ( W `  ( s `  ( H `  d
) ) ) ) v  <->  ( u  e.  ( W `  (
s `  ( H `  c ) ) )  /\  v  e.  ( W `  ( s `
 ( H `  d ) ) ) ) )
119 mclsppslem.12 . . . . . . . . . . . . . . 15  |-  ( ph  ->  A. z A. w
( z m w  ->  ( ( W `
 ( s `  ( H `  z ) ) )  X.  ( W `  ( s `  ( H `  w
) ) ) ) 
C_  M ) )
120 vex 3025 . . . . . . . . . . . . . . . 16  |-  c  e. 
_V
121 vex 3025 . . . . . . . . . . . . . . . 16  |-  d  e. 
_V
122 breq12 4371 . . . . . . . . . . . . . . . . . 18  |-  ( ( z  =  c  /\  w  =  d )  ->  ( z m w  <-> 
c m d ) )
123 simpl 458 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( z  =  c  /\  w  =  d )  ->  z  =  c )
124123fveq2d 5829 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( z  =  c  /\  w  =  d )  ->  ( H `  z
)  =  ( H `
 c ) )
125124fveq2d 5829 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( z  =  c  /\  w  =  d )  ->  ( s `  ( H `  z )
)  =  ( s `
 ( H `  c ) ) )
126125fveq2d 5829 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( z  =  c  /\  w  =  d )  ->  ( W `  (
s `  ( H `  z ) ) )  =  ( W `  ( s `  ( H `  c )
) ) )
127 simpr 462 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( z  =  c  /\  w  =  d )  ->  w  =  d )
128127fveq2d 5829 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( z  =  c  /\  w  =  d )  ->  ( H `  w
)  =  ( H `
 d ) )
129128fveq2d 5829 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( z  =  c  /\  w  =  d )  ->  ( s `  ( H `  w )
)  =  ( s `
 ( H `  d ) ) )
130129fveq2d 5829 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( z  =  c  /\  w  =  d )  ->  ( W `  (
s `  ( H `  w ) ) )  =  ( W `  ( s `  ( H `  d )
) ) )
131126, 130xpeq12d 4821 . . . . . . . . . . . . . . . . . . 19  |-  ( ( z  =  c  /\  w  =  d )  ->  ( ( W `  ( s `  ( H `  z )
) )  X.  ( W `  ( s `  ( H `  w
) ) ) )  =  ( ( W `
 ( s `  ( H `  c ) ) )  X.  ( W `  ( s `  ( H `  d
) ) ) ) )
132131sseq1d 3434 . . . . . . . . . . . . . . . . . 18  |-  ( ( z  =  c  /\  w  =  d )  ->  ( ( ( W `
 ( s `  ( H `  z ) ) )  X.  ( W `  ( s `  ( H `  w
) ) ) ) 
C_  M  <->  ( ( W `  ( s `  ( H `  c
) ) )  X.  ( W `  (
s `  ( H `  d ) ) ) )  C_  M )
)
133122, 132imbi12d 321 . . . . . . . . . . . . . . . . 17  |-  ( ( z  =  c  /\  w  =  d )  ->  ( ( z m w  ->  ( ( W `  ( s `  ( H `  z
) ) )  X.  ( W `  (
s `  ( H `  w ) ) ) )  C_  M )  <->  ( c m d  -> 
( ( W `  ( s `  ( H `  c )
) )  X.  ( W `  ( s `  ( H `  d
) ) ) ) 
C_  M ) ) )
134133spc2gv 3112 . . . . . . . . . . . . . . . 16  |-  ( ( c  e.  _V  /\  d  e.  _V )  ->  ( A. z A. w ( z m w  ->  ( ( W `  ( s `  ( H `  z
) ) )  X.  ( W `  (
s `  ( H `  w ) ) ) )  C_  M )  ->  ( c m d  ->  ( ( W `
 ( s `  ( H `  c ) ) )  X.  ( W `  ( s `  ( H `  d
) ) ) ) 
C_  M ) ) )
135120, 121, 134mp2an 676 . . . . . . . . . . . . . . 15  |-  ( A. z A. w ( z m w  ->  (
( W `  (
s `  ( H `  z ) ) )  X.  ( W `  ( s `  ( H `  w )
) ) )  C_  M )  ->  (
c m d  -> 
( ( W `  ( s `  ( H `  c )
) )  X.  ( W `  ( s `  ( H `  d
) ) ) ) 
C_  M ) )
136119, 135syl 17 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( c m d  ->  ( ( W `
 ( s `  ( H `  c ) ) )  X.  ( W `  ( s `  ( H `  d
) ) ) ) 
C_  M ) )
137136imp 430 . . . . . . . . . . . . 13  |-  ( (
ph  /\  c m
d )  ->  (
( W `  (
s `  ( H `  c ) ) )  X.  ( W `  ( s `  ( H `  d )
) ) )  C_  M )
138137ssbrd 4408 . . . . . . . . . . . 12  |-  ( (
ph  /\  c m
d )  ->  (
u ( ( W `
 ( s `  ( H `  c ) ) )  X.  ( W `  ( s `  ( H `  d
) ) ) ) v  ->  u M
v ) )
139118, 138syl5bir 221 . . . . . . . . . . 11  |-  ( (
ph  /\  c m
d )  ->  (
( u  e.  ( W `  ( s `
 ( H `  c ) ) )  /\  v  e.  ( W `  ( s `
 ( H `  d ) ) ) )  ->  u M
v ) )
140139imp 430 . . . . . . . . . 10  |-  ( ( ( ph  /\  c
m d )  /\  ( u  e.  ( W `  ( s `  ( H `  c
) ) )  /\  v  e.  ( W `  ( s `  ( H `  d )
) ) ) )  ->  u M v )
141 vex 3025 . . . . . . . . . . . . 13  |-  u  e. 
_V
142 vex 3025 . . . . . . . . . . . . 13  |-  v  e. 
_V
143 breq12 4371 . . . . . . . . . . . . . . . 16  |-  ( ( x  =  u  /\  y  =  v )  ->  ( x M y  <-> 
u M v ) )
144 simpl 458 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  =  u  /\  y  =  v )  ->  x  =  u )
145144fveq2d 5829 . . . . . . . . . . . . . . . . . . 19  |-  ( ( x  =  u  /\  y  =  v )  ->  ( H `  x
)  =  ( H `
 u ) )
146145fveq2d 5829 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  =  u  /\  y  =  v )  ->  ( S `  ( H `  x )
)  =  ( S `
 ( H `  u ) ) )
147146fveq2d 5829 . . . . . . . . . . . . . . . . 17  |-  ( ( x  =  u  /\  y  =  v )  ->  ( W `  ( S `  ( H `  x ) ) )  =  ( W `  ( S `  ( H `
 u ) ) ) )
148147eleq2d 2491 . . . . . . . . . . . . . . . 16  |-  ( ( x  =  u  /\  y  =  v )  ->  ( a  e.  ( W `  ( S `
 ( H `  x ) ) )  <-> 
a  e.  ( W `
 ( S `  ( H `  u ) ) ) ) )
149 simpr 462 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( x  =  u  /\  y  =  v )  ->  y  =  v )
150149fveq2d 5829 . . . . . . . . . . . . . . . . . . 19  |-  ( ( x  =  u  /\  y  =  v )  ->  ( H `  y
)  =  ( H `
 v ) )
151150fveq2d 5829 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  =  u  /\  y  =  v )  ->  ( S `  ( H `  y )
)  =  ( S `
 ( H `  v ) ) )
152151fveq2d 5829 . . . . . . . . . . . . . . . . 17  |-  ( ( x  =  u  /\  y  =  v )  ->  ( W `  ( S `  ( H `  y ) ) )  =  ( W `  ( S `  ( H `
 v ) ) ) )
153152eleq2d 2491 . . . . . . . . . . . . . . . 16  |-  ( ( x  =  u  /\  y  =  v )  ->  ( b  e.  ( W `  ( S `
 ( H `  y ) ) )  <-> 
b  e.  ( W `
 ( S `  ( H `  v ) ) ) ) )
154143, 148, 1533anbi123d 1335 . . . . . . . . . . . . . . 15  |-  ( ( x  =  u  /\  y  =  v )  ->  ( ( x M y  /\  a  e.  ( W `  ( S `  ( H `  x ) ) )  /\  b  e.  ( W `  ( S `
 ( H `  y ) ) ) )  <->  ( u M v  /\  a  e.  ( W `  ( S `  ( H `  u ) ) )  /\  b  e.  ( W `  ( S `
 ( H `  v ) ) ) ) ) )
155154anbi2d 708 . . . . . . . . . . . . . 14  |-  ( ( x  =  u  /\  y  =  v )  ->  ( ( ph  /\  ( x M y  /\  a  e.  ( W `  ( S `
 ( H `  x ) ) )  /\  b  e.  ( W `  ( S `
 ( H `  y ) ) ) ) )  <->  ( ph  /\  ( u M v  /\  a  e.  ( W `  ( S `
 ( H `  u ) ) )  /\  b  e.  ( W `  ( S `
 ( H `  v ) ) ) ) ) ) )
156155imbi1d 318 . . . . . . . . . . . . 13  |-  ( ( x  =  u  /\  y  =  v )  ->  ( ( ( ph  /\  ( x M y  /\  a  e.  ( W `  ( S `
 ( H `  x ) ) )  /\  b  e.  ( W `  ( S `
 ( H `  y ) ) ) ) )  ->  a K b )  <->  ( ( ph  /\  ( u M v  /\  a  e.  ( W `  ( S `  ( H `  u ) ) )  /\  b  e.  ( W `  ( S `
 ( H `  v ) ) ) ) )  ->  a K b ) ) )
157 mclspps.8 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( x M y  /\  a  e.  ( W `  ( S `  ( H `  x ) ) )  /\  b  e.  ( W `  ( S `
 ( H `  y ) ) ) ) )  ->  a K b )
158141, 142, 156, 157vtocl2 3077 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( u M v  /\  a  e.  ( W `  ( S `  ( H `  u ) ) )  /\  b  e.  ( W `  ( S `
 ( H `  v ) ) ) ) )  ->  a K b )
1591583exp2 1223 . . . . . . . . . . 11  |-  ( ph  ->  ( u M v  ->  ( a  e.  ( W `  ( S `  ( H `  u ) ) )  ->  ( b  e.  ( W `  ( S `  ( H `  v ) ) )  ->  a K b ) ) ) )
160159imp4b 593 . . . . . . . . . 10  |-  ( (
ph  /\  u M
v )  ->  (
( a  e.  ( W `  ( S `
 ( H `  u ) ) )  /\  b  e.  ( W `  ( S `
 ( H `  v ) ) ) )  ->  a K
b ) )
161117, 140, 160syl2anc 665 . . . . . . . . 9  |-  ( ( ( ph  /\  c
m d )  /\  ( u  e.  ( W `  ( s `  ( H `  c
) ) )  /\  v  e.  ( W `  ( s `  ( H `  d )
) ) ) )  ->  ( ( a  e.  ( W `  ( S `  ( H `
 u ) ) )  /\  b  e.  ( W `  ( S `  ( H `  v ) ) ) )  ->  a K
b ) )
162161rexlimdvva 2863 . . . . . . . 8  |-  ( (
ph  /\  c m
d )  ->  ( E. u  e.  ( W `  ( s `  ( H `  c
) ) ) E. v  e.  ( W `
 ( s `  ( H `  d ) ) ) ( a  e.  ( W `  ( S `  ( H `
 u ) ) )  /\  b  e.  ( W `  ( S `  ( H `  v ) ) ) )  ->  a K
b ) )
163116, 162syl5bir 221 . . . . . . 7  |-  ( (
ph  /\  c m
d )  ->  (
( E. u  e.  ( W `  (
s `  ( H `  c ) ) ) a  e.  ( W `
 ( S `  ( H `  u ) ) )  /\  E. v  e.  ( W `  ( s `  ( H `  d )
) ) b  e.  ( W `  ( S `  ( H `  v ) ) ) )  ->  a K
b ) )
164115, 163sylbid 218 . . . . . 6  |-  ( (
ph  /\  c m
d )  ->  (
( a  e.  ( W `  ( ( S  o.  s ) `
 ( H `  c ) ) )  /\  b  e.  ( W `  ( ( S  o.  s ) `
 ( H `  d ) ) ) )  ->  a K
b ) )
165164exp4b 610 . . . . 5  |-  ( ph  ->  ( c m d  ->  ( a  e.  ( W `  (
( S  o.  s
) `  ( H `  c ) ) )  ->  ( b  e.  ( W `  (
( S  o.  s
) `  ( H `  d ) ) )  ->  a K b ) ) ) )
1661653imp2 1220 . . . 4  |-  ( (
ph  /\  ( c
m d  /\  a  e.  ( W `  (
( S  o.  s
) `  ( H `  c ) ) )  /\  b  e.  ( W `  ( ( S  o.  s ) `
 ( H `  d ) ) ) ) )  ->  a K b )
16716, 3, 23, 6, 24, 25, 7, 2, 26, 27, 28, 14, 31, 64, 75, 166mclsax 30159 . . 3  |-  ( ph  ->  ( ( S  o.  s ) `  p
)  e.  ( K C B ) )
16822, 167eqeltrrd 2507 . 2  |-  ( ph  ->  ( S `  (
s `  p )
)  e.  ( K C B ) )
169 ffn 5689 . . . 4  |-  ( S : E --> E  ->  S  Fn  E )
17033, 169syl 17 . . 3  |-  ( ph  ->  S  Fn  E )
171 elpreima 5961 . . 3  |-  ( S  Fn  E  ->  (
( s `  p
)  e.  ( `' S " ( K C B ) )  <-> 
( ( s `  p )  e.  E  /\  ( S `  (
s `  p )
)  e.  ( K C B ) ) ) )
172170, 171syl 17 . 2  |-  ( ph  ->  ( ( s `  p )  e.  ( `' S " ( K C B ) )  <-> 
( ( s `  p )  e.  E  /\  ( S `  (
s `  p )
)  e.  ( K C B ) ) ) )
17320, 168, 172mpbir2and 930 1  |-  ( ph  ->  ( s `  p
)  e.  ( `' S " ( K C B ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    /\ wa 370    /\ w3a 982   A.wal 1435    = wceq 1437    e. wcel 1872   E.wrex 2715   _Vcvv 3022    \ cdif 3376    u. cun 3377    C_ wss 3379   <.cotp 3949   U_ciun 4242   class class class wbr 4366    _I cid 4706    X. cxp 4794   `'ccnv 4795   dom cdm 4796   ran crn 4797   "cima 4799    o. ccom 4800   Fun wfun 5538    Fn wfn 5539   -->wf 5540   ` cfv 5544  (class class class)co 6249   Fincfn 7524  mVRcmvar 30051  mAxcmax 30055  mExcmex 30057  mDVcmdv 30058  mVarscmvrs 30059  mSubstcmsub 30061  mVHcmvh 30062  mPreStcmpst 30063  mStatcmsta 30065  mFScmfs 30066  mClscmcls 30067  mPPStcmpps 30068
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-8 1874  ax-9 1876  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408  ax-rep 4479  ax-sep 4489  ax-nul 4498  ax-pow 4545  ax-pr 4603  ax-un 6541  ax-cnex 9546  ax-resscn 9547  ax-1cn 9548  ax-icn 9549  ax-addcl 9550  ax-addrcl 9551  ax-mulcl 9552  ax-mulrcl 9553  ax-mulcom 9554  ax-addass 9555  ax-mulass 9556  ax-distr 9557  ax-i2m1 9558  ax-1ne0 9559  ax-1rid 9560  ax-rnegex 9561  ax-rrecex 9562  ax-cnre 9563  ax-pre-lttri 9564  ax-pre-lttrn 9565  ax-pre-ltadd 9566  ax-pre-mulgt0 9567
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-fal 1443  df-ex 1658  df-nf 1662  df-sb 1791  df-eu 2280  df-mo 2281  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-ne 2601  df-nel 2602  df-ral 2719  df-rex 2720  df-reu 2721  df-rmo 2722  df-rab 2723  df-v 3024  df-sbc 3243  df-csb 3339  df-dif 3382  df-un 3384  df-in 3386  df-ss 3393  df-pss 3395  df-nul 3705  df-if 3855  df-pw 3926  df-sn 3942  df-pr 3944  df-tp 3946  df-op 3948  df-ot 3950  df-uni 4163  df-int 4199  df-iun 4244  df-br 4367  df-opab 4426  df-mpt 4427  df-tr 4462  df-eprel 4707  df-id 4711  df-po 4717  df-so 4718  df-fr 4755  df-we 4757  df-xp 4802  df-rel 4803  df-cnv 4804  df-co 4805  df-dm 4806  df-rn 4807  df-res 4808  df-ima 4809  df-pred 5342  df-ord 5388  df-on 5389  df-lim 5390  df-suc 5391  df-iota 5508  df-fun 5546  df-fn 5547  df-f 5548  df-f1 5549  df-fo 5550  df-f1o 5551  df-fv 5552  df-riota 6211  df-ov 6252  df-oprab 6253  df-mpt2 6254  df-om 6651  df-1st 6751  df-2nd 6752  df-wrecs 6983  df-recs 7045  df-rdg 7083  df-1o 7137  df-oadd 7141  df-er 7318  df-map 7429  df-pm 7430  df-en 7525  df-dom 7526  df-sdom 7527  df-fin 7528  df-card 8325  df-cda 8549  df-pnf 9628  df-mnf 9629  df-xr 9630  df-ltxr 9631  df-le 9632  df-sub 9813  df-neg 9814  df-nn 10561  df-2 10619  df-n0 10821  df-z 10889  df-uz 11111  df-fz 11736  df-fzo 11867  df-seq 12164  df-hash 12466  df-word 12612  df-lsw 12613  df-concat 12614  df-s1 12615  df-substr 12616  df-struct 15066  df-ndx 15067  df-slot 15068  df-base 15069  df-sets 15070  df-ress 15071  df-plusg 15146  df-0g 15283  df-gsum 15284  df-mgm 16431  df-sgrp 16470  df-mnd 16480  df-mhm 16525  df-submnd 16526  df-frmd 16576  df-vrmd 16577  df-mrex 30076  df-mex 30077  df-mdv 30078  df-mvrs 30079  df-mrsub 30080  df-msub 30081  df-mvh 30082  df-mpst 30083  df-msr 30084  df-msta 30085  df-mfs 30086  df-mcls 30087
This theorem is referenced by:  mclspps  30174
  Copyright terms: Public domain W3C validator