Metamath Proof Explorer


Theorem hoidmvlelem3

Description: This is the contradiction proven in step (d) in the proof of Lemma 115B of Fremlin1 p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Hypotheses hoidmvlelem3.l 𝐿 = ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘𝑥 ( vol ‘ ( ( 𝑎𝑘 ) [,) ( 𝑏𝑘 ) ) ) ) ) )
hoidmvlelem3.x ( 𝜑𝑋 ∈ Fin )
hoidmvlelem3.y ( 𝜑𝑌𝑋 )
hoidmvlelem3.z ( 𝜑𝑍 ∈ ( 𝑋𝑌 ) )
hoidmvlelem3.w 𝑊 = ( 𝑌 ∪ { 𝑍 } )
hoidmvlelem3.a ( 𝜑𝐴 : 𝑊 ⟶ ℝ )
hoidmvlelem3.b ( 𝜑𝐵 : 𝑊 ⟶ ℝ )
hoidmvlelem3.lt ( ( 𝜑𝑘𝑊 ) → ( 𝐴𝑘 ) < ( 𝐵𝑘 ) )
hoidmvlelem3.f 𝐹 = ( 𝑦𝑌 ↦ 0 )
hoidmvlelem3.c ( 𝜑𝐶 : ℕ ⟶ ( ℝ ↑m 𝑊 ) )
hoidmvlelem3.j 𝐽 = ( 𝑗 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑗 ) ↾ 𝑌 ) , 𝐹 ) )
hoidmvlelem3.d ( 𝜑𝐷 : ℕ ⟶ ( ℝ ↑m 𝑊 ) )
hoidmvlelem3.k 𝐾 = ( 𝑗 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑗 ) ↾ 𝑌 ) , 𝐹 ) )
hoidmvlelem3.r ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( 𝐷𝑗 ) ) ) ) ∈ ℝ )
hoidmvlelem3.h 𝐻 = ( 𝑥 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑗𝑊 ↦ if ( 𝑗𝑌 , ( 𝑐𝑗 ) , if ( ( 𝑐𝑗 ) ≤ 𝑥 , ( 𝑐𝑗 ) , 𝑥 ) ) ) ) )
hoidmvlelem3.g 𝐺 = ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) )
hoidmvlelem3.e ( 𝜑𝐸 ∈ ℝ+ )
hoidmvlelem3.u 𝑈 = { 𝑧 ∈ ( ( 𝐴𝑍 ) [,] ( 𝐵𝑍 ) ) ∣ ( 𝐺 · ( 𝑧 − ( 𝐴𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑧 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) }
hoidmvlelem3.s ( 𝜑𝑆𝑈 )
hoidmvlelem3.sb ( 𝜑𝑆 < ( 𝐵𝑍 ) )
hoidmvlelem3.p 𝑃 = ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) )
hoidmvlelem3.i ( 𝜑 → ∀ 𝑒 ∈ ( ℝ ↑m 𝑌 ) ∀ 𝑓 ∈ ( ℝ ↑m 𝑌 ) ∀ 𝑔 ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ∀ ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ( X 𝑘𝑌 ( ( 𝑒𝑘 ) [,) ( 𝑓𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( 𝑒 ( 𝐿𝑌 ) 𝑓 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) )
hoidmvlelem3.i2 ( 𝜑X 𝑘𝑊 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) )
hoidmvlelem3.o 𝑂 = ( 𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ↦ ( 𝑘𝑊 ↦ if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) ) )
Assertion hoidmvlelem3 ( 𝜑 → ∃ 𝑢𝑈 𝑆 < 𝑢 )

Proof

Step Hyp Ref Expression
1 hoidmvlelem3.l 𝐿 = ( 𝑥 ∈ Fin ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑥 ) , 𝑏 ∈ ( ℝ ↑m 𝑥 ) ↦ if ( 𝑥 = ∅ , 0 , ∏ 𝑘𝑥 ( vol ‘ ( ( 𝑎𝑘 ) [,) ( 𝑏𝑘 ) ) ) ) ) )
2 hoidmvlelem3.x ( 𝜑𝑋 ∈ Fin )
3 hoidmvlelem3.y ( 𝜑𝑌𝑋 )
4 hoidmvlelem3.z ( 𝜑𝑍 ∈ ( 𝑋𝑌 ) )
5 hoidmvlelem3.w 𝑊 = ( 𝑌 ∪ { 𝑍 } )
6 hoidmvlelem3.a ( 𝜑𝐴 : 𝑊 ⟶ ℝ )
7 hoidmvlelem3.b ( 𝜑𝐵 : 𝑊 ⟶ ℝ )
8 hoidmvlelem3.lt ( ( 𝜑𝑘𝑊 ) → ( 𝐴𝑘 ) < ( 𝐵𝑘 ) )
9 hoidmvlelem3.f 𝐹 = ( 𝑦𝑌 ↦ 0 )
10 hoidmvlelem3.c ( 𝜑𝐶 : ℕ ⟶ ( ℝ ↑m 𝑊 ) )
11 hoidmvlelem3.j 𝐽 = ( 𝑗 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑗 ) ↾ 𝑌 ) , 𝐹 ) )
12 hoidmvlelem3.d ( 𝜑𝐷 : ℕ ⟶ ( ℝ ↑m 𝑊 ) )
13 hoidmvlelem3.k 𝐾 = ( 𝑗 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑗 ) ↾ 𝑌 ) , 𝐹 ) )
14 hoidmvlelem3.r ( 𝜑 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( 𝐷𝑗 ) ) ) ) ∈ ℝ )
15 hoidmvlelem3.h 𝐻 = ( 𝑥 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑗𝑊 ↦ if ( 𝑗𝑌 , ( 𝑐𝑗 ) , if ( ( 𝑐𝑗 ) ≤ 𝑥 , ( 𝑐𝑗 ) , 𝑥 ) ) ) ) )
16 hoidmvlelem3.g 𝐺 = ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) )
17 hoidmvlelem3.e ( 𝜑𝐸 ∈ ℝ+ )
18 hoidmvlelem3.u 𝑈 = { 𝑧 ∈ ( ( 𝐴𝑍 ) [,] ( 𝐵𝑍 ) ) ∣ ( 𝐺 · ( 𝑧 − ( 𝐴𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑧 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) }
19 hoidmvlelem3.s ( 𝜑𝑆𝑈 )
20 hoidmvlelem3.sb ( 𝜑𝑆 < ( 𝐵𝑍 ) )
21 hoidmvlelem3.p 𝑃 = ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) )
22 hoidmvlelem3.i ( 𝜑 → ∀ 𝑒 ∈ ( ℝ ↑m 𝑌 ) ∀ 𝑓 ∈ ( ℝ ↑m 𝑌 ) ∀ 𝑔 ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ∀ ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ( X 𝑘𝑌 ( ( 𝑒𝑘 ) [,) ( 𝑓𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( 𝑒 ( 𝐿𝑌 ) 𝑓 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) )
23 hoidmvlelem3.i2 ( 𝜑X 𝑘𝑊 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) )
24 hoidmvlelem3.o 𝑂 = ( 𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ↦ ( 𝑘𝑊 ↦ if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) ) )
25 1nn 1 ∈ ℕ
26 25 a1i ( ( 𝜑𝑌 = ∅ ) → 1 ∈ ℕ )
27 0le0 0 ≤ 0
28 27 a1i ( ( 𝜑𝑌 = ∅ ) → 0 ≤ 0 )
29 16 a1i ( ( 𝜑𝑌 = ∅ ) → 𝐺 = ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) )
30 fveq2 ( 𝑌 = ∅ → ( 𝐿𝑌 ) = ( 𝐿 ‘ ∅ ) )
31 reseq2 ( 𝑌 = ∅ → ( 𝐴𝑌 ) = ( 𝐴 ↾ ∅ ) )
32 res0 ( 𝐴 ↾ ∅ ) = ∅
33 32 a1i ( 𝑌 = ∅ → ( 𝐴 ↾ ∅ ) = ∅ )
34 31 33 eqtrd ( 𝑌 = ∅ → ( 𝐴𝑌 ) = ∅ )
35 reseq2 ( 𝑌 = ∅ → ( 𝐵𝑌 ) = ( 𝐵 ↾ ∅ ) )
36 res0 ( 𝐵 ↾ ∅ ) = ∅
37 36 a1i ( 𝑌 = ∅ → ( 𝐵 ↾ ∅ ) = ∅ )
38 35 37 eqtrd ( 𝑌 = ∅ → ( 𝐵𝑌 ) = ∅ )
39 30 34 38 oveq123d ( 𝑌 = ∅ → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) = ( ∅ ( 𝐿 ‘ ∅ ) ∅ ) )
40 39 adantl ( ( 𝜑𝑌 = ∅ ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) = ( ∅ ( 𝐿 ‘ ∅ ) ∅ ) )
41 f0 ∅ : ∅ ⟶ ℝ
42 41 a1i ( ( 𝜑𝑌 = ∅ ) → ∅ : ∅ ⟶ ℝ )
43 1 42 42 hoidmv0val ( ( 𝜑𝑌 = ∅ ) → ( ∅ ( 𝐿 ‘ ∅ ) ∅ ) = 0 )
44 29 40 43 3eqtrd ( ( 𝜑𝑌 = ∅ ) → 𝐺 = 0 )
45 nfcvd ( 𝜑 𝑗 ( 𝑃 ‘ 1 ) )
46 nfv 𝑗 𝜑
47 simpr ( ( 𝜑𝑗 = 1 ) → 𝑗 = 1 )
48 47 fveq2d ( ( 𝜑𝑗 = 1 ) → ( 𝑃𝑗 ) = ( 𝑃 ‘ 1 ) )
49 1red ( 𝜑 → 1 ∈ ℝ )
50 rge0ssre ( 0 [,) +∞ ) ⊆ ℝ
51 id ( 𝜑𝜑 )
52 25 a1i ( 𝜑 → 1 ∈ ℕ )
53 25 elexi 1 ∈ V
54 eleq1 ( 𝑗 = 1 → ( 𝑗 ∈ ℕ ↔ 1 ∈ ℕ ) )
55 54 anbi2d ( 𝑗 = 1 → ( ( 𝜑𝑗 ∈ ℕ ) ↔ ( 𝜑 ∧ 1 ∈ ℕ ) ) )
56 fveq2 ( 𝑗 = 1 → ( 𝑃𝑗 ) = ( 𝑃 ‘ 1 ) )
57 56 eleq1d ( 𝑗 = 1 → ( ( 𝑃𝑗 ) ∈ ( 0 [,) +∞ ) ↔ ( 𝑃 ‘ 1 ) ∈ ( 0 [,) +∞ ) ) )
58 55 57 imbi12d ( 𝑗 = 1 → ( ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝑃𝑗 ) ∈ ( 0 [,) +∞ ) ) ↔ ( ( 𝜑 ∧ 1 ∈ ℕ ) → ( 𝑃 ‘ 1 ) ∈ ( 0 [,) +∞ ) ) ) )
59 id ( 𝑗 ∈ ℕ → 𝑗 ∈ ℕ )
60 ovexd ( 𝑗 ∈ ℕ → ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) ∈ V )
61 21 fvmpt2 ( ( 𝑗 ∈ ℕ ∧ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) ∈ V ) → ( 𝑃𝑗 ) = ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) )
62 59 60 61 syl2anc ( 𝑗 ∈ ℕ → ( 𝑃𝑗 ) = ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) )
63 62 adantl ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝑃𝑗 ) = ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) )
64 5 a1i ( 𝜑𝑊 = ( 𝑌 ∪ { 𝑍 } ) )
65 4 eldifad ( 𝜑𝑍𝑋 )
66 snssi ( 𝑍𝑋 → { 𝑍 } ⊆ 𝑋 )
67 65 66 syl ( 𝜑 → { 𝑍 } ⊆ 𝑋 )
68 3 67 unssd ( 𝜑 → ( 𝑌 ∪ { 𝑍 } ) ⊆ 𝑋 )
69 64 68 eqsstrd ( 𝜑𝑊𝑋 )
70 2 69 ssfid ( 𝜑𝑊 ∈ Fin )
71 ssun1 𝑌 ⊆ ( 𝑌 ∪ { 𝑍 } )
72 5 eqcomi ( 𝑌 ∪ { 𝑍 } ) = 𝑊
73 71 72 sseqtri 𝑌𝑊
74 73 a1i ( 𝜑𝑌𝑊 )
75 70 74 ssfid ( 𝜑𝑌 ∈ Fin )
76 75 adantr ( ( 𝜑𝑗 ∈ ℕ ) → 𝑌 ∈ Fin )
77 iftrue ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) → if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑗 ) ↾ 𝑌 ) , 𝐹 ) = ( ( 𝐶𝑗 ) ↾ 𝑌 ) )
78 77 adantl ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑗 ) ↾ 𝑌 ) , 𝐹 ) = ( ( 𝐶𝑗 ) ↾ 𝑌 ) )
79 10 ffvelrnda ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝐶𝑗 ) ∈ ( ℝ ↑m 𝑊 ) )
80 elmapi ( ( 𝐶𝑗 ) ∈ ( ℝ ↑m 𝑊 ) → ( 𝐶𝑗 ) : 𝑊 ⟶ ℝ )
81 79 80 syl ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝐶𝑗 ) : 𝑊 ⟶ ℝ )
82 71 5 sseqtrri 𝑌𝑊
83 82 a1i ( ( 𝜑𝑗 ∈ ℕ ) → 𝑌𝑊 )
84 81 83 fssresd ( ( 𝜑𝑗 ∈ ℕ ) → ( ( 𝐶𝑗 ) ↾ 𝑌 ) : 𝑌 ⟶ ℝ )
85 reex ℝ ∈ V
86 85 a1i ( ( 𝜑𝑗 ∈ ℕ ) → ℝ ∈ V )
87 70 74 ssexd ( 𝜑𝑌 ∈ V )
88 87 adantr ( ( 𝜑𝑗 ∈ ℕ ) → 𝑌 ∈ V )
89 86 88 elmapd ( ( 𝜑𝑗 ∈ ℕ ) → ( ( ( 𝐶𝑗 ) ↾ 𝑌 ) ∈ ( ℝ ↑m 𝑌 ) ↔ ( ( 𝐶𝑗 ) ↾ 𝑌 ) : 𝑌 ⟶ ℝ ) )
90 84 89 mpbird ( ( 𝜑𝑗 ∈ ℕ ) → ( ( 𝐶𝑗 ) ↾ 𝑌 ) ∈ ( ℝ ↑m 𝑌 ) )
91 90 adantr ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → ( ( 𝐶𝑗 ) ↾ 𝑌 ) ∈ ( ℝ ↑m 𝑌 ) )
92 78 91 eqeltrd ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑗 ) ↾ 𝑌 ) , 𝐹 ) ∈ ( ℝ ↑m 𝑌 ) )
93 iffalse ( ¬ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) → if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑗 ) ↾ 𝑌 ) , 𝐹 ) = 𝐹 )
94 93 adantl ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ¬ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑗 ) ↾ 𝑌 ) , 𝐹 ) = 𝐹 )
95 0red ( ( 𝜑𝑦𝑌 ) → 0 ∈ ℝ )
96 95 9 fmptd ( 𝜑𝐹 : 𝑌 ⟶ ℝ )
97 85 a1i ( 𝜑 → ℝ ∈ V )
98 97 75 elmapd ( 𝜑 → ( 𝐹 ∈ ( ℝ ↑m 𝑌 ) ↔ 𝐹 : 𝑌 ⟶ ℝ ) )
99 96 98 mpbird ( 𝜑𝐹 ∈ ( ℝ ↑m 𝑌 ) )
100 99 ad2antrr ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ¬ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → 𝐹 ∈ ( ℝ ↑m 𝑌 ) )
101 94 100 eqeltrd ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ¬ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑗 ) ↾ 𝑌 ) , 𝐹 ) ∈ ( ℝ ↑m 𝑌 ) )
102 92 101 pm2.61dan ( ( 𝜑𝑗 ∈ ℕ ) → if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑗 ) ↾ 𝑌 ) , 𝐹 ) ∈ ( ℝ ↑m 𝑌 ) )
103 102 11 fmptd ( 𝜑𝐽 : ℕ ⟶ ( ℝ ↑m 𝑌 ) )
104 103 ffvelrnda ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝐽𝑗 ) ∈ ( ℝ ↑m 𝑌 ) )
105 elmapi ( ( 𝐽𝑗 ) ∈ ( ℝ ↑m 𝑌 ) → ( 𝐽𝑗 ) : 𝑌 ⟶ ℝ )
106 104 105 syl ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝐽𝑗 ) : 𝑌 ⟶ ℝ )
107 iftrue ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) → if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑗 ) ↾ 𝑌 ) , 𝐹 ) = ( ( 𝐷𝑗 ) ↾ 𝑌 ) )
108 107 adantl ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑗 ) ↾ 𝑌 ) , 𝐹 ) = ( ( 𝐷𝑗 ) ↾ 𝑌 ) )
109 12 ffvelrnda ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝐷𝑗 ) ∈ ( ℝ ↑m 𝑊 ) )
110 elmapi ( ( 𝐷𝑗 ) ∈ ( ℝ ↑m 𝑊 ) → ( 𝐷𝑗 ) : 𝑊 ⟶ ℝ )
111 109 110 syl ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝐷𝑗 ) : 𝑊 ⟶ ℝ )
112 111 83 fssresd ( ( 𝜑𝑗 ∈ ℕ ) → ( ( 𝐷𝑗 ) ↾ 𝑌 ) : 𝑌 ⟶ ℝ )
113 86 88 elmapd ( ( 𝜑𝑗 ∈ ℕ ) → ( ( ( 𝐷𝑗 ) ↾ 𝑌 ) ∈ ( ℝ ↑m 𝑌 ) ↔ ( ( 𝐷𝑗 ) ↾ 𝑌 ) : 𝑌 ⟶ ℝ ) )
114 112 113 mpbird ( ( 𝜑𝑗 ∈ ℕ ) → ( ( 𝐷𝑗 ) ↾ 𝑌 ) ∈ ( ℝ ↑m 𝑌 ) )
115 114 adantr ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → ( ( 𝐷𝑗 ) ↾ 𝑌 ) ∈ ( ℝ ↑m 𝑌 ) )
116 108 115 eqeltrd ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑗 ) ↾ 𝑌 ) , 𝐹 ) ∈ ( ℝ ↑m 𝑌 ) )
117 iffalse ( ¬ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) → if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑗 ) ↾ 𝑌 ) , 𝐹 ) = 𝐹 )
118 117 adantl ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ¬ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑗 ) ↾ 𝑌 ) , 𝐹 ) = 𝐹 )
119 118 100 eqeltrd ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ¬ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑗 ) ↾ 𝑌 ) , 𝐹 ) ∈ ( ℝ ↑m 𝑌 ) )
120 116 119 pm2.61dan ( ( 𝜑𝑗 ∈ ℕ ) → if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑗 ) ↾ 𝑌 ) , 𝐹 ) ∈ ( ℝ ↑m 𝑌 ) )
121 120 13 fmptd ( 𝜑𝐾 : ℕ ⟶ ( ℝ ↑m 𝑌 ) )
122 121 ffvelrnda ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝐾𝑗 ) ∈ ( ℝ ↑m 𝑌 ) )
123 elmapi ( ( 𝐾𝑗 ) ∈ ( ℝ ↑m 𝑌 ) → ( 𝐾𝑗 ) : 𝑌 ⟶ ℝ )
124 122 123 syl ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝐾𝑗 ) : 𝑌 ⟶ ℝ )
125 1 76 106 124 hoidmvcl ( ( 𝜑𝑗 ∈ ℕ ) → ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) ∈ ( 0 [,) +∞ ) )
126 63 125 eqeltrd ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝑃𝑗 ) ∈ ( 0 [,) +∞ ) )
127 53 58 126 vtocl ( ( 𝜑 ∧ 1 ∈ ℕ ) → ( 𝑃 ‘ 1 ) ∈ ( 0 [,) +∞ ) )
128 51 52 127 syl2anc ( 𝜑 → ( 𝑃 ‘ 1 ) ∈ ( 0 [,) +∞ ) )
129 50 128 sseldi ( 𝜑 → ( 𝑃 ‘ 1 ) ∈ ℝ )
130 129 recnd ( 𝜑 → ( 𝑃 ‘ 1 ) ∈ ℂ )
131 45 46 48 49 130 sumsnd ( 𝜑 → Σ 𝑗 ∈ { 1 } ( 𝑃𝑗 ) = ( 𝑃 ‘ 1 ) )
132 131 adantr ( ( 𝜑𝑌 = ∅ ) → Σ 𝑗 ∈ { 1 } ( 𝑃𝑗 ) = ( 𝑃 ‘ 1 ) )
133 fveq2 ( 𝑗 = 1 → ( 𝐽𝑗 ) = ( 𝐽 ‘ 1 ) )
134 fveq2 ( 𝑗 = 1 → ( 𝐾𝑗 ) = ( 𝐾 ‘ 1 ) )
135 133 134 oveq12d ( 𝑗 = 1 → ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) = ( ( 𝐽 ‘ 1 ) ( 𝐿𝑌 ) ( 𝐾 ‘ 1 ) ) )
136 ovex ( ( 𝐽 ‘ 1 ) ( 𝐿𝑌 ) ( 𝐾 ‘ 1 ) ) ∈ V
137 135 21 136 fvmpt ( 1 ∈ ℕ → ( 𝑃 ‘ 1 ) = ( ( 𝐽 ‘ 1 ) ( 𝐿𝑌 ) ( 𝐾 ‘ 1 ) ) )
138 25 137 ax-mp ( 𝑃 ‘ 1 ) = ( ( 𝐽 ‘ 1 ) ( 𝐿𝑌 ) ( 𝐾 ‘ 1 ) )
139 138 a1i ( ( 𝜑𝑌 = ∅ ) → ( 𝑃 ‘ 1 ) = ( ( 𝐽 ‘ 1 ) ( 𝐿𝑌 ) ( 𝐾 ‘ 1 ) ) )
140 30 oveqd ( 𝑌 = ∅ → ( ( 𝐽 ‘ 1 ) ( 𝐿𝑌 ) ( 𝐾 ‘ 1 ) ) = ( ( 𝐽 ‘ 1 ) ( 𝐿 ‘ ∅ ) ( 𝐾 ‘ 1 ) ) )
141 140 adantl ( ( 𝜑𝑌 = ∅ ) → ( ( 𝐽 ‘ 1 ) ( 𝐿𝑌 ) ( 𝐾 ‘ 1 ) ) = ( ( 𝐽 ‘ 1 ) ( 𝐿 ‘ ∅ ) ( 𝐾 ‘ 1 ) ) )
142 133 feq1d ( 𝑗 = 1 → ( ( 𝐽𝑗 ) : 𝑌 ⟶ ℝ ↔ ( 𝐽 ‘ 1 ) : 𝑌 ⟶ ℝ ) )
143 55 142 imbi12d ( 𝑗 = 1 → ( ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝐽𝑗 ) : 𝑌 ⟶ ℝ ) ↔ ( ( 𝜑 ∧ 1 ∈ ℕ ) → ( 𝐽 ‘ 1 ) : 𝑌 ⟶ ℝ ) ) )
144 84 adantr ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → ( ( 𝐶𝑗 ) ↾ 𝑌 ) : 𝑌 ⟶ ℝ )
145 78 feq1d ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → ( if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑗 ) ↾ 𝑌 ) , 𝐹 ) : 𝑌 ⟶ ℝ ↔ ( ( 𝐶𝑗 ) ↾ 𝑌 ) : 𝑌 ⟶ ℝ ) )
146 144 145 mpbird ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑗 ) ↾ 𝑌 ) , 𝐹 ) : 𝑌 ⟶ ℝ )
147 96 ad2antrr ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ¬ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → 𝐹 : 𝑌 ⟶ ℝ )
148 94 feq1d ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ¬ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → ( if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑗 ) ↾ 𝑌 ) , 𝐹 ) : 𝑌 ⟶ ℝ ↔ 𝐹 : 𝑌 ⟶ ℝ ) )
149 147 148 mpbird ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ¬ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑗 ) ↾ 𝑌 ) , 𝐹 ) : 𝑌 ⟶ ℝ )
150 146 149 pm2.61dan ( ( 𝜑𝑗 ∈ ℕ ) → if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑗 ) ↾ 𝑌 ) , 𝐹 ) : 𝑌 ⟶ ℝ )
151 simpr ( ( 𝜑𝑗 ∈ ℕ ) → 𝑗 ∈ ℕ )
152 fvex ( 𝐶𝑗 ) ∈ V
153 152 resex ( ( 𝐶𝑗 ) ↾ 𝑌 ) ∈ V
154 78 153 eqeltrdi ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑗 ) ↾ 𝑌 ) , 𝐹 ) ∈ V )
155 99 elexd ( 𝜑𝐹 ∈ V )
156 155 adantr ( ( 𝜑𝑗 ∈ ℕ ) → 𝐹 ∈ V )
157 156 adantr ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ¬ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → 𝐹 ∈ V )
158 94 157 eqeltrd ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ ¬ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑗 ) ↾ 𝑌 ) , 𝐹 ) ∈ V )
159 154 158 pm2.61dan ( ( 𝜑𝑗 ∈ ℕ ) → if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑗 ) ↾ 𝑌 ) , 𝐹 ) ∈ V )
160 11 fvmpt2 ( ( 𝑗 ∈ ℕ ∧ if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑗 ) ↾ 𝑌 ) , 𝐹 ) ∈ V ) → ( 𝐽𝑗 ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑗 ) ↾ 𝑌 ) , 𝐹 ) )
161 151 159 160 syl2anc ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝐽𝑗 ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑗 ) ↾ 𝑌 ) , 𝐹 ) )
162 161 feq1d ( ( 𝜑𝑗 ∈ ℕ ) → ( ( 𝐽𝑗 ) : 𝑌 ⟶ ℝ ↔ if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑗 ) ↾ 𝑌 ) , 𝐹 ) : 𝑌 ⟶ ℝ ) )
163 150 162 mpbird ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝐽𝑗 ) : 𝑌 ⟶ ℝ )
164 53 143 163 vtocl ( ( 𝜑 ∧ 1 ∈ ℕ ) → ( 𝐽 ‘ 1 ) : 𝑌 ⟶ ℝ )
165 51 52 164 syl2anc ( 𝜑 → ( 𝐽 ‘ 1 ) : 𝑌 ⟶ ℝ )
166 165 adantr ( ( 𝜑𝑌 = ∅ ) → ( 𝐽 ‘ 1 ) : 𝑌 ⟶ ℝ )
167 id ( 𝑌 = ∅ → 𝑌 = ∅ )
168 167 eqcomd ( 𝑌 = ∅ → ∅ = 𝑌 )
169 168 feq2d ( 𝑌 = ∅ → ( ( 𝐽 ‘ 1 ) : ∅ ⟶ ℝ ↔ ( 𝐽 ‘ 1 ) : 𝑌 ⟶ ℝ ) )
170 169 adantl ( ( 𝜑𝑌 = ∅ ) → ( ( 𝐽 ‘ 1 ) : ∅ ⟶ ℝ ↔ ( 𝐽 ‘ 1 ) : 𝑌 ⟶ ℝ ) )
171 166 170 mpbird ( ( 𝜑𝑌 = ∅ ) → ( 𝐽 ‘ 1 ) : ∅ ⟶ ℝ )
172 134 feq1d ( 𝑗 = 1 → ( ( 𝐾𝑗 ) : 𝑌 ⟶ ℝ ↔ ( 𝐾 ‘ 1 ) : 𝑌 ⟶ ℝ ) )
173 55 172 imbi12d ( 𝑗 = 1 → ( ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝐾𝑗 ) : 𝑌 ⟶ ℝ ) ↔ ( ( 𝜑 ∧ 1 ∈ ℕ ) → ( 𝐾 ‘ 1 ) : 𝑌 ⟶ ℝ ) ) )
174 53 173 124 vtocl ( ( 𝜑 ∧ 1 ∈ ℕ ) → ( 𝐾 ‘ 1 ) : 𝑌 ⟶ ℝ )
175 51 52 174 syl2anc ( 𝜑 → ( 𝐾 ‘ 1 ) : 𝑌 ⟶ ℝ )
176 175 adantr ( ( 𝜑𝑌 = ∅ ) → ( 𝐾 ‘ 1 ) : 𝑌 ⟶ ℝ )
177 168 feq2d ( 𝑌 = ∅ → ( ( 𝐾 ‘ 1 ) : ∅ ⟶ ℝ ↔ ( 𝐾 ‘ 1 ) : 𝑌 ⟶ ℝ ) )
178 177 adantl ( ( 𝜑𝑌 = ∅ ) → ( ( 𝐾 ‘ 1 ) : ∅ ⟶ ℝ ↔ ( 𝐾 ‘ 1 ) : 𝑌 ⟶ ℝ ) )
179 176 178 mpbird ( ( 𝜑𝑌 = ∅ ) → ( 𝐾 ‘ 1 ) : ∅ ⟶ ℝ )
180 1 171 179 hoidmv0val ( ( 𝜑𝑌 = ∅ ) → ( ( 𝐽 ‘ 1 ) ( 𝐿 ‘ ∅ ) ( 𝐾 ‘ 1 ) ) = 0 )
181 141 180 eqtrd ( ( 𝜑𝑌 = ∅ ) → ( ( 𝐽 ‘ 1 ) ( 𝐿𝑌 ) ( 𝐾 ‘ 1 ) ) = 0 )
182 132 139 181 3eqtrd ( ( 𝜑𝑌 = ∅ ) → Σ 𝑗 ∈ { 1 } ( 𝑃𝑗 ) = 0 )
183 182 oveq2d ( ( 𝜑𝑌 = ∅ ) → ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ { 1 } ( 𝑃𝑗 ) ) = ( ( 1 + 𝐸 ) · 0 ) )
184 17 rpred ( 𝜑𝐸 ∈ ℝ )
185 49 184 readdcld ( 𝜑 → ( 1 + 𝐸 ) ∈ ℝ )
186 185 recnd ( 𝜑 → ( 1 + 𝐸 ) ∈ ℂ )
187 186 mul01d ( 𝜑 → ( ( 1 + 𝐸 ) · 0 ) = 0 )
188 187 adantr ( ( 𝜑𝑌 = ∅ ) → ( ( 1 + 𝐸 ) · 0 ) = 0 )
189 eqidd ( ( 𝜑𝑌 = ∅ ) → 0 = 0 )
190 183 188 189 3eqtrd ( ( 𝜑𝑌 = ∅ ) → ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ { 1 } ( 𝑃𝑗 ) ) = 0 )
191 44 190 breq12d ( ( 𝜑𝑌 = ∅ ) → ( 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ { 1 } ( 𝑃𝑗 ) ) ↔ 0 ≤ 0 ) )
192 28 191 mpbird ( ( 𝜑𝑌 = ∅ ) → 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ { 1 } ( 𝑃𝑗 ) ) )
193 oveq2 ( 𝑚 = 1 → ( 1 ... 𝑚 ) = ( 1 ... 1 ) )
194 25 nnzi 1 ∈ ℤ
195 fzsn ( 1 ∈ ℤ → ( 1 ... 1 ) = { 1 } )
196 194 195 ax-mp ( 1 ... 1 ) = { 1 }
197 196 a1i ( 𝑚 = 1 → ( 1 ... 1 ) = { 1 } )
198 193 197 eqtrd ( 𝑚 = 1 → ( 1 ... 𝑚 ) = { 1 } )
199 198 sumeq1d ( 𝑚 = 1 → Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) = Σ 𝑗 ∈ { 1 } ( 𝑃𝑗 ) )
200 199 oveq2d ( 𝑚 = 1 → ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) = ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ { 1 } ( 𝑃𝑗 ) ) )
201 200 breq2d ( 𝑚 = 1 → ( 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) ↔ 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ { 1 } ( 𝑃𝑗 ) ) ) )
202 201 rspcev ( ( 1 ∈ ℕ ∧ 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ { 1 } ( 𝑃𝑗 ) ) ) → ∃ 𝑚 ∈ ℕ 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) )
203 26 192 202 syl2anc ( ( 𝜑𝑌 = ∅ ) → ∃ 𝑚 ∈ ℕ 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) )
204 simpl ( ( 𝜑 ∧ ¬ 𝑌 = ∅ ) → 𝜑 )
205 neqne ( ¬ 𝑌 = ∅ → 𝑌 ≠ ∅ )
206 205 adantl ( ( 𝜑 ∧ ¬ 𝑌 = ∅ ) → 𝑌 ≠ ∅ )
207 nfv 𝑗 ( 𝜑𝑌 ≠ ∅ )
208 194 a1i ( ( 𝜑𝑌 ≠ ∅ ) → 1 ∈ ℤ )
209 nnuz ℕ = ( ℤ ‘ 1 )
210 126 adantlr ( ( ( 𝜑𝑌 ≠ ∅ ) ∧ 𝑗 ∈ ℕ ) → ( 𝑃𝑗 ) ∈ ( 0 [,) +∞ ) )
211 82 a1i ( 𝜑𝑌𝑊 )
212 6 211 fssresd ( 𝜑 → ( 𝐴𝑌 ) : 𝑌 ⟶ ℝ )
213 7 211 fssresd ( 𝜑 → ( 𝐵𝑌 ) : 𝑌 ⟶ ℝ )
214 1 75 212 213 hoidmvcl ( 𝜑 → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ∈ ( 0 [,) +∞ ) )
215 50 214 sseldi ( 𝜑 → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ∈ ℝ )
216 16 215 eqeltrid ( 𝜑𝐺 ∈ ℝ )
217 0red ( 𝜑 → 0 ∈ ℝ )
218 1rp 1 ∈ ℝ+
219 218 a1i ( 𝜑 → 1 ∈ ℝ+ )
220 219 17 jca ( 𝜑 → ( 1 ∈ ℝ+𝐸 ∈ ℝ+ ) )
221 rpaddcl ( ( 1 ∈ ℝ+𝐸 ∈ ℝ+ ) → ( 1 + 𝐸 ) ∈ ℝ+ )
222 220 221 syl ( 𝜑 → ( 1 + 𝐸 ) ∈ ℝ+ )
223 rpgt0 ( ( 1 + 𝐸 ) ∈ ℝ+ → 0 < ( 1 + 𝐸 ) )
224 222 223 syl ( 𝜑 → 0 < ( 1 + 𝐸 ) )
225 217 224 gtned ( 𝜑 → ( 1 + 𝐸 ) ≠ 0 )
226 216 185 225 redivcld ( 𝜑 → ( 𝐺 / ( 1 + 𝐸 ) ) ∈ ℝ )
227 226 adantr ( ( 𝜑𝑌 ≠ ∅ ) → ( 𝐺 / ( 1 + 𝐸 ) ) ∈ ℝ )
228 226 ltpnfd ( 𝜑 → ( 𝐺 / ( 1 + 𝐸 ) ) < +∞ )
229 228 adantr ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝑃𝑗 ) ) ) = +∞ ) → ( 𝐺 / ( 1 + 𝐸 ) ) < +∞ )
230 id ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝑃𝑗 ) ) ) = +∞ → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝑃𝑗 ) ) ) = +∞ )
231 230 eqcomd ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝑃𝑗 ) ) ) = +∞ → +∞ = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝑃𝑗 ) ) ) )
232 231 adantl ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝑃𝑗 ) ) ) = +∞ ) → +∞ = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝑃𝑗 ) ) ) )
233 229 232 breqtrd ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝑃𝑗 ) ) ) = +∞ ) → ( 𝐺 / ( 1 + 𝐸 ) ) < ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝑃𝑗 ) ) ) )
234 233 adantlr ( ( ( 𝜑𝑌 ≠ ∅ ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝑃𝑗 ) ) ) = +∞ ) → ( 𝐺 / ( 1 + 𝐸 ) ) < ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝑃𝑗 ) ) ) )
235 simpl ( ( ( 𝜑𝑌 ≠ ∅ ) ∧ ¬ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝑃𝑗 ) ) ) = +∞ ) → ( 𝜑𝑌 ≠ ∅ ) )
236 simpr ( ( 𝜑 ∧ ¬ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝑃𝑗 ) ) ) = +∞ ) → ¬ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝑃𝑗 ) ) ) = +∞ )
237 nnex ℕ ∈ V
238 237 a1i ( ( 𝜑 ∧ ¬ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝑃𝑗 ) ) ) = +∞ ) → ℕ ∈ V )
239 icossicc ( 0 [,) +∞ ) ⊆ ( 0 [,] +∞ )
240 239 126 sseldi ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝑃𝑗 ) ∈ ( 0 [,] +∞ ) )
241 eqid ( 𝑗 ∈ ℕ ↦ ( 𝑃𝑗 ) ) = ( 𝑗 ∈ ℕ ↦ ( 𝑃𝑗 ) )
242 240 241 fmptd ( 𝜑 → ( 𝑗 ∈ ℕ ↦ ( 𝑃𝑗 ) ) : ℕ ⟶ ( 0 [,] +∞ ) )
243 242 adantr ( ( 𝜑 ∧ ¬ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝑃𝑗 ) ) ) = +∞ ) → ( 𝑗 ∈ ℕ ↦ ( 𝑃𝑗 ) ) : ℕ ⟶ ( 0 [,] +∞ ) )
244 238 243 sge0repnf ( ( 𝜑 ∧ ¬ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝑃𝑗 ) ) ) = +∞ ) → ( ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝑃𝑗 ) ) ) ∈ ℝ ↔ ¬ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝑃𝑗 ) ) ) = +∞ ) )
245 236 244 mpbird ( ( 𝜑 ∧ ¬ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝑃𝑗 ) ) ) = +∞ ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝑃𝑗 ) ) ) ∈ ℝ )
246 245 adantlr ( ( ( 𝜑𝑌 ≠ ∅ ) ∧ ¬ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝑃𝑗 ) ) ) = +∞ ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝑃𝑗 ) ) ) ∈ ℝ )
247 227 adantr ( ( ( 𝜑𝑌 ≠ ∅ ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝑃𝑗 ) ) ) ∈ ℝ ) → ( 𝐺 / ( 1 + 𝐸 ) ) ∈ ℝ )
248 216 adantr ( ( 𝜑 ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝑃𝑗 ) ) ) ∈ ℝ ) → 𝐺 ∈ ℝ )
249 248 adantlr ( ( ( 𝜑𝑌 ≠ ∅ ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝑃𝑗 ) ) ) ∈ ℝ ) → 𝐺 ∈ ℝ )
250 simpr ( ( ( 𝜑𝑌 ≠ ∅ ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝑃𝑗 ) ) ) ∈ ℝ ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝑃𝑗 ) ) ) ∈ ℝ )
251 49 17 ltaddrpd ( 𝜑 → 1 < ( 1 + 𝐸 ) )
252 251 adantr ( ( 𝜑𝑌 ≠ ∅ ) → 1 < ( 1 + 𝐸 ) )
253 75 adantr ( ( 𝜑𝑌 ≠ ∅ ) → 𝑌 ∈ Fin )
254 simpr ( ( 𝜑𝑌 ≠ ∅ ) → 𝑌 ≠ ∅ )
255 212 adantr ( ( 𝜑𝑌 ≠ ∅ ) → ( 𝐴𝑌 ) : 𝑌 ⟶ ℝ )
256 213 adantr ( ( 𝜑𝑌 ≠ ∅ ) → ( 𝐵𝑌 ) : 𝑌 ⟶ ℝ )
257 1 253 254 255 256 hoidmvn0val ( ( 𝜑𝑌 ≠ ∅ ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) = ∏ 𝑘𝑌 ( vol ‘ ( ( ( 𝐴𝑌 ) ‘ 𝑘 ) [,) ( ( 𝐵𝑌 ) ‘ 𝑘 ) ) ) )
258 16 a1i ( ( 𝜑𝑌 ≠ ∅ ) → 𝐺 = ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) )
259 fvres ( 𝑘𝑌 → ( ( 𝐴𝑌 ) ‘ 𝑘 ) = ( 𝐴𝑘 ) )
260 fvres ( 𝑘𝑌 → ( ( 𝐵𝑌 ) ‘ 𝑘 ) = ( 𝐵𝑘 ) )
261 259 260 oveq12d ( 𝑘𝑌 → ( ( ( 𝐴𝑌 ) ‘ 𝑘 ) [,) ( ( 𝐵𝑌 ) ‘ 𝑘 ) ) = ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) )
262 261 fveq2d ( 𝑘𝑌 → ( vol ‘ ( ( ( 𝐴𝑌 ) ‘ 𝑘 ) [,) ( ( 𝐵𝑌 ) ‘ 𝑘 ) ) ) = ( vol ‘ ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) )
263 262 adantl ( ( 𝜑𝑘𝑌 ) → ( vol ‘ ( ( ( 𝐴𝑌 ) ‘ 𝑘 ) [,) ( ( 𝐵𝑌 ) ‘ 𝑘 ) ) ) = ( vol ‘ ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) )
264 6 adantr ( ( 𝜑𝑘𝑌 ) → 𝐴 : 𝑊 ⟶ ℝ )
265 elun1 ( 𝑘𝑌𝑘 ∈ ( 𝑌 ∪ { 𝑍 } ) )
266 265 5 eleqtrrdi ( 𝑘𝑌𝑘𝑊 )
267 266 adantl ( ( 𝜑𝑘𝑌 ) → 𝑘𝑊 )
268 264 267 ffvelrnd ( ( 𝜑𝑘𝑌 ) → ( 𝐴𝑘 ) ∈ ℝ )
269 7 adantr ( ( 𝜑𝑘𝑌 ) → 𝐵 : 𝑊 ⟶ ℝ )
270 269 267 ffvelrnd ( ( 𝜑𝑘𝑌 ) → ( 𝐵𝑘 ) ∈ ℝ )
271 volico ( ( ( 𝐴𝑘 ) ∈ ℝ ∧ ( 𝐵𝑘 ) ∈ ℝ ) → ( vol ‘ ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) = if ( ( 𝐴𝑘 ) < ( 𝐵𝑘 ) , ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) , 0 ) )
272 268 270 271 syl2anc ( ( 𝜑𝑘𝑌 ) → ( vol ‘ ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) = if ( ( 𝐴𝑘 ) < ( 𝐵𝑘 ) , ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) , 0 ) )
273 267 8 syldan ( ( 𝜑𝑘𝑌 ) → ( 𝐴𝑘 ) < ( 𝐵𝑘 ) )
274 273 iftrued ( ( 𝜑𝑘𝑌 ) → if ( ( 𝐴𝑘 ) < ( 𝐵𝑘 ) , ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) , 0 ) = ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) )
275 263 272 274 3eqtrd ( ( 𝜑𝑘𝑌 ) → ( vol ‘ ( ( ( 𝐴𝑌 ) ‘ 𝑘 ) [,) ( ( 𝐵𝑌 ) ‘ 𝑘 ) ) ) = ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) )
276 275 prodeq2dv ( 𝜑 → ∏ 𝑘𝑌 ( vol ‘ ( ( ( 𝐴𝑌 ) ‘ 𝑘 ) [,) ( ( 𝐵𝑌 ) ‘ 𝑘 ) ) ) = ∏ 𝑘𝑌 ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) )
277 276 eqcomd ( 𝜑 → ∏ 𝑘𝑌 ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) = ∏ 𝑘𝑌 ( vol ‘ ( ( ( 𝐴𝑌 ) ‘ 𝑘 ) [,) ( ( 𝐵𝑌 ) ‘ 𝑘 ) ) ) )
278 277 adantr ( ( 𝜑𝑌 ≠ ∅ ) → ∏ 𝑘𝑌 ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) = ∏ 𝑘𝑌 ( vol ‘ ( ( ( 𝐴𝑌 ) ‘ 𝑘 ) [,) ( ( 𝐵𝑌 ) ‘ 𝑘 ) ) ) )
279 257 258 278 3eqtr4d ( ( 𝜑𝑌 ≠ ∅ ) → 𝐺 = ∏ 𝑘𝑌 ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) )
280 difrp ( ( ( 𝐴𝑘 ) ∈ ℝ ∧ ( 𝐵𝑘 ) ∈ ℝ ) → ( ( 𝐴𝑘 ) < ( 𝐵𝑘 ) ↔ ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) ∈ ℝ+ ) )
281 268 270 280 syl2anc ( ( 𝜑𝑘𝑌 ) → ( ( 𝐴𝑘 ) < ( 𝐵𝑘 ) ↔ ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) ∈ ℝ+ ) )
282 273 281 mpbid ( ( 𝜑𝑘𝑌 ) → ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) ∈ ℝ+ )
283 75 282 fprodrpcl ( 𝜑 → ∏ 𝑘𝑌 ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) ∈ ℝ+ )
284 283 adantr ( ( 𝜑𝑌 ≠ ∅ ) → ∏ 𝑘𝑌 ( ( 𝐵𝑘 ) − ( 𝐴𝑘 ) ) ∈ ℝ+ )
285 279 284 eqeltrd ( ( 𝜑𝑌 ≠ ∅ ) → 𝐺 ∈ ℝ+ )
286 222 adantr ( ( 𝜑𝑌 ≠ ∅ ) → ( 1 + 𝐸 ) ∈ ℝ+ )
287 285 286 ltdivgt1 ( ( 𝜑𝑌 ≠ ∅ ) → ( 1 < ( 1 + 𝐸 ) ↔ ( 𝐺 / ( 1 + 𝐸 ) ) < 𝐺 ) )
288 252 287 mpbid ( ( 𝜑𝑌 ≠ ∅ ) → ( 𝐺 / ( 1 + 𝐸 ) ) < 𝐺 )
289 288 adantr ( ( ( 𝜑𝑌 ≠ ∅ ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝑃𝑗 ) ) ) ∈ ℝ ) → ( 𝐺 / ( 1 + 𝐸 ) ) < 𝐺 )
290 23 adantr ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) → X 𝑘𝑊 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) )
291 fvexd ( 𝜑 → ( 𝑥𝑘 ) ∈ V )
292 19 elexd ( 𝜑𝑆 ∈ V )
293 291 292 ifcld ( 𝜑 → if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) ∈ V )
294 293 ralrimivw ( 𝜑 → ∀ 𝑘𝑊 if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) ∈ V )
295 294 adantr ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) → ∀ 𝑘𝑊 if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) ∈ V )
296 eqid ( 𝑘𝑊 ↦ if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) ) = ( 𝑘𝑊 ↦ if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) )
297 296 fnmpt ( ∀ 𝑘𝑊 if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) ∈ V → ( 𝑘𝑊 ↦ if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) ) Fn 𝑊 )
298 295 297 syl ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) → ( 𝑘𝑊 ↦ if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) ) Fn 𝑊 )
299 simpr ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) → 𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) )
300 mptexg ( 𝑊 ∈ Fin → ( 𝑘𝑊 ↦ if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) ) ∈ V )
301 70 300 syl ( 𝜑 → ( 𝑘𝑊 ↦ if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) ) ∈ V )
302 301 adantr ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) → ( 𝑘𝑊 ↦ if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) ) ∈ V )
303 24 fvmpt2 ( ( 𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ∧ ( 𝑘𝑊 ↦ if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) ) ∈ V ) → ( 𝑂𝑥 ) = ( 𝑘𝑊 ↦ if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) ) )
304 299 302 303 syl2anc ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) → ( 𝑂𝑥 ) = ( 𝑘𝑊 ↦ if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) ) )
305 304 fneq1d ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) → ( ( 𝑂𝑥 ) Fn 𝑊 ↔ ( 𝑘𝑊 ↦ if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) ) Fn 𝑊 ) )
306 298 305 mpbird ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) → ( 𝑂𝑥 ) Fn 𝑊 )
307 nfv 𝑘 𝜑
308 nfcv 𝑘 𝑥
309 nfixp1 𝑘 X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) )
310 308 309 nfel 𝑘 𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) )
311 307 310 nfan 𝑘 ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) )
312 304 fveq1d ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) → ( ( 𝑂𝑥 ) ‘ 𝑘 ) = ( ( 𝑘𝑊 ↦ if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) ) ‘ 𝑘 ) )
313 312 adantr ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑘𝑊 ) → ( ( 𝑂𝑥 ) ‘ 𝑘 ) = ( ( 𝑘𝑊 ↦ if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) ) ‘ 𝑘 ) )
314 simpr ( ( 𝜑𝑘𝑊 ) → 𝑘𝑊 )
315 293 adantr ( ( 𝜑𝑘𝑊 ) → if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) ∈ V )
316 296 fvmpt2 ( ( 𝑘𝑊 ∧ if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) ∈ V ) → ( ( 𝑘𝑊 ↦ if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) ) ‘ 𝑘 ) = if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) )
317 314 315 316 syl2anc ( ( 𝜑𝑘𝑊 ) → ( ( 𝑘𝑊 ↦ if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) ) ‘ 𝑘 ) = if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) )
318 317 adantlr ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑘𝑊 ) → ( ( 𝑘𝑊 ↦ if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) ) ‘ 𝑘 ) = if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) )
319 313 318 eqtrd ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑘𝑊 ) → ( ( 𝑂𝑥 ) ‘ 𝑘 ) = if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) )
320 iftrue ( 𝑘𝑌 → if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) = ( 𝑥𝑘 ) )
321 320 adantl ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑘𝑊 ) ∧ 𝑘𝑌 ) → if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) = ( 𝑥𝑘 ) )
322 vex 𝑥 ∈ V
323 322 elixp ( 𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ↔ ( 𝑥 Fn 𝑌 ∧ ∀ 𝑘𝑌 ( 𝑥𝑘 ) ∈ ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) )
324 323 simprbi ( 𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) → ∀ 𝑘𝑌 ( 𝑥𝑘 ) ∈ ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) )
325 324 adantr ( ( 𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ∧ 𝑘𝑌 ) → ∀ 𝑘𝑌 ( 𝑥𝑘 ) ∈ ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) )
326 simpr ( ( 𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ∧ 𝑘𝑌 ) → 𝑘𝑌 )
327 rspa ( ( ∀ 𝑘𝑌 ( 𝑥𝑘 ) ∈ ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ∧ 𝑘𝑌 ) → ( 𝑥𝑘 ) ∈ ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) )
328 325 326 327 syl2anc ( ( 𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ∧ 𝑘𝑌 ) → ( 𝑥𝑘 ) ∈ ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) )
329 328 ad4ant24 ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑘𝑊 ) ∧ 𝑘𝑌 ) → ( 𝑥𝑘 ) ∈ ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) )
330 321 329 eqeltrd ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑘𝑊 ) ∧ 𝑘𝑌 ) → if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) ∈ ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) )
331 snidg ( 𝑍 ∈ ( 𝑋𝑌 ) → 𝑍 ∈ { 𝑍 } )
332 4 331 syl ( 𝜑𝑍 ∈ { 𝑍 } )
333 elun2 ( 𝑍 ∈ { 𝑍 } → 𝑍 ∈ ( 𝑌 ∪ { 𝑍 } ) )
334 332 333 syl ( 𝜑𝑍 ∈ ( 𝑌 ∪ { 𝑍 } ) )
335 72 a1i ( 𝜑 → ( 𝑌 ∪ { 𝑍 } ) = 𝑊 )
336 334 335 eleqtrd ( 𝜑𝑍𝑊 )
337 6 336 ffvelrnd ( 𝜑 → ( 𝐴𝑍 ) ∈ ℝ )
338 337 rexrd ( 𝜑 → ( 𝐴𝑍 ) ∈ ℝ* )
339 7 336 ffvelrnd ( 𝜑 → ( 𝐵𝑍 ) ∈ ℝ )
340 339 rexrd ( 𝜑 → ( 𝐵𝑍 ) ∈ ℝ* )
341 iccssxr ( ( 𝐴𝑍 ) [,] ( 𝐵𝑍 ) ) ⊆ ℝ*
342 ssrab2 { 𝑧 ∈ ( ( 𝐴𝑍 ) [,] ( 𝐵𝑍 ) ) ∣ ( 𝐺 · ( 𝑧 − ( 𝐴𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑧 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) } ⊆ ( ( 𝐴𝑍 ) [,] ( 𝐵𝑍 ) )
343 18 342 eqsstri 𝑈 ⊆ ( ( 𝐴𝑍 ) [,] ( 𝐵𝑍 ) )
344 343 19 sseldi ( 𝜑𝑆 ∈ ( ( 𝐴𝑍 ) [,] ( 𝐵𝑍 ) ) )
345 341 344 sseldi ( 𝜑𝑆 ∈ ℝ* )
346 iccgelb ( ( ( 𝐴𝑍 ) ∈ ℝ* ∧ ( 𝐵𝑍 ) ∈ ℝ*𝑆 ∈ ( ( 𝐴𝑍 ) [,] ( 𝐵𝑍 ) ) ) → ( 𝐴𝑍 ) ≤ 𝑆 )
347 338 340 344 346 syl3anc ( 𝜑 → ( 𝐴𝑍 ) ≤ 𝑆 )
348 338 340 345 347 20 elicod ( 𝜑𝑆 ∈ ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) )
349 348 ad2antrr ( ( ( 𝜑𝑘𝑊 ) ∧ ¬ 𝑘𝑌 ) → 𝑆 ∈ ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) )
350 iffalse ( ¬ 𝑘𝑌 → if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) = 𝑆 )
351 350 adantl ( ( ( 𝜑𝑘𝑊 ) ∧ ¬ 𝑘𝑌 ) → if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) = 𝑆 )
352 5 eleq2i ( 𝑘𝑊𝑘 ∈ ( 𝑌 ∪ { 𝑍 } ) )
353 352 biimpi ( 𝑘𝑊𝑘 ∈ ( 𝑌 ∪ { 𝑍 } ) )
354 353 adantr ( ( 𝑘𝑊 ∧ ¬ 𝑘𝑌 ) → 𝑘 ∈ ( 𝑌 ∪ { 𝑍 } ) )
355 simpr ( ( 𝑘𝑊 ∧ ¬ 𝑘𝑌 ) → ¬ 𝑘𝑌 )
356 elunnel1 ( ( 𝑘 ∈ ( 𝑌 ∪ { 𝑍 } ) ∧ ¬ 𝑘𝑌 ) → 𝑘 ∈ { 𝑍 } )
357 354 355 356 syl2anc ( ( 𝑘𝑊 ∧ ¬ 𝑘𝑌 ) → 𝑘 ∈ { 𝑍 } )
358 elsni ( 𝑘 ∈ { 𝑍 } → 𝑘 = 𝑍 )
359 357 358 syl ( ( 𝑘𝑊 ∧ ¬ 𝑘𝑌 ) → 𝑘 = 𝑍 )
360 fveq2 ( 𝑘 = 𝑍 → ( 𝐴𝑘 ) = ( 𝐴𝑍 ) )
361 fveq2 ( 𝑘 = 𝑍 → ( 𝐵𝑘 ) = ( 𝐵𝑍 ) )
362 360 361 oveq12d ( 𝑘 = 𝑍 → ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) = ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) )
363 359 362 syl ( ( 𝑘𝑊 ∧ ¬ 𝑘𝑌 ) → ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) = ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) )
364 363 adantll ( ( ( 𝜑𝑘𝑊 ) ∧ ¬ 𝑘𝑌 ) → ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) = ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) )
365 351 364 eleq12d ( ( ( 𝜑𝑘𝑊 ) ∧ ¬ 𝑘𝑌 ) → ( if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) ∈ ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ↔ 𝑆 ∈ ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) ) )
366 349 365 mpbird ( ( ( 𝜑𝑘𝑊 ) ∧ ¬ 𝑘𝑌 ) → if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) ∈ ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) )
367 366 adantllr ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑘𝑊 ) ∧ ¬ 𝑘𝑌 ) → if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) ∈ ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) )
368 330 367 pm2.61dan ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑘𝑊 ) → if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) ∈ ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) )
369 319 368 eqeltrd ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑘𝑊 ) → ( ( 𝑂𝑥 ) ‘ 𝑘 ) ∈ ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) )
370 369 ex ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) → ( 𝑘𝑊 → ( ( 𝑂𝑥 ) ‘ 𝑘 ) ∈ ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) )
371 311 370 ralrimi ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) → ∀ 𝑘𝑊 ( ( 𝑂𝑥 ) ‘ 𝑘 ) ∈ ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) )
372 306 371 jca ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) → ( ( 𝑂𝑥 ) Fn 𝑊 ∧ ∀ 𝑘𝑊 ( ( 𝑂𝑥 ) ‘ 𝑘 ) ∈ ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) )
373 fvex ( 𝑂𝑥 ) ∈ V
374 373 elixp ( ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ↔ ( ( 𝑂𝑥 ) Fn 𝑊 ∧ ∀ 𝑘𝑊 ( ( 𝑂𝑥 ) ‘ 𝑘 ) ∈ ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) )
375 372 374 sylibr ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) → ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) )
376 290 375 sseldd ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) → ( 𝑂𝑥 ) ∈ 𝑗 ∈ ℕ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) )
377 eliun ( ( 𝑂𝑥 ) ∈ 𝑗 ∈ ℕ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ↔ ∃ 𝑗 ∈ ℕ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) )
378 376 377 sylib ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) → ∃ 𝑗 ∈ ℕ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) )
379 ixpfn ( 𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) → 𝑥 Fn 𝑌 )
380 379 adantl ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) → 𝑥 Fn 𝑌 )
381 380 ad2antrr ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) → 𝑥 Fn 𝑌 )
382 nfv 𝑘 𝑗 ∈ ℕ
383 311 382 nfan 𝑘 ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ )
384 nfcv 𝑘 ( 𝑂𝑥 )
385 nfixp1 𝑘 X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) )
386 384 385 nfel 𝑘 ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) )
387 383 386 nfan 𝑘 ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) )
388 312 3adant3 ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ∧ 𝑘𝑌 ) → ( ( 𝑂𝑥 ) ‘ 𝑘 ) = ( ( 𝑘𝑊 ↦ if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) ) ‘ 𝑘 ) )
389 293 adantr ( ( 𝜑𝑘𝑌 ) → if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) ∈ V )
390 267 389 316 syl2anc ( ( 𝜑𝑘𝑌 ) → ( ( 𝑘𝑊 ↦ if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) ) ‘ 𝑘 ) = if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) )
391 390 3adant2 ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ∧ 𝑘𝑌 ) → ( ( 𝑘𝑊 ↦ if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) ) ‘ 𝑘 ) = if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) )
392 320 3ad2ant3 ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ∧ 𝑘𝑌 ) → if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) = ( 𝑥𝑘 ) )
393 388 391 392 3eqtrrd ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ∧ 𝑘𝑌 ) → ( 𝑥𝑘 ) = ( ( 𝑂𝑥 ) ‘ 𝑘 ) )
394 393 ad5ant125 ( ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘𝑌 ) → ( 𝑥𝑘 ) = ( ( 𝑂𝑥 ) ‘ 𝑘 ) )
395 simpl ( ( ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ∧ 𝑘𝑌 ) → ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) )
396 373 elixp ( ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ↔ ( ( 𝑂𝑥 ) Fn 𝑊 ∧ ∀ 𝑘𝑊 ( ( 𝑂𝑥 ) ‘ 𝑘 ) ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) )
397 395 396 sylib ( ( ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ∧ 𝑘𝑌 ) → ( ( 𝑂𝑥 ) Fn 𝑊 ∧ ∀ 𝑘𝑊 ( ( 𝑂𝑥 ) ‘ 𝑘 ) ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) )
398 397 simprd ( ( ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ∧ 𝑘𝑌 ) → ∀ 𝑘𝑊 ( ( 𝑂𝑥 ) ‘ 𝑘 ) ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) )
399 266 adantl ( ( ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ∧ 𝑘𝑌 ) → 𝑘𝑊 )
400 rspa ( ( ∀ 𝑘𝑊 ( ( 𝑂𝑥 ) ‘ 𝑘 ) ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ∧ 𝑘𝑊 ) → ( ( 𝑂𝑥 ) ‘ 𝑘 ) ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) )
401 398 399 400 syl2anc ( ( ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ∧ 𝑘𝑌 ) → ( ( 𝑂𝑥 ) ‘ 𝑘 ) ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) )
402 401 adantll ( ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘𝑌 ) → ( ( 𝑂𝑥 ) ‘ 𝑘 ) ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) )
403 394 402 eqeltrd ( ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘𝑌 ) → ( 𝑥𝑘 ) ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) )
404 51 ad3antrrr ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) → 𝜑 )
405 59 ad2antlr ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) → 𝑗 ∈ ℕ )
406 304 fveq1d ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) → ( ( 𝑂𝑥 ) ‘ 𝑍 ) = ( ( 𝑘𝑊 ↦ if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) ) ‘ 𝑍 ) )
407 eqidd ( 𝜑 → ( 𝑘𝑊 ↦ if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) ) = ( 𝑘𝑊 ↦ if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) ) )
408 eleq1 ( 𝑘 = 𝑍 → ( 𝑘𝑌𝑍𝑌 ) )
409 fveq2 ( 𝑘 = 𝑍 → ( 𝑥𝑘 ) = ( 𝑥𝑍 ) )
410 408 409 ifbieq1d ( 𝑘 = 𝑍 → if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) = if ( 𝑍𝑌 , ( 𝑥𝑍 ) , 𝑆 ) )
411 410 adantl ( ( 𝜑𝑘 = 𝑍 ) → if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) = if ( 𝑍𝑌 , ( 𝑥𝑍 ) , 𝑆 ) )
412 fvexd ( 𝜑 → ( 𝑥𝑍 ) ∈ V )
413 412 292 ifcld ( 𝜑 → if ( 𝑍𝑌 , ( 𝑥𝑍 ) , 𝑆 ) ∈ V )
414 407 411 336 413 fvmptd ( 𝜑 → ( ( 𝑘𝑊 ↦ if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) ) ‘ 𝑍 ) = if ( 𝑍𝑌 , ( 𝑥𝑍 ) , 𝑆 ) )
415 414 adantr ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) → ( ( 𝑘𝑊 ↦ if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) ) ‘ 𝑍 ) = if ( 𝑍𝑌 , ( 𝑥𝑍 ) , 𝑆 ) )
416 4 eldifbd ( 𝜑 → ¬ 𝑍𝑌 )
417 416 iffalsed ( 𝜑 → if ( 𝑍𝑌 , ( 𝑥𝑍 ) , 𝑆 ) = 𝑆 )
418 417 adantr ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) → if ( 𝑍𝑌 , ( 𝑥𝑍 ) , 𝑆 ) = 𝑆 )
419 406 415 418 3eqtrrd ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) → 𝑆 = ( ( 𝑂𝑥 ) ‘ 𝑍 ) )
420 419 ad2antrr ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) → 𝑆 = ( ( 𝑂𝑥 ) ‘ 𝑍 ) )
421 404 336 syl ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) → 𝑍𝑊 )
422 396 simprbi ( ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) → ∀ 𝑘𝑊 ( ( 𝑂𝑥 ) ‘ 𝑘 ) ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) )
423 422 adantl ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) → ∀ 𝑘𝑊 ( ( 𝑂𝑥 ) ‘ 𝑘 ) ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) )
424 fveq2 ( 𝑘 = 𝑍 → ( ( 𝑂𝑥 ) ‘ 𝑘 ) = ( ( 𝑂𝑥 ) ‘ 𝑍 ) )
425 fveq2 ( 𝑘 = 𝑍 → ( ( 𝐶𝑗 ) ‘ 𝑘 ) = ( ( 𝐶𝑗 ) ‘ 𝑍 ) )
426 fveq2 ( 𝑘 = 𝑍 → ( ( 𝐷𝑗 ) ‘ 𝑘 ) = ( ( 𝐷𝑗 ) ‘ 𝑍 ) )
427 425 426 oveq12d ( 𝑘 = 𝑍 → ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) = ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) )
428 424 427 eleq12d ( 𝑘 = 𝑍 → ( ( ( 𝑂𝑥 ) ‘ 𝑘 ) ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ↔ ( ( 𝑂𝑥 ) ‘ 𝑍 ) ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) )
429 428 rspcva ( ( 𝑍𝑊 ∧ ∀ 𝑘𝑊 ( ( 𝑂𝑥 ) ‘ 𝑘 ) ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) → ( ( 𝑂𝑥 ) ‘ 𝑍 ) ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) )
430 421 423 429 syl2anc ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) → ( ( 𝑂𝑥 ) ‘ 𝑍 ) ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) )
431 420 430 eqeltrd ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) → 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) )
432 161 3adant3 ( ( 𝜑𝑗 ∈ ℕ ∧ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → ( 𝐽𝑗 ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑗 ) ↾ 𝑌 ) , 𝐹 ) )
433 77 3ad2ant3 ( ( 𝜑𝑗 ∈ ℕ ∧ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑗 ) ↾ 𝑌 ) , 𝐹 ) = ( ( 𝐶𝑗 ) ↾ 𝑌 ) )
434 432 433 eqtrd ( ( 𝜑𝑗 ∈ ℕ ∧ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → ( 𝐽𝑗 ) = ( ( 𝐶𝑗 ) ↾ 𝑌 ) )
435 434 fveq1d ( ( 𝜑𝑗 ∈ ℕ ∧ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → ( ( 𝐽𝑗 ) ‘ 𝑘 ) = ( ( ( 𝐶𝑗 ) ↾ 𝑌 ) ‘ 𝑘 ) )
436 404 405 431 435 syl3anc ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) → ( ( 𝐽𝑗 ) ‘ 𝑘 ) = ( ( ( 𝐶𝑗 ) ↾ 𝑌 ) ‘ 𝑘 ) )
437 436 adantr ( ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘𝑌 ) → ( ( 𝐽𝑗 ) ‘ 𝑘 ) = ( ( ( 𝐶𝑗 ) ↾ 𝑌 ) ‘ 𝑘 ) )
438 fvres ( 𝑘𝑌 → ( ( ( 𝐶𝑗 ) ↾ 𝑌 ) ‘ 𝑘 ) = ( ( 𝐶𝑗 ) ‘ 𝑘 ) )
439 438 adantl ( ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘𝑌 ) → ( ( ( 𝐶𝑗 ) ↾ 𝑌 ) ‘ 𝑘 ) = ( ( 𝐶𝑗 ) ‘ 𝑘 ) )
440 437 439 eqtrd ( ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘𝑌 ) → ( ( 𝐽𝑗 ) ‘ 𝑘 ) = ( ( 𝐶𝑗 ) ‘ 𝑘 ) )
441 120 elexd ( ( 𝜑𝑗 ∈ ℕ ) → if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑗 ) ↾ 𝑌 ) , 𝐹 ) ∈ V )
442 13 fvmpt2 ( ( 𝑗 ∈ ℕ ∧ if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑗 ) ↾ 𝑌 ) , 𝐹 ) ∈ V ) → ( 𝐾𝑗 ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑗 ) ↾ 𝑌 ) , 𝐹 ) )
443 151 441 442 syl2anc ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝐾𝑗 ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑗 ) ↾ 𝑌 ) , 𝐹 ) )
444 443 3adant3 ( ( 𝜑𝑗 ∈ ℕ ∧ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → ( 𝐾𝑗 ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑗 ) ↾ 𝑌 ) , 𝐹 ) )
445 107 3ad2ant3 ( ( 𝜑𝑗 ∈ ℕ ∧ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑗 ) ↾ 𝑌 ) , 𝐹 ) = ( ( 𝐷𝑗 ) ↾ 𝑌 ) )
446 444 445 eqtrd ( ( 𝜑𝑗 ∈ ℕ ∧ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → ( 𝐾𝑗 ) = ( ( 𝐷𝑗 ) ↾ 𝑌 ) )
447 446 fveq1d ( ( 𝜑𝑗 ∈ ℕ ∧ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → ( ( 𝐾𝑗 ) ‘ 𝑘 ) = ( ( ( 𝐷𝑗 ) ↾ 𝑌 ) ‘ 𝑘 ) )
448 404 405 431 447 syl3anc ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) → ( ( 𝐾𝑗 ) ‘ 𝑘 ) = ( ( ( 𝐷𝑗 ) ↾ 𝑌 ) ‘ 𝑘 ) )
449 448 adantr ( ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘𝑌 ) → ( ( 𝐾𝑗 ) ‘ 𝑘 ) = ( ( ( 𝐷𝑗 ) ↾ 𝑌 ) ‘ 𝑘 ) )
450 fvres ( 𝑘𝑌 → ( ( ( 𝐷𝑗 ) ↾ 𝑌 ) ‘ 𝑘 ) = ( ( 𝐷𝑗 ) ‘ 𝑘 ) )
451 450 adantl ( ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘𝑌 ) → ( ( ( 𝐷𝑗 ) ↾ 𝑌 ) ‘ 𝑘 ) = ( ( 𝐷𝑗 ) ‘ 𝑘 ) )
452 449 451 eqtrd ( ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘𝑌 ) → ( ( 𝐾𝑗 ) ‘ 𝑘 ) = ( ( 𝐷𝑗 ) ‘ 𝑘 ) )
453 440 452 oveq12d ( ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘𝑌 ) → ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) = ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) )
454 453 eqcomd ( ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘𝑌 ) → ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) = ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) )
455 403 454 eleqtrd ( ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘𝑌 ) → ( 𝑥𝑘 ) ∈ ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) )
456 455 ex ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) → ( 𝑘𝑌 → ( 𝑥𝑘 ) ∈ ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) ) )
457 387 456 ralrimi ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) → ∀ 𝑘𝑌 ( 𝑥𝑘 ) ∈ ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) )
458 381 457 jca ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) → ( 𝑥 Fn 𝑌 ∧ ∀ 𝑘𝑌 ( 𝑥𝑘 ) ∈ ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) ) )
459 322 elixp ( 𝑥X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) ↔ ( 𝑥 Fn 𝑌 ∧ ∀ 𝑘𝑌 ( 𝑥𝑘 ) ∈ ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) ) )
460 458 459 sylibr ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) → 𝑥X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) )
461 460 ex ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) → 𝑥X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) ) )
462 461 reximdva ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) → ( ∃ 𝑗 ∈ ℕ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) → ∃ 𝑗 ∈ ℕ 𝑥X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) ) )
463 378 462 mpd ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) → ∃ 𝑗 ∈ ℕ 𝑥X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) )
464 eliun ( 𝑥 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) ↔ ∃ 𝑗 ∈ ℕ 𝑥X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) )
465 463 464 sylibr ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) → 𝑥 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) )
466 465 ralrimiva ( 𝜑 → ∀ 𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) 𝑥 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) )
467 dfss3 ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) ↔ ∀ 𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) 𝑥 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) )
468 466 467 sylibr ( 𝜑X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) )
469 ovexd ( 𝜑 → ( ℝ ↑m 𝑌 ) ∈ V )
470 237 a1i ( 𝜑 → ℕ ∈ V )
471 469 470 elmapd ( 𝜑 → ( 𝐾 ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ↔ 𝐾 : ℕ ⟶ ( ℝ ↑m 𝑌 ) ) )
472 121 471 mpbird ( 𝜑𝐾 ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) )
473 469 470 elmapd ( 𝜑 → ( 𝐽 ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ↔ 𝐽 : ℕ ⟶ ( ℝ ↑m 𝑌 ) ) )
474 103 473 mpbird ( 𝜑𝐽 ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) )
475 97 87 elmapd ( 𝜑 → ( ( 𝐵𝑌 ) ∈ ( ℝ ↑m 𝑌 ) ↔ ( 𝐵𝑌 ) : 𝑌 ⟶ ℝ ) )
476 213 475 mpbird ( 𝜑 → ( 𝐵𝑌 ) ∈ ( ℝ ↑m 𝑌 ) )
477 97 87 elmapd ( 𝜑 → ( ( 𝐴𝑌 ) ∈ ( ℝ ↑m 𝑌 ) ↔ ( 𝐴𝑌 ) : 𝑌 ⟶ ℝ ) )
478 212 477 mpbird ( 𝜑 → ( 𝐴𝑌 ) ∈ ( ℝ ↑m 𝑌 ) )
479 fveq1 ( 𝑒 = ( 𝐴𝑌 ) → ( 𝑒𝑘 ) = ( ( 𝐴𝑌 ) ‘ 𝑘 ) )
480 479 adantr ( ( 𝑒 = ( 𝐴𝑌 ) ∧ 𝑘𝑌 ) → ( 𝑒𝑘 ) = ( ( 𝐴𝑌 ) ‘ 𝑘 ) )
481 259 adantl ( ( 𝑒 = ( 𝐴𝑌 ) ∧ 𝑘𝑌 ) → ( ( 𝐴𝑌 ) ‘ 𝑘 ) = ( 𝐴𝑘 ) )
482 480 481 eqtrd ( ( 𝑒 = ( 𝐴𝑌 ) ∧ 𝑘𝑌 ) → ( 𝑒𝑘 ) = ( 𝐴𝑘 ) )
483 482 oveq1d ( ( 𝑒 = ( 𝐴𝑌 ) ∧ 𝑘𝑌 ) → ( ( 𝑒𝑘 ) [,) ( 𝑓𝑘 ) ) = ( ( 𝐴𝑘 ) [,) ( 𝑓𝑘 ) ) )
484 483 ixpeq2dva ( 𝑒 = ( 𝐴𝑌 ) → X 𝑘𝑌 ( ( 𝑒𝑘 ) [,) ( 𝑓𝑘 ) ) = X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝑓𝑘 ) ) )
485 484 sseq1d ( 𝑒 = ( 𝐴𝑌 ) → ( X 𝑘𝑌 ( ( 𝑒𝑘 ) [,) ( 𝑓𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) ↔ X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝑓𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) ) )
486 oveq1 ( 𝑒 = ( 𝐴𝑌 ) → ( 𝑒 ( 𝐿𝑌 ) 𝑓 ) = ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) 𝑓 ) )
487 486 breq1d ( 𝑒 = ( 𝐴𝑌 ) → ( ( 𝑒 ( 𝐿𝑌 ) 𝑓 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ↔ ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) 𝑓 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) )
488 485 487 imbi12d ( 𝑒 = ( 𝐴𝑌 ) → ( ( X 𝑘𝑌 ( ( 𝑒𝑘 ) [,) ( 𝑓𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( 𝑒 ( 𝐿𝑌 ) 𝑓 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) ↔ ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝑓𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) 𝑓 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) ) )
489 488 ralbidv ( 𝑒 = ( 𝐴𝑌 ) → ( ∀ ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ( X 𝑘𝑌 ( ( 𝑒𝑘 ) [,) ( 𝑓𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( 𝑒 ( 𝐿𝑌 ) 𝑓 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) ↔ ∀ ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝑓𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) 𝑓 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) ) )
490 489 ralbidv ( 𝑒 = ( 𝐴𝑌 ) → ( ∀ 𝑔 ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ∀ ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ( X 𝑘𝑌 ( ( 𝑒𝑘 ) [,) ( 𝑓𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( 𝑒 ( 𝐿𝑌 ) 𝑓 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) ↔ ∀ 𝑔 ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ∀ ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝑓𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) 𝑓 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) ) )
491 490 ralbidv ( 𝑒 = ( 𝐴𝑌 ) → ( ∀ 𝑓 ∈ ( ℝ ↑m 𝑌 ) ∀ 𝑔 ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ∀ ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ( X 𝑘𝑌 ( ( 𝑒𝑘 ) [,) ( 𝑓𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( 𝑒 ( 𝐿𝑌 ) 𝑓 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) ↔ ∀ 𝑓 ∈ ( ℝ ↑m 𝑌 ) ∀ 𝑔 ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ∀ ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝑓𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) 𝑓 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) ) )
492 491 rspcva ( ( ( 𝐴𝑌 ) ∈ ( ℝ ↑m 𝑌 ) ∧ ∀ 𝑒 ∈ ( ℝ ↑m 𝑌 ) ∀ 𝑓 ∈ ( ℝ ↑m 𝑌 ) ∀ 𝑔 ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ∀ ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ( X 𝑘𝑌 ( ( 𝑒𝑘 ) [,) ( 𝑓𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( 𝑒 ( 𝐿𝑌 ) 𝑓 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) ) → ∀ 𝑓 ∈ ( ℝ ↑m 𝑌 ) ∀ 𝑔 ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ∀ ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝑓𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) 𝑓 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) )
493 478 22 492 syl2anc ( 𝜑 → ∀ 𝑓 ∈ ( ℝ ↑m 𝑌 ) ∀ 𝑔 ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ∀ ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝑓𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) 𝑓 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) )
494 fveq1 ( 𝑓 = ( 𝐵𝑌 ) → ( 𝑓𝑘 ) = ( ( 𝐵𝑌 ) ‘ 𝑘 ) )
495 494 adantr ( ( 𝑓 = ( 𝐵𝑌 ) ∧ 𝑘𝑌 ) → ( 𝑓𝑘 ) = ( ( 𝐵𝑌 ) ‘ 𝑘 ) )
496 260 adantl ( ( 𝑓 = ( 𝐵𝑌 ) ∧ 𝑘𝑌 ) → ( ( 𝐵𝑌 ) ‘ 𝑘 ) = ( 𝐵𝑘 ) )
497 495 496 eqtrd ( ( 𝑓 = ( 𝐵𝑌 ) ∧ 𝑘𝑌 ) → ( 𝑓𝑘 ) = ( 𝐵𝑘 ) )
498 497 oveq2d ( ( 𝑓 = ( 𝐵𝑌 ) ∧ 𝑘𝑌 ) → ( ( 𝐴𝑘 ) [,) ( 𝑓𝑘 ) ) = ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) )
499 498 ixpeq2dva ( 𝑓 = ( 𝐵𝑌 ) → X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝑓𝑘 ) ) = X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) )
500 499 sseq1d ( 𝑓 = ( 𝐵𝑌 ) → ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝑓𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) ↔ X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) ) )
501 oveq2 ( 𝑓 = ( 𝐵𝑌 ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) 𝑓 ) = ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) )
502 501 breq1d ( 𝑓 = ( 𝐵𝑌 ) → ( ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) 𝑓 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ↔ ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) )
503 500 502 imbi12d ( 𝑓 = ( 𝐵𝑌 ) → ( ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝑓𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) 𝑓 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) ↔ ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) ) )
504 503 ralbidv ( 𝑓 = ( 𝐵𝑌 ) → ( ∀ ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝑓𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) 𝑓 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) ↔ ∀ ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) ) )
505 504 ralbidv ( 𝑓 = ( 𝐵𝑌 ) → ( ∀ 𝑔 ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ∀ ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝑓𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) 𝑓 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) ↔ ∀ 𝑔 ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ∀ ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) ) )
506 505 rspcva ( ( ( 𝐵𝑌 ) ∈ ( ℝ ↑m 𝑌 ) ∧ ∀ 𝑓 ∈ ( ℝ ↑m 𝑌 ) ∀ 𝑔 ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ∀ ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝑓𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) 𝑓 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) ) → ∀ 𝑔 ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ∀ ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) )
507 476 493 506 syl2anc ( 𝜑 → ∀ 𝑔 ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ∀ ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) )
508 fveq1 ( 𝑔 = 𝐽 → ( 𝑔𝑗 ) = ( 𝐽𝑗 ) )
509 508 fveq1d ( 𝑔 = 𝐽 → ( ( 𝑔𝑗 ) ‘ 𝑘 ) = ( ( 𝐽𝑗 ) ‘ 𝑘 ) )
510 509 oveq1d ( 𝑔 = 𝐽 → ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) = ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) )
511 510 ixpeq2dv ( 𝑔 = 𝐽X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) = X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) )
512 511 iuneq2d ( 𝑔 = 𝐽 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) = 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) )
513 512 sseq2d ( 𝑔 = 𝐽 → ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) ↔ X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) ) )
514 508 oveq1d ( 𝑔 = 𝐽 → ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) = ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) )
515 514 mpteq2dv ( 𝑔 = 𝐽 → ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) = ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) )
516 515 fveq2d ( 𝑔 = 𝐽 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) )
517 516 breq2d ( 𝑔 = 𝐽 → ( ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ↔ ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) )
518 513 517 imbi12d ( 𝑔 = 𝐽 → ( ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) ↔ ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) ) )
519 518 ralbidv ( 𝑔 = 𝐽 → ( ∀ ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) ↔ ∀ ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) ) )
520 519 rspcva ( ( 𝐽 ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ∧ ∀ 𝑔 ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ∀ ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) ) → ∀ ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) )
521 474 507 520 syl2anc ( 𝜑 → ∀ ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) )
522 fveq1 ( = 𝐾 → ( 𝑗 ) = ( 𝐾𝑗 ) )
523 522 fveq1d ( = 𝐾 → ( ( 𝑗 ) ‘ 𝑘 ) = ( ( 𝐾𝑗 ) ‘ 𝑘 ) )
524 523 oveq2d ( = 𝐾 → ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) = ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) )
525 524 ixpeq2dv ( = 𝐾X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) = X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) )
526 525 iuneq2d ( = 𝐾 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) = 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) )
527 526 sseq2d ( = 𝐾 → ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) ↔ X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) ) )
528 522 oveq2d ( = 𝐾 → ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) = ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) )
529 528 mpteq2dv ( = 𝐾 → ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) = ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) ) )
530 529 fveq2d ( = 𝐾 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) ) ) )
531 530 breq2d ( = 𝐾 → ( ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ↔ ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) ) ) ) )
532 527 531 imbi12d ( = 𝐾 → ( ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) ↔ ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) ) ) ) ) )
533 532 rspcva ( ( 𝐾 ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ∧ ∀ ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) ) → ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) ) ) ) )
534 472 521 533 syl2anc ( 𝜑 → ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) ) ) ) )
535 468 534 mpd ( 𝜑 → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) ) ) )
536 idd ( 𝜑 → ( ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) ) ) ) )
537 535 536 mpd ( 𝜑 → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) ) ) )
538 537 adantr ( ( 𝜑𝑌 ≠ ∅ ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) ) ) )
539 62 adantl ( ( ( 𝜑𝑌 ≠ ∅ ) ∧ 𝑗 ∈ ℕ ) → ( 𝑃𝑗 ) = ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) )
540 539 mpteq2dva ( ( 𝜑𝑌 ≠ ∅ ) → ( 𝑗 ∈ ℕ ↦ ( 𝑃𝑗 ) ) = ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) ) )
541 540 fveq2d ( ( 𝜑𝑌 ≠ ∅ ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝑃𝑗 ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) ) ) )
542 258 541 breq12d ( ( 𝜑𝑌 ≠ ∅ ) → ( 𝐺 ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝑃𝑗 ) ) ) ↔ ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) ) ) ) )
543 538 542 mpbird ( ( 𝜑𝑌 ≠ ∅ ) → 𝐺 ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝑃𝑗 ) ) ) )
544 543 adantr ( ( ( 𝜑𝑌 ≠ ∅ ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝑃𝑗 ) ) ) ∈ ℝ ) → 𝐺 ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝑃𝑗 ) ) ) )
545 247 249 250 289 544 ltletrd ( ( ( 𝜑𝑌 ≠ ∅ ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝑃𝑗 ) ) ) ∈ ℝ ) → ( 𝐺 / ( 1 + 𝐸 ) ) < ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝑃𝑗 ) ) ) )
546 235 246 545 syl2anc ( ( ( 𝜑𝑌 ≠ ∅ ) ∧ ¬ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝑃𝑗 ) ) ) = +∞ ) → ( 𝐺 / ( 1 + 𝐸 ) ) < ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝑃𝑗 ) ) ) )
547 234 546 pm2.61dan ( ( 𝜑𝑌 ≠ ∅ ) → ( 𝐺 / ( 1 + 𝐸 ) ) < ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝑃𝑗 ) ) ) )
548 207 208 209 210 227 547 sge0uzfsumgt ( ( 𝜑𝑌 ≠ ∅ ) → ∃ 𝑚 ∈ ℕ ( 𝐺 / ( 1 + 𝐸 ) ) < Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) )
549 226 adantr ( ( 𝜑 ∧ ( 𝐺 / ( 1 + 𝐸 ) ) < Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) → ( 𝐺 / ( 1 + 𝐸 ) ) ∈ ℝ )
550 fzfid ( 𝜑 → ( 1 ... 𝑚 ) ∈ Fin )
551 simpl ( ( 𝜑𝑗 ∈ ( 1 ... 𝑚 ) ) → 𝜑 )
552 elfznn ( 𝑗 ∈ ( 1 ... 𝑚 ) → 𝑗 ∈ ℕ )
553 552 adantl ( ( 𝜑𝑗 ∈ ( 1 ... 𝑚 ) ) → 𝑗 ∈ ℕ )
554 50 126 sseldi ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝑃𝑗 ) ∈ ℝ )
555 551 553 554 syl2anc ( ( 𝜑𝑗 ∈ ( 1 ... 𝑚 ) ) → ( 𝑃𝑗 ) ∈ ℝ )
556 550 555 fsumrecl ( 𝜑 → Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ∈ ℝ )
557 556 adantr ( ( 𝜑 ∧ ( 𝐺 / ( 1 + 𝐸 ) ) < Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) → Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ∈ ℝ )
558 simpr ( ( 𝜑 ∧ ( 𝐺 / ( 1 + 𝐸 ) ) < Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) → ( 𝐺 / ( 1 + 𝐸 ) ) < Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) )
559 549 557 558 ltled ( ( 𝜑 ∧ ( 𝐺 / ( 1 + 𝐸 ) ) < Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) → ( 𝐺 / ( 1 + 𝐸 ) ) ≤ Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) )
560 216 adantr ( ( 𝜑 ∧ ( 𝐺 / ( 1 + 𝐸 ) ) < Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) → 𝐺 ∈ ℝ )
561 222 adantr ( ( 𝜑 ∧ ( 𝐺 / ( 1 + 𝐸 ) ) < Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) → ( 1 + 𝐸 ) ∈ ℝ+ )
562 560 557 561 ledivmuld ( ( 𝜑 ∧ ( 𝐺 / ( 1 + 𝐸 ) ) < Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) → ( ( 𝐺 / ( 1 + 𝐸 ) ) ≤ Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ↔ 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) ) )
563 559 562 mpbid ( ( 𝜑 ∧ ( 𝐺 / ( 1 + 𝐸 ) ) < Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) → 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) )
564 563 ex ( 𝜑 → ( ( 𝐺 / ( 1 + 𝐸 ) ) < Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) → 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) ) )
565 564 adantr ( ( 𝜑𝑚 ∈ ℕ ) → ( ( 𝐺 / ( 1 + 𝐸 ) ) < Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) → 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) ) )
566 565 adantlr ( ( ( 𝜑𝑌 ≠ ∅ ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝐺 / ( 1 + 𝐸 ) ) < Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) → 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) ) )
567 566 reximdva ( ( 𝜑𝑌 ≠ ∅ ) → ( ∃ 𝑚 ∈ ℕ ( 𝐺 / ( 1 + 𝐸 ) ) < Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) → ∃ 𝑚 ∈ ℕ 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) ) )
568 548 567 mpd ( ( 𝜑𝑌 ≠ ∅ ) → ∃ 𝑚 ∈ ℕ 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) )
569 204 206 568 syl2anc ( ( 𝜑 ∧ ¬ 𝑌 = ∅ ) → ∃ 𝑚 ∈ ℕ 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) )
570 203 569 pm2.61dan ( 𝜑 → ∃ 𝑚 ∈ ℕ 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) )
571 2 3ad2ant1 ( ( 𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) ) → 𝑋 ∈ Fin )
572 3 3ad2ant1 ( ( 𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) ) → 𝑌𝑋 )
573 4 3ad2ant1 ( ( 𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) ) → 𝑍 ∈ ( 𝑋𝑌 ) )
574 6 3ad2ant1 ( ( 𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) ) → 𝐴 : 𝑊 ⟶ ℝ )
575 7 3ad2ant1 ( ( 𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) ) → 𝐵 : 𝑊 ⟶ ℝ )
576 10 3ad2ant1 ( ( 𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) ) → 𝐶 : ℕ ⟶ ( ℝ ↑m 𝑊 ) )
577 eqid ( 𝑦𝑌 ↦ 0 ) = ( 𝑦𝑌 ↦ 0 )
578 eqid ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) = ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) )
579 12 3ad2ant1 ( ( 𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) ) → 𝐷 : ℕ ⟶ ( ℝ ↑m 𝑊 ) )
580 eqid ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) = ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) )
581 fveq2 ( 𝑖 = 𝑗 → ( 𝐶𝑖 ) = ( 𝐶𝑗 ) )
582 fveq2 ( 𝑖 = 𝑗 → ( 𝐷𝑖 ) = ( 𝐷𝑗 ) )
583 581 582 oveq12d ( 𝑖 = 𝑗 → ( ( 𝐶𝑖 ) ( 𝐿𝑊 ) ( 𝐷𝑖 ) ) = ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( 𝐷𝑗 ) ) )
584 583 cbvmptv ( 𝑖 ∈ ℕ ↦ ( ( 𝐶𝑖 ) ( 𝐿𝑊 ) ( 𝐷𝑖 ) ) ) = ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( 𝐷𝑗 ) ) )
585 584 fveq2i ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( ( 𝐶𝑖 ) ( 𝐿𝑊 ) ( 𝐷𝑖 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( 𝐷𝑗 ) ) ) )
586 585 14 eqeltrid ( 𝜑 → ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( ( 𝐶𝑖 ) ( 𝐿𝑊 ) ( 𝐷𝑖 ) ) ) ) ∈ ℝ )
587 586 3ad2ant1 ( ( 𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) ) → ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( ( 𝐶𝑖 ) ( 𝐿𝑊 ) ( 𝐷𝑖 ) ) ) ) ∈ ℝ )
588 eleq1w ( 𝑗 = 𝑖 → ( 𝑗𝑌𝑖𝑌 ) )
589 fveq2 ( 𝑗 = 𝑖 → ( 𝑐𝑗 ) = ( 𝑐𝑖 ) )
590 589 breq1d ( 𝑗 = 𝑖 → ( ( 𝑐𝑗 ) ≤ 𝑥 ↔ ( 𝑐𝑖 ) ≤ 𝑥 ) )
591 590 589 ifbieq1d ( 𝑗 = 𝑖 → if ( ( 𝑐𝑗 ) ≤ 𝑥 , ( 𝑐𝑗 ) , 𝑥 ) = if ( ( 𝑐𝑖 ) ≤ 𝑥 , ( 𝑐𝑖 ) , 𝑥 ) )
592 588 589 591 ifbieq12d ( 𝑗 = 𝑖 → if ( 𝑗𝑌 , ( 𝑐𝑗 ) , if ( ( 𝑐𝑗 ) ≤ 𝑥 , ( 𝑐𝑗 ) , 𝑥 ) ) = if ( 𝑖𝑌 , ( 𝑐𝑖 ) , if ( ( 𝑐𝑖 ) ≤ 𝑥 , ( 𝑐𝑖 ) , 𝑥 ) ) )
593 592 cbvmptv ( 𝑗𝑊 ↦ if ( 𝑗𝑌 , ( 𝑐𝑗 ) , if ( ( 𝑐𝑗 ) ≤ 𝑥 , ( 𝑐𝑗 ) , 𝑥 ) ) ) = ( 𝑖𝑊 ↦ if ( 𝑖𝑌 , ( 𝑐𝑖 ) , if ( ( 𝑐𝑖 ) ≤ 𝑥 , ( 𝑐𝑖 ) , 𝑥 ) ) )
594 593 mpteq2i ( 𝑐 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑗𝑊 ↦ if ( 𝑗𝑌 , ( 𝑐𝑗 ) , if ( ( 𝑐𝑗 ) ≤ 𝑥 , ( 𝑐𝑗 ) , 𝑥 ) ) ) ) = ( 𝑐 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖𝑊 ↦ if ( 𝑖𝑌 , ( 𝑐𝑖 ) , if ( ( 𝑐𝑖 ) ≤ 𝑥 , ( 𝑐𝑖 ) , 𝑥 ) ) ) )
595 594 mpteq2i ( 𝑥 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑗𝑊 ↦ if ( 𝑗𝑌 , ( 𝑐𝑗 ) , if ( ( 𝑐𝑗 ) ≤ 𝑥 , ( 𝑐𝑗 ) , 𝑥 ) ) ) ) ) = ( 𝑥 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖𝑊 ↦ if ( 𝑖𝑌 , ( 𝑐𝑖 ) , if ( ( 𝑐𝑖 ) ≤ 𝑥 , ( 𝑐𝑖 ) , 𝑥 ) ) ) ) )
596 15 595 eqtri 𝐻 = ( 𝑥 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖𝑊 ↦ if ( 𝑖𝑌 , ( 𝑐𝑖 ) , if ( ( 𝑐𝑖 ) ≤ 𝑥 , ( 𝑐𝑖 ) , 𝑥 ) ) ) ) )
597 17 3ad2ant1 ( ( 𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) ) → 𝐸 ∈ ℝ+ )
598 fveq2 ( 𝑗 = 𝑖 → ( 𝐶𝑗 ) = ( 𝐶𝑖 ) )
599 fveq2 ( 𝑗 = 𝑖 → ( 𝐷𝑗 ) = ( 𝐷𝑖 ) )
600 599 fveq2d ( 𝑗 = 𝑖 → ( ( 𝐻𝑧 ) ‘ ( 𝐷𝑗 ) ) = ( ( 𝐻𝑧 ) ‘ ( 𝐷𝑖 ) ) )
601 598 600 oveq12d ( 𝑗 = 𝑖 → ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑧 ) ‘ ( 𝐷𝑗 ) ) ) = ( ( 𝐶𝑖 ) ( 𝐿𝑊 ) ( ( 𝐻𝑧 ) ‘ ( 𝐷𝑖 ) ) ) )
602 601 cbvmptv ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑧 ) ‘ ( 𝐷𝑗 ) ) ) ) = ( 𝑖 ∈ ℕ ↦ ( ( 𝐶𝑖 ) ( 𝐿𝑊 ) ( ( 𝐻𝑧 ) ‘ ( 𝐷𝑖 ) ) ) )
603 602 fveq2i ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑧 ) ‘ ( 𝐷𝑗 ) ) ) ) ) = ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( ( 𝐶𝑖 ) ( 𝐿𝑊 ) ( ( 𝐻𝑧 ) ‘ ( 𝐷𝑖 ) ) ) ) )
604 603 oveq2i ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑧 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) = ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( ( 𝐶𝑖 ) ( 𝐿𝑊 ) ( ( 𝐻𝑧 ) ‘ ( 𝐷𝑖 ) ) ) ) ) )
605 604 breq2i ( ( 𝐺 · ( 𝑧 − ( 𝐴𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑧 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) ↔ ( 𝐺 · ( 𝑧 − ( 𝐴𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( ( 𝐶𝑖 ) ( 𝐿𝑊 ) ( ( 𝐻𝑧 ) ‘ ( 𝐷𝑖 ) ) ) ) ) ) )
606 605 rabbii { 𝑧 ∈ ( ( 𝐴𝑍 ) [,] ( 𝐵𝑍 ) ) ∣ ( 𝐺 · ( 𝑧 − ( 𝐴𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑧 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) } = { 𝑧 ∈ ( ( 𝐴𝑍 ) [,] ( 𝐵𝑍 ) ) ∣ ( 𝐺 · ( 𝑧 − ( 𝐴𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( ( 𝐶𝑖 ) ( 𝐿𝑊 ) ( ( 𝐻𝑧 ) ‘ ( 𝐷𝑖 ) ) ) ) ) ) }
607 18 606 eqtri 𝑈 = { 𝑧 ∈ ( ( 𝐴𝑍 ) [,] ( 𝐵𝑍 ) ) ∣ ( 𝐺 · ( 𝑧 − ( 𝐴𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( ( 𝐶𝑖 ) ( 𝐿𝑊 ) ( ( 𝐻𝑧 ) ‘ ( 𝐷𝑖 ) ) ) ) ) ) }
608 19 3ad2ant1 ( ( 𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) ) → 𝑆𝑈 )
609 20 3ad2ant1 ( ( 𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) ) → 𝑆 < ( 𝐵𝑍 ) )
610 eqid ( 𝑖 ∈ ℕ ↦ ( ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ( 𝐿𝑌 ) ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ) ) = ( 𝑖 ∈ ℕ ↦ ( ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ( 𝐿𝑌 ) ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ) )
611 simp2 ( ( 𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) ) → 𝑚 ∈ ℕ )
612 id ( 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) → 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) )
613 fveq2 ( 𝑗 = 𝑖 → ( 𝑃𝑗 ) = ( 𝑃𝑖 ) )
614 613 cbvsumv Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) = Σ 𝑖 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑖 )
615 614 oveq2i ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) = ( ( 1 + 𝐸 ) · Σ 𝑖 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑖 ) )
616 615 a1i ( 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) → ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) = ( ( 1 + 𝐸 ) · Σ 𝑖 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑖 ) ) )
617 612 616 breqtrd ( 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) → 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑖 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑖 ) ) )
618 617 3ad2ant3 ( ( 𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) ) → 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑖 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑖 ) ) )
619 simpl ( ( 𝜑𝑖 ∈ ( 1 ... 𝑚 ) ) → 𝜑 )
620 elfznn ( 𝑖 ∈ ( 1 ... 𝑚 ) → 𝑖 ∈ ℕ )
621 620 adantl ( ( 𝜑𝑖 ∈ ( 1 ... 𝑚 ) ) → 𝑖 ∈ ℕ )
622 eleq1w ( 𝑗 = 𝑖 → ( 𝑗 ∈ ℕ ↔ 𝑖 ∈ ℕ ) )
623 fveq2 ( 𝑗 = 𝑖 → ( 𝐽𝑗 ) = ( 𝐽𝑖 ) )
624 fveq2 ( 𝑗 = 𝑖 → ( 𝐾𝑗 ) = ( 𝐾𝑖 ) )
625 623 624 oveq12d ( 𝑗 = 𝑖 → ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) = ( ( 𝐽𝑖 ) ( 𝐿𝑌 ) ( 𝐾𝑖 ) ) )
626 613 625 eqeq12d ( 𝑗 = 𝑖 → ( ( 𝑃𝑗 ) = ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) ↔ ( 𝑃𝑖 ) = ( ( 𝐽𝑖 ) ( 𝐿𝑌 ) ( 𝐾𝑖 ) ) ) )
627 622 626 imbi12d ( 𝑗 = 𝑖 → ( ( 𝑗 ∈ ℕ → ( 𝑃𝑗 ) = ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) ) ↔ ( 𝑖 ∈ ℕ → ( 𝑃𝑖 ) = ( ( 𝐽𝑖 ) ( 𝐿𝑌 ) ( 𝐾𝑖 ) ) ) ) )
628 627 62 chvarvv ( 𝑖 ∈ ℕ → ( 𝑃𝑖 ) = ( ( 𝐽𝑖 ) ( 𝐿𝑌 ) ( 𝐾𝑖 ) ) )
629 628 adantl ( ( 𝜑𝑖 ∈ ℕ ) → ( 𝑃𝑖 ) = ( ( 𝐽𝑖 ) ( 𝐿𝑌 ) ( 𝐾𝑖 ) ) )
630 622 anbi2d ( 𝑗 = 𝑖 → ( ( 𝜑𝑗 ∈ ℕ ) ↔ ( 𝜑𝑖 ∈ ℕ ) ) )
631 598 fveq1d ( 𝑗 = 𝑖 → ( ( 𝐶𝑗 ) ‘ 𝑍 ) = ( ( 𝐶𝑖 ) ‘ 𝑍 ) )
632 599 fveq1d ( 𝑗 = 𝑖 → ( ( 𝐷𝑗 ) ‘ 𝑍 ) = ( ( 𝐷𝑖 ) ‘ 𝑍 ) )
633 631 632 oveq12d ( 𝑗 = 𝑖 → ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) = ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) )
634 633 eleq2d ( 𝑗 = 𝑖 → ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ↔ 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) ) )
635 598 reseq1d ( 𝑗 = 𝑖 → ( ( 𝐶𝑗 ) ↾ 𝑌 ) = ( ( 𝐶𝑖 ) ↾ 𝑌 ) )
636 634 635 ifbieq1d ( 𝑗 = 𝑖 → if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑗 ) ↾ 𝑌 ) , 𝐹 ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , 𝐹 ) )
637 623 636 eqeq12d ( 𝑗 = 𝑖 → ( ( 𝐽𝑗 ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑗 ) ↾ 𝑌 ) , 𝐹 ) ↔ ( 𝐽𝑖 ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , 𝐹 ) ) )
638 630 637 imbi12d ( 𝑗 = 𝑖 → ( ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝐽𝑗 ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑗 ) ↾ 𝑌 ) , 𝐹 ) ) ↔ ( ( 𝜑𝑖 ∈ ℕ ) → ( 𝐽𝑖 ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , 𝐹 ) ) ) )
639 638 161 chvarvv ( ( 𝜑𝑖 ∈ ℕ ) → ( 𝐽𝑖 ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , 𝐹 ) )
640 599 reseq1d ( 𝑗 = 𝑖 → ( ( 𝐷𝑗 ) ↾ 𝑌 ) = ( ( 𝐷𝑖 ) ↾ 𝑌 ) )
641 634 640 ifbieq1d ( 𝑗 = 𝑖 → if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑗 ) ↾ 𝑌 ) , 𝐹 ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , 𝐹 ) )
642 624 641 eqeq12d ( 𝑗 = 𝑖 → ( ( 𝐾𝑗 ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑗 ) ↾ 𝑌 ) , 𝐹 ) ↔ ( 𝐾𝑖 ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , 𝐹 ) ) )
643 630 642 imbi12d ( 𝑗 = 𝑖 → ( ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝐾𝑗 ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑗 ) ↾ 𝑌 ) , 𝐹 ) ) ↔ ( ( 𝜑𝑖 ∈ ℕ ) → ( 𝐾𝑖 ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , 𝐹 ) ) ) )
644 643 443 chvarvv ( ( 𝜑𝑖 ∈ ℕ ) → ( 𝐾𝑖 ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , 𝐹 ) )
645 639 644 oveq12d ( ( 𝜑𝑖 ∈ ℕ ) → ( ( 𝐽𝑖 ) ( 𝐿𝑌 ) ( 𝐾𝑖 ) ) = ( if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , 𝐹 ) ( 𝐿𝑌 ) if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , 𝐹 ) ) )
646 629 645 eqtrd ( ( 𝜑𝑖 ∈ ℕ ) → ( 𝑃𝑖 ) = ( if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , 𝐹 ) ( 𝐿𝑌 ) if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , 𝐹 ) ) )
647 simpr ( ( 𝜑𝑖 ∈ ℕ ) → 𝑖 ∈ ℕ )
648 ovexd ( ( 𝜑𝑖 ∈ ℕ ) → ( ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ( 𝐿𝑌 ) ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ) ∈ V )
649 610 fvmpt2 ( ( 𝑖 ∈ ℕ ∧ ( ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ( 𝐿𝑌 ) ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ) ∈ V ) → ( ( 𝑖 ∈ ℕ ↦ ( ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ( 𝐿𝑌 ) ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ) ) ‘ 𝑖 ) = ( ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ( 𝐿𝑌 ) ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ) )
650 647 648 649 syl2anc ( ( 𝜑𝑖 ∈ ℕ ) → ( ( 𝑖 ∈ ℕ ↦ ( ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ( 𝐿𝑌 ) ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ) ) ‘ 𝑖 ) = ( ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ( 𝐿𝑌 ) ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ) )
651 fvex ( 𝐶𝑖 ) ∈ V
652 651 resex ( ( 𝐶𝑖 ) ↾ 𝑌 ) ∈ V
653 652 a1i ( 𝜑 → ( ( 𝐶𝑖 ) ↾ 𝑌 ) ∈ V )
654 9 155 eqeltrrid ( 𝜑 → ( 𝑦𝑌 ↦ 0 ) ∈ V )
655 653 654 ifcld ( 𝜑 → if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ∈ V )
656 655 adantr ( ( 𝜑𝑖 ∈ ℕ ) → if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ∈ V )
657 578 fvmpt2 ( ( 𝑖 ∈ ℕ ∧ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ∈ V ) → ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) )
658 647 656 657 syl2anc ( ( 𝜑𝑖 ∈ ℕ ) → ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) )
659 9 eqcomi ( 𝑦𝑌 ↦ 0 ) = 𝐹
660 ifeq2 ( ( 𝑦𝑌 ↦ 0 ) = 𝐹 → if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , 𝐹 ) )
661 659 660 ax-mp if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , 𝐹 )
662 661 a1i ( ( 𝜑𝑖 ∈ ℕ ) → if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , 𝐹 ) )
663 658 662 eqtrd ( ( 𝜑𝑖 ∈ ℕ ) → ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , 𝐹 ) )
664 fvex ( 𝐷𝑖 ) ∈ V
665 664 resex ( ( 𝐷𝑖 ) ↾ 𝑌 ) ∈ V
666 665 a1i ( 𝜑 → ( ( 𝐷𝑖 ) ↾ 𝑌 ) ∈ V )
667 666 654 ifcld ( 𝜑 → if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ∈ V )
668 667 adantr ( ( 𝜑𝑖 ∈ ℕ ) → if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ∈ V )
669 580 fvmpt2 ( ( 𝑖 ∈ ℕ ∧ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ∈ V ) → ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) )
670 647 668 669 syl2anc ( ( 𝜑𝑖 ∈ ℕ ) → ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) )
671 biid ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) ↔ 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) )
672 671 659 ifbieq2i if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , 𝐹 )
673 672 a1i ( ( 𝜑𝑖 ∈ ℕ ) → if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , 𝐹 ) )
674 670 673 eqtrd ( ( 𝜑𝑖 ∈ ℕ ) → ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , 𝐹 ) )
675 663 674 oveq12d ( ( 𝜑𝑖 ∈ ℕ ) → ( ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ( 𝐿𝑌 ) ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ) = ( if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , 𝐹 ) ( 𝐿𝑌 ) if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , 𝐹 ) ) )
676 650 675 eqtrd ( ( 𝜑𝑖 ∈ ℕ ) → ( ( 𝑖 ∈ ℕ ↦ ( ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ( 𝐿𝑌 ) ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ) ) ‘ 𝑖 ) = ( if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , 𝐹 ) ( 𝐿𝑌 ) if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , 𝐹 ) ) )
677 646 676 eqtr4d ( ( 𝜑𝑖 ∈ ℕ ) → ( 𝑃𝑖 ) = ( ( 𝑖 ∈ ℕ ↦ ( ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ( 𝐿𝑌 ) ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ) ) ‘ 𝑖 ) )
678 619 621 677 syl2anc ( ( 𝜑𝑖 ∈ ( 1 ... 𝑚 ) ) → ( 𝑃𝑖 ) = ( ( 𝑖 ∈ ℕ ↦ ( ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ( 𝐿𝑌 ) ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ) ) ‘ 𝑖 ) )
679 678 3ad2antl1 ( ( ( 𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑚 ) ) → ( 𝑃𝑖 ) = ( ( 𝑖 ∈ ℕ ↦ ( ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ( 𝐿𝑌 ) ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ) ) ‘ 𝑖 ) )
680 679 sumeq2dv ( ( 𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) ) → Σ 𝑖 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑖 ) = Σ 𝑖 ∈ ( 1 ... 𝑚 ) ( ( 𝑖 ∈ ℕ ↦ ( ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ( 𝐿𝑌 ) ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ) ) ‘ 𝑖 ) )
681 680 oveq2d ( ( 𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) ) → ( ( 1 + 𝐸 ) · Σ 𝑖 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑖 ) ) = ( ( 1 + 𝐸 ) · Σ 𝑖 ∈ ( 1 ... 𝑚 ) ( ( 𝑖 ∈ ℕ ↦ ( ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ( 𝐿𝑌 ) ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ) ) ‘ 𝑖 ) ) )
682 618 681 breqtrd ( ( 𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) ) → 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑖 ∈ ( 1 ... 𝑚 ) ( ( 𝑖 ∈ ℕ ↦ ( ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ( 𝐿𝑌 ) ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ) ) ‘ 𝑖 ) ) )
683 fveq2 ( 𝑗 = → ( 𝐷𝑗 ) = ( 𝐷 ) )
684 683 fveq1d ( 𝑗 = → ( ( 𝐷𝑗 ) ‘ 𝑍 ) = ( ( 𝐷 ) ‘ 𝑍 ) )
685 684 cbvmptv ( 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝑚 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) } ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) = ( ∈ { 𝑖 ∈ ( 1 ... 𝑚 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) } ↦ ( ( 𝐷 ) ‘ 𝑍 ) )
686 685 rneqi ran ( 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝑚 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) } ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) = ran ( ∈ { 𝑖 ∈ ( 1 ... 𝑚 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) } ↦ ( ( 𝐷 ) ‘ 𝑍 ) )
687 fveq2 ( = 𝑖 → ( 𝐶 ) = ( 𝐶𝑖 ) )
688 687 fveq1d ( = 𝑖 → ( ( 𝐶 ) ‘ 𝑍 ) = ( ( 𝐶𝑖 ) ‘ 𝑍 ) )
689 fveq2 ( = 𝑖 → ( 𝐷 ) = ( 𝐷𝑖 ) )
690 689 fveq1d ( = 𝑖 → ( ( 𝐷 ) ‘ 𝑍 ) = ( ( 𝐷𝑖 ) ‘ 𝑍 ) )
691 688 690 oveq12d ( = 𝑖 → ( ( ( 𝐶 ) ‘ 𝑍 ) [,) ( ( 𝐷 ) ‘ 𝑍 ) ) = ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) )
692 691 eleq2d ( = 𝑖 → ( 𝑆 ∈ ( ( ( 𝐶 ) ‘ 𝑍 ) [,) ( ( 𝐷 ) ‘ 𝑍 ) ) ↔ 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) ) )
693 692 cbvrabv { ∈ ( 1 ... 𝑚 ) ∣ 𝑆 ∈ ( ( ( 𝐶 ) ‘ 𝑍 ) [,) ( ( 𝐷 ) ‘ 𝑍 ) ) } = { 𝑖 ∈ ( 1 ... 𝑚 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) }
694 693 mpteq1i ( 𝑗 ∈ { ∈ ( 1 ... 𝑚 ) ∣ 𝑆 ∈ ( ( ( 𝐶 ) ‘ 𝑍 ) [,) ( ( 𝐷 ) ‘ 𝑍 ) ) } ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) = ( 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝑚 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) } ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) )
695 694 rneqi ran ( 𝑗 ∈ { ∈ ( 1 ... 𝑚 ) ∣ 𝑆 ∈ ( ( ( 𝐶 ) ‘ 𝑍 ) [,) ( ( 𝐷 ) ‘ 𝑍 ) ) } ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) = ran ( 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝑚 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) } ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) )
696 695 uneq2i ( { ( 𝐵𝑍 ) } ∪ ran ( 𝑗 ∈ { ∈ ( 1 ... 𝑚 ) ∣ 𝑆 ∈ ( ( ( 𝐶 ) ‘ 𝑍 ) [,) ( ( 𝐷 ) ‘ 𝑍 ) ) } ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) = ( { ( 𝐵𝑍 ) } ∪ ran ( 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝑚 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) } ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) )
697 eqid inf ( ( { ( 𝐵𝑍 ) } ∪ ran ( 𝑗 ∈ { ∈ ( 1 ... 𝑚 ) ∣ 𝑆 ∈ ( ( ( 𝐶 ) ‘ 𝑍 ) [,) ( ( 𝐷 ) ‘ 𝑍 ) ) } ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) , ℝ , < ) = inf ( ( { ( 𝐵𝑍 ) } ∪ ran ( 𝑗 ∈ { ∈ ( 1 ... 𝑚 ) ∣ 𝑆 ∈ ( ( ( 𝐶 ) ‘ 𝑍 ) [,) ( ( 𝐷 ) ‘ 𝑍 ) ) } ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) , ℝ , < )
698 1 571 572 573 5 574 575 576 577 578 579 580 587 596 16 597 607 608 609 610 611 682 686 696 697 hoidmvlelem2 ( ( 𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) ) → ∃ 𝑢𝑈 𝑆 < 𝑢 )
699 698 3exp ( 𝜑 → ( 𝑚 ∈ ℕ → ( 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) → ∃ 𝑢𝑈 𝑆 < 𝑢 ) ) )
700 699 rexlimdv ( 𝜑 → ( ∃ 𝑚 ∈ ℕ 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) → ∃ 𝑢𝑈 𝑆 < 𝑢 ) )
701 570 700 mpd ( 𝜑 → ∃ 𝑢𝑈 𝑆 < 𝑢 )