Metamath Proof Explorer

Theorem mclsax

Description: The closure is closed under axiom application. (Contributed by Mario Carneiro, 18-Jul-2016)

Ref Expression
Hypotheses mclsval.d 
|- D = ( mDV ` T )
mclsval.e 
|- E = ( mEx ` T )
mclsval.c 
|- C = ( mCls ` T )
mclsval.1 
|- ( ph -> T e. mFS )
mclsval.2 
|- ( ph -> K C_ D )
mclsval.3 
|- ( ph -> B C_ E )
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 mclsax 
|- ( ph -> ( S ` P ) e. ( K C B ) )

Proof

Step Hyp Ref Expression
1 mclsval.d 
 |-  D = ( mDV ` T )
2 mclsval.e 
 |-  E = ( mEx ` T )
3 mclsval.c 
 |-  C = ( mCls ` T )
4 mclsval.1 
 |-  ( ph -> T e. mFS )
5 mclsval.2 
 |-  ( ph -> K C_ D )
6 mclsval.3 
 |-  ( ph -> B C_ E )
7 mclsax.a 
 |-  A = ( mAx ` T )
8 mclsax.l 
 |-  L = ( mSubst ` T )
9 mclsax.v 
 |-  V = ( mVR ` T )
10 mclsax.h 
 |-  H = ( mVH ` T )
11 mclsax.w 
 |-  W = ( mVars ` T )
12 mclsax.4 
 |-  ( ph -> <. M , O , P >. e. A )
13 mclsax.5 
 |-  ( ph -> S e. ran L )
14 mclsax.6 
 |-  ( ( ph /\ x e. O ) -> ( S ` x ) e. ( K C B ) )
15 mclsax.7 
 |-  ( ( ph /\ v e. V ) -> ( S ` ( H ` v ) ) e. ( K C B ) )
16 mclsax.8 
 |-  ( ( ph /\ ( x M y /\ a e. ( W ` ( S ` ( H ` x ) ) ) /\ b e. ( W ` ( S ` ( H ` y ) ) ) ) ) -> a K b )
17 abid 
 |-  ( 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 ) ) ) )
18 intss1 
 |-  ( 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 )
19 17 18 sylbir 
 |-  ( ( ( 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 )
20 1 2 3 4 5 6 10 7 8 11 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 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 ) ) ) } )
21 20 sseq1d 
 |-  ( 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 ) )
22 19 21 syl5ibr 
 |-  ( 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 ) )
23 sstr2 
 |-  ( ( s " ( o u. ran H ) ) C_ ( K C B ) -> ( ( K C B ) C_ c -> ( s " ( o u. ran H ) ) C_ c ) )
24 23 com12 
 |-  ( ( K C B ) C_ c -> ( ( s " ( o u. ran H ) ) C_ ( K C B ) -> ( s " ( o u. ran H ) ) C_ c ) )
25 24 anim1d 
 |-  ( ( 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 ) ) ) )
26 25 imim1d 
 |-  ( ( 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 ) ) )
27 26 ralimdv 
 |-  ( ( 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 ) ) )
28 27 imim2d 
 |-  ( ( 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 ) ) ) )
29 28 alimdv 
 |-  ( ( 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 ) ) ) )
30 29 2alimdv 
 |-  ( ( 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 ) ) ) )
31 30 com12 
 |-  ( 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 ) ) ) )
32 31 adantl 
 |-  ( ( ( 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 ) ) ) )
33 22 32 sylcom 
 |-  ( 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 ) ) ) )
34 eqid 
 |-  ( mPreSt ` T ) = ( mPreSt ` T )
35 eqid 
 |-  ( mStat ` T ) = ( mStat ` T )
36 34 35 mstapst 
 |-  ( mStat ` T ) C_ ( mPreSt ` T )
37 7 35 maxsta 
 |-  ( T e. mFS -> A C_ ( mStat ` T ) )
38 4 37 syl 
 |-  ( ph -> A C_ ( mStat ` T ) )
39 38 12 sseldd 
 |-  ( ph -> <. M , O , P >. e. ( mStat ` T ) )
40 36 39 sselid 
 |-  ( ph -> <. M , O , P >. e. ( mPreSt ` T ) )
41 34 mpstrcl 
 |-  ( <. M , O , P >. e. ( mPreSt ` T ) -> ( M e. _V /\ O e. _V /\ P e. _V ) )
42 simp1 
 |-  ( ( m = M /\ o = O /\ p = P ) -> m = M )
43 simp2 
 |-  ( ( m = M /\ o = O /\ p = P ) -> o = O )
44 simp3 
 |-  ( ( m = M /\ o = O /\ p = P ) -> p = P )
45 42 43 44 oteq123d 
 |-  ( ( m = M /\ o = O /\ p = P ) -> <. m , o , p >. = <. M , O , P >. )
46 45 eleq1d 
 |-  ( ( m = M /\ o = O /\ p = P ) -> ( <. m , o , p >. e. A <-> <. M , O , P >. e. A ) )
47 43 uneq1d 
 |-  ( ( m = M /\ o = O /\ p = P ) -> ( o u. ran H ) = ( O u. ran H ) )
48 47 imaeq2d 
 |-  ( ( m = M /\ o = O /\ p = P ) -> ( s " ( o u. ran H ) ) = ( s " ( O u. ran H ) ) )
49 48 sseq1d 
 |-  ( ( m = M /\ o = O /\ p = P ) -> ( ( s " ( o u. ran H ) ) C_ ( K C B ) <-> ( s " ( O u. ran H ) ) C_ ( K C B ) ) )
50 42 breqd 
 |-  ( ( m = M /\ o = O /\ p = P ) -> ( x m y <-> x M y ) )
51 50 imbi1d 
 |-  ( ( 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 ) ) )
52 51 2albidv 
 |-  ( ( 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 ) ) )
53 49 52 anbi12d 
 |-  ( ( 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 ) ) ) )
54 44 fveq2d 
 |-  ( ( m = M /\ o = O /\ p = P ) -> ( s ` p ) = ( s ` P ) )
55 54 eleq1d 
 |-  ( ( m = M /\ o = O /\ p = P ) -> ( ( s ` p ) e. c <-> ( s ` P ) e. c ) )
56 53 55 imbi12d 
 |-  ( ( 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 ) ) )
57 56 ralbidv 
 |-  ( ( 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 ) ) )
58 46 57 imbi12d 
 |-  ( ( 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 ) ) ) )
59 58 spc3gv 
 |-  ( ( 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 ) ) ) )
60 40 41 59 3syl 
 |-  ( 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 ) ) ) )
61 elun 
 |-  ( x e. ( O u. ran H ) <-> ( x e. O \/ x e. ran H ) )
62 15 ralrimiva 
 |-  ( ph -> A. v e. V ( S ` ( H ` v ) ) e. ( K C B ) )
63 9 2 10 mvhf 
 |-  ( T e. mFS -> H : V --> E )
64 4 63 syl 
 |-  ( ph -> H : V --> E )
65 ffn 
 |-  ( H : V --> E -> H Fn V )
66 fveq2 
 |-  ( x = ( H ` v ) -> ( S ` x ) = ( S ` ( H ` v ) ) )
67 66 eleq1d 
 |-  ( x = ( H ` v ) -> ( ( S ` x ) e. ( K C B ) <-> ( S ` ( H ` v ) ) e. ( K C B ) ) )
68 67 ralrn 
 |-  ( 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 ) ) )
69 64 65 68 3syl 
 |-  ( ph -> ( A. x e. ran H ( S ` x ) e. ( K C B ) <-> A. v e. V ( S ` ( H ` v ) ) e. ( K C B ) ) )
70 62 69 mpbird 
 |-  ( ph -> A. x e. ran H ( S ` x ) e. ( K C B ) )
71 70 r19.21bi 
 |-  ( ( ph /\ x e. ran H ) -> ( S ` x ) e. ( K C B ) )
72 14 71 jaodan 
 |-  ( ( ph /\ ( x e. O \/ x e. ran H ) ) -> ( S ` x ) e. ( K C B ) )
73 61 72 sylan2b 
 |-  ( ( ph /\ x e. ( O u. ran H ) ) -> ( S ` x ) e. ( K C B ) )
74 73 ralrimiva 
 |-  ( ph -> A. x e. ( O u. ran H ) ( S ` x ) e. ( K C B ) )
75 8 2 msubf 
 |-  ( S e. ran L -> S : E --> E )
76 13 75 syl 
 |-  ( ph -> S : E --> E )
77 76 ffund 
 |-  ( ph -> Fun S )
78 1 2 34 elmpst 
 |-  ( <. M , O , P >. e. ( mPreSt ` T ) <-> ( ( M C_ D /\ `' M = M ) /\ ( O C_ E /\ O e. Fin ) /\ P e. E ) )
79 40 78 sylib 
 |-  ( ph -> ( ( M C_ D /\ `' M = M ) /\ ( O C_ E /\ O e. Fin ) /\ P e. E ) )
80 79 simp2d 
 |-  ( ph -> ( O C_ E /\ O e. Fin ) )
81 80 simpld 
 |-  ( ph -> O C_ E )
82 76 fdmd 
 |-  ( ph -> dom S = E )
83 81 82 sseqtrrd 
 |-  ( ph -> O C_ dom S )
84 64 frnd 
 |-  ( ph -> ran H C_ E )
85 84 82 sseqtrrd 
 |-  ( ph -> ran H C_ dom S )
86 83 85 unssd 
 |-  ( ph -> ( O u. ran H ) C_ dom S )
87 funimass4 
 |-  ( ( 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 ) ) )
88 77 86 87 syl2anc 
 |-  ( ph -> ( ( S " ( O u. ran H ) ) C_ ( K C B ) <-> A. x e. ( O u. ran H ) ( S ` x ) e. ( K C B ) ) )
89 74 88 mpbird 
 |-  ( ph -> ( S " ( O u. ran H ) ) C_ ( K C B ) )
90 16 3exp2 
 |-  ( ph -> ( x M y -> ( a e. ( W ` ( S ` ( H ` x ) ) ) -> ( b e. ( W ` ( S ` ( H ` y ) ) ) -> a K b ) ) ) )
91 90 imp4b 
 |-  ( ( ph /\ x M y ) -> ( ( a e. ( W ` ( S ` ( H ` x ) ) ) /\ b e. ( W ` ( S ` ( H ` y ) ) ) ) -> a K b ) )
92 91 ralrimivv 
 |-  ( ( ph /\ x M y ) -> A. a e. ( W ` ( S ` ( H ` x ) ) ) A. b e. ( W ` ( S ` ( H ` y ) ) ) a K b )
93 dfss3 
 |-  ( ( ( 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 )
94 eleq1 
 |-  ( z = <. a , b >. -> ( z e. K <-> <. a , b >. e. K ) )
95 df-br 
 |-  ( a K b <-> <. a , b >. e. K )
96 94 95 bitr4di 
 |-  ( z = <. a , b >. -> ( z e. K <-> a K b ) )
97 96 ralxp 
 |-  ( 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 )
98 93 97 bitri 
 |-  ( ( ( 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 )
99 92 98 sylibr 
 |-  ( ( ph /\ x M y ) -> ( ( W ` ( S ` ( H ` x ) ) ) X. ( W ` ( S ` ( H ` y ) ) ) ) C_ K )
100 99 ex 
 |-  ( ph -> ( x M y -> ( ( W ` ( S ` ( H ` x ) ) ) X. ( W ` ( S ` ( H ` y ) ) ) ) C_ K ) )
101 100 alrimivv 
 |-  ( ph -> A. x A. y ( x M y -> ( ( W ` ( S ` ( H ` x ) ) ) X. ( W ` ( S ` ( H ` y ) ) ) ) C_ K ) )
102 89 101 jca 
 |-  ( 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 ) ) )
103 imaeq1 
 |-  ( s = S -> ( s " ( O u. ran H ) ) = ( S " ( O u. ran H ) ) )
104 103 sseq1d 
 |-  ( s = S -> ( ( s " ( O u. ran H ) ) C_ ( K C B ) <-> ( S " ( O u. ran H ) ) C_ ( K C B ) ) )
105 fveq1 
 |-  ( s = S -> ( s ` ( H ` x ) ) = ( S ` ( H ` x ) ) )
106 105 fveq2d 
 |-  ( s = S -> ( W ` ( s ` ( H ` x ) ) ) = ( W ` ( S ` ( H ` x ) ) ) )
107 fveq1 
 |-  ( s = S -> ( s ` ( H ` y ) ) = ( S ` ( H ` y ) ) )
108 107 fveq2d 
 |-  ( s = S -> ( W ` ( s ` ( H ` y ) ) ) = ( W ` ( S ` ( H ` y ) ) ) )
109 106 108 xpeq12d 
 |-  ( s = S -> ( ( W ` ( s ` ( H ` x ) ) ) X. ( W ` ( s ` ( H ` y ) ) ) ) = ( ( W ` ( S ` ( H ` x ) ) ) X. ( W ` ( S ` ( H ` y ) ) ) ) )
110 109 sseq1d 
 |-  ( s = S -> ( ( ( W ` ( s ` ( H ` x ) ) ) X. ( W ` ( s ` ( H ` y ) ) ) ) C_ K <-> ( ( W ` ( S ` ( H ` x ) ) ) X. ( W ` ( S ` ( H ` y ) ) ) ) C_ K ) )
111 110 imbi2d 
 |-  ( 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 ) ) )
112 111 2albidv 
 |-  ( 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 ) ) )
113 104 112 anbi12d 
 |-  ( 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 ) ) ) )
114 fveq1 
 |-  ( s = S -> ( s ` P ) = ( S ` P ) )
115 114 eleq1d 
 |-  ( s = S -> ( ( s ` P ) e. c <-> ( S ` P ) e. c ) )
116 113 115 imbi12d 
 |-  ( 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 ) ) )
117 116 rspcv 
 |-  ( 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 ) ) )
118 13 117 syl 
 |-  ( 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 ) ) )
119 102 118 mpid 
 |-  ( 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 ) )
120 12 119 embantd 
 |-  ( 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 ) )
121 33 60 120 3syld 
 |-  ( 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 ) )
122 121 alrimiv 
 |-  ( 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 ) )
123 fvex 
 |-  ( S ` P ) e. _V
124 123 elintab 
 |-  ( ( 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 ) )
125 122 124 sylibr 
 |-  ( 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 ) ) ) } )
126 125 20 eleqtrrd 
 |-  ( ph -> ( S ` P ) e. ( K C B ) )