Metamath Proof Explorer

Theorem hbtlem6

Description: There is a finite set of polynomials matching any single stage of the image. (Contributed by Stefan O'Rear, 1-Apr-2015)

Ref Expression
Hypotheses hbtlem.p 
|- P = ( Poly1 ` R )
hbtlem.u 
|- U = ( LIdeal ` P )
hbtlem.s 
|- S = ( ldgIdlSeq ` R )
hbtlem6.n 
|- N = ( RSpan ` P )
hbtlem6.r 
|- ( ph -> R e. LNoeR )
hbtlem6.i 
|- ( ph -> I e. U )
hbtlem6.x 
|- ( ph -> X e. NN0 )
Assertion hbtlem6 
|- ( ph -> E. k e. ( ~P I i^i Fin ) ( ( S ` I ) ` X ) C_ ( ( S ` ( N ` k ) ) ` X ) )

Proof

Step Hyp Ref Expression
1 hbtlem.p 
 |-  P = ( Poly1 ` R )
2 hbtlem.u 
 |-  U = ( LIdeal ` P )
3 hbtlem.s 
 |-  S = ( ldgIdlSeq ` R )
4 hbtlem6.n 
 |-  N = ( RSpan ` P )
5 hbtlem6.r 
 |-  ( ph -> R e. LNoeR )
6 hbtlem6.i 
 |-  ( ph -> I e. U )
7 hbtlem6.x 
 |-  ( ph -> X e. NN0 )
8 lnrring 
 |-  ( R e. LNoeR -> R e. Ring )
9 5 8 syl 
 |-  ( ph -> R e. Ring )
10 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
11 1 2 3 10 hbtlem2 
 |-  ( ( R e. Ring /\ I e. U /\ X e. NN0 ) -> ( ( S ` I ) ` X ) e. ( LIdeal ` R ) )
12 9 6 7 11 syl3anc 
 |-  ( ph -> ( ( S ` I ) ` X ) e. ( LIdeal ` R ) )
13 eqid 
 |-  ( RSpan ` R ) = ( RSpan ` R )
14 10 13 lnr2i 
 |-  ( ( R e. LNoeR /\ ( ( S ` I ) ` X ) e. ( LIdeal ` R ) ) -> E. a e. ( ~P ( ( S ` I ) ` X ) i^i Fin ) ( ( S ` I ) ` X ) = ( ( RSpan ` R ) ` a ) )
15 5 12 14 syl2anc 
 |-  ( ph -> E. a e. ( ~P ( ( S ` I ) ` X ) i^i Fin ) ( ( S ` I ) ` X ) = ( ( RSpan ` R ) ` a ) )
16 elfpw 
 |-  ( a e. ( ~P ( ( S ` I ) ` X ) i^i Fin ) <-> ( a C_ ( ( S ` I ) ` X ) /\ a e. Fin ) )
17 fvex 
 |-  ( ( coe1 ` b ) ` X ) e. _V
18 eqid 
 |-  ( b e. { c e. I | ( ( deg1 ` R ) ` c ) <_ X } |-> ( ( coe1 ` b ) ` X ) ) = ( b e. { c e. I | ( ( deg1 ` R ) ` c ) <_ X } |-> ( ( coe1 ` b ) ` X ) )
19 17 18 fnmpti 
 |-  ( b e. { c e. I | ( ( deg1 ` R ) ` c ) <_ X } |-> ( ( coe1 ` b ) ` X ) ) Fn { c e. I | ( ( deg1 ` R ) ` c ) <_ X }
20 19 a1i 
 |-  ( ( ph /\ ( a C_ ( ( S ` I ) ` X ) /\ a e. Fin ) ) -> ( b e. { c e. I | ( ( deg1 ` R ) ` c ) <_ X } |-> ( ( coe1 ` b ) ` X ) ) Fn { c e. I | ( ( deg1 ` R ) ` c ) <_ X } )
21 simprl 
 |-  ( ( ph /\ ( a C_ ( ( S ` I ) ` X ) /\ a e. Fin ) ) -> a C_ ( ( S ` I ) ` X ) )
22 eqid 
 |-  ( deg1 ` R ) = ( deg1 ` R )
23 1 2 3 22 hbtlem1 
 |-  ( ( R e. LNoeR /\ I e. U /\ X e. NN0 ) -> ( ( S ` I ) ` X ) = { d | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ d = ( ( coe1 ` b ) ` X ) ) } )
24 5 6 7 23 syl3anc 
 |-  ( ph -> ( ( S ` I ) ` X ) = { d | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ d = ( ( coe1 ` b ) ` X ) ) } )
25 18 rnmpt 
 |-  ran ( b e. { c e. I | ( ( deg1 ` R ) ` c ) <_ X } |-> ( ( coe1 ` b ) ` X ) ) = { d | E. b e. { c e. I | ( ( deg1 ` R ) ` c ) <_ X } d = ( ( coe1 ` b ) ` X ) }
26 fveq2 
 |-  ( c = b -> ( ( deg1 ` R ) ` c ) = ( ( deg1 ` R ) ` b ) )
27 26 breq1d 
 |-  ( c = b -> ( ( ( deg1 ` R ) ` c ) <_ X <-> ( ( deg1 ` R ) ` b ) <_ X ) )
28 27 rexrab 
 |-  ( E. b e. { c e. I | ( ( deg1 ` R ) ` c ) <_ X } d = ( ( coe1 ` b ) ` X ) <-> E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ d = ( ( coe1 ` b ) ` X ) ) )
29 28 abbii 
 |-  { d | E. b e. { c e. I | ( ( deg1 ` R ) ` c ) <_ X } d = ( ( coe1 ` b ) ` X ) } = { d | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ d = ( ( coe1 ` b ) ` X ) ) }
30 25 29 eqtri 
 |-  ran ( b e. { c e. I | ( ( deg1 ` R ) ` c ) <_ X } |-> ( ( coe1 ` b ) ` X ) ) = { d | E. b e. I ( ( ( deg1 ` R ) ` b ) <_ X /\ d = ( ( coe1 ` b ) ` X ) ) }
31 24 30 eqtr4di 
 |-  ( ph -> ( ( S ` I ) ` X ) = ran ( b e. { c e. I | ( ( deg1 ` R ) ` c ) <_ X } |-> ( ( coe1 ` b ) ` X ) ) )
32 31 adantr 
 |-  ( ( ph /\ ( a C_ ( ( S ` I ) ` X ) /\ a e. Fin ) ) -> ( ( S ` I ) ` X ) = ran ( b e. { c e. I | ( ( deg1 ` R ) ` c ) <_ X } |-> ( ( coe1 ` b ) ` X ) ) )
33 21 32 sseqtrd 
 |-  ( ( ph /\ ( a C_ ( ( S ` I ) ` X ) /\ a e. Fin ) ) -> a C_ ran ( b e. { c e. I | ( ( deg1 ` R ) ` c ) <_ X } |-> ( ( coe1 ` b ) ` X ) ) )
34 simprr 
 |-  ( ( ph /\ ( a C_ ( ( S ` I ) ` X ) /\ a e. Fin ) ) -> a e. Fin )
35 fipreima 
 |-  ( ( ( b e. { c e. I | ( ( deg1 ` R ) ` c ) <_ X } |-> ( ( coe1 ` b ) ` X ) ) Fn { c e. I | ( ( deg1 ` R ) ` c ) <_ X } /\ a C_ ran ( b e. { c e. I | ( ( deg1 ` R ) ` c ) <_ X } |-> ( ( coe1 ` b ) ` X ) ) /\ a e. Fin ) -> E. k e. ( ~P { c e. I | ( ( deg1 ` R ) ` c ) <_ X } i^i Fin ) ( ( b e. { c e. I | ( ( deg1 ` R ) ` c ) <_ X } |-> ( ( coe1 ` b ) ` X ) ) " k ) = a )
36 20 33 34 35 syl3anc 
 |-  ( ( ph /\ ( a C_ ( ( S ` I ) ` X ) /\ a e. Fin ) ) -> E. k e. ( ~P { c e. I | ( ( deg1 ` R ) ` c ) <_ X } i^i Fin ) ( ( b e. { c e. I | ( ( deg1 ` R ) ` c ) <_ X } |-> ( ( coe1 ` b ) ` X ) ) " k ) = a )
37 elfpw 
 |-  ( k e. ( ~P { c e. I | ( ( deg1 ` R ) ` c ) <_ X } i^i Fin ) <-> ( k C_ { c e. I | ( ( deg1 ` R ) ` c ) <_ X } /\ k e. Fin ) )
38 ssrab2 
 |-  { c e. I | ( ( deg1 ` R ) ` c ) <_ X } C_ I
39 sstr2 
 |-  ( k C_ { c e. I | ( ( deg1 ` R ) ` c ) <_ X } -> ( { c e. I | ( ( deg1 ` R ) ` c ) <_ X } C_ I -> k C_ I ) )
40 38 39 mpi 
 |-  ( k C_ { c e. I | ( ( deg1 ` R ) ` c ) <_ X } -> k C_ I )
41 40 adantl 
 |-  ( ( ph /\ k C_ { c e. I | ( ( deg1 ` R ) ` c ) <_ X } ) -> k C_ I )
42 velpw 
 |-  ( k e. ~P I <-> k C_ I )
43 41 42 sylibr 
 |-  ( ( ph /\ k C_ { c e. I | ( ( deg1 ` R ) ` c ) <_ X } ) -> k e. ~P I )
44 43 adantrr 
 |-  ( ( ph /\ ( k C_ { c e. I | ( ( deg1 ` R ) ` c ) <_ X } /\ k e. Fin ) ) -> k e. ~P I )
45 simprr 
 |-  ( ( ph /\ ( k C_ { c e. I | ( ( deg1 ` R ) ` c ) <_ X } /\ k e. Fin ) ) -> k e. Fin )
46 44 45 elind 
 |-  ( ( ph /\ ( k C_ { c e. I | ( ( deg1 ` R ) ` c ) <_ X } /\ k e. Fin ) ) -> k e. ( ~P I i^i Fin ) )
47 9 adantr 
 |-  ( ( ph /\ ( k C_ { c e. I | ( ( deg1 ` R ) ` c ) <_ X } /\ k e. Fin ) ) -> R e. Ring )
48 1 ply1ring 
 |-  ( R e. Ring -> P e. Ring )
49 9 48 syl 
 |-  ( ph -> P e. Ring )
50 49 adantr 
 |-  ( ( ph /\ ( k C_ { c e. I | ( ( deg1 ` R ) ` c ) <_ X } /\ k e. Fin ) ) -> P e. Ring )
51 simprl 
 |-  ( ( ph /\ ( k C_ { c e. I | ( ( deg1 ` R ) ` c ) <_ X } /\ k e. Fin ) ) -> k C_ { c e. I | ( ( deg1 ` R ) ` c ) <_ X } )
52 51 38 sstrdi 
 |-  ( ( ph /\ ( k C_ { c e. I | ( ( deg1 ` R ) ` c ) <_ X } /\ k e. Fin ) ) -> k C_ I )
53 eqid 
 |-  ( Base ` P ) = ( Base ` P )
54 53 2 lidlss 
 |-  ( I e. U -> I C_ ( Base ` P ) )
55 6 54 syl 
 |-  ( ph -> I C_ ( Base ` P ) )
56 55 adantr 
 |-  ( ( ph /\ ( k C_ { c e. I | ( ( deg1 ` R ) ` c ) <_ X } /\ k e. Fin ) ) -> I C_ ( Base ` P ) )
57 52 56 sstrd 
 |-  ( ( ph /\ ( k C_ { c e. I | ( ( deg1 ` R ) ` c ) <_ X } /\ k e. Fin ) ) -> k C_ ( Base ` P ) )
58 4 53 2 rspcl 
 |-  ( ( P e. Ring /\ k C_ ( Base ` P ) ) -> ( N ` k ) e. U )
59 50 57 58 syl2anc 
 |-  ( ( ph /\ ( k C_ { c e. I | ( ( deg1 ` R ) ` c ) <_ X } /\ k e. Fin ) ) -> ( N ` k ) e. U )
60 7 adantr 
 |-  ( ( ph /\ ( k C_ { c e. I | ( ( deg1 ` R ) ` c ) <_ X } /\ k e. Fin ) ) -> X e. NN0 )
61 1 2 3 10 hbtlem2 
 |-  ( ( R e. Ring /\ ( N ` k ) e. U /\ X e. NN0 ) -> ( ( S ` ( N ` k ) ) ` X ) e. ( LIdeal ` R ) )
62 47 59 60 61 syl3anc 
 |-  ( ( ph /\ ( k C_ { c e. I | ( ( deg1 ` R ) ` c ) <_ X } /\ k e. Fin ) ) -> ( ( S ` ( N ` k ) ) ` X ) e. ( LIdeal ` R ) )
63 df-ima 
 |-  ( ( b e. { c e. I | ( ( deg1 ` R ) ` c ) <_ X } |-> ( ( coe1 ` b ) ` X ) ) " k ) = ran ( ( b e. { c e. I | ( ( deg1 ` R ) ` c ) <_ X } |-> ( ( coe1 ` b ) ` X ) ) |` k )
64 4 53 rspssid 
 |-  ( ( P e. Ring /\ k C_ ( Base ` P ) ) -> k C_ ( N ` k ) )
65 50 57 64 syl2anc 
 |-  ( ( ph /\ ( k C_ { c e. I | ( ( deg1 ` R ) ` c ) <_ X } /\ k e. Fin ) ) -> k C_ ( N ` k ) )
66 ssrab 
 |-  ( k C_ { c e. I | ( ( deg1 ` R ) ` c ) <_ X } <-> ( k C_ I /\ A. c e. k ( ( deg1 ` R ) ` c ) <_ X ) )
67 66 simprbi 
 |-  ( k C_ { c e. I | ( ( deg1 ` R ) ` c ) <_ X } -> A. c e. k ( ( deg1 ` R ) ` c ) <_ X )
68 67 ad2antrl 
 |-  ( ( ph /\ ( k C_ { c e. I | ( ( deg1 ` R ) ` c ) <_ X } /\ k e. Fin ) ) -> A. c e. k ( ( deg1 ` R ) ` c ) <_ X )
69 ssrab 
 |-  ( k C_ { c e. ( N ` k ) | ( ( deg1 ` R ) ` c ) <_ X } <-> ( k C_ ( N ` k ) /\ A. c e. k ( ( deg1 ` R ) ` c ) <_ X ) )
70 65 68 69 sylanbrc 
 |-  ( ( ph /\ ( k C_ { c e. I | ( ( deg1 ` R ) ` c ) <_ X } /\ k e. Fin ) ) -> k C_ { c e. ( N ` k ) | ( ( deg1 ` R ) ` c ) <_ X } )
71 70 resmptd 
 |-  ( ( ph /\ ( k C_ { c e. I | ( ( deg1 ` R ) ` c ) <_ X } /\ k e. Fin ) ) -> ( ( b e. { c e. ( N ` k ) | ( ( deg1 ` R ) ` c ) <_ X } |-> ( ( coe1 ` b ) ` X ) ) |` k ) = ( b e. k |-> ( ( coe1 ` b ) ` X ) ) )
72 resmpt 
 |-  ( k C_ { c e. I | ( ( deg1 ` R ) ` c ) <_ X } -> ( ( b e. { c e. I | ( ( deg1 ` R ) ` c ) <_ X } |-> ( ( coe1 ` b ) ` X ) ) |` k ) = ( b e. k |-> ( ( coe1 ` b ) ` X ) ) )
73 72 ad2antrl 
 |-  ( ( ph /\ ( k C_ { c e. I | ( ( deg1 ` R ) ` c ) <_ X } /\ k e. Fin ) ) -> ( ( b e. { c e. I | ( ( deg1 ` R ) ` c ) <_ X } |-> ( ( coe1 ` b ) ` X ) ) |` k ) = ( b e. k |-> ( ( coe1 ` b ) ` X ) ) )
74 71 73 eqtr4d 
 |-  ( ( ph /\ ( k C_ { c e. I | ( ( deg1 ` R ) ` c ) <_ X } /\ k e. Fin ) ) -> ( ( b e. { c e. ( N ` k ) | ( ( deg1 ` R ) ` c ) <_ X } |-> ( ( coe1 ` b ) ` X ) ) |` k ) = ( ( b e. { c e. I | ( ( deg1 ` R ) ` c ) <_ X } |-> ( ( coe1 ` b ) ` X ) ) |` k ) )
75 resss 
 |-  ( ( b e. { c e. ( N ` k ) | ( ( deg1 ` R ) ` c ) <_ X } |-> ( ( coe1 ` b ) ` X ) ) |` k ) C_ ( b e. { c e. ( N ` k ) | ( ( deg1 ` R ) ` c ) <_ X } |-> ( ( coe1 ` b ) ` X ) )
76 74 75 eqsstrrdi 
 |-  ( ( ph /\ ( k C_ { c e. I | ( ( deg1 ` R ) ` c ) <_ X } /\ k e. Fin ) ) -> ( ( b e. { c e. I | ( ( deg1 ` R ) ` c ) <_ X } |-> ( ( coe1 ` b ) ` X ) ) |` k ) C_ ( b e. { c e. ( N ` k ) | ( ( deg1 ` R ) ` c ) <_ X } |-> ( ( coe1 ` b ) ` X ) ) )
77 rnss 
 |-  ( ( ( b e. { c e. I | ( ( deg1 ` R ) ` c ) <_ X } |-> ( ( coe1 ` b ) ` X ) ) |` k ) C_ ( b e. { c e. ( N ` k ) | ( ( deg1 ` R ) ` c ) <_ X } |-> ( ( coe1 ` b ) ` X ) ) -> ran ( ( b e. { c e. I | ( ( deg1 ` R ) ` c ) <_ X } |-> ( ( coe1 ` b ) ` X ) ) |` k ) C_ ran ( b e. { c e. ( N ` k ) | ( ( deg1 ` R ) ` c ) <_ X } |-> ( ( coe1 ` b ) ` X ) ) )
78 76 77 syl 
 |-  ( ( ph /\ ( k C_ { c e. I | ( ( deg1 ` R ) ` c ) <_ X } /\ k e. Fin ) ) -> ran ( ( b e. { c e. I | ( ( deg1 ` R ) ` c ) <_ X } |-> ( ( coe1 ` b ) ` X ) ) |` k ) C_ ran ( b e. { c e. ( N ` k ) | ( ( deg1 ` R ) ` c ) <_ X } |-> ( ( coe1 ` b ) ` X ) ) )
79 63 78 eqsstrid 
 |-  ( ( ph /\ ( k C_ { c e. I | ( ( deg1 ` R ) ` c ) <_ X } /\ k e. Fin ) ) -> ( ( b e. { c e. I | ( ( deg1 ` R ) ` c ) <_ X } |-> ( ( coe1 ` b ) ` X ) ) " k ) C_ ran ( b e. { c e. ( N ` k ) | ( ( deg1 ` R ) ` c ) <_ X } |-> ( ( coe1 ` b ) ` X ) ) )
80 1 2 3 22 hbtlem1 
 |-  ( ( R e. Ring /\ ( N ` k ) e. U /\ X e. NN0 ) -> ( ( S ` ( N ` k ) ) ` X ) = { e | E. b e. ( N ` k ) ( ( ( deg1 ` R ) ` b ) <_ X /\ e = ( ( coe1 ` b ) ` X ) ) } )
81 47 59 60 80 syl3anc 
 |-  ( ( ph /\ ( k C_ { c e. I | ( ( deg1 ` R ) ` c ) <_ X } /\ k e. Fin ) ) -> ( ( S ` ( N ` k ) ) ` X ) = { e | E. b e. ( N ` k ) ( ( ( deg1 ` R ) ` b ) <_ X /\ e = ( ( coe1 ` b ) ` X ) ) } )
82 eqid 
 |-  ( b e. { c e. ( N ` k ) | ( ( deg1 ` R ) ` c ) <_ X } |-> ( ( coe1 ` b ) ` X ) ) = ( b e. { c e. ( N ` k ) | ( ( deg1 ` R ) ` c ) <_ X } |-> ( ( coe1 ` b ) ` X ) )
83 82 rnmpt 
 |-  ran ( b e. { c e. ( N ` k ) | ( ( deg1 ` R ) ` c ) <_ X } |-> ( ( coe1 ` b ) ` X ) ) = { e | E. b e. { c e. ( N ` k ) | ( ( deg1 ` R ) ` c ) <_ X } e = ( ( coe1 ` b ) ` X ) }
84 27 rexrab 
 |-  ( E. b e. { c e. ( N ` k ) | ( ( deg1 ` R ) ` c ) <_ X } e = ( ( coe1 ` b ) ` X ) <-> E. b e. ( N ` k ) ( ( ( deg1 ` R ) ` b ) <_ X /\ e = ( ( coe1 ` b ) ` X ) ) )
85 84 abbii 
 |-  { e | E. b e. { c e. ( N ` k ) | ( ( deg1 ` R ) ` c ) <_ X } e = ( ( coe1 ` b ) ` X ) } = { e | E. b e. ( N ` k ) ( ( ( deg1 ` R ) ` b ) <_ X /\ e = ( ( coe1 ` b ) ` X ) ) }
86 83 85 eqtri 
 |-  ran ( b e. { c e. ( N ` k ) | ( ( deg1 ` R ) ` c ) <_ X } |-> ( ( coe1 ` b ) ` X ) ) = { e | E. b e. ( N ` k ) ( ( ( deg1 ` R ) ` b ) <_ X /\ e = ( ( coe1 ` b ) ` X ) ) }
87 81 86 eqtr4di 
 |-  ( ( ph /\ ( k C_ { c e. I | ( ( deg1 ` R ) ` c ) <_ X } /\ k e. Fin ) ) -> ( ( S ` ( N ` k ) ) ` X ) = ran ( b e. { c e. ( N ` k ) | ( ( deg1 ` R ) ` c ) <_ X } |-> ( ( coe1 ` b ) ` X ) ) )
88 79 87 sseqtrrd 
 |-  ( ( ph /\ ( k C_ { c e. I | ( ( deg1 ` R ) ` c ) <_ X } /\ k e. Fin ) ) -> ( ( b e. { c e. I | ( ( deg1 ` R ) ` c ) <_ X } |-> ( ( coe1 ` b ) ` X ) ) " k ) C_ ( ( S ` ( N ` k ) ) ` X ) )
89 13 10 rspssp 
 |-  ( ( R e. Ring /\ ( ( S ` ( N ` k ) ) ` X ) e. ( LIdeal ` R ) /\ ( ( b e. { c e. I | ( ( deg1 ` R ) ` c ) <_ X } |-> ( ( coe1 ` b ) ` X ) ) " k ) C_ ( ( S ` ( N ` k ) ) ` X ) ) -> ( ( RSpan ` R ) ` ( ( b e. { c e. I | ( ( deg1 ` R ) ` c ) <_ X } |-> ( ( coe1 ` b ) ` X ) ) " k ) ) C_ ( ( S ` ( N ` k ) ) ` X ) )
90 47 62 88 89 syl3anc 
 |-  ( ( ph /\ ( k C_ { c e. I | ( ( deg1 ` R ) ` c ) <_ X } /\ k e. Fin ) ) -> ( ( RSpan ` R ) ` ( ( b e. { c e. I | ( ( deg1 ` R ) ` c ) <_ X } |-> ( ( coe1 ` b ) ` X ) ) " k ) ) C_ ( ( S ` ( N ` k ) ) ` X ) )
91 46 90 jca 
 |-  ( ( ph /\ ( k C_ { c e. I | ( ( deg1 ` R ) ` c ) <_ X } /\ k e. Fin ) ) -> ( k e. ( ~P I i^i Fin ) /\ ( ( RSpan ` R ) ` ( ( b e. { c e. I | ( ( deg1 ` R ) ` c ) <_ X } |-> ( ( coe1 ` b ) ` X ) ) " k ) ) C_ ( ( S ` ( N ` k ) ) ` X ) ) )
92 fveq2 
 |-  ( ( ( b e. { c e. I | ( ( deg1 ` R ) ` c ) <_ X } |-> ( ( coe1 ` b ) ` X ) ) " k ) = a -> ( ( RSpan ` R ) ` ( ( b e. { c e. I | ( ( deg1 ` R ) ` c ) <_ X } |-> ( ( coe1 ` b ) ` X ) ) " k ) ) = ( ( RSpan ` R ) ` a ) )
93 92 sseq1d 
 |-  ( ( ( b e. { c e. I | ( ( deg1 ` R ) ` c ) <_ X } |-> ( ( coe1 ` b ) ` X ) ) " k ) = a -> ( ( ( RSpan ` R ) ` ( ( b e. { c e. I | ( ( deg1 ` R ) ` c ) <_ X } |-> ( ( coe1 ` b ) ` X ) ) " k ) ) C_ ( ( S ` ( N ` k ) ) ` X ) <-> ( ( RSpan ` R ) ` a ) C_ ( ( S ` ( N ` k ) ) ` X ) ) )
94 93 anbi2d 
 |-  ( ( ( b e. { c e. I | ( ( deg1 ` R ) ` c ) <_ X } |-> ( ( coe1 ` b ) ` X ) ) " k ) = a -> ( ( k e. ( ~P I i^i Fin ) /\ ( ( RSpan ` R ) ` ( ( b e. { c e. I | ( ( deg1 ` R ) ` c ) <_ X } |-> ( ( coe1 ` b ) ` X ) ) " k ) ) C_ ( ( S ` ( N ` k ) ) ` X ) ) <-> ( k e. ( ~P I i^i Fin ) /\ ( ( RSpan ` R ) ` a ) C_ ( ( S ` ( N ` k ) ) ` X ) ) ) )
95 91 94 syl5ibcom 
 |-  ( ( ph /\ ( k C_ { c e. I | ( ( deg1 ` R ) ` c ) <_ X } /\ k e. Fin ) ) -> ( ( ( b e. { c e. I | ( ( deg1 ` R ) ` c ) <_ X } |-> ( ( coe1 ` b ) ` X ) ) " k ) = a -> ( k e. ( ~P I i^i Fin ) /\ ( ( RSpan ` R ) ` a ) C_ ( ( S ` ( N ` k ) ) ` X ) ) ) )
96 37 95 sylan2b 
 |-  ( ( ph /\ k e. ( ~P { c e. I | ( ( deg1 ` R ) ` c ) <_ X } i^i Fin ) ) -> ( ( ( b e. { c e. I | ( ( deg1 ` R ) ` c ) <_ X } |-> ( ( coe1 ` b ) ` X ) ) " k ) = a -> ( k e. ( ~P I i^i Fin ) /\ ( ( RSpan ` R ) ` a ) C_ ( ( S ` ( N ` k ) ) ` X ) ) ) )
97 96 expimpd 
 |-  ( ph -> ( ( k e. ( ~P { c e. I | ( ( deg1 ` R ) ` c ) <_ X } i^i Fin ) /\ ( ( b e. { c e. I | ( ( deg1 ` R ) ` c ) <_ X } |-> ( ( coe1 ` b ) ` X ) ) " k ) = a ) -> ( k e. ( ~P I i^i Fin ) /\ ( ( RSpan ` R ) ` a ) C_ ( ( S ` ( N ` k ) ) ` X ) ) ) )
98 97 adantr 
 |-  ( ( ph /\ ( a C_ ( ( S ` I ) ` X ) /\ a e. Fin ) ) -> ( ( k e. ( ~P { c e. I | ( ( deg1 ` R ) ` c ) <_ X } i^i Fin ) /\ ( ( b e. { c e. I | ( ( deg1 ` R ) ` c ) <_ X } |-> ( ( coe1 ` b ) ` X ) ) " k ) = a ) -> ( k e. ( ~P I i^i Fin ) /\ ( ( RSpan ` R ) ` a ) C_ ( ( S ` ( N ` k ) ) ` X ) ) ) )
99 98 reximdv2 
 |-  ( ( ph /\ ( a C_ ( ( S ` I ) ` X ) /\ a e. Fin ) ) -> ( E. k e. ( ~P { c e. I | ( ( deg1 ` R ) ` c ) <_ X } i^i Fin ) ( ( b e. { c e. I | ( ( deg1 ` R ) ` c ) <_ X } |-> ( ( coe1 ` b ) ` X ) ) " k ) = a -> E. k e. ( ~P I i^i Fin ) ( ( RSpan ` R ) ` a ) C_ ( ( S ` ( N ` k ) ) ` X ) ) )
100 36 99 mpd 
 |-  ( ( ph /\ ( a C_ ( ( S ` I ) ` X ) /\ a e. Fin ) ) -> E. k e. ( ~P I i^i Fin ) ( ( RSpan ` R ) ` a ) C_ ( ( S ` ( N ` k ) ) ` X ) )
101 16 100 sylan2b 
 |-  ( ( ph /\ a e. ( ~P ( ( S ` I ) ` X ) i^i Fin ) ) -> E. k e. ( ~P I i^i Fin ) ( ( RSpan ` R ) ` a ) C_ ( ( S ` ( N ` k ) ) ` X ) )
102 sseq1 
 |-  ( ( ( S ` I ) ` X ) = ( ( RSpan ` R ) ` a ) -> ( ( ( S ` I ) ` X ) C_ ( ( S ` ( N ` k ) ) ` X ) <-> ( ( RSpan ` R ) ` a ) C_ ( ( S ` ( N ` k ) ) ` X ) ) )
103 102 rexbidv 
 |-  ( ( ( S ` I ) ` X ) = ( ( RSpan ` R ) ` a ) -> ( E. k e. ( ~P I i^i Fin ) ( ( S ` I ) ` X ) C_ ( ( S ` ( N ` k ) ) ` X ) <-> E. k e. ( ~P I i^i Fin ) ( ( RSpan ` R ) ` a ) C_ ( ( S ` ( N ` k ) ) ` X ) ) )
104 101 103 syl5ibrcom 
 |-  ( ( ph /\ a e. ( ~P ( ( S ` I ) ` X ) i^i Fin ) ) -> ( ( ( S ` I ) ` X ) = ( ( RSpan ` R ) ` a ) -> E. k e. ( ~P I i^i Fin ) ( ( S ` I ) ` X ) C_ ( ( S ` ( N ` k ) ) ` X ) ) )
105 104 rexlimdva 
 |-  ( ph -> ( E. a e. ( ~P ( ( S ` I ) ` X ) i^i Fin ) ( ( S ` I ) ` X ) = ( ( RSpan ` R ) ` a ) -> E. k e. ( ~P I i^i Fin ) ( ( S ` I ) ` X ) C_ ( ( S ` ( N ` k ) ) ` X ) ) )
106 15 105 mpd 
 |-  ( ph -> E. k e. ( ~P I i^i Fin ) ( ( S ` I ) ` X ) C_ ( ( S ` ( N ` k ) ) ` X ) )