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 ffvelcdmda ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝐶𝑗 ) ∈ ( ℝ ↑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 ffvelcdmda ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝐽𝑗 ) ∈ ( ℝ ↑m 𝑌 ) )
105 elmapi ( ( 𝐽𝑗 ) ∈ ( ℝ ↑m 𝑌 ) → ( 𝐽𝑗 ) : 𝑌 ⟶ ℝ )
106 104 105 syl ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝐽𝑗 ) : 𝑌 ⟶ ℝ )
107 iftrue ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) → if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑗 ) ↾ 𝑌 ) , 𝐹 ) = ( ( 𝐷𝑗 ) ↾ 𝑌 ) )
108 107 adantl ( ( ( 𝜑𝑗 ∈ ℕ ) ∧ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑗 ) ↾ 𝑌 ) , 𝐹 ) = ( ( 𝐷𝑗 ) ↾ 𝑌 ) )
109 12 ffvelcdmda ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝐷𝑗 ) ∈ ( ℝ ↑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 ffvelcdmda ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝐾𝑗 ) ∈ ( ℝ ↑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 sselid ( 𝜑 → ( 𝑃 ‘ 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 sselid ( 𝜑 → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ∈ ℝ )
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 sselid ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝑃𝑗 ) ∈ ( 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 ffvelcdmd ( ( 𝜑𝑘𝑌 ) → ( 𝐴𝑘 ) ∈ ℝ )
269 7 adantr ( ( 𝜑𝑘𝑌 ) → 𝐵 : 𝑊 ⟶ ℝ )
270 269 267 ffvelcdmd ( ( 𝜑𝑘𝑌 ) → ( 𝐵𝑘 ) ∈ ℝ )
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 ffvelcdmd ( 𝜑 → ( 𝐴𝑍 ) ∈ ℝ )
338 337 rexrd ( 𝜑 → ( 𝐴𝑍 ) ∈ ℝ* )
339 7 336 ffvelcdmd ( 𝜑 → ( 𝐵𝑍 ) ∈ ℝ )
340 339 rexrd ( 𝜑 → ( 𝐵𝑍 ) ∈ ℝ* )
341 iccssxr ( ( 𝐴𝑍 ) [,] ( 𝐵𝑍 ) ) ⊆ ℝ*
342 ssrab2 { 𝑧 ∈ ( ( 𝐴𝑍 ) [,] ( 𝐵𝑍 ) ) ∣ ( 𝐺 · ( 𝑧 − ( 𝐴𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑧 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) } ⊆ ( ( 𝐴𝑍 ) [,] ( 𝐵𝑍 ) )
343 18 342 eqsstri 𝑈 ⊆ ( ( 𝐴𝑍 ) [,] ( 𝐵𝑍 ) )
344 343 19 sselid ( 𝜑𝑆 ∈ ( ( 𝐴𝑍 ) [,] ( 𝐵𝑍 ) ) )
345 341 344 sselid ( 𝜑𝑆 ∈ ℝ* )
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 birani ( ( 𝑘𝑊 ∧ ¬ 𝑘𝑌 ) → 𝑘 ∈ ( 𝑌 ∪ { 𝑍 } ) )
354 simpr ( ( 𝑘𝑊 ∧ ¬ 𝑘𝑌 ) → ¬ 𝑘𝑌 )
355 elunnel1 ( ( 𝑘 ∈ ( 𝑌 ∪ { 𝑍 } ) ∧ ¬ 𝑘𝑌 ) → 𝑘 ∈ { 𝑍 } )
356 353 354 355 syl2anc ( ( 𝑘𝑊 ∧ ¬ 𝑘𝑌 ) → 𝑘 ∈ { 𝑍 } )
357 elsni ( 𝑘 ∈ { 𝑍 } → 𝑘 = 𝑍 )
358 356 357 syl ( ( 𝑘𝑊 ∧ ¬ 𝑘𝑌 ) → 𝑘 = 𝑍 )
359 fveq2 ( 𝑘 = 𝑍 → ( 𝐴𝑘 ) = ( 𝐴𝑍 ) )
360 fveq2 ( 𝑘 = 𝑍 → ( 𝐵𝑘 ) = ( 𝐵𝑍 ) )
361 359 360 oveq12d ( 𝑘 = 𝑍 → ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) = ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) )
362 358 361 syl ( ( 𝑘𝑊 ∧ ¬ 𝑘𝑌 ) → ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) = ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) )
363 362 adantll ( ( ( 𝜑𝑘𝑊 ) ∧ ¬ 𝑘𝑌 ) → ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) = ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) )
364 351 363 eleq12d ( ( ( 𝜑𝑘𝑊 ) ∧ ¬ 𝑘𝑌 ) → ( if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) ∈ ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ↔ 𝑆 ∈ ( ( 𝐴𝑍 ) [,) ( 𝐵𝑍 ) ) ) )
365 349 364 mpbird ( ( ( 𝜑𝑘𝑊 ) ∧ ¬ 𝑘𝑌 ) → if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) ∈ ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) )
366 365 adantllr ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑘𝑊 ) ∧ ¬ 𝑘𝑌 ) → if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) ∈ ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) )
367 330 366 pm2.61dan ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑘𝑊 ) → if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) ∈ ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) )
368 319 367 eqeltrd ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑘𝑊 ) → ( ( 𝑂𝑥 ) ‘ 𝑘 ) ∈ ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) )
369 368 ex ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) → ( 𝑘𝑊 → ( ( 𝑂𝑥 ) ‘ 𝑘 ) ∈ ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) )
370 311 369 ralrimi ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) → ∀ 𝑘𝑊 ( ( 𝑂𝑥 ) ‘ 𝑘 ) ∈ ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) )
371 306 370 jca ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) → ( ( 𝑂𝑥 ) Fn 𝑊 ∧ ∀ 𝑘𝑊 ( ( 𝑂𝑥 ) ‘ 𝑘 ) ∈ ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) )
372 fvex ( 𝑂𝑥 ) ∈ V
373 372 elixp ( ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ↔ ( ( 𝑂𝑥 ) Fn 𝑊 ∧ ∀ 𝑘𝑊 ( ( 𝑂𝑥 ) ‘ 𝑘 ) ∈ ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) )
374 371 373 sylibr ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) → ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) )
375 290 374 sseldd ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) → ( 𝑂𝑥 ) ∈ 𝑗 ∈ ℕ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) )
376 eliun ( ( 𝑂𝑥 ) ∈ 𝑗 ∈ ℕ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ↔ ∃ 𝑗 ∈ ℕ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) )
377 375 376 sylib ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) → ∃ 𝑗 ∈ ℕ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) )
378 ixpfn ( 𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) → 𝑥 Fn 𝑌 )
379 378 adantl ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) → 𝑥 Fn 𝑌 )
380 379 ad2antrr ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) → 𝑥 Fn 𝑌 )
381 nfv 𝑘 𝑗 ∈ ℕ
382 311 381 nfan 𝑘 ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ )
383 nfcv 𝑘 ( 𝑂𝑥 )
384 nfixp1 𝑘 X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) )
385 383 384 nfel 𝑘 ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) )
386 382 385 nfan 𝑘 ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) )
387 312 3adant3 ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ∧ 𝑘𝑌 ) → ( ( 𝑂𝑥 ) ‘ 𝑘 ) = ( ( 𝑘𝑊 ↦ if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) ) ‘ 𝑘 ) )
388 293 adantr ( ( 𝜑𝑘𝑌 ) → if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) ∈ V )
389 267 388 316 syl2anc ( ( 𝜑𝑘𝑌 ) → ( ( 𝑘𝑊 ↦ if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) ) ‘ 𝑘 ) = if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) )
390 389 3adant2 ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ∧ 𝑘𝑌 ) → ( ( 𝑘𝑊 ↦ if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) ) ‘ 𝑘 ) = if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) )
391 320 3ad2ant3 ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ∧ 𝑘𝑌 ) → if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) = ( 𝑥𝑘 ) )
392 387 390 391 3eqtrrd ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ∧ 𝑘𝑌 ) → ( 𝑥𝑘 ) = ( ( 𝑂𝑥 ) ‘ 𝑘 ) )
393 392 ad5ant125 ( ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘𝑌 ) → ( 𝑥𝑘 ) = ( ( 𝑂𝑥 ) ‘ 𝑘 ) )
394 372 elixp ( ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ↔ ( ( 𝑂𝑥 ) Fn 𝑊 ∧ ∀ 𝑘𝑊 ( ( 𝑂𝑥 ) ‘ 𝑘 ) ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) )
395 394 birani ( ( ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ∧ 𝑘𝑌 ) → ( ( 𝑂𝑥 ) Fn 𝑊 ∧ ∀ 𝑘𝑊 ( ( 𝑂𝑥 ) ‘ 𝑘 ) ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) )
396 395 simprd ( ( ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ∧ 𝑘𝑌 ) → ∀ 𝑘𝑊 ( ( 𝑂𝑥 ) ‘ 𝑘 ) ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) )
397 266 adantl ( ( ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ∧ 𝑘𝑌 ) → 𝑘𝑊 )
398 rspa ( ( ∀ 𝑘𝑊 ( ( 𝑂𝑥 ) ‘ 𝑘 ) ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ∧ 𝑘𝑊 ) → ( ( 𝑂𝑥 ) ‘ 𝑘 ) ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) )
399 396 397 398 syl2anc ( ( ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ∧ 𝑘𝑌 ) → ( ( 𝑂𝑥 ) ‘ 𝑘 ) ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) )
400 399 adantll ( ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘𝑌 ) → ( ( 𝑂𝑥 ) ‘ 𝑘 ) ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) )
401 393 400 eqeltrd ( ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘𝑌 ) → ( 𝑥𝑘 ) ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) )
402 51 ad3antrrr ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) → 𝜑 )
403 59 ad2antlr ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) → 𝑗 ∈ ℕ )
404 304 fveq1d ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) → ( ( 𝑂𝑥 ) ‘ 𝑍 ) = ( ( 𝑘𝑊 ↦ if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) ) ‘ 𝑍 ) )
405 eqidd ( 𝜑 → ( 𝑘𝑊 ↦ if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) ) = ( 𝑘𝑊 ↦ if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) ) )
406 eleq1 ( 𝑘 = 𝑍 → ( 𝑘𝑌𝑍𝑌 ) )
407 fveq2 ( 𝑘 = 𝑍 → ( 𝑥𝑘 ) = ( 𝑥𝑍 ) )
408 406 407 ifbieq1d ( 𝑘 = 𝑍 → if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) = if ( 𝑍𝑌 , ( 𝑥𝑍 ) , 𝑆 ) )
409 408 adantl ( ( 𝜑𝑘 = 𝑍 ) → if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) = if ( 𝑍𝑌 , ( 𝑥𝑍 ) , 𝑆 ) )
410 fvexd ( 𝜑 → ( 𝑥𝑍 ) ∈ V )
411 410 292 ifcld ( 𝜑 → if ( 𝑍𝑌 , ( 𝑥𝑍 ) , 𝑆 ) ∈ V )
412 405 409 336 411 fvmptd ( 𝜑 → ( ( 𝑘𝑊 ↦ if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) ) ‘ 𝑍 ) = if ( 𝑍𝑌 , ( 𝑥𝑍 ) , 𝑆 ) )
413 412 adantr ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) → ( ( 𝑘𝑊 ↦ if ( 𝑘𝑌 , ( 𝑥𝑘 ) , 𝑆 ) ) ‘ 𝑍 ) = if ( 𝑍𝑌 , ( 𝑥𝑍 ) , 𝑆 ) )
414 4 eldifbd ( 𝜑 → ¬ 𝑍𝑌 )
415 414 iffalsed ( 𝜑 → if ( 𝑍𝑌 , ( 𝑥𝑍 ) , 𝑆 ) = 𝑆 )
416 415 adantr ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) → if ( 𝑍𝑌 , ( 𝑥𝑍 ) , 𝑆 ) = 𝑆 )
417 404 413 416 3eqtrrd ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) → 𝑆 = ( ( 𝑂𝑥 ) ‘ 𝑍 ) )
418 417 ad2antrr ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) → 𝑆 = ( ( 𝑂𝑥 ) ‘ 𝑍 ) )
419 402 336 syl ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) → 𝑍𝑊 )
420 394 simprbi ( ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) → ∀ 𝑘𝑊 ( ( 𝑂𝑥 ) ‘ 𝑘 ) ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) )
421 420 adantl ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) → ∀ 𝑘𝑊 ( ( 𝑂𝑥 ) ‘ 𝑘 ) ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) )
422 fveq2 ( 𝑘 = 𝑍 → ( ( 𝑂𝑥 ) ‘ 𝑘 ) = ( ( 𝑂𝑥 ) ‘ 𝑍 ) )
423 fveq2 ( 𝑘 = 𝑍 → ( ( 𝐶𝑗 ) ‘ 𝑘 ) = ( ( 𝐶𝑗 ) ‘ 𝑍 ) )
424 fveq2 ( 𝑘 = 𝑍 → ( ( 𝐷𝑗 ) ‘ 𝑘 ) = ( ( 𝐷𝑗 ) ‘ 𝑍 ) )
425 423 424 oveq12d ( 𝑘 = 𝑍 → ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) = ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) )
426 422 425 eleq12d ( 𝑘 = 𝑍 → ( ( ( 𝑂𝑥 ) ‘ 𝑘 ) ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ↔ ( ( 𝑂𝑥 ) ‘ 𝑍 ) ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) )
427 426 rspcva ( ( 𝑍𝑊 ∧ ∀ 𝑘𝑊 ( ( 𝑂𝑥 ) ‘ 𝑘 ) ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) → ( ( 𝑂𝑥 ) ‘ 𝑍 ) ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) )
428 419 421 427 syl2anc ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) → ( ( 𝑂𝑥 ) ‘ 𝑍 ) ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) )
429 418 428 eqeltrd ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) → 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) )
430 161 3adant3 ( ( 𝜑𝑗 ∈ ℕ ∧ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → ( 𝐽𝑗 ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑗 ) ↾ 𝑌 ) , 𝐹 ) )
431 77 3ad2ant3 ( ( 𝜑𝑗 ∈ ℕ ∧ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑗 ) ↾ 𝑌 ) , 𝐹 ) = ( ( 𝐶𝑗 ) ↾ 𝑌 ) )
432 430 431 eqtrd ( ( 𝜑𝑗 ∈ ℕ ∧ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → ( 𝐽𝑗 ) = ( ( 𝐶𝑗 ) ↾ 𝑌 ) )
433 432 fveq1d ( ( 𝜑𝑗 ∈ ℕ ∧ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → ( ( 𝐽𝑗 ) ‘ 𝑘 ) = ( ( ( 𝐶𝑗 ) ↾ 𝑌 ) ‘ 𝑘 ) )
434 402 403 429 433 syl3anc ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) → ( ( 𝐽𝑗 ) ‘ 𝑘 ) = ( ( ( 𝐶𝑗 ) ↾ 𝑌 ) ‘ 𝑘 ) )
435 434 adantr ( ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘𝑌 ) → ( ( 𝐽𝑗 ) ‘ 𝑘 ) = ( ( ( 𝐶𝑗 ) ↾ 𝑌 ) ‘ 𝑘 ) )
436 fvres ( 𝑘𝑌 → ( ( ( 𝐶𝑗 ) ↾ 𝑌 ) ‘ 𝑘 ) = ( ( 𝐶𝑗 ) ‘ 𝑘 ) )
437 436 adantl ( ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘𝑌 ) → ( ( ( 𝐶𝑗 ) ↾ 𝑌 ) ‘ 𝑘 ) = ( ( 𝐶𝑗 ) ‘ 𝑘 ) )
438 435 437 eqtrd ( ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘𝑌 ) → ( ( 𝐽𝑗 ) ‘ 𝑘 ) = ( ( 𝐶𝑗 ) ‘ 𝑘 ) )
439 120 elexd ( ( 𝜑𝑗 ∈ ℕ ) → if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑗 ) ↾ 𝑌 ) , 𝐹 ) ∈ V )
440 13 fvmpt2 ( ( 𝑗 ∈ ℕ ∧ if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑗 ) ↾ 𝑌 ) , 𝐹 ) ∈ V ) → ( 𝐾𝑗 ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑗 ) ↾ 𝑌 ) , 𝐹 ) )
441 151 439 440 syl2anc ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝐾𝑗 ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑗 ) ↾ 𝑌 ) , 𝐹 ) )
442 441 3adant3 ( ( 𝜑𝑗 ∈ ℕ ∧ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → ( 𝐾𝑗 ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑗 ) ↾ 𝑌 ) , 𝐹 ) )
443 107 3ad2ant3 ( ( 𝜑𝑗 ∈ ℕ ∧ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑗 ) ↾ 𝑌 ) , 𝐹 ) = ( ( 𝐷𝑗 ) ↾ 𝑌 ) )
444 442 443 eqtrd ( ( 𝜑𝑗 ∈ ℕ ∧ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → ( 𝐾𝑗 ) = ( ( 𝐷𝑗 ) ↾ 𝑌 ) )
445 444 fveq1d ( ( 𝜑𝑗 ∈ ℕ ∧ 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) → ( ( 𝐾𝑗 ) ‘ 𝑘 ) = ( ( ( 𝐷𝑗 ) ↾ 𝑌 ) ‘ 𝑘 ) )
446 402 403 429 445 syl3anc ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) → ( ( 𝐾𝑗 ) ‘ 𝑘 ) = ( ( ( 𝐷𝑗 ) ↾ 𝑌 ) ‘ 𝑘 ) )
447 446 adantr ( ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘𝑌 ) → ( ( 𝐾𝑗 ) ‘ 𝑘 ) = ( ( ( 𝐷𝑗 ) ↾ 𝑌 ) ‘ 𝑘 ) )
448 fvres ( 𝑘𝑌 → ( ( ( 𝐷𝑗 ) ↾ 𝑌 ) ‘ 𝑘 ) = ( ( 𝐷𝑗 ) ‘ 𝑘 ) )
449 448 adantl ( ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘𝑌 ) → ( ( ( 𝐷𝑗 ) ↾ 𝑌 ) ‘ 𝑘 ) = ( ( 𝐷𝑗 ) ‘ 𝑘 ) )
450 447 449 eqtrd ( ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘𝑌 ) → ( ( 𝐾𝑗 ) ‘ 𝑘 ) = ( ( 𝐷𝑗 ) ‘ 𝑘 ) )
451 438 450 oveq12d ( ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘𝑌 ) → ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) = ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) )
452 451 eqcomd ( ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘𝑌 ) → ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) = ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) )
453 401 452 eleqtrd ( ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) ∧ 𝑘𝑌 ) → ( 𝑥𝑘 ) ∈ ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) )
454 453 ex ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) → ( 𝑘𝑌 → ( 𝑥𝑘 ) ∈ ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) ) )
455 386 454 ralrimi ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) → ∀ 𝑘𝑌 ( 𝑥𝑘 ) ∈ ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) )
456 380 455 jca ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) → ( 𝑥 Fn 𝑌 ∧ ∀ 𝑘𝑌 ( 𝑥𝑘 ) ∈ ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) ) )
457 322 elixp ( 𝑥X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) ↔ ( 𝑥 Fn 𝑌 ∧ ∀ 𝑘𝑌 ( 𝑥𝑘 ) ∈ ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) ) )
458 456 457 sylibr ( ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) ∧ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) ) → 𝑥X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) )
459 458 ex ( ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) ∧ 𝑗 ∈ ℕ ) → ( ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) → 𝑥X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) ) )
460 459 reximdva ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) → ( ∃ 𝑗 ∈ ℕ ( 𝑂𝑥 ) ∈ X 𝑘𝑊 ( ( ( 𝐶𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑘 ) ) → ∃ 𝑗 ∈ ℕ 𝑥X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) ) )
461 377 460 mpd ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) → ∃ 𝑗 ∈ ℕ 𝑥X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) )
462 eliun ( 𝑥 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) ↔ ∃ 𝑗 ∈ ℕ 𝑥X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) )
463 461 462 sylibr ( ( 𝜑𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ) → 𝑥 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) )
464 463 ralrimiva ( 𝜑 → ∀ 𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) 𝑥 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) )
465 dfss3 ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) ↔ ∀ 𝑥X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) 𝑥 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) )
466 464 465 sylibr ( 𝜑X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) )
467 ovexd ( 𝜑 → ( ℝ ↑m 𝑌 ) ∈ V )
468 237 a1i ( 𝜑 → ℕ ∈ V )
469 467 468 elmapd ( 𝜑 → ( 𝐾 ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ↔ 𝐾 : ℕ ⟶ ( ℝ ↑m 𝑌 ) ) )
470 121 469 mpbird ( 𝜑𝐾 ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) )
471 467 468 elmapd ( 𝜑 → ( 𝐽 ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ↔ 𝐽 : ℕ ⟶ ( ℝ ↑m 𝑌 ) ) )
472 103 471 mpbird ( 𝜑𝐽 ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) )
473 97 87 elmapd ( 𝜑 → ( ( 𝐵𝑌 ) ∈ ( ℝ ↑m 𝑌 ) ↔ ( 𝐵𝑌 ) : 𝑌 ⟶ ℝ ) )
474 213 473 mpbird ( 𝜑 → ( 𝐵𝑌 ) ∈ ( ℝ ↑m 𝑌 ) )
475 97 87 elmapd ( 𝜑 → ( ( 𝐴𝑌 ) ∈ ( ℝ ↑m 𝑌 ) ↔ ( 𝐴𝑌 ) : 𝑌 ⟶ ℝ ) )
476 212 475 mpbird ( 𝜑 → ( 𝐴𝑌 ) ∈ ( ℝ ↑m 𝑌 ) )
477 fveq1 ( 𝑒 = ( 𝐴𝑌 ) → ( 𝑒𝑘 ) = ( ( 𝐴𝑌 ) ‘ 𝑘 ) )
478 477 adantr ( ( 𝑒 = ( 𝐴𝑌 ) ∧ 𝑘𝑌 ) → ( 𝑒𝑘 ) = ( ( 𝐴𝑌 ) ‘ 𝑘 ) )
479 259 adantl ( ( 𝑒 = ( 𝐴𝑌 ) ∧ 𝑘𝑌 ) → ( ( 𝐴𝑌 ) ‘ 𝑘 ) = ( 𝐴𝑘 ) )
480 478 479 eqtrd ( ( 𝑒 = ( 𝐴𝑌 ) ∧ 𝑘𝑌 ) → ( 𝑒𝑘 ) = ( 𝐴𝑘 ) )
481 480 oveq1d ( ( 𝑒 = ( 𝐴𝑌 ) ∧ 𝑘𝑌 ) → ( ( 𝑒𝑘 ) [,) ( 𝑓𝑘 ) ) = ( ( 𝐴𝑘 ) [,) ( 𝑓𝑘 ) ) )
482 481 ixpeq2dva ( 𝑒 = ( 𝐴𝑌 ) → X 𝑘𝑌 ( ( 𝑒𝑘 ) [,) ( 𝑓𝑘 ) ) = X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝑓𝑘 ) ) )
483 482 sseq1d ( 𝑒 = ( 𝐴𝑌 ) → ( X 𝑘𝑌 ( ( 𝑒𝑘 ) [,) ( 𝑓𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) ↔ X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝑓𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) ) )
484 oveq1 ( 𝑒 = ( 𝐴𝑌 ) → ( 𝑒 ( 𝐿𝑌 ) 𝑓 ) = ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) 𝑓 ) )
485 484 breq1d ( 𝑒 = ( 𝐴𝑌 ) → ( ( 𝑒 ( 𝐿𝑌 ) 𝑓 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ↔ ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) 𝑓 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) )
486 483 485 imbi12d ( 𝑒 = ( 𝐴𝑌 ) → ( ( X 𝑘𝑌 ( ( 𝑒𝑘 ) [,) ( 𝑓𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( 𝑒 ( 𝐿𝑌 ) 𝑓 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) ↔ ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝑓𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) 𝑓 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) ) )
487 486 ralbidv ( 𝑒 = ( 𝐴𝑌 ) → ( ∀ ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ( X 𝑘𝑌 ( ( 𝑒𝑘 ) [,) ( 𝑓𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( 𝑒 ( 𝐿𝑌 ) 𝑓 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) ↔ ∀ ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝑓𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) 𝑓 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) ) )
488 487 ralbidv ( 𝑒 = ( 𝐴𝑌 ) → ( ∀ 𝑔 ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ∀ ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ( X 𝑘𝑌 ( ( 𝑒𝑘 ) [,) ( 𝑓𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( 𝑒 ( 𝐿𝑌 ) 𝑓 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) ↔ ∀ 𝑔 ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ∀ ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝑓𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) 𝑓 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) ) )
489 488 ralbidv ( 𝑒 = ( 𝐴𝑌 ) → ( ∀ 𝑓 ∈ ( ℝ ↑m 𝑌 ) ∀ 𝑔 ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ∀ ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ( X 𝑘𝑌 ( ( 𝑒𝑘 ) [,) ( 𝑓𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( 𝑒 ( 𝐿𝑌 ) 𝑓 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) ↔ ∀ 𝑓 ∈ ( ℝ ↑m 𝑌 ) ∀ 𝑔 ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ∀ ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝑓𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) 𝑓 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) ) )
490 489 rspcva ( ( ( 𝐴𝑌 ) ∈ ( ℝ ↑m 𝑌 ) ∧ ∀ 𝑒 ∈ ( ℝ ↑m 𝑌 ) ∀ 𝑓 ∈ ( ℝ ↑m 𝑌 ) ∀ 𝑔 ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ∀ ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ( X 𝑘𝑌 ( ( 𝑒𝑘 ) [,) ( 𝑓𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( 𝑒 ( 𝐿𝑌 ) 𝑓 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) ) → ∀ 𝑓 ∈ ( ℝ ↑m 𝑌 ) ∀ 𝑔 ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ∀ ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝑓𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) 𝑓 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) )
491 476 22 490 syl2anc ( 𝜑 → ∀ 𝑓 ∈ ( ℝ ↑m 𝑌 ) ∀ 𝑔 ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ∀ ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝑓𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) 𝑓 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) )
492 fveq1 ( 𝑓 = ( 𝐵𝑌 ) → ( 𝑓𝑘 ) = ( ( 𝐵𝑌 ) ‘ 𝑘 ) )
493 492 adantr ( ( 𝑓 = ( 𝐵𝑌 ) ∧ 𝑘𝑌 ) → ( 𝑓𝑘 ) = ( ( 𝐵𝑌 ) ‘ 𝑘 ) )
494 260 adantl ( ( 𝑓 = ( 𝐵𝑌 ) ∧ 𝑘𝑌 ) → ( ( 𝐵𝑌 ) ‘ 𝑘 ) = ( 𝐵𝑘 ) )
495 493 494 eqtrd ( ( 𝑓 = ( 𝐵𝑌 ) ∧ 𝑘𝑌 ) → ( 𝑓𝑘 ) = ( 𝐵𝑘 ) )
496 495 oveq2d ( ( 𝑓 = ( 𝐵𝑌 ) ∧ 𝑘𝑌 ) → ( ( 𝐴𝑘 ) [,) ( 𝑓𝑘 ) ) = ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) )
497 496 ixpeq2dva ( 𝑓 = ( 𝐵𝑌 ) → X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝑓𝑘 ) ) = X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) )
498 497 sseq1d ( 𝑓 = ( 𝐵𝑌 ) → ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝑓𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) ↔ X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) ) )
499 oveq2 ( 𝑓 = ( 𝐵𝑌 ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) 𝑓 ) = ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) )
500 499 breq1d ( 𝑓 = ( 𝐵𝑌 ) → ( ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) 𝑓 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ↔ ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) )
501 498 500 imbi12d ( 𝑓 = ( 𝐵𝑌 ) → ( ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝑓𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) 𝑓 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) ↔ ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) ) )
502 501 ralbidv ( 𝑓 = ( 𝐵𝑌 ) → ( ∀ ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝑓𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) 𝑓 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) ↔ ∀ ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) ) )
503 502 ralbidv ( 𝑓 = ( 𝐵𝑌 ) → ( ∀ 𝑔 ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ∀ ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝑓𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) 𝑓 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) ↔ ∀ 𝑔 ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ∀ ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) ) )
504 503 rspcva ( ( ( 𝐵𝑌 ) ∈ ( ℝ ↑m 𝑌 ) ∧ ∀ 𝑓 ∈ ( ℝ ↑m 𝑌 ) ∀ 𝑔 ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ∀ ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝑓𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) 𝑓 ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) ) → ∀ 𝑔 ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ∀ ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) )
505 474 491 504 syl2anc ( 𝜑 → ∀ 𝑔 ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ∀ ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) )
506 fveq1 ( 𝑔 = 𝐽 → ( 𝑔𝑗 ) = ( 𝐽𝑗 ) )
507 506 fveq1d ( 𝑔 = 𝐽 → ( ( 𝑔𝑗 ) ‘ 𝑘 ) = ( ( 𝐽𝑗 ) ‘ 𝑘 ) )
508 507 oveq1d ( 𝑔 = 𝐽 → ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) = ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) )
509 508 ixpeq2dv ( 𝑔 = 𝐽X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) = X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) )
510 509 iuneq2d ( 𝑔 = 𝐽 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) = 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) )
511 510 sseq2d ( 𝑔 = 𝐽 → ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) ↔ X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) ) )
512 506 oveq1d ( 𝑔 = 𝐽 → ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) = ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) )
513 512 mpteq2dv ( 𝑔 = 𝐽 → ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) = ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) )
514 513 fveq2d ( 𝑔 = 𝐽 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) )
515 514 breq2d ( 𝑔 = 𝐽 → ( ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ↔ ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) )
516 511 515 imbi12d ( 𝑔 = 𝐽 → ( ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) ↔ ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) ) )
517 516 ralbidv ( 𝑔 = 𝐽 → ( ∀ ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) ↔ ∀ ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) ) )
518 517 rspcva ( ( 𝐽 ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ∧ ∀ 𝑔 ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ∀ ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝑔𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝑔𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) ) → ∀ ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) )
519 472 505 518 syl2anc ( 𝜑 → ∀ ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) )
520 fveq1 ( = 𝐾 → ( 𝑗 ) = ( 𝐾𝑗 ) )
521 520 fveq1d ( = 𝐾 → ( ( 𝑗 ) ‘ 𝑘 ) = ( ( 𝐾𝑗 ) ‘ 𝑘 ) )
522 521 oveq2d ( = 𝐾 → ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) = ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) )
523 522 ixpeq2dv ( = 𝐾X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) = X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) )
524 523 iuneq2d ( = 𝐾 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) = 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) )
525 524 sseq2d ( = 𝐾 → ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) ↔ X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) ) )
526 520 oveq2d ( = 𝐾 → ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) = ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) )
527 526 mpteq2dv ( = 𝐾 → ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) = ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) ) )
528 527 fveq2d ( = 𝐾 → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) ) ) )
529 528 breq2d ( = 𝐾 → ( ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ↔ ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) ) ) ) )
530 525 529 imbi12d ( = 𝐾 → ( ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) ↔ ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) ) ) ) ) )
531 530 rspcva ( ( 𝐾 ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ∧ ∀ ∈ ( ( ℝ ↑m 𝑌 ) ↑m ℕ ) ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝑗 ) ‘ 𝑘 ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝑗 ) ) ) ) ) ) → ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) ) ) ) )
532 470 519 531 syl2anc ( 𝜑 → ( X 𝑘𝑌 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) ⊆ 𝑗 ∈ ℕ X 𝑘𝑌 ( ( ( 𝐽𝑗 ) ‘ 𝑘 ) [,) ( ( 𝐾𝑗 ) ‘ 𝑘 ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) ) ) ) )
533 466 532 mpd ( 𝜑 → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) ) ) )
534 idd ( 𝜑 → ( ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) ) ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) ) ) ) )
535 533 534 mpd ( 𝜑 → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) ) ) )
536 535 adantr ( ( 𝜑𝑌 ≠ ∅ ) → ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) ) ) )
537 62 adantl ( ( ( 𝜑𝑌 ≠ ∅ ) ∧ 𝑗 ∈ ℕ ) → ( 𝑃𝑗 ) = ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) )
538 537 mpteq2dva ( ( 𝜑𝑌 ≠ ∅ ) → ( 𝑗 ∈ ℕ ↦ ( 𝑃𝑗 ) ) = ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) ) )
539 538 fveq2d ( ( 𝜑𝑌 ≠ ∅ ) → ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝑃𝑗 ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) ) ) )
540 258 539 breq12d ( ( 𝜑𝑌 ≠ ∅ ) → ( 𝐺 ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝑃𝑗 ) ) ) ↔ ( ( 𝐴𝑌 ) ( 𝐿𝑌 ) ( 𝐵𝑌 ) ) ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) ) ) ) )
541 536 540 mpbird ( ( 𝜑𝑌 ≠ ∅ ) → 𝐺 ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝑃𝑗 ) ) ) )
542 541 adantr ( ( ( 𝜑𝑌 ≠ ∅ ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝑃𝑗 ) ) ) ∈ ℝ ) → 𝐺 ≤ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝑃𝑗 ) ) ) )
543 247 249 250 289 542 ltletrd ( ( ( 𝜑𝑌 ≠ ∅ ) ∧ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝑃𝑗 ) ) ) ∈ ℝ ) → ( 𝐺 / ( 1 + 𝐸 ) ) < ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝑃𝑗 ) ) ) )
544 235 246 543 syl2anc ( ( ( 𝜑𝑌 ≠ ∅ ) ∧ ¬ ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝑃𝑗 ) ) ) = +∞ ) → ( 𝐺 / ( 1 + 𝐸 ) ) < ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝑃𝑗 ) ) ) )
545 234 544 pm2.61dan ( ( 𝜑𝑌 ≠ ∅ ) → ( 𝐺 / ( 1 + 𝐸 ) ) < ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( 𝑃𝑗 ) ) ) )
546 207 208 209 210 227 545 sge0uzfsumgt ( ( 𝜑𝑌 ≠ ∅ ) → ∃ 𝑚 ∈ ℕ ( 𝐺 / ( 1 + 𝐸 ) ) < Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) )
547 226 adantr ( ( 𝜑 ∧ ( 𝐺 / ( 1 + 𝐸 ) ) < Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) → ( 𝐺 / ( 1 + 𝐸 ) ) ∈ ℝ )
548 fzfid ( 𝜑 → ( 1 ... 𝑚 ) ∈ Fin )
549 simpl ( ( 𝜑𝑗 ∈ ( 1 ... 𝑚 ) ) → 𝜑 )
550 elfznn ( 𝑗 ∈ ( 1 ... 𝑚 ) → 𝑗 ∈ ℕ )
551 550 adantl ( ( 𝜑𝑗 ∈ ( 1 ... 𝑚 ) ) → 𝑗 ∈ ℕ )
552 50 126 sselid ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝑃𝑗 ) ∈ ℝ )
553 549 551 552 syl2anc ( ( 𝜑𝑗 ∈ ( 1 ... 𝑚 ) ) → ( 𝑃𝑗 ) ∈ ℝ )
554 548 553 fsumrecl ( 𝜑 → Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ∈ ℝ )
555 554 adantr ( ( 𝜑 ∧ ( 𝐺 / ( 1 + 𝐸 ) ) < Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) → Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ∈ ℝ )
556 simpr ( ( 𝜑 ∧ ( 𝐺 / ( 1 + 𝐸 ) ) < Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) → ( 𝐺 / ( 1 + 𝐸 ) ) < Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) )
557 547 555 556 ltled ( ( 𝜑 ∧ ( 𝐺 / ( 1 + 𝐸 ) ) < Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) → ( 𝐺 / ( 1 + 𝐸 ) ) ≤ Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) )
558 216 adantr ( ( 𝜑 ∧ ( 𝐺 / ( 1 + 𝐸 ) ) < Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) → 𝐺 ∈ ℝ )
559 222 adantr ( ( 𝜑 ∧ ( 𝐺 / ( 1 + 𝐸 ) ) < Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) → ( 1 + 𝐸 ) ∈ ℝ+ )
560 558 555 559 ledivmuld ( ( 𝜑 ∧ ( 𝐺 / ( 1 + 𝐸 ) ) < Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) → ( ( 𝐺 / ( 1 + 𝐸 ) ) ≤ Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ↔ 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) ) )
561 557 560 mpbid ( ( 𝜑 ∧ ( 𝐺 / ( 1 + 𝐸 ) ) < Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) → 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) )
562 561 ex ( 𝜑 → ( ( 𝐺 / ( 1 + 𝐸 ) ) < Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) → 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) ) )
563 562 adantr ( ( 𝜑𝑚 ∈ ℕ ) → ( ( 𝐺 / ( 1 + 𝐸 ) ) < Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) → 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) ) )
564 563 adantlr ( ( ( 𝜑𝑌 ≠ ∅ ) ∧ 𝑚 ∈ ℕ ) → ( ( 𝐺 / ( 1 + 𝐸 ) ) < Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) → 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) ) )
565 564 reximdva ( ( 𝜑𝑌 ≠ ∅ ) → ( ∃ 𝑚 ∈ ℕ ( 𝐺 / ( 1 + 𝐸 ) ) < Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) → ∃ 𝑚 ∈ ℕ 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) ) )
566 546 565 mpd ( ( 𝜑𝑌 ≠ ∅ ) → ∃ 𝑚 ∈ ℕ 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) )
567 204 206 566 syl2anc ( ( 𝜑 ∧ ¬ 𝑌 = ∅ ) → ∃ 𝑚 ∈ ℕ 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) )
568 203 567 pm2.61dan ( 𝜑 → ∃ 𝑚 ∈ ℕ 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) )
569 2 3ad2ant1 ( ( 𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) ) → 𝑋 ∈ Fin )
570 3 3ad2ant1 ( ( 𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) ) → 𝑌𝑋 )
571 4 3ad2ant1 ( ( 𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) ) → 𝑍 ∈ ( 𝑋𝑌 ) )
572 6 3ad2ant1 ( ( 𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) ) → 𝐴 : 𝑊 ⟶ ℝ )
573 7 3ad2ant1 ( ( 𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) ) → 𝐵 : 𝑊 ⟶ ℝ )
574 10 3ad2ant1 ( ( 𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) ) → 𝐶 : ℕ ⟶ ( ℝ ↑m 𝑊 ) )
575 eqid ( 𝑦𝑌 ↦ 0 ) = ( 𝑦𝑌 ↦ 0 )
576 eqid ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) = ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) )
577 12 3ad2ant1 ( ( 𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) ) → 𝐷 : ℕ ⟶ ( ℝ ↑m 𝑊 ) )
578 eqid ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) = ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) )
579 fveq2 ( 𝑖 = 𝑗 → ( 𝐶𝑖 ) = ( 𝐶𝑗 ) )
580 fveq2 ( 𝑖 = 𝑗 → ( 𝐷𝑖 ) = ( 𝐷𝑗 ) )
581 579 580 oveq12d ( 𝑖 = 𝑗 → ( ( 𝐶𝑖 ) ( 𝐿𝑊 ) ( 𝐷𝑖 ) ) = ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( 𝐷𝑗 ) ) )
582 581 cbvmptv ( 𝑖 ∈ ℕ ↦ ( ( 𝐶𝑖 ) ( 𝐿𝑊 ) ( 𝐷𝑖 ) ) ) = ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( 𝐷𝑗 ) ) )
583 582 fveq2i ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( ( 𝐶𝑖 ) ( 𝐿𝑊 ) ( 𝐷𝑖 ) ) ) ) = ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( 𝐷𝑗 ) ) ) )
584 583 14 eqeltrid ( 𝜑 → ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( ( 𝐶𝑖 ) ( 𝐿𝑊 ) ( 𝐷𝑖 ) ) ) ) ∈ ℝ )
585 584 3ad2ant1 ( ( 𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) ) → ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( ( 𝐶𝑖 ) ( 𝐿𝑊 ) ( 𝐷𝑖 ) ) ) ) ∈ ℝ )
586 eleq1w ( 𝑗 = 𝑖 → ( 𝑗𝑌𝑖𝑌 ) )
587 fveq2 ( 𝑗 = 𝑖 → ( 𝑐𝑗 ) = ( 𝑐𝑖 ) )
588 587 breq1d ( 𝑗 = 𝑖 → ( ( 𝑐𝑗 ) ≤ 𝑥 ↔ ( 𝑐𝑖 ) ≤ 𝑥 ) )
589 588 587 ifbieq1d ( 𝑗 = 𝑖 → if ( ( 𝑐𝑗 ) ≤ 𝑥 , ( 𝑐𝑗 ) , 𝑥 ) = if ( ( 𝑐𝑖 ) ≤ 𝑥 , ( 𝑐𝑖 ) , 𝑥 ) )
590 586 587 589 ifbieq12d ( 𝑗 = 𝑖 → if ( 𝑗𝑌 , ( 𝑐𝑗 ) , if ( ( 𝑐𝑗 ) ≤ 𝑥 , ( 𝑐𝑗 ) , 𝑥 ) ) = if ( 𝑖𝑌 , ( 𝑐𝑖 ) , if ( ( 𝑐𝑖 ) ≤ 𝑥 , ( 𝑐𝑖 ) , 𝑥 ) ) )
591 590 cbvmptv ( 𝑗𝑊 ↦ if ( 𝑗𝑌 , ( 𝑐𝑗 ) , if ( ( 𝑐𝑗 ) ≤ 𝑥 , ( 𝑐𝑗 ) , 𝑥 ) ) ) = ( 𝑖𝑊 ↦ if ( 𝑖𝑌 , ( 𝑐𝑖 ) , if ( ( 𝑐𝑖 ) ≤ 𝑥 , ( 𝑐𝑖 ) , 𝑥 ) ) )
592 591 mpteq2i ( 𝑐 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑗𝑊 ↦ if ( 𝑗𝑌 , ( 𝑐𝑗 ) , if ( ( 𝑐𝑗 ) ≤ 𝑥 , ( 𝑐𝑗 ) , 𝑥 ) ) ) ) = ( 𝑐 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖𝑊 ↦ if ( 𝑖𝑌 , ( 𝑐𝑖 ) , if ( ( 𝑐𝑖 ) ≤ 𝑥 , ( 𝑐𝑖 ) , 𝑥 ) ) ) )
593 592 mpteq2i ( 𝑥 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑗𝑊 ↦ if ( 𝑗𝑌 , ( 𝑐𝑗 ) , if ( ( 𝑐𝑗 ) ≤ 𝑥 , ( 𝑐𝑗 ) , 𝑥 ) ) ) ) ) = ( 𝑥 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖𝑊 ↦ if ( 𝑖𝑌 , ( 𝑐𝑖 ) , if ( ( 𝑐𝑖 ) ≤ 𝑥 , ( 𝑐𝑖 ) , 𝑥 ) ) ) ) )
594 15 593 eqtri 𝐻 = ( 𝑥 ∈ ℝ ↦ ( 𝑐 ∈ ( ℝ ↑m 𝑊 ) ↦ ( 𝑖𝑊 ↦ if ( 𝑖𝑌 , ( 𝑐𝑖 ) , if ( ( 𝑐𝑖 ) ≤ 𝑥 , ( 𝑐𝑖 ) , 𝑥 ) ) ) ) )
595 17 3ad2ant1 ( ( 𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) ) → 𝐸 ∈ ℝ+ )
596 fveq2 ( 𝑗 = 𝑖 → ( 𝐶𝑗 ) = ( 𝐶𝑖 ) )
597 fveq2 ( 𝑗 = 𝑖 → ( 𝐷𝑗 ) = ( 𝐷𝑖 ) )
598 597 fveq2d ( 𝑗 = 𝑖 → ( ( 𝐻𝑧 ) ‘ ( 𝐷𝑗 ) ) = ( ( 𝐻𝑧 ) ‘ ( 𝐷𝑖 ) ) )
599 596 598 oveq12d ( 𝑗 = 𝑖 → ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑧 ) ‘ ( 𝐷𝑗 ) ) ) = ( ( 𝐶𝑖 ) ( 𝐿𝑊 ) ( ( 𝐻𝑧 ) ‘ ( 𝐷𝑖 ) ) ) )
600 599 cbvmptv ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑧 ) ‘ ( 𝐷𝑗 ) ) ) ) = ( 𝑖 ∈ ℕ ↦ ( ( 𝐶𝑖 ) ( 𝐿𝑊 ) ( ( 𝐻𝑧 ) ‘ ( 𝐷𝑖 ) ) ) )
601 600 fveq2i ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑧 ) ‘ ( 𝐷𝑗 ) ) ) ) ) = ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( ( 𝐶𝑖 ) ( 𝐿𝑊 ) ( ( 𝐻𝑧 ) ‘ ( 𝐷𝑖 ) ) ) ) )
602 601 oveq2i ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑧 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) = ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( ( 𝐶𝑖 ) ( 𝐿𝑊 ) ( ( 𝐻𝑧 ) ‘ ( 𝐷𝑖 ) ) ) ) ) )
603 602 breq2i ( ( 𝐺 · ( 𝑧 − ( 𝐴𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑧 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) ↔ ( 𝐺 · ( 𝑧 − ( 𝐴𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( ( 𝐶𝑖 ) ( 𝐿𝑊 ) ( ( 𝐻𝑧 ) ‘ ( 𝐷𝑖 ) ) ) ) ) ) )
604 603 rabbii { 𝑧 ∈ ( ( 𝐴𝑍 ) [,] ( 𝐵𝑍 ) ) ∣ ( 𝐺 · ( 𝑧 − ( 𝐴𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑗 ∈ ℕ ↦ ( ( 𝐶𝑗 ) ( 𝐿𝑊 ) ( ( 𝐻𝑧 ) ‘ ( 𝐷𝑗 ) ) ) ) ) ) } = { 𝑧 ∈ ( ( 𝐴𝑍 ) [,] ( 𝐵𝑍 ) ) ∣ ( 𝐺 · ( 𝑧 − ( 𝐴𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( ( 𝐶𝑖 ) ( 𝐿𝑊 ) ( ( 𝐻𝑧 ) ‘ ( 𝐷𝑖 ) ) ) ) ) ) }
605 18 604 eqtri 𝑈 = { 𝑧 ∈ ( ( 𝐴𝑍 ) [,] ( 𝐵𝑍 ) ) ∣ ( 𝐺 · ( 𝑧 − ( 𝐴𝑍 ) ) ) ≤ ( ( 1 + 𝐸 ) · ( Σ^ ‘ ( 𝑖 ∈ ℕ ↦ ( ( 𝐶𝑖 ) ( 𝐿𝑊 ) ( ( 𝐻𝑧 ) ‘ ( 𝐷𝑖 ) ) ) ) ) ) }
606 19 3ad2ant1 ( ( 𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) ) → 𝑆𝑈 )
607 20 3ad2ant1 ( ( 𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) ) → 𝑆 < ( 𝐵𝑍 ) )
608 eqid ( 𝑖 ∈ ℕ ↦ ( ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ( 𝐿𝑌 ) ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ) ) = ( 𝑖 ∈ ℕ ↦ ( ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ( 𝐿𝑌 ) ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ) )
609 simp2 ( ( 𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) ) → 𝑚 ∈ ℕ )
610 id ( 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) → 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) )
611 fveq2 ( 𝑗 = 𝑖 → ( 𝑃𝑗 ) = ( 𝑃𝑖 ) )
612 611 cbvsumv Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) = Σ 𝑖 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑖 )
613 612 oveq2i ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) = ( ( 1 + 𝐸 ) · Σ 𝑖 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑖 ) )
614 613 a1i ( 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) → ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) = ( ( 1 + 𝐸 ) · Σ 𝑖 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑖 ) ) )
615 610 614 breqtrd ( 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) → 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑖 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑖 ) ) )
616 615 3ad2ant3 ( ( 𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) ) → 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑖 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑖 ) ) )
617 simpl ( ( 𝜑𝑖 ∈ ( 1 ... 𝑚 ) ) → 𝜑 )
618 elfznn ( 𝑖 ∈ ( 1 ... 𝑚 ) → 𝑖 ∈ ℕ )
619 618 adantl ( ( 𝜑𝑖 ∈ ( 1 ... 𝑚 ) ) → 𝑖 ∈ ℕ )
620 eleq1w ( 𝑗 = 𝑖 → ( 𝑗 ∈ ℕ ↔ 𝑖 ∈ ℕ ) )
621 fveq2 ( 𝑗 = 𝑖 → ( 𝐽𝑗 ) = ( 𝐽𝑖 ) )
622 fveq2 ( 𝑗 = 𝑖 → ( 𝐾𝑗 ) = ( 𝐾𝑖 ) )
623 621 622 oveq12d ( 𝑗 = 𝑖 → ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) = ( ( 𝐽𝑖 ) ( 𝐿𝑌 ) ( 𝐾𝑖 ) ) )
624 611 623 eqeq12d ( 𝑗 = 𝑖 → ( ( 𝑃𝑗 ) = ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) ↔ ( 𝑃𝑖 ) = ( ( 𝐽𝑖 ) ( 𝐿𝑌 ) ( 𝐾𝑖 ) ) ) )
625 620 624 imbi12d ( 𝑗 = 𝑖 → ( ( 𝑗 ∈ ℕ → ( 𝑃𝑗 ) = ( ( 𝐽𝑗 ) ( 𝐿𝑌 ) ( 𝐾𝑗 ) ) ) ↔ ( 𝑖 ∈ ℕ → ( 𝑃𝑖 ) = ( ( 𝐽𝑖 ) ( 𝐿𝑌 ) ( 𝐾𝑖 ) ) ) ) )
626 625 62 chvarvv ( 𝑖 ∈ ℕ → ( 𝑃𝑖 ) = ( ( 𝐽𝑖 ) ( 𝐿𝑌 ) ( 𝐾𝑖 ) ) )
627 626 adantl ( ( 𝜑𝑖 ∈ ℕ ) → ( 𝑃𝑖 ) = ( ( 𝐽𝑖 ) ( 𝐿𝑌 ) ( 𝐾𝑖 ) ) )
628 620 anbi2d ( 𝑗 = 𝑖 → ( ( 𝜑𝑗 ∈ ℕ ) ↔ ( 𝜑𝑖 ∈ ℕ ) ) )
629 596 fveq1d ( 𝑗 = 𝑖 → ( ( 𝐶𝑗 ) ‘ 𝑍 ) = ( ( 𝐶𝑖 ) ‘ 𝑍 ) )
630 597 fveq1d ( 𝑗 = 𝑖 → ( ( 𝐷𝑗 ) ‘ 𝑍 ) = ( ( 𝐷𝑖 ) ‘ 𝑍 ) )
631 629 630 oveq12d ( 𝑗 = 𝑖 → ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) = ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) )
632 631 eleq2d ( 𝑗 = 𝑖 → ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ↔ 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) ) )
633 596 reseq1d ( 𝑗 = 𝑖 → ( ( 𝐶𝑗 ) ↾ 𝑌 ) = ( ( 𝐶𝑖 ) ↾ 𝑌 ) )
634 632 633 ifbieq1d ( 𝑗 = 𝑖 → if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑗 ) ↾ 𝑌 ) , 𝐹 ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , 𝐹 ) )
635 621 634 eqeq12d ( 𝑗 = 𝑖 → ( ( 𝐽𝑗 ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑗 ) ↾ 𝑌 ) , 𝐹 ) ↔ ( 𝐽𝑖 ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , 𝐹 ) ) )
636 628 635 imbi12d ( 𝑗 = 𝑖 → ( ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝐽𝑗 ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑗 ) ↾ 𝑌 ) , 𝐹 ) ) ↔ ( ( 𝜑𝑖 ∈ ℕ ) → ( 𝐽𝑖 ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , 𝐹 ) ) ) )
637 636 161 chvarvv ( ( 𝜑𝑖 ∈ ℕ ) → ( 𝐽𝑖 ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , 𝐹 ) )
638 597 reseq1d ( 𝑗 = 𝑖 → ( ( 𝐷𝑗 ) ↾ 𝑌 ) = ( ( 𝐷𝑖 ) ↾ 𝑌 ) )
639 632 638 ifbieq1d ( 𝑗 = 𝑖 → if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑗 ) ↾ 𝑌 ) , 𝐹 ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , 𝐹 ) )
640 622 639 eqeq12d ( 𝑗 = 𝑖 → ( ( 𝐾𝑗 ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑗 ) ↾ 𝑌 ) , 𝐹 ) ↔ ( 𝐾𝑖 ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , 𝐹 ) ) )
641 628 640 imbi12d ( 𝑗 = 𝑖 → ( ( ( 𝜑𝑗 ∈ ℕ ) → ( 𝐾𝑗 ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑗 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑗 ) ↾ 𝑌 ) , 𝐹 ) ) ↔ ( ( 𝜑𝑖 ∈ ℕ ) → ( 𝐾𝑖 ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , 𝐹 ) ) ) )
642 641 441 chvarvv ( ( 𝜑𝑖 ∈ ℕ ) → ( 𝐾𝑖 ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , 𝐹 ) )
643 637 642 oveq12d ( ( 𝜑𝑖 ∈ ℕ ) → ( ( 𝐽𝑖 ) ( 𝐿𝑌 ) ( 𝐾𝑖 ) ) = ( if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , 𝐹 ) ( 𝐿𝑌 ) if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , 𝐹 ) ) )
644 627 643 eqtrd ( ( 𝜑𝑖 ∈ ℕ ) → ( 𝑃𝑖 ) = ( if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , 𝐹 ) ( 𝐿𝑌 ) if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , 𝐹 ) ) )
645 simpr ( ( 𝜑𝑖 ∈ ℕ ) → 𝑖 ∈ ℕ )
646 ovexd ( ( 𝜑𝑖 ∈ ℕ ) → ( ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ( 𝐿𝑌 ) ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ) ∈ V )
647 608 fvmpt2 ( ( 𝑖 ∈ ℕ ∧ ( ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ( 𝐿𝑌 ) ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ) ∈ V ) → ( ( 𝑖 ∈ ℕ ↦ ( ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ( 𝐿𝑌 ) ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ) ) ‘ 𝑖 ) = ( ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ( 𝐿𝑌 ) ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ) )
648 645 646 647 syl2anc ( ( 𝜑𝑖 ∈ ℕ ) → ( ( 𝑖 ∈ ℕ ↦ ( ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ( 𝐿𝑌 ) ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ) ) ‘ 𝑖 ) = ( ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ( 𝐿𝑌 ) ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ) )
649 fvex ( 𝐶𝑖 ) ∈ V
650 649 resex ( ( 𝐶𝑖 ) ↾ 𝑌 ) ∈ V
651 650 a1i ( 𝜑 → ( ( 𝐶𝑖 ) ↾ 𝑌 ) ∈ V )
652 9 155 eqeltrrid ( 𝜑 → ( 𝑦𝑌 ↦ 0 ) ∈ V )
653 651 652 ifcld ( 𝜑 → if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ∈ V )
654 653 adantr ( ( 𝜑𝑖 ∈ ℕ ) → if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ∈ V )
655 576 fvmpt2 ( ( 𝑖 ∈ ℕ ∧ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ∈ V ) → ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) )
656 645 654 655 syl2anc ( ( 𝜑𝑖 ∈ ℕ ) → ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) )
657 9 eqcomi ( 𝑦𝑌 ↦ 0 ) = 𝐹
658 ifeq2 ( ( 𝑦𝑌 ↦ 0 ) = 𝐹 → if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , 𝐹 ) )
659 657 658 ax-mp if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , 𝐹 )
660 659 a1i ( ( 𝜑𝑖 ∈ ℕ ) → if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , 𝐹 ) )
661 656 660 eqtrd ( ( 𝜑𝑖 ∈ ℕ ) → ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , 𝐹 ) )
662 fvex ( 𝐷𝑖 ) ∈ V
663 662 resex ( ( 𝐷𝑖 ) ↾ 𝑌 ) ∈ V
664 663 a1i ( 𝜑 → ( ( 𝐷𝑖 ) ↾ 𝑌 ) ∈ V )
665 664 652 ifcld ( 𝜑 → if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ∈ V )
666 665 adantr ( ( 𝜑𝑖 ∈ ℕ ) → if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ∈ V )
667 578 fvmpt2 ( ( 𝑖 ∈ ℕ ∧ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ∈ V ) → ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) )
668 645 666 667 syl2anc ( ( 𝜑𝑖 ∈ ℕ ) → ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) )
669 biid ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) ↔ 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) )
670 669 657 ifbieq2i if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , 𝐹 )
671 670 a1i ( ( 𝜑𝑖 ∈ ℕ ) → if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , 𝐹 ) )
672 668 671 eqtrd ( ( 𝜑𝑖 ∈ ℕ ) → ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) = if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , 𝐹 ) )
673 661 672 oveq12d ( ( 𝜑𝑖 ∈ ℕ ) → ( ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ( 𝐿𝑌 ) ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ) = ( if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , 𝐹 ) ( 𝐿𝑌 ) if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , 𝐹 ) ) )
674 648 673 eqtrd ( ( 𝜑𝑖 ∈ ℕ ) → ( ( 𝑖 ∈ ℕ ↦ ( ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ( 𝐿𝑌 ) ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ) ) ‘ 𝑖 ) = ( if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , 𝐹 ) ( 𝐿𝑌 ) if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , 𝐹 ) ) )
675 644 674 eqtr4d ( ( 𝜑𝑖 ∈ ℕ ) → ( 𝑃𝑖 ) = ( ( 𝑖 ∈ ℕ ↦ ( ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ( 𝐿𝑌 ) ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ) ) ‘ 𝑖 ) )
676 617 619 675 syl2anc ( ( 𝜑𝑖 ∈ ( 1 ... 𝑚 ) ) → ( 𝑃𝑖 ) = ( ( 𝑖 ∈ ℕ ↦ ( ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ( 𝐿𝑌 ) ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ) ) ‘ 𝑖 ) )
677 676 3ad2antl1 ( ( ( 𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) ) ∧ 𝑖 ∈ ( 1 ... 𝑚 ) ) → ( 𝑃𝑖 ) = ( ( 𝑖 ∈ ℕ ↦ ( ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ( 𝐿𝑌 ) ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ) ) ‘ 𝑖 ) )
678 677 sumeq2dv ( ( 𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) ) → Σ 𝑖 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑖 ) = Σ 𝑖 ∈ ( 1 ... 𝑚 ) ( ( 𝑖 ∈ ℕ ↦ ( ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ( 𝐿𝑌 ) ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ) ) ‘ 𝑖 ) )
679 678 oveq2d ( ( 𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) ) → ( ( 1 + 𝐸 ) · Σ 𝑖 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑖 ) ) = ( ( 1 + 𝐸 ) · Σ 𝑖 ∈ ( 1 ... 𝑚 ) ( ( 𝑖 ∈ ℕ ↦ ( ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ( 𝐿𝑌 ) ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ) ) ‘ 𝑖 ) ) )
680 616 679 breqtrd ( ( 𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) ) → 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑖 ∈ ( 1 ... 𝑚 ) ( ( 𝑖 ∈ ℕ ↦ ( ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐶𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ( 𝐿𝑌 ) ( ( 𝑖 ∈ ℕ ↦ if ( 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) , ( ( 𝐷𝑖 ) ↾ 𝑌 ) , ( 𝑦𝑌 ↦ 0 ) ) ) ‘ 𝑖 ) ) ) ‘ 𝑖 ) ) )
681 fveq2 ( 𝑗 = → ( 𝐷𝑗 ) = ( 𝐷 ) )
682 681 fveq1d ( 𝑗 = → ( ( 𝐷𝑗 ) ‘ 𝑍 ) = ( ( 𝐷 ) ‘ 𝑍 ) )
683 682 cbvmptv ( 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝑚 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) } ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) = ( ∈ { 𝑖 ∈ ( 1 ... 𝑚 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) } ↦ ( ( 𝐷 ) ‘ 𝑍 ) )
684 683 rneqi ran ( 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝑚 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) } ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) = ran ( ∈ { 𝑖 ∈ ( 1 ... 𝑚 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) } ↦ ( ( 𝐷 ) ‘ 𝑍 ) )
685 fveq2 ( = 𝑖 → ( 𝐶 ) = ( 𝐶𝑖 ) )
686 685 fveq1d ( = 𝑖 → ( ( 𝐶 ) ‘ 𝑍 ) = ( ( 𝐶𝑖 ) ‘ 𝑍 ) )
687 fveq2 ( = 𝑖 → ( 𝐷 ) = ( 𝐷𝑖 ) )
688 687 fveq1d ( = 𝑖 → ( ( 𝐷 ) ‘ 𝑍 ) = ( ( 𝐷𝑖 ) ‘ 𝑍 ) )
689 686 688 oveq12d ( = 𝑖 → ( ( ( 𝐶 ) ‘ 𝑍 ) [,) ( ( 𝐷 ) ‘ 𝑍 ) ) = ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) )
690 689 eleq2d ( = 𝑖 → ( 𝑆 ∈ ( ( ( 𝐶 ) ‘ 𝑍 ) [,) ( ( 𝐷 ) ‘ 𝑍 ) ) ↔ 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) ) )
691 690 cbvrabv { ∈ ( 1 ... 𝑚 ) ∣ 𝑆 ∈ ( ( ( 𝐶 ) ‘ 𝑍 ) [,) ( ( 𝐷 ) ‘ 𝑍 ) ) } = { 𝑖 ∈ ( 1 ... 𝑚 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) }
692 691 mpteq1i ( 𝑗 ∈ { ∈ ( 1 ... 𝑚 ) ∣ 𝑆 ∈ ( ( ( 𝐶 ) ‘ 𝑍 ) [,) ( ( 𝐷 ) ‘ 𝑍 ) ) } ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) = ( 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝑚 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) } ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) )
693 692 rneqi ran ( 𝑗 ∈ { ∈ ( 1 ... 𝑚 ) ∣ 𝑆 ∈ ( ( ( 𝐶 ) ‘ 𝑍 ) [,) ( ( 𝐷 ) ‘ 𝑍 ) ) } ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) = ran ( 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝑚 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) } ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) )
694 693 uneq2i ( { ( 𝐵𝑍 ) } ∪ ran ( 𝑗 ∈ { ∈ ( 1 ... 𝑚 ) ∣ 𝑆 ∈ ( ( ( 𝐶 ) ‘ 𝑍 ) [,) ( ( 𝐷 ) ‘ 𝑍 ) ) } ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) = ( { ( 𝐵𝑍 ) } ∪ ran ( 𝑗 ∈ { 𝑖 ∈ ( 1 ... 𝑚 ) ∣ 𝑆 ∈ ( ( ( 𝐶𝑖 ) ‘ 𝑍 ) [,) ( ( 𝐷𝑖 ) ‘ 𝑍 ) ) } ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) )
695 eqid inf ( ( { ( 𝐵𝑍 ) } ∪ ran ( 𝑗 ∈ { ∈ ( 1 ... 𝑚 ) ∣ 𝑆 ∈ ( ( ( 𝐶 ) ‘ 𝑍 ) [,) ( ( 𝐷 ) ‘ 𝑍 ) ) } ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) , ℝ , < ) = inf ( ( { ( 𝐵𝑍 ) } ∪ ran ( 𝑗 ∈ { ∈ ( 1 ... 𝑚 ) ∣ 𝑆 ∈ ( ( ( 𝐶 ) ‘ 𝑍 ) [,) ( ( 𝐷 ) ‘ 𝑍 ) ) } ↦ ( ( 𝐷𝑗 ) ‘ 𝑍 ) ) ) , ℝ , < )
696 1 569 570 571 5 572 573 574 575 576 577 578 585 594 16 595 605 606 607 608 609 680 684 694 695 hoidmvlelem2 ( ( 𝜑𝑚 ∈ ℕ ∧ 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) ) → ∃ 𝑢𝑈 𝑆 < 𝑢 )
697 696 3exp ( 𝜑 → ( 𝑚 ∈ ℕ → ( 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) → ∃ 𝑢𝑈 𝑆 < 𝑢 ) ) )
698 697 rexlimdv ( 𝜑 → ( ∃ 𝑚 ∈ ℕ 𝐺 ≤ ( ( 1 + 𝐸 ) · Σ 𝑗 ∈ ( 1 ... 𝑚 ) ( 𝑃𝑗 ) ) → ∃ 𝑢𝑈 𝑆 < 𝑢 ) )
699 568 698 mpd ( 𝜑 → ∃ 𝑢𝑈 𝑆 < 𝑢 )