Metamath Proof Explorer

Theorem mclsppslem

Description: The closure is closed under application of provable pre-statements. (Compare mclsax .) 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)

Ref Expression
Hypotheses 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 mclsppslem 
|- ( ph -> ( s ` p ) e. ( `' S " ( K C B ) ) )

Proof

Step Hyp Ref Expression
1 mclspps.d 
 |-  D = ( mDV ` T )
2 mclspps.e 
 |-  E = ( mEx ` T )
3 mclspps.c 
 |-  C = ( mCls ` T )
4 mclspps.1 
 |-  ( ph -> T e. mFS )
5 mclspps.2 
 |-  ( ph -> K C_ D )
6 mclspps.3 
 |-  ( ph -> B C_ E )
7 mclspps.j 
 |-  J = ( mPPSt ` T )
8 mclspps.l 
 |-  L = ( mSubst ` T )
9 mclspps.v 
 |-  V = ( mVR ` T )
10 mclspps.h 
 |-  H = ( mVH ` T )
11 mclspps.w 
 |-  W = ( mVars ` T )
12 mclspps.4 
 |-  ( ph -> <. M , O , P >. e. J )
13 mclspps.5 
 |-  ( ph -> S e. ran L )
14 mclspps.6 
 |-  ( ( ph /\ x e. O ) -> ( S ` x ) e. ( K C B ) )
15 mclspps.7 
 |-  ( ( ph /\ v e. V ) -> ( S ` ( H ` v ) ) e. ( K C B ) )
16 mclspps.8 
 |-  ( ( ph /\ ( x M y /\ a e. ( W ` ( S ` ( H ` x ) ) ) /\ b e. ( W ` ( S ` ( H ` y ) ) ) ) ) -> a K b )
17 mclsppslem.9 
 |-  ( ph -> <. m , o , p >. e. ( mAx ` T ) )
18 mclsppslem.10 
 |-  ( ph -> s e. ran L )
19 mclsppslem.11 
 |-  ( ph -> ( s " ( o u. ran H ) ) C_ ( `' S " ( K C B ) ) )
20 mclsppslem.12 
 |-  ( ph -> A. z A. w ( z m w -> ( ( W ` ( s ` ( H ` z ) ) ) X. ( W ` ( s ` ( H ` w ) ) ) ) C_ M ) )
21 8 2 msubf 
 |-  ( s e. ran L -> s : E --> E )
22 18 21 syl 
 |-  ( ph -> s : E --> E )
23 eqid 
 |-  ( mAx ` T ) = ( mAx ` T )
24 eqid 
 |-  ( mStat ` T ) = ( mStat ` T )
25 23 24 maxsta 
 |-  ( T e. mFS -> ( mAx ` T ) C_ ( mStat ` T ) )
26 4 25 syl 
 |-  ( ph -> ( mAx ` T ) C_ ( mStat ` T ) )
27 eqid 
 |-  ( mPreSt ` T ) = ( mPreSt ` T )
28 27 24 mstapst 
 |-  ( mStat ` T ) C_ ( mPreSt ` T )
29 26 28 sstrdi 
 |-  ( ph -> ( mAx ` T ) C_ ( mPreSt ` T ) )
30 29 17 sseldd 
 |-  ( ph -> <. m , o , p >. e. ( mPreSt ` T ) )
31 1 2 27 elmpst 
 |-  ( <. m , o , p >. e. ( mPreSt ` T ) <-> ( ( m C_ D /\ `' m = m ) /\ ( o C_ E /\ o e. Fin ) /\ p e. E ) )
32 30 31 sylib 
 |-  ( ph -> ( ( m C_ D /\ `' m = m ) /\ ( o C_ E /\ o e. Fin ) /\ p e. E ) )
33 32 simp3d 
 |-  ( ph -> p e. E )
34 22 33 ffvelcdmd 
 |-  ( ph -> ( s ` p ) e. E )
35 fvco3 
 |-  ( ( s : E --> E /\ p e. E ) -> ( ( S o. s ) ` p ) = ( S ` ( s ` p ) ) )
36 22 33 35 syl2anc 
 |-  ( ph -> ( ( S o. s ) ` p ) = ( S ` ( s ` p ) ) )
37 8 msubco 
 |-  ( ( S e. ran L /\ s e. ran L ) -> ( S o. s ) e. ran L )
38 13 18 37 syl2anc 
 |-  ( ph -> ( S o. s ) e. ran L )
39 8 2 msubf 
 |-  ( S e. ran L -> S : E --> E )
40 13 39 syl 
 |-  ( ph -> S : E --> E )
41 fco 
 |-  ( ( S : E --> E /\ s : E --> E ) -> ( S o. s ) : E --> E )
42 40 22 41 syl2anc 
 |-  ( ph -> ( S o. s ) : E --> E )
43 42 ffnd 
 |-  ( ph -> ( S o. s ) Fn E )
44 43 adantr 
 |-  ( ( ph /\ c e. o ) -> ( S o. s ) Fn E )
45 22 ffund 
 |-  ( ph -> Fun s )
46 31 simp2bi 
 |-  ( <. m , o , p >. e. ( mPreSt ` T ) -> ( o C_ E /\ o e. Fin ) )
47 30 46 syl 
 |-  ( ph -> ( o C_ E /\ o e. Fin ) )
48 47 simpld 
 |-  ( ph -> o C_ E )
49 9 2 10 mvhf 
 |-  ( T e. mFS -> H : V --> E )
50 frn 
 |-  ( H : V --> E -> ran H C_ E )
51 4 49 50 3syl 
 |-  ( ph -> ran H C_ E )
52 48 51 unssd 
 |-  ( ph -> ( o u. ran H ) C_ E )
53 22 fdmd 
 |-  ( ph -> dom s = E )
54 52 53 sseqtrrd 
 |-  ( ph -> ( o u. ran H ) C_ dom s )
55 funimass3 
 |-  ( ( 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 ) ) ) ) )
56 45 54 55 syl2anc 
 |-  ( ph -> ( ( s " ( o u. ran H ) ) C_ ( `' S " ( K C B ) ) <-> ( o u. ran H ) C_ ( `' s " ( `' S " ( K C B ) ) ) ) )
57 19 56 mpbid 
 |-  ( ph -> ( o u. ran H ) C_ ( `' s " ( `' S " ( K C B ) ) ) )
58 cnvco 
 |-  `' ( S o. s ) = ( `' s o. `' S )
59 58 imaeq1i 
 |-  ( `' ( S o. s ) " ( K C B ) ) = ( ( `' s o. `' S ) " ( K C B ) )
60 imaco 
 |-  ( ( `' s o. `' S ) " ( K C B ) ) = ( `' s " ( `' S " ( K C B ) ) )
61 59 60 eqtri 
 |-  ( `' ( S o. s ) " ( K C B ) ) = ( `' s " ( `' S " ( K C B ) ) )
62 57 61 sseqtrrdi 
 |-  ( ph -> ( o u. ran H ) C_ ( `' ( S o. s ) " ( K C B ) ) )
63 62 unssad 
 |-  ( ph -> o C_ ( `' ( S o. s ) " ( K C B ) ) )
64 63 sselda 
 |-  ( ( ph /\ c e. o ) -> c e. ( `' ( S o. s ) " ( K C B ) ) )
65 elpreima 
 |-  ( ( S o. s ) Fn E -> ( c e. ( `' ( S o. s ) " ( K C B ) ) <-> ( c e. E /\ ( ( S o. s ) ` c ) e. ( K C B ) ) ) )
66 65 simplbda 
 |-  ( ( ( S o. s ) Fn E /\ c e. ( `' ( S o. s ) " ( K C B ) ) ) -> ( ( S o. s ) ` c ) e. ( K C B ) )
67 44 64 66 syl2anc 
 |-  ( ( ph /\ c e. o ) -> ( ( S o. s ) ` c ) e. ( K C B ) )
68 43 adantr 
 |-  ( ( ph /\ t e. V ) -> ( S o. s ) Fn E )
69 62 unssbd 
 |-  ( ph -> ran H C_ ( `' ( S o. s ) " ( K C B ) ) )
70 69 adantr 
 |-  ( ( ph /\ t e. V ) -> ran H C_ ( `' ( S o. s ) " ( K C B ) ) )
71 ffn 
 |-  ( H : V --> E -> H Fn V )
72 4 49 71 3syl 
 |-  ( ph -> H Fn V )
73 fnfvelrn 
 |-  ( ( H Fn V /\ t e. V ) -> ( H ` t ) e. ran H )
74 72 73 sylan 
 |-  ( ( ph /\ t e. V ) -> ( H ` t ) e. ran H )
75 70 74 sseldd 
 |-  ( ( ph /\ t e. V ) -> ( H ` t ) e. ( `' ( S o. s ) " ( K C B ) ) )
76 elpreima 
 |-  ( ( 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 ) ) ) )
77 76 simplbda 
 |-  ( ( ( S o. s ) Fn E /\ ( H ` t ) e. ( `' ( S o. s ) " ( K C B ) ) ) -> ( ( S o. s ) ` ( H ` t ) ) e. ( K C B ) )
78 68 75 77 syl2anc 
 |-  ( ( ph /\ t e. V ) -> ( ( S o. s ) ` ( H ` t ) ) e. ( K C B ) )
79 22 adantr 
 |-  ( ( ph /\ c m d ) -> s : E --> E )
80 4 49 syl 
 |-  ( ph -> H : V --> E )
81 80 adantr 
 |-  ( ( ph /\ c m d ) -> H : V --> E )
82 32 simp1d 
 |-  ( ph -> ( m C_ D /\ `' m = m ) )
83 82 simpld 
 |-  ( ph -> m C_ D )
84 9 1 mdvval 
 |-  D = ( ( V X. V ) \ _I )
85 difss 
 |-  ( ( V X. V ) \ _I ) C_ ( V X. V )
86 84 85 eqsstri 
 |-  D C_ ( V X. V )
87 83 86 sstrdi 
 |-  ( ph -> m C_ ( V X. V ) )
88 87 ssbrd 
 |-  ( ph -> ( c m d -> c ( V X. V ) d ) )
89 88 imp 
 |-  ( ( ph /\ c m d ) -> c ( V X. V ) d )
90 brxp 
 |-  ( c ( V X. V ) d <-> ( c e. V /\ d e. V ) )
91 89 90 sylib 
 |-  ( ( ph /\ c m d ) -> ( c e. V /\ d e. V ) )
92 91 simpld 
 |-  ( ( ph /\ c m d ) -> c e. V )
93 81 92 ffvelcdmd 
 |-  ( ( ph /\ c m d ) -> ( H ` c ) e. E )
94 fvco3 
 |-  ( ( s : E --> E /\ ( H ` c ) e. E ) -> ( ( S o. s ) ` ( H ` c ) ) = ( S ` ( s ` ( H ` c ) ) ) )
95 79 93 94 syl2anc 
 |-  ( ( ph /\ c m d ) -> ( ( S o. s ) ` ( H ` c ) ) = ( S ` ( s ` ( H ` c ) ) ) )
96 95 fveq2d 
 |-  ( ( ph /\ c m d ) -> ( W ` ( ( S o. s ) ` ( H ` c ) ) ) = ( W ` ( S ` ( s ` ( H ` c ) ) ) ) )
97 4 adantr 
 |-  ( ( ph /\ c m d ) -> T e. mFS )
98 13 adantr 
 |-  ( ( ph /\ c m d ) -> S e. ran L )
99 79 93 ffvelcdmd 
 |-  ( ( ph /\ c m d ) -> ( s ` ( H ` c ) ) e. E )
100 8 2 11 10 msubvrs 
 |-  ( ( 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 ) ) ) )
101 97 98 99 100 syl3anc 
 |-  ( ( ph /\ c m d ) -> ( W ` ( S ` ( s ` ( H ` c ) ) ) ) = U_ u e. ( W ` ( s ` ( H ` c ) ) ) ( W ` ( S ` ( H ` u ) ) ) )
102 96 101 eqtrd 
 |-  ( ( ph /\ c m d ) -> ( W ` ( ( S o. s ) ` ( H ` c ) ) ) = U_ u e. ( W ` ( s ` ( H ` c ) ) ) ( W ` ( S ` ( H ` u ) ) ) )
103 102 eleq2d 
 |-  ( ( 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 ) ) ) ) )
104 eliun 
 |-  ( 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 ) ) ) )
105 103 104 bitrdi 
 |-  ( ( 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 ) ) ) ) )
106 91 simprd 
 |-  ( ( ph /\ c m d ) -> d e. V )
107 81 106 ffvelcdmd 
 |-  ( ( ph /\ c m d ) -> ( H ` d ) e. E )
108 fvco3 
 |-  ( ( s : E --> E /\ ( H ` d ) e. E ) -> ( ( S o. s ) ` ( H ` d ) ) = ( S ` ( s ` ( H ` d ) ) ) )
109 79 107 108 syl2anc 
 |-  ( ( ph /\ c m d ) -> ( ( S o. s ) ` ( H ` d ) ) = ( S ` ( s ` ( H ` d ) ) ) )
110 109 fveq2d 
 |-  ( ( ph /\ c m d ) -> ( W ` ( ( S o. s ) ` ( H ` d ) ) ) = ( W ` ( S ` ( s ` ( H ` d ) ) ) ) )
111 79 107 ffvelcdmd 
 |-  ( ( ph /\ c m d ) -> ( s ` ( H ` d ) ) e. E )
112 8 2 11 10 msubvrs 
 |-  ( ( 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 ) ) ) )
113 97 98 111 112 syl3anc 
 |-  ( ( ph /\ c m d ) -> ( W ` ( S ` ( s ` ( H ` d ) ) ) ) = U_ v e. ( W ` ( s ` ( H ` d ) ) ) ( W ` ( S ` ( H ` v ) ) ) )
114 110 113 eqtrd 
 |-  ( ( ph /\ c m d ) -> ( W ` ( ( S o. s ) ` ( H ` d ) ) ) = U_ v e. ( W ` ( s ` ( H ` d ) ) ) ( W ` ( S ` ( H ` v ) ) ) )
115 114 eleq2d 
 |-  ( ( 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 ) ) ) ) )
116 eliun 
 |-  ( 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 ) ) ) )
117 115 116 bitrdi 
 |-  ( ( 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 ) ) ) ) )
118 105 117 anbi12d 
 |-  ( ( 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 ) ) ) ) ) )
119 reeanv 
 |-  ( 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 ) ) ) ) )
120 simpll 
 |-  ( ( ( ph /\ c m d ) /\ ( u e. ( W ` ( s ` ( H ` c ) ) ) /\ v e. ( W ` ( s ` ( H ` d ) ) ) ) ) -> ph )
121 brxp 
 |-  ( u ( ( W ` ( s ` ( H ` c ) ) ) X. ( W ` ( s ` ( H ` d ) ) ) ) v <-> ( u e. ( W ` ( s ` ( H ` c ) ) ) /\ v e. ( W ` ( s ` ( H ` d ) ) ) ) )
122 breq12 
 |-  ( ( z = c /\ w = d ) -> ( z m w <-> c m d ) )
123 simpl 
 |-  ( ( z = c /\ w = d ) -> z = c )
124 123 fveq2d 
 |-  ( ( z = c /\ w = d ) -> ( H ` z ) = ( H ` c ) )
125 124 fveq2d 
 |-  ( ( z = c /\ w = d ) -> ( s ` ( H ` z ) ) = ( s ` ( H ` c ) ) )
126 125 fveq2d 
 |-  ( ( z = c /\ w = d ) -> ( W ` ( s ` ( H ` z ) ) ) = ( W ` ( s ` ( H ` c ) ) ) )
127 simpr 
 |-  ( ( z = c /\ w = d ) -> w = d )
128 127 fveq2d 
 |-  ( ( z = c /\ w = d ) -> ( H ` w ) = ( H ` d ) )
129 128 fveq2d 
 |-  ( ( z = c /\ w = d ) -> ( s ` ( H ` w ) ) = ( s ` ( H ` d ) ) )
130 129 fveq2d 
 |-  ( ( z = c /\ w = d ) -> ( W ` ( s ` ( H ` w ) ) ) = ( W ` ( s ` ( H ` d ) ) ) )
131 126 130 xpeq12d 
 |-  ( ( z = c /\ w = d ) -> ( ( W ` ( s ` ( H ` z ) ) ) X. ( W ` ( s ` ( H ` w ) ) ) ) = ( ( W ` ( s ` ( H ` c ) ) ) X. ( W ` ( s ` ( H ` d ) ) ) ) )
132 131 sseq1d 
 |-  ( ( 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 ) )
133 122 132 imbi12d 
 |-  ( ( 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 ) ) )
134 133 spc2gv 
 |-  ( ( 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 ) ) )
135 134 el2v 
 |-  ( 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 ) )
136 20 135 syl 
 |-  ( ph -> ( c m d -> ( ( W ` ( s ` ( H ` c ) ) ) X. ( W ` ( s ` ( H ` d ) ) ) ) C_ M ) )
137 136 imp 
 |-  ( ( ph /\ c m d ) -> ( ( W ` ( s ` ( H ` c ) ) ) X. ( W ` ( s ` ( H ` d ) ) ) ) C_ M )
138 137 ssbrd 
 |-  ( ( ph /\ c m d ) -> ( u ( ( W ` ( s ` ( H ` c ) ) ) X. ( W ` ( s ` ( H ` d ) ) ) ) v -> u M v ) )
139 121 138 biimtrrid 
 |-  ( ( ph /\ c m d ) -> ( ( u e. ( W ` ( s ` ( H ` c ) ) ) /\ v e. ( W ` ( s ` ( H ` d ) ) ) ) -> u M v ) )
140 139 imp 
 |-  ( ( ( ph /\ c m d ) /\ ( u e. ( W ` ( s ` ( H ` c ) ) ) /\ v e. ( W ` ( s ` ( H ` d ) ) ) ) ) -> u M v )
141 vex 
 |-  u e. _V
142 vex 
 |-  v e. _V
143 breq12 
 |-  ( ( x = u /\ y = v ) -> ( x M y <-> u M v ) )
144 simpl 
 |-  ( ( x = u /\ y = v ) -> x = u )
145 144 fveq2d 
 |-  ( ( x = u /\ y = v ) -> ( H ` x ) = ( H ` u ) )
146 145 fveq2d 
 |-  ( ( x = u /\ y = v ) -> ( S ` ( H ` x ) ) = ( S ` ( H ` u ) ) )
147 146 fveq2d 
 |-  ( ( x = u /\ y = v ) -> ( W ` ( S ` ( H ` x ) ) ) = ( W ` ( S ` ( H ` u ) ) ) )
148 147 eleq2d 
 |-  ( ( x = u /\ y = v ) -> ( a e. ( W ` ( S ` ( H ` x ) ) ) <-> a e. ( W ` ( S ` ( H ` u ) ) ) ) )
149 simpr 
 |-  ( ( x = u /\ y = v ) -> y = v )
150 149 fveq2d 
 |-  ( ( x = u /\ y = v ) -> ( H ` y ) = ( H ` v ) )
151 150 fveq2d 
 |-  ( ( x = u /\ y = v ) -> ( S ` ( H ` y ) ) = ( S ` ( H ` v ) ) )
152 151 fveq2d 
 |-  ( ( x = u /\ y = v ) -> ( W ` ( S ` ( H ` y ) ) ) = ( W ` ( S ` ( H ` v ) ) ) )
153 152 eleq2d 
 |-  ( ( x = u /\ y = v ) -> ( b e. ( W ` ( S ` ( H ` y ) ) ) <-> b e. ( W ` ( S ` ( H ` v ) ) ) ) )
154 143 148 153 3anbi123d 
 |-  ( ( 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 ) ) ) ) ) )
155 154 anbi2d 
 |-  ( ( 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 ) ) ) ) ) ) )
156 155 imbi1d 
 |-  ( ( 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 141 142 156 16 vtocl2 
 |-  ( ( ph /\ ( u M v /\ a e. ( W ` ( S ` ( H ` u ) ) ) /\ b e. ( W ` ( S ` ( H ` v ) ) ) ) ) -> a K b )
158 157 3exp2 
 |-  ( ph -> ( u M v -> ( a e. ( W ` ( S ` ( H ` u ) ) ) -> ( b e. ( W ` ( S ` ( H ` v ) ) ) -> a K b ) ) ) )
159 158 imp4b 
 |-  ( ( ph /\ u M v ) -> ( ( a e. ( W ` ( S ` ( H ` u ) ) ) /\ b e. ( W ` ( S ` ( H ` v ) ) ) ) -> a K b ) )
160 120 140 159 syl2anc 
 |-  ( ( ( 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 ) )
161 160 rexlimdvva 
 |-  ( ( 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 ) )
162 119 161 biimtrrid 
 |-  ( ( 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 ) )
163 118 162 sylbid 
 |-  ( ( ph /\ c m d ) -> ( ( a e. ( W ` ( ( S o. s ) ` ( H ` c ) ) ) /\ b e. ( W ` ( ( S o. s ) ` ( H ` d ) ) ) ) -> a K b ) )
164 163 exp4b 
 |-  ( ph -> ( c m d -> ( a e. ( W ` ( ( S o. s ) ` ( H ` c ) ) ) -> ( b e. ( W ` ( ( S o. s ) ` ( H ` d ) ) ) -> a K b ) ) ) )
165 164 3imp2 
 |-  ( ( ph /\ ( c m d /\ a e. ( W ` ( ( S o. s ) ` ( H ` c ) ) ) /\ b e. ( W ` ( ( S o. s ) ` ( H ` d ) ) ) ) ) -> a K b )
166 1 2 3 4 5 6 23 8 9 10 11 17 38 67 78 165 mclsax 
 |-  ( ph -> ( ( S o. s ) ` p ) e. ( K C B ) )
167 36 166 eqeltrrd 
 |-  ( ph -> ( S ` ( s ` p ) ) e. ( K C B ) )
168 40 ffnd 
 |-  ( ph -> S Fn E )
169 elpreima 
 |-  ( S Fn E -> ( ( s ` p ) e. ( `' S " ( K C B ) ) <-> ( ( s ` p ) e. E /\ ( S ` ( s ` p ) ) e. ( K C B ) ) ) )
170 168 169 syl 
 |-  ( ph -> ( ( s ` p ) e. ( `' S " ( K C B ) ) <-> ( ( s ` p ) e. E /\ ( S ` ( s ` p ) ) e. ( K C B ) ) ) )
171 34 167 170 mpbir2and 
 |-  ( ph -> ( s ` p ) e. ( `' S " ( K C B ) ) )