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 ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
hbtlem.u ⊢ 𝑈 = ( LIdeal ‘ 𝑃 )
hbtlem.s ⊢ 𝑆 = ( ldgIdlSeq ‘ 𝑅 )
hbtlem6.n ⊢ 𝑁 = ( RSpan ‘ 𝑃 )
hbtlem6.r ⊢ ( 𝜑 → 𝑅 ∈ LNoeR )
hbtlem6.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑈 )
hbtlem6.x ⊢ ( 𝜑 → 𝑋 ∈ ℕ0 )
Assertion hbtlem6 ( 𝜑 → ∃ 𝑘 ∈ ( 𝒫 𝐼 ∩ Fin ) ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ⊆ ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 hbtlem.p ⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2 hbtlem.u ⊢ 𝑈 = ( LIdeal ‘ 𝑃 )
3 hbtlem.s ⊢ 𝑆 = ( ldgIdlSeq ‘ 𝑅 )
4 hbtlem6.n ⊢ 𝑁 = ( RSpan ‘ 𝑃 )
5 hbtlem6.r ⊢ ( 𝜑 → 𝑅 ∈ LNoeR )
6 hbtlem6.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑈 )
7 hbtlem6.x ⊢ ( 𝜑 → 𝑋 ∈ ℕ0 )
8 lnrring ⊢ ( 𝑅 ∈ LNoeR → 𝑅 ∈ Ring )
9 5 8 syl ⊢ ( 𝜑 → 𝑅 ∈ Ring )
10 eqid ⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
11 1 2 3 10 hbtlem2 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) → ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ∈ ( LIdeal ‘ 𝑅 ) )
12 9 6 7 11 syl3anc ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ∈ ( LIdeal ‘ 𝑅 ) )
13 eqid ⊢ ( RSpan ‘ 𝑅 ) = ( RSpan ‘ 𝑅 )
14 10 13 lnr2i ⊢ ( ( 𝑅 ∈ LNoeR ∧ ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ∈ ( LIdeal ‘ 𝑅 ) ) → ∃ 𝑎 ∈ ( 𝒫 ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ∩ Fin ) ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) = ( ( RSpan ‘ 𝑅 ) ‘ 𝑎 ) )
15 5 12 14 syl2anc ⊢ ( 𝜑 → ∃ 𝑎 ∈ ( 𝒫 ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ∩ Fin ) ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) = ( ( RSpan ‘ 𝑅 ) ‘ 𝑎 ) )
16 elfpw ⊢ ( 𝑎 ∈ ( 𝒫 ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ∩ Fin ) ↔ ( 𝑎 ⊆ ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ∧ 𝑎 ∈ Fin ) )
17 fvex ⊢ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ∈ V
18 eqid ⊢ ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) = ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) )
19 17 18 fnmpti ⊢ ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) Fn { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 }
20 19 a1i ⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ∧ 𝑎 ∈ Fin ) ) → ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) Fn { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } )
21 simprl ⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ∧ 𝑎 ∈ Fin ) ) → 𝑎 ⊆ ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) )
22 eqid ⊢ ( deg1 ‘ 𝑅 ) = ( deg1 ‘ 𝑅 )
23 1 2 3 22 hbtlem1 ⊢ ( ( 𝑅 ∈ LNoeR ∧ 𝐼 ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) → ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) = { 𝑑 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑑 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } )
24 5 6 7 23 syl3anc ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) = { 𝑑 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑑 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } )
25 18 rnmpt ⊢ ran ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) = { 𝑑 ∣ ∃ 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } 𝑑 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) }
26 fveq2 ⊢ ( 𝑐 = 𝑏 → ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) = ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) )
27 26 breq1d ⊢ ( 𝑐 = 𝑏 → ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 ↔ ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ) )
28 27 rexrab ⊢ ( ∃ 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } 𝑑 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ↔ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑑 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) )
29 28 abbii ⊢ { 𝑑 ∣ ∃ 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } 𝑑 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) } = { 𝑑 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑑 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) }
30 25 29 eqtri ⊢ ran ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) = { 𝑑 ∣ ∃ 𝑏 ∈ 𝐼 ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑑 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) }
31 24 30 eqtr4di ⊢ ( 𝜑 → ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) = ran ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) )
32 31 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ∧ 𝑎 ∈ Fin ) ) → ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) = ran ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) )
33 21 32 sseqtrd ⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ∧ 𝑎 ∈ Fin ) ) → 𝑎 ⊆ ran ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) )
34 simprr ⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ∧ 𝑎 ∈ Fin ) ) → 𝑎 ∈ Fin )
35 fipreima ⊢ ( ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) Fn { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑎 ⊆ ran ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ∧ 𝑎 ∈ Fin ) → ∃ 𝑘 ∈ ( 𝒫 { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∩ Fin ) ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) = 𝑎 )
36 20 33 34 35 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ∧ 𝑎 ∈ Fin ) ) → ∃ 𝑘 ∈ ( 𝒫 { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∩ Fin ) ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) = 𝑎 )
37 elfpw ⊢ ( 𝑘 ∈ ( 𝒫 { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∩ Fin ) ↔ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) )
38 ssrab2 ⊢ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ⊆ 𝐼
39 sstr2 ⊢ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } → ( { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ⊆ 𝐼 → 𝑘 ⊆ 𝐼 ) )
40 38 39 mpi ⊢ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } → 𝑘 ⊆ 𝐼 )
41 40 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ) → 𝑘 ⊆ 𝐼 )
42 velpw ⊢ ( 𝑘 ∈ 𝒫 𝐼 ↔ 𝑘 ⊆ 𝐼 )
43 41 42 sylibr ⊢ ( ( 𝜑 ∧ 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ) → 𝑘 ∈ 𝒫 𝐼 )
44 43 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → 𝑘 ∈ 𝒫 𝐼 )
45 simprr ⊢ ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → 𝑘 ∈ Fin )
46 44 45 elind ⊢ ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → 𝑘 ∈ ( 𝒫 𝐼 ∩ Fin ) )
47 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → 𝑅 ∈ Ring )
48 1 ply1ring ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
49 9 48 syl ⊢ ( 𝜑 → 𝑃 ∈ Ring )
50 49 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → 𝑃 ∈ Ring )
51 simprl ⊢ ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } )
52 51 38 sstrdi ⊢ ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → 𝑘 ⊆ 𝐼 )
53 eqid ⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
54 53 2 lidlss ⊢ ( 𝐼 ∈ 𝑈 → 𝐼 ⊆ ( Base ‘ 𝑃 ) )
55 6 54 syl ⊢ ( 𝜑 → 𝐼 ⊆ ( Base ‘ 𝑃 ) )
56 55 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → 𝐼 ⊆ ( Base ‘ 𝑃 ) )
57 52 56 sstrd ⊢ ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → 𝑘 ⊆ ( Base ‘ 𝑃 ) )
58 4 53 2 rspcl ⊢ ( ( 𝑃 ∈ Ring ∧ 𝑘 ⊆ ( Base ‘ 𝑃 ) ) → ( 𝑁 ‘ 𝑘 ) ∈ 𝑈 )
59 50 57 58 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → ( 𝑁 ‘ 𝑘 ) ∈ 𝑈 )
60 7 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → 𝑋 ∈ ℕ0 )
61 1 2 3 10 hbtlem2 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 ‘ 𝑘 ) ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) → ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) ∈ ( LIdeal ‘ 𝑅 ) )
62 47 59 60 61 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) ∈ ( LIdeal ‘ 𝑅 ) )
63 df-ima ⊢ ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) = ran ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ↾ 𝑘 )
64 4 53 rspssid ⊢ ( ( 𝑃 ∈ Ring ∧ 𝑘 ⊆ ( Base ‘ 𝑃 ) ) → 𝑘 ⊆ ( 𝑁 ‘ 𝑘 ) )
65 50 57 64 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → 𝑘 ⊆ ( 𝑁 ‘ 𝑘 ) )
66 ssrab ⊢ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↔ ( 𝑘 ⊆ 𝐼 ∧ ∀ 𝑐 ∈ 𝑘 ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 ) )
67 66 simprbi ⊢ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } → ∀ 𝑐 ∈ 𝑘 ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 )
68 67 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → ∀ 𝑐 ∈ 𝑘 ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 )
69 ssrab ⊢ ( 𝑘 ⊆ { 𝑐 ∈ ( 𝑁 ‘ 𝑘 ) ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↔ ( 𝑘 ⊆ ( 𝑁 ‘ 𝑘 ) ∧ ∀ 𝑐 ∈ 𝑘 ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 ) )
70 65 68 69 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → 𝑘 ⊆ { 𝑐 ∈ ( 𝑁 ‘ 𝑘 ) ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } )
71 70 resmptd ⊢ ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → ( ( 𝑏 ∈ { 𝑐 ∈ ( 𝑁 ‘ 𝑘 ) ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ↾ 𝑘 ) = ( 𝑏 ∈ 𝑘 ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) )
72 resmpt ⊢ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } → ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ↾ 𝑘 ) = ( 𝑏 ∈ 𝑘 ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) )
73 72 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ↾ 𝑘 ) = ( 𝑏 ∈ 𝑘 ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) )
74 71 73 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → ( ( 𝑏 ∈ { 𝑐 ∈ ( 𝑁 ‘ 𝑘 ) ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ↾ 𝑘 ) = ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ↾ 𝑘 ) )
75 resss ⊢ ( ( 𝑏 ∈ { 𝑐 ∈ ( 𝑁 ‘ 𝑘 ) ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ↾ 𝑘 ) ⊆ ( 𝑏 ∈ { 𝑐 ∈ ( 𝑁 ‘ 𝑘 ) ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) )
76 74 75 eqsstrrdi ⊢ ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ↾ 𝑘 ) ⊆ ( 𝑏 ∈ { 𝑐 ∈ ( 𝑁 ‘ 𝑘 ) ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) )
77 rnss ⊢ ( ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ↾ 𝑘 ) ⊆ ( 𝑏 ∈ { 𝑐 ∈ ( 𝑁 ‘ 𝑘 ) ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) → ran ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ↾ 𝑘 ) ⊆ ran ( 𝑏 ∈ { 𝑐 ∈ ( 𝑁 ‘ 𝑘 ) ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) )
78 76 77 syl ⊢ ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → ran ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) ↾ 𝑘 ) ⊆ ran ( 𝑏 ∈ { 𝑐 ∈ ( 𝑁 ‘ 𝑘 ) ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) )
79 63 78 eqsstrid ⊢ ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) ⊆ ran ( 𝑏 ∈ { 𝑐 ∈ ( 𝑁 ‘ 𝑘 ) ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) )
80 1 2 3 22 hbtlem1 ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑁 ‘ 𝑘 ) ∈ 𝑈 ∧ 𝑋 ∈ ℕ0 ) → ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) = { 𝑒 ∣ ∃ 𝑏 ∈ ( 𝑁 ‘ 𝑘 ) ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑒 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } )
81 47 59 60 80 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) = { 𝑒 ∣ ∃ 𝑏 ∈ ( 𝑁 ‘ 𝑘 ) ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑒 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) } )
82 eqid ⊢ ( 𝑏 ∈ { 𝑐 ∈ ( 𝑁 ‘ 𝑘 ) ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) = ( 𝑏 ∈ { 𝑐 ∈ ( 𝑁 ‘ 𝑘 ) ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) )
83 82 rnmpt ⊢ ran ( 𝑏 ∈ { 𝑐 ∈ ( 𝑁 ‘ 𝑘 ) ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) = { 𝑒 ∣ ∃ 𝑏 ∈ { 𝑐 ∈ ( 𝑁 ‘ 𝑘 ) ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } 𝑒 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) }
84 27 rexrab ⊢ ( ∃ 𝑏 ∈ { 𝑐 ∈ ( 𝑁 ‘ 𝑘 ) ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } 𝑒 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ↔ ∃ 𝑏 ∈ ( 𝑁 ‘ 𝑘 ) ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑒 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) )
85 84 abbii ⊢ { 𝑒 ∣ ∃ 𝑏 ∈ { 𝑐 ∈ ( 𝑁 ‘ 𝑘 ) ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } 𝑒 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) } = { 𝑒 ∣ ∃ 𝑏 ∈ ( 𝑁 ‘ 𝑘 ) ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑒 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) }
86 83 85 eqtri ⊢ ran ( 𝑏 ∈ { 𝑐 ∈ ( 𝑁 ‘ 𝑘 ) ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) = { 𝑒 ∣ ∃ 𝑏 ∈ ( 𝑁 ‘ 𝑘 ) ( ( ( deg1 ‘ 𝑅 ) ‘ 𝑏 ) ≤ 𝑋 ∧ 𝑒 = ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) }
87 81 86 eqtr4di ⊢ ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) = ran ( 𝑏 ∈ { 𝑐 ∈ ( 𝑁 ‘ 𝑘 ) ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) )
88 79 87 sseqtrrd ⊢ ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) ⊆ ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) )
89 13 10 rspssp ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) ∈ ( LIdeal ‘ 𝑅 ) ∧ ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) ⊆ ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) ) → ( ( RSpan ‘ 𝑅 ) ‘ ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) ) ⊆ ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) )
90 47 62 88 89 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → ( ( RSpan ‘ 𝑅 ) ‘ ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) ) ⊆ ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) )
91 46 90 jca ⊢ ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → ( 𝑘 ∈ ( 𝒫 𝐼 ∩ Fin ) ∧ ( ( RSpan ‘ 𝑅 ) ‘ ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) ) ⊆ ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) ) )
92 fveq2 ⊢ ( ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) = 𝑎 → ( ( RSpan ‘ 𝑅 ) ‘ ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) ) = ( ( RSpan ‘ 𝑅 ) ‘ 𝑎 ) )
93 92 sseq1d ⊢ ( ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) = 𝑎 → ( ( ( RSpan ‘ 𝑅 ) ‘ ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) ) ⊆ ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) ↔ ( ( RSpan ‘ 𝑅 ) ‘ 𝑎 ) ⊆ ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) ) )
94 93 anbi2d ⊢ ( ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) = 𝑎 → ( ( 𝑘 ∈ ( 𝒫 𝐼 ∩ Fin ) ∧ ( ( RSpan ‘ 𝑅 ) ‘ ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) ) ⊆ ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) ) ↔ ( 𝑘 ∈ ( 𝒫 𝐼 ∩ Fin ) ∧ ( ( RSpan ‘ 𝑅 ) ‘ 𝑎 ) ⊆ ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) ) ) )
95 91 94 syl5ibcom ⊢ ( ( 𝜑 ∧ ( 𝑘 ⊆ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∧ 𝑘 ∈ Fin ) ) → ( ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) = 𝑎 → ( 𝑘 ∈ ( 𝒫 𝐼 ∩ Fin ) ∧ ( ( RSpan ‘ 𝑅 ) ‘ 𝑎 ) ⊆ ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) ) ) )
96 37 95 sylan2b ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝒫 { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∩ Fin ) ) → ( ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) = 𝑎 → ( 𝑘 ∈ ( 𝒫 𝐼 ∩ Fin ) ∧ ( ( RSpan ‘ 𝑅 ) ‘ 𝑎 ) ⊆ ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) ) ) )
97 96 expimpd ⊢ ( 𝜑 → ( ( 𝑘 ∈ ( 𝒫 { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∩ Fin ) ∧ ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) = 𝑎 ) → ( 𝑘 ∈ ( 𝒫 𝐼 ∩ Fin ) ∧ ( ( RSpan ‘ 𝑅 ) ‘ 𝑎 ) ⊆ ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) ) ) )
98 97 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ∧ 𝑎 ∈ Fin ) ) → ( ( 𝑘 ∈ ( 𝒫 { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∩ Fin ) ∧ ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) = 𝑎 ) → ( 𝑘 ∈ ( 𝒫 𝐼 ∩ Fin ) ∧ ( ( RSpan ‘ 𝑅 ) ‘ 𝑎 ) ⊆ ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) ) ) )
99 98 reximdv2 ⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ∧ 𝑎 ∈ Fin ) ) → ( ∃ 𝑘 ∈ ( 𝒫 { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ∩ Fin ) ( ( 𝑏 ∈ { 𝑐 ∈ 𝐼 ∣ ( ( deg1 ‘ 𝑅 ) ‘ 𝑐 ) ≤ 𝑋 } ↦ ( ( coe1 ‘ 𝑏 ) ‘ 𝑋 ) ) “ 𝑘 ) = 𝑎 → ∃ 𝑘 ∈ ( 𝒫 𝐼 ∩ Fin ) ( ( RSpan ‘ 𝑅 ) ‘ 𝑎 ) ⊆ ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) ) )
100 36 99 mpd ⊢ ( ( 𝜑 ∧ ( 𝑎 ⊆ ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ∧ 𝑎 ∈ Fin ) ) → ∃ 𝑘 ∈ ( 𝒫 𝐼 ∩ Fin ) ( ( RSpan ‘ 𝑅 ) ‘ 𝑎 ) ⊆ ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) )
101 16 100 sylan2b ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ∩ Fin ) ) → ∃ 𝑘 ∈ ( 𝒫 𝐼 ∩ Fin ) ( ( RSpan ‘ 𝑅 ) ‘ 𝑎 ) ⊆ ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) )
102 sseq1 ⊢ ( ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) = ( ( RSpan ‘ 𝑅 ) ‘ 𝑎 ) → ( ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ⊆ ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) ↔ ( ( RSpan ‘ 𝑅 ) ‘ 𝑎 ) ⊆ ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) ) )
103 102 rexbidv ⊢ ( ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) = ( ( RSpan ‘ 𝑅 ) ‘ 𝑎 ) → ( ∃ 𝑘 ∈ ( 𝒫 𝐼 ∩ Fin ) ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ⊆ ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) ↔ ∃ 𝑘 ∈ ( 𝒫 𝐼 ∩ Fin ) ( ( RSpan ‘ 𝑅 ) ‘ 𝑎 ) ⊆ ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) ) )
104 101 103 syl5ibrcom ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ∩ Fin ) ) → ( ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) = ( ( RSpan ‘ 𝑅 ) ‘ 𝑎 ) → ∃ 𝑘 ∈ ( 𝒫 𝐼 ∩ Fin ) ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ⊆ ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) ) )
105 104 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑎 ∈ ( 𝒫 ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ∩ Fin ) ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) = ( ( RSpan ‘ 𝑅 ) ‘ 𝑎 ) → ∃ 𝑘 ∈ ( 𝒫 𝐼 ∩ Fin ) ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ⊆ ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) ) )
106 15 105 mpd ⊢ ( 𝜑 → ∃ 𝑘 ∈ ( 𝒫 𝐼 ∩ Fin ) ( ( 𝑆 ‘ 𝐼 ) ‘ 𝑋 ) ⊆ ( ( 𝑆 ‘ ( 𝑁 ‘ 𝑘 ) ) ‘ 𝑋 ) )