Metamath Proof Explorer

Theorem esum2d

Description: Write a double extended sum as a sum over a two-dimensional region. Note that B ( j ) is a function of j . This can be seen as "slicing" the relation A . (Contributed by Thierry Arnoux, 17-May-2020)

Ref Expression
Hypotheses esum2d.0 ⊢ Ⅎ 𝑘 𝐹
esum2d.1 ⊢ ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ → 𝐹 = 𝐶 )
esum2d.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
esum2d.3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 )
esum2d.4 ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ) → 𝐶 ∈ ( 0 [,] +∞ ) )
Assertion esum2d ( 𝜑 → Σ* 𝑗 ∈ 𝐴 Σ* 𝑘 ∈ 𝐵 𝐶 = Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 )

Proof

Step Hyp Ref Expression
1 esum2d.0 ⊢ Ⅎ 𝑘 𝐹
2 esum2d.1 ⊢ ( 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ → 𝐹 = 𝐶 )
3 esum2d.2 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
4 esum2d.3 ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐵 ∈ 𝑊 )
5 esum2d.4 ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵 ) ) → 𝐶 ∈ ( 0 [,] +∞ ) )
6 xrltso ⊢ < Or ℝ*
7 6 a1i ⊢ ( 𝜑 → < Or ℝ* )
8 nfv ⊢ Ⅎ 𝑐 𝜑
9 nfcv ⊢ Ⅎ 𝑐 𝑠
10 nfmpt1 ⊢ Ⅎ 𝑐 ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) )
11 10 nfrn ⊢ Ⅎ 𝑐 ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) )
12 9 11 nfel ⊢ Ⅎ 𝑐 𝑠 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) )
13 8 12 nfan ⊢ Ⅎ 𝑐 ( 𝜑 ∧ 𝑠 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) )
14 iccssxr ⊢ ( 0 [,] +∞ ) ⊆ ℝ*
15 xrge0base ⊢ ( 0 [,] +∞ ) = ( Base ‘ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) )
16 xrge0cmn ⊢ ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ CMnd
17 16 a1i ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) → ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ CMnd )
18 simpr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) → 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) )
19 18 elin2d ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) → 𝑐 ∈ Fin )
20 simpll ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑧 ∈ 𝑐 ) → 𝜑 )
21 18 elin1d ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) → 𝑐 ∈ 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) )
22 21 adantr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑧 ∈ 𝑐 ) → 𝑐 ∈ 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) )
23 vex ⊢ 𝑐 ∈ V
24 23 elpw ⊢ ( 𝑐 ∈ 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ↔ 𝑐 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) )
25 22 24 sylib ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑧 ∈ 𝑐 ) → 𝑐 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) )
26 simpr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑧 ∈ 𝑐 ) → 𝑧 ∈ 𝑐 )
27 25 26 sseldd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑧 ∈ 𝑐 ) → 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) )
28 nfv ⊢ Ⅎ 𝑗 𝜑
29 nfcv ⊢ Ⅎ 𝑗 𝑧
30 nfiu1 ⊢ Ⅎ 𝑗 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 )
31 29 30 nfel ⊢ Ⅎ 𝑗 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 )
32 28 31 nfan ⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) )
33 nfv ⊢ Ⅎ 𝑘 ( ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) )
34 nfcv ⊢ Ⅎ 𝑘 ( 0 [,] +∞ )
35 1 34 nfel ⊢ Ⅎ 𝑘 𝐹 ∈ ( 0 [,] +∞ )
36 2 adantl ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) ∧ 𝑘 ∈ 𝐵 ) ∧ 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ) → 𝐹 = 𝐶 )
37 simp-5l ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) ∧ 𝑘 ∈ 𝐵 ) ∧ 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ) → 𝜑 )
38 simp-4r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) ∧ 𝑘 ∈ 𝐵 ) ∧ 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ) → 𝑗 ∈ 𝐴 )
39 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) ∧ 𝑘 ∈ 𝐵 ) ∧ 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ) → 𝑘 ∈ 𝐵 )
40 37 38 39 5 syl12anc ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) ∧ 𝑘 ∈ 𝐵 ) ∧ 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ) → 𝐶 ∈ ( 0 [,] +∞ ) )
41 36 40 eqeltrd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) ∧ 𝑘 ∈ 𝐵 ) ∧ 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ) → 𝐹 ∈ ( 0 [,] +∞ ) )
42 elsnxp ⊢ ( 𝑗 ∈ 𝐴 → ( 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ↔ ∃ 𝑘 ∈ 𝐵 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ ) )
43 42 biimpa ⊢ ( ( 𝑗 ∈ 𝐴 ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) → ∃ 𝑘 ∈ 𝐵 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ )
44 43 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) → ∃ 𝑘 ∈ 𝐵 𝑧 = ⟨ 𝑗 , 𝑘 ⟩ )
45 33 35 41 44 r19.29af2 ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑗 } × 𝐵 ) ) → 𝐹 ∈ ( 0 [,] +∞ ) )
46 simpr ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) → 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) )
47 eliun ⊢ ( 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ↔ ∃ 𝑗 ∈ 𝐴 𝑧 ∈ ( { 𝑗 } × 𝐵 ) )
48 46 47 sylib ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) → ∃ 𝑗 ∈ 𝐴 𝑧 ∈ ( { 𝑗 } × 𝐵 ) )
49 32 45 48 r19.29af ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) → 𝐹 ∈ ( 0 [,] +∞ ) )
50 20 27 49 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑧 ∈ 𝑐 ) → 𝐹 ∈ ( 0 [,] +∞ ) )
51 50 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) → ∀ 𝑧 ∈ 𝑐 𝐹 ∈ ( 0 [,] +∞ ) )
52 15 17 19 51 gsummptcl ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ∈ ( 0 [,] +∞ ) )
53 14 52 sselid ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ∈ ℝ* )
54 53 ralrimiva ⊢ ( 𝜑 → ∀ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ∈ ℝ* )
55 eqid ⊢ ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) = ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) )
56 55 rnmptss ⊢ ( ∀ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ∈ ℝ* → ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ⊆ ℝ* )
57 54 56 syl ⊢ ( 𝜑 → ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ⊆ ℝ* )
58 57 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑠 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) → ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ⊆ ℝ* )
59 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑠 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) → 𝑠 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) )
60 58 59 sseldd ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑠 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) → 𝑠 ∈ ℝ* )
61 snex ⊢ { 𝑗 } ∈ V
62 xpexg ⊢ ( ( { 𝑗 } ∈ V ∧ 𝐵 ∈ 𝑊 ) → ( { 𝑗 } × 𝐵 ) ∈ V )
63 61 4 62 sylancr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( { 𝑗 } × 𝐵 ) ∈ V )
64 63 ralrimiva ⊢ ( 𝜑 → ∀ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∈ V )
65 iunexg ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∈ V ) → ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∈ V )
66 3 64 65 syl2anc ⊢ ( 𝜑 → ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∈ V )
67 49 ralrimiva ⊢ ( 𝜑 → ∀ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 ∈ ( 0 [,] +∞ ) )
68 nfcv ⊢ Ⅎ 𝑧 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 )
69 68 esumcl ⊢ ( ( ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∈ V ∧ ∀ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 ∈ ( 0 [,] +∞ ) ) → Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 ∈ ( 0 [,] +∞ ) )
70 66 67 69 syl2anc ⊢ ( 𝜑 → Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 ∈ ( 0 [,] +∞ ) )
71 14 70 sselid ⊢ ( 𝜑 → Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 ∈ ℝ* )
72 71 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑠 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) → Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 ∈ ℝ* )
73 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑠 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) → 𝑠 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) )
74 nfv ⊢ Ⅎ 𝑧 ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) )
75 nfcv ⊢ Ⅎ 𝑧 𝑐
76 74 75 19 50 esumgsum ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) → Σ* 𝑧 ∈ 𝑐 𝐹 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) )
77 66 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) → ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∈ V )
78 49 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) → 𝐹 ∈ ( 0 [,] +∞ ) )
79 21 24 sylib ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) → 𝑐 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) )
80 74 77 78 79 esummono ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) → Σ* 𝑧 ∈ 𝑐 𝐹 ≤ Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 )
81 76 80 eqbrtrrd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ≤ Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 )
82 81 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ≤ Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 )
83 82 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑠 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ≤ Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 )
84 73 83 eqbrtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑠 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) → 𝑠 ≤ Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 )
85 xrlenlt ⊢ ( ( 𝑠 ∈ ℝ* ∧ Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 ∈ ℝ* ) → ( 𝑠 ≤ Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 ↔ ¬ Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 < 𝑠 ) )
86 85 biimpa ⊢ ( ( ( 𝑠 ∈ ℝ* ∧ Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 ∈ ℝ* ) ∧ 𝑠 ≤ Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 ) → ¬ Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 < 𝑠 )
87 60 72 84 86 syl21anc ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑠 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) → ¬ Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 < 𝑠 )
88 simpr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ) → 𝑠 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) )
89 ovex ⊢ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ∈ V
90 55 89 elrnmpti ⊢ ( 𝑠 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ↔ ∃ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) 𝑠 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) )
91 88 90 sylib ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ) → ∃ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) 𝑠 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) )
92 13 87 91 r19.29af ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ) → ¬ Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 < 𝑠 )
93 92 ralrimiva ⊢ ( 𝜑 → ∀ 𝑠 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ¬ Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 < 𝑠 )
94 nfv ⊢ Ⅎ 𝑐 ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑠 < Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 )
95 nfv ⊢ Ⅎ 𝑐 𝑠 < 𝑡
96 11 95 nfrex ⊢ Ⅎ 𝑐 ∃ 𝑡 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) 𝑠 < 𝑡
97 76 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) → Σ* 𝑧 ∈ 𝑐 𝐹 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) )
98 97 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑠 < Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) → Σ* 𝑧 ∈ 𝑐 𝐹 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) )
99 98 adantr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑠 < Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑠 < Σ* 𝑧 ∈ 𝑐 𝐹 ) → Σ* 𝑧 ∈ 𝑐 𝐹 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) )
100 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑠 < Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑠 < Σ* 𝑧 ∈ 𝑐 𝐹 ) → 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) )
101 89 a1i ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑠 < Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑠 < Σ* 𝑧 ∈ 𝑐 𝐹 ) → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ∈ V )
102 55 elrnmpt1 ⊢ ( ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ∧ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ∈ V ) → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) )
103 100 101 102 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑠 < Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑠 < Σ* 𝑧 ∈ 𝑐 𝐹 ) → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) )
104 99 103 eqeltrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑠 < Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑠 < Σ* 𝑧 ∈ 𝑐 𝐹 ) → Σ* 𝑧 ∈ 𝑐 𝐹 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) )
105 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑠 < Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑠 < Σ* 𝑧 ∈ 𝑐 𝐹 ) ∧ 𝑡 = Σ* 𝑧 ∈ 𝑐 𝐹 ) → 𝑡 = Σ* 𝑧 ∈ 𝑐 𝐹 )
106 105 breq2d ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑠 < Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑠 < Σ* 𝑧 ∈ 𝑐 𝐹 ) ∧ 𝑡 = Σ* 𝑧 ∈ 𝑐 𝐹 ) → ( 𝑠 < 𝑡 ↔ 𝑠 < Σ* 𝑧 ∈ 𝑐 𝐹 ) )
107 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑠 < Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑠 < Σ* 𝑧 ∈ 𝑐 𝐹 ) → 𝑠 < Σ* 𝑧 ∈ 𝑐 𝐹 )
108 104 106 107 rspcedvd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑠 < Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑠 < Σ* 𝑧 ∈ 𝑐 𝐹 ) → ∃ 𝑡 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) 𝑠 < 𝑡 )
109 nfv ⊢ Ⅎ 𝑧 ( 𝜑 ∧ 𝑠 ∈ ℝ* )
110 nfcv ⊢ Ⅎ 𝑧 𝑠
111 nfcv ⊢ Ⅎ 𝑧 <
112 68 nfesum1 ⊢ Ⅎ 𝑧 Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹
113 110 111 112 nfbr ⊢ Ⅎ 𝑧 𝑠 < Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹
114 109 113 nfan ⊢ Ⅎ 𝑧 ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑠 < Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 )
115 66 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑠 < Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 ) → ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∈ V )
116 49 3ad2antr3 ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ℝ* ∧ 𝑠 < Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) ) → 𝐹 ∈ ( 0 [,] +∞ ) )
117 116 3anassrs ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑠 < Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 ) ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) → 𝐹 ∈ ( 0 [,] +∞ ) )
118 simplr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑠 < Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 ) → 𝑠 ∈ ℝ* )
119 simpr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑠 < Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 ) → 𝑠 < Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 )
120 114 115 117 118 119 esumlub ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑠 < Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 ) → ∃ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) 𝑠 < Σ* 𝑧 ∈ 𝑐 𝐹 )
121 94 96 108 120 r19.29af2 ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑠 < Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 ) → ∃ 𝑡 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) 𝑠 < 𝑡 )
122 121 ex ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) → ( 𝑠 < Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 → ∃ 𝑡 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) 𝑠 < 𝑡 ) )
123 122 ralrimiva ⊢ ( 𝜑 → ∀ 𝑠 ∈ ℝ* ( 𝑠 < Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 → ∃ 𝑡 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) 𝑠 < 𝑡 ) )
124 93 123 jca ⊢ ( 𝜑 → ( ∀ 𝑠 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ¬ Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 < 𝑠 ∧ ∀ 𝑠 ∈ ℝ* ( 𝑠 < Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 → ∃ 𝑡 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) 𝑠 < 𝑡 ) ) )
125 simpr ⊢ ( ( 𝜑 ∧ 𝑟 = Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 ) → 𝑟 = Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 )
126 125 breq1d ⊢ ( ( 𝜑 ∧ 𝑟 = Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 ) → ( 𝑟 < 𝑠 ↔ Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 < 𝑠 ) )
127 126 notbid ⊢ ( ( 𝜑 ∧ 𝑟 = Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 ) → ( ¬ 𝑟 < 𝑠 ↔ ¬ Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 < 𝑠 ) )
128 127 ralbidv ⊢ ( ( 𝜑 ∧ 𝑟 = Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 ) → ( ∀ 𝑠 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ¬ 𝑟 < 𝑠 ↔ ∀ 𝑠 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ¬ Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 < 𝑠 ) )
129 125 breq2d ⊢ ( ( 𝜑 ∧ 𝑟 = Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 ) → ( 𝑠 < 𝑟 ↔ 𝑠 < Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 ) )
130 129 imbi1d ⊢ ( ( 𝜑 ∧ 𝑟 = Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 ) → ( ( 𝑠 < 𝑟 → ∃ 𝑡 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) 𝑠 < 𝑡 ) ↔ ( 𝑠 < Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 → ∃ 𝑡 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) 𝑠 < 𝑡 ) ) )
131 130 ralbidv ⊢ ( ( 𝜑 ∧ 𝑟 = Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 ) → ( ∀ 𝑠 ∈ ℝ* ( 𝑠 < 𝑟 → ∃ 𝑡 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) 𝑠 < 𝑡 ) ↔ ∀ 𝑠 ∈ ℝ* ( 𝑠 < Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 → ∃ 𝑡 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) 𝑠 < 𝑡 ) ) )
132 128 131 anbi12d ⊢ ( ( 𝜑 ∧ 𝑟 = Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 ) → ( ( ∀ 𝑠 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ¬ 𝑟 < 𝑠 ∧ ∀ 𝑠 ∈ ℝ* ( 𝑠 < 𝑟 → ∃ 𝑡 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) 𝑠 < 𝑡 ) ) ↔ ( ∀ 𝑠 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ¬ Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 < 𝑠 ∧ ∀ 𝑠 ∈ ℝ* ( 𝑠 < Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 → ∃ 𝑡 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) 𝑠 < 𝑡 ) ) ) )
133 71 132 rspcedv ⊢ ( 𝜑 → ( ( ∀ 𝑠 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ¬ Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 < 𝑠 ∧ ∀ 𝑠 ∈ ℝ* ( 𝑠 < Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 → ∃ 𝑡 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) 𝑠 < 𝑡 ) ) → ∃ 𝑟 ∈ ℝ* ( ∀ 𝑠 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ¬ 𝑟 < 𝑠 ∧ ∀ 𝑠 ∈ ℝ* ( 𝑠 < 𝑟 → ∃ 𝑡 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) 𝑠 < 𝑡 ) ) ) )
134 124 133 mpd ⊢ ( 𝜑 → ∃ 𝑟 ∈ ℝ* ( ∀ 𝑠 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ¬ 𝑟 < 𝑠 ∧ ∀ 𝑠 ∈ ℝ* ( 𝑠 < 𝑟 → ∃ 𝑡 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) 𝑠 < 𝑡 ) ) )
135 7 134 supcl ⊢ ( 𝜑 → sup ( ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) , ℝ* , < ) ∈ ℝ* )
136 nfv ⊢ Ⅎ 𝑎 𝜑
137 nfcv ⊢ Ⅎ 𝑎 𝑠
138 nfmpt1 ⊢ Ⅎ 𝑎 ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) )
139 138 nfrn ⊢ Ⅎ 𝑎 ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) )
140 137 139 nfel ⊢ Ⅎ 𝑎 𝑠 ∈ ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) )
141 136 140 nfan ⊢ Ⅎ 𝑎 ( 𝜑 ∧ 𝑠 ∈ ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) ) )
142 simpr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) )
143 simpll ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑗 ∈ 𝑎 ) → 𝜑 )
144 142 elin1d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑎 ∈ 𝒫 𝐴 )
145 elpwi ⊢ ( 𝑎 ∈ 𝒫 𝐴 → 𝑎 ⊆ 𝐴 )
146 144 145 syl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑎 ⊆ 𝐴 )
147 146 sselda ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑗 ∈ 𝑎 ) → 𝑗 ∈ 𝐴 )
148 143 147 4 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑗 ∈ 𝑎 ) → 𝐵 ∈ 𝑊 )
149 143 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑗 ∈ 𝑎 ∧ 𝑘 ∈ 𝐵 ) ) → 𝜑 )
150 147 adantrr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑗 ∈ 𝑎 ∧ 𝑘 ∈ 𝐵 ) ) → 𝑗 ∈ 𝐴 )
151 simprr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑗 ∈ 𝑎 ∧ 𝑘 ∈ 𝐵 ) ) → 𝑘 ∈ 𝐵 )
152 149 150 151 5 syl12anc ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑗 ∈ 𝑎 ∧ 𝑘 ∈ 𝐵 ) ) → 𝐶 ∈ ( 0 [,] +∞ ) )
153 142 elin2d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑎 ∈ Fin )
154 1 2 142 148 152 153 esum2dlem ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ* 𝑗 ∈ 𝑎 Σ* 𝑘 ∈ 𝐵 𝐶 = Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝑎 ( { 𝑗 } × 𝐵 ) 𝐹 )
155 nfv ⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) )
156 nfcv ⊢ Ⅎ 𝑗 𝑎
157 5 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
158 157 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ∀ 𝑘 ∈ 𝐵 𝐶 ∈ ( 0 [,] +∞ ) )
159 nfcv ⊢ Ⅎ 𝑘 𝐵
160 159 esumcl ⊢ ( ( 𝐵 ∈ 𝑊 ∧ ∀ 𝑘 ∈ 𝐵 𝐶 ∈ ( 0 [,] +∞ ) ) → Σ* 𝑘 ∈ 𝐵 𝐶 ∈ ( 0 [,] +∞ ) )
161 4 158 160 syl2anc ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → Σ* 𝑘 ∈ 𝐵 𝐶 ∈ ( 0 [,] +∞ ) )
162 143 147 161 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑗 ∈ 𝑎 ) → Σ* 𝑘 ∈ 𝐵 𝐶 ∈ ( 0 [,] +∞ ) )
163 155 156 153 162 esumgsum ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ* 𝑗 ∈ 𝑎 Σ* 𝑘 ∈ 𝐵 𝐶 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) )
164 154 163 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝑎 ( { 𝑗 } × 𝐵 ) 𝐹 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) )
165 nfv ⊢ Ⅎ 𝑧 ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) )
166 66 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∈ V )
167 49 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ) → 𝐹 ∈ ( 0 [,] +∞ ) )
168 iunss1 ⊢ ( 𝑎 ⊆ 𝐴 → ∪ 𝑗 ∈ 𝑎 ( { 𝑗 } × 𝐵 ) ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) )
169 146 168 syl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ∪ 𝑗 ∈ 𝑎 ( { 𝑗 } × 𝐵 ) ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) )
170 165 166 167 169 esummono ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝑎 ( { 𝑗 } × 𝐵 ) 𝐹 ≤ Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 )
171 164 170 eqbrtrrd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) ≤ Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 )
172 16 a1i ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ CMnd )
173 162 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ∀ 𝑗 ∈ 𝑎 Σ* 𝑘 ∈ 𝐵 𝐶 ∈ ( 0 [,] +∞ ) )
174 15 172 153 173 gsummptcl ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) ∈ ( 0 [,] +∞ ) )
175 14 174 sselid ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) ∈ ℝ* )
176 71 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 ∈ ℝ* )
177 xrlenlt ⊢ ( ( ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) ∈ ℝ* ∧ Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 ∈ ℝ* ) → ( ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) ≤ Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 ↔ ¬ Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 < ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) ) )
178 175 176 177 syl2anc ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) ≤ Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 ↔ ¬ Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 < ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) ) )
179 171 178 mpbid ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ¬ Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 < ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) )
180 nfv ⊢ Ⅎ 𝑧 𝜑
181 eqidd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) )
182 180 68 66 49 181 esumval ⊢ ( 𝜑 → Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 = sup ( ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) , ℝ* , < ) )
183 182 adantr ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 = sup ( ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) , ℝ* , < ) )
184 183 breq1d ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 < ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) ↔ sup ( ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) , ℝ* , < ) < ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) ) )
185 179 184 mtbid ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ¬ sup ( ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) , ℝ* , < ) < ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) )
186 185 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) ) ) ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ¬ sup ( ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) , ℝ* , < ) < ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) )
187 186 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) ) ) ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑠 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) ) → ¬ sup ( ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) , ℝ* , < ) < ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) )
188 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) ) ) ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑠 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) ) → 𝑠 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) )
189 188 breq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) ) ) ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑠 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) ) → ( sup ( ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) , ℝ* , < ) < 𝑠 ↔ sup ( ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) , ℝ* , < ) < ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) ) )
190 189 notbid ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) ) ) ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑠 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) ) → ( ¬ sup ( ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) , ℝ* , < ) < 𝑠 ↔ ¬ sup ( ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) , ℝ* , < ) < ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) ) )
191 187 190 mpbird ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) ) ) ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑠 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) ) → ¬ sup ( ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) , ℝ* , < ) < 𝑠 )
192 eqid ⊢ ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) ) = ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) )
193 ovex ⊢ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) ∈ V
194 192 193 elrnmpti ⊢ ( 𝑠 ∈ ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) ) ↔ ∃ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝑠 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) )
195 194 biimpi ⊢ ( 𝑠 ∈ ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) ) → ∃ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝑠 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) )
196 195 adantl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) ) ) → ∃ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) 𝑠 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) )
197 141 191 196 r19.29af ⊢ ( ( 𝜑 ∧ 𝑠 ∈ ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) ) ) → ¬ sup ( ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) , ℝ* , < ) < 𝑠 )
198 9 nfel1 ⊢ Ⅎ 𝑐 𝑠 ∈ ℝ*
199 nfcv ⊢ Ⅎ 𝑐 <
200 nfcv ⊢ Ⅎ 𝑐 ℝ*
201 11 200 199 nfsup ⊢ Ⅎ 𝑐 sup ( ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) , ℝ* , < )
202 9 199 201 nfbr ⊢ Ⅎ 𝑐 𝑠 < sup ( ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) , ℝ* , < )
203 198 202 nfan ⊢ Ⅎ 𝑐 ( 𝑠 ∈ ℝ* ∧ 𝑠 < sup ( ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) , ℝ* , < ) )
204 8 203 nfan ⊢ Ⅎ 𝑐 ( 𝜑 ∧ ( 𝑠 ∈ ℝ* ∧ 𝑠 < sup ( ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) , ℝ* , < ) ) )
205 nfcv ⊢ Ⅎ 𝑐 𝑢
206 205 11 nfel ⊢ Ⅎ 𝑐 𝑢 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) )
207 204 206 nfan ⊢ Ⅎ 𝑐 ( ( 𝜑 ∧ ( 𝑠 ∈ ℝ* ∧ 𝑠 < sup ( ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) , ℝ* , < ) ) ) ∧ 𝑢 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) )
208 nfv ⊢ Ⅎ 𝑐 𝑠 < 𝑢
209 207 208 nfan ⊢ Ⅎ 𝑐 ( ( ( 𝜑 ∧ ( 𝑠 ∈ ℝ* ∧ 𝑠 < sup ( ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) , ℝ* , < ) ) ) ∧ 𝑢 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ) ∧ 𝑠 < 𝑢 )
210 simp-5l ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ℝ* ∧ 𝑠 < sup ( ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) , ℝ* , < ) ) ) ∧ 𝑢 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ) ∧ 𝑠 < 𝑢 ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑢 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) → 𝜑 )
211 simpr1l ⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ℝ* ∧ 𝑠 < sup ( ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) , ℝ* , < ) ) ∧ 𝑢 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ∧ ( 𝑠 < 𝑢 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ∧ 𝑢 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ) ) → 𝑠 ∈ ℝ* )
212 211 3anassrs ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ℝ* ∧ 𝑠 < sup ( ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) , ℝ* , < ) ) ) ∧ 𝑢 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ) ∧ ( 𝑠 < 𝑢 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ∧ 𝑢 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ) → 𝑠 ∈ ℝ* )
213 212 3anassrs ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ℝ* ∧ 𝑠 < sup ( ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) , ℝ* , < ) ) ) ∧ 𝑢 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ) ∧ 𝑠 < 𝑢 ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑢 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) → 𝑠 ∈ ℝ* )
214 210 213 jca ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ℝ* ∧ 𝑠 < sup ( ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) , ℝ* , < ) ) ) ∧ 𝑢 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ) ∧ 𝑠 < 𝑢 ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑢 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) → ( 𝜑 ∧ 𝑠 ∈ ℝ* ) )
215 simpr1r ⊢ ( ( 𝜑 ∧ ( ( 𝑠 ∈ ℝ* ∧ 𝑠 < sup ( ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) , ℝ* , < ) ) ∧ 𝑢 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ∧ ( 𝑠 < 𝑢 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ∧ 𝑢 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ) ) → 𝑠 < sup ( ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) , ℝ* , < ) )
216 215 3anassrs ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ℝ* ∧ 𝑠 < sup ( ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) , ℝ* , < ) ) ) ∧ 𝑢 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ) ∧ ( 𝑠 < 𝑢 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ∧ 𝑢 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ) → 𝑠 < sup ( ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) , ℝ* , < ) )
217 216 3anassrs ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ℝ* ∧ 𝑠 < sup ( ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) , ℝ* , < ) ) ) ∧ 𝑢 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ) ∧ 𝑠 < 𝑢 ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑢 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) → 𝑠 < sup ( ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) , ℝ* , < ) )
218 214 217 jca ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ℝ* ∧ 𝑠 < sup ( ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) , ℝ* , < ) ) ) ∧ 𝑢 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ) ∧ 𝑠 < 𝑢 ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑢 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) → ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑠 < sup ( ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) , ℝ* , < ) ) )
219 simpllr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ℝ* ∧ 𝑠 < sup ( ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) , ℝ* , < ) ) ) ∧ 𝑢 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ) ∧ 𝑠 < 𝑢 ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑢 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) → 𝑠 < 𝑢 )
220 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ℝ* ∧ 𝑠 < sup ( ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) , ℝ* , < ) ) ) ∧ 𝑢 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ) ∧ 𝑠 < 𝑢 ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑢 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) → 𝑢 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) )
221 219 220 breqtrd ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ℝ* ∧ 𝑠 < sup ( ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) , ℝ* , < ) ) ) ∧ 𝑢 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ) ∧ 𝑠 < 𝑢 ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑢 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) → 𝑠 < ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) )
222 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ℝ* ∧ 𝑠 < sup ( ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) , ℝ* , < ) ) ) ∧ 𝑢 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ) ∧ 𝑠 < 𝑢 ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑢 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) → 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) )
223 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑠 < ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) → 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) )
224 223 elin1d ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑠 < ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) → 𝑐 ∈ 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) )
225 elpwi ⊢ ( 𝑐 ∈ 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) → 𝑐 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) )
226 dmss ⊢ ( 𝑐 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) → dom 𝑐 ⊆ dom ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) )
227 dmiun ⊢ dom ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) = ∪ 𝑗 ∈ 𝐴 dom ( { 𝑗 } × 𝐵 )
228 226 227 sseqtrdi ⊢ ( 𝑐 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) → dom 𝑐 ⊆ ∪ 𝑗 ∈ 𝐴 dom ( { 𝑗 } × 𝐵 ) )
229 dmxpss ⊢ dom ( { 𝑗 } × 𝐵 ) ⊆ { 𝑗 }
230 229 a1i ⊢ ( 𝑗 ∈ 𝐴 → dom ( { 𝑗 } × 𝐵 ) ⊆ { 𝑗 } )
231 snssi ⊢ ( 𝑗 ∈ 𝐴 → { 𝑗 } ⊆ 𝐴 )
232 230 231 sstrd ⊢ ( 𝑗 ∈ 𝐴 → dom ( { 𝑗 } × 𝐵 ) ⊆ 𝐴 )
233 232 rgen ⊢ ∀ 𝑗 ∈ 𝐴 dom ( { 𝑗 } × 𝐵 ) ⊆ 𝐴
234 iunss ⊢ ( ∪ 𝑗 ∈ 𝐴 dom ( { 𝑗 } × 𝐵 ) ⊆ 𝐴 ↔ ∀ 𝑗 ∈ 𝐴 dom ( { 𝑗 } × 𝐵 ) ⊆ 𝐴 )
235 233 234 mpbir ⊢ ∪ 𝑗 ∈ 𝐴 dom ( { 𝑗 } × 𝐵 ) ⊆ 𝐴
236 228 235 sstrdi ⊢ ( 𝑐 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) → dom 𝑐 ⊆ 𝐴 )
237 23 dmex ⊢ dom 𝑐 ∈ V
238 237 elpw ⊢ ( dom 𝑐 ∈ 𝒫 𝐴 ↔ dom 𝑐 ⊆ 𝐴 )
239 236 238 sylibr ⊢ ( 𝑐 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) → dom 𝑐 ∈ 𝒫 𝐴 )
240 224 225 239 3syl ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑠 < ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) → dom 𝑐 ∈ 𝒫 𝐴 )
241 223 elin2d ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑠 < ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) → 𝑐 ∈ Fin )
242 dmfi ⊢ ( 𝑐 ∈ Fin → dom 𝑐 ∈ Fin )
243 241 242 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑠 < ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) → dom 𝑐 ∈ Fin )
244 240 243 elind ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑠 < ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) → dom 𝑐 ∈ ( 𝒫 𝐴 ∩ Fin ) )
245 ovex ⊢ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ dom 𝑐 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) ∈ V
246 245 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑠 < ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ dom 𝑐 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) ∈ V )
247 mpteq1 ⊢ ( 𝑎 = dom 𝑐 → ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) = ( 𝑗 ∈ dom 𝑐 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) )
248 247 oveq2d ⊢ ( 𝑎 = dom 𝑐 → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ dom 𝑐 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) )
249 192 248 elrnmpt1s ⊢ ( ( dom 𝑐 ∈ ( 𝒫 𝐴 ∩ Fin ) ∧ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ dom 𝑐 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) ∈ V ) → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ dom 𝑐 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) ∈ ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) ) )
250 244 246 249 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑠 < ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ dom 𝑐 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) ∈ ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) ) )
251 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑠 < ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑡 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ dom 𝑐 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) ) → 𝑡 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ dom 𝑐 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) )
252 251 breq2d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑠 < ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑡 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ dom 𝑐 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) ) → ( 𝑠 < 𝑡 ↔ 𝑠 < ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ dom 𝑐 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) ) )
253 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑠 < ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) → 𝑠 ∈ ℝ* )
254 16 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑠 < ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) → ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) ∈ CMnd )
255 nfcv ⊢ Ⅎ 𝑧 ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) )
256 nfcv ⊢ Ⅎ 𝑧 Σg
257 nfmpt1 ⊢ Ⅎ 𝑧 ( 𝑧 ∈ 𝑐 ↦ 𝐹 )
258 255 256 257 nfov ⊢ Ⅎ 𝑧 ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) )
259 110 111 258 nfbr ⊢ Ⅎ 𝑧 𝑠 < ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) )
260 109 259 nfan ⊢ Ⅎ 𝑧 ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑠 < ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) )
261 nfv ⊢ Ⅎ 𝑧 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin )
262 260 261 nfan ⊢ Ⅎ 𝑧 ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑠 < ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) )
263 simp-4l ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑠 < ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑧 ∈ 𝑐 ) → 𝜑 )
264 224 225 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑠 < ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) → 𝑐 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) )
265 264 sselda ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑠 < ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑧 ∈ 𝑐 ) → 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) )
266 263 265 49 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑠 < ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑧 ∈ 𝑐 ) → 𝐹 ∈ ( 0 [,] +∞ ) )
267 266 ex ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑠 < ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) → ( 𝑧 ∈ 𝑐 → 𝐹 ∈ ( 0 [,] +∞ ) ) )
268 262 267 ralrimi ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑠 < ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) → ∀ 𝑧 ∈ 𝑐 𝐹 ∈ ( 0 [,] +∞ ) )
269 15 254 241 268 gsummptcl ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑠 < ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ∈ ( 0 [,] +∞ ) )
270 14 269 sselid ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑠 < ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ∈ ℝ* )
271 nfv ⊢ Ⅎ 𝑗 ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑠 < ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) )
272 nfcv ⊢ Ⅎ 𝑗 𝑐
273 30 nfpw ⊢ Ⅎ 𝑗 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 )
274 nfcv ⊢ Ⅎ 𝑗 Fin
275 273 274 nfin ⊢ Ⅎ 𝑗 ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin )
276 272 275 nfel ⊢ Ⅎ 𝑗 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin )
277 271 276 nfan ⊢ Ⅎ 𝑗 ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑠 < ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) )
278 simpll ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑗 ∈ dom 𝑐 ) → 𝜑 )
279 79 236 syl ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) → dom 𝑐 ⊆ 𝐴 )
280 279 sselda ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑗 ∈ dom 𝑐 ) → 𝑗 ∈ 𝐴 )
281 278 280 161 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑗 ∈ dom 𝑐 ) → Σ* 𝑘 ∈ 𝐵 𝐶 ∈ ( 0 [,] +∞ ) )
282 281 adantllr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑗 ∈ dom 𝑐 ) → Σ* 𝑘 ∈ 𝐵 𝐶 ∈ ( 0 [,] +∞ ) )
283 282 adantllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑠 < ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑗 ∈ dom 𝑐 ) → Σ* 𝑘 ∈ 𝐵 𝐶 ∈ ( 0 [,] +∞ ) )
284 283 ex ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑠 < ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) → ( 𝑗 ∈ dom 𝑐 → Σ* 𝑘 ∈ 𝐵 𝐶 ∈ ( 0 [,] +∞ ) ) )
285 277 284 ralrimi ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑠 < ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) → ∀ 𝑗 ∈ dom 𝑐 Σ* 𝑘 ∈ 𝐵 𝐶 ∈ ( 0 [,] +∞ ) )
286 15 254 243 285 gsummptcl ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑠 < ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ dom 𝑐 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) ∈ ( 0 [,] +∞ ) )
287 14 286 sselid ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑠 < ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ dom 𝑐 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) ∈ ℝ* )
288 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑠 < ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) → 𝑠 < ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) )
289 28 276 nfan ⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) )
290 id ⊢ ( 𝑐 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) → 𝑐 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) )
291 xpss ⊢ ( { 𝑗 } × 𝐵 ) ⊆ ( V × V )
292 291 rgenw ⊢ ∀ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ⊆ ( V × V )
293 iunss ⊢ ( ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ⊆ ( V × V ) ↔ ∀ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ⊆ ( V × V ) )
294 292 293 mpbir ⊢ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ⊆ ( V × V )
295 294 a1i ⊢ ( 𝑐 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) → ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ⊆ ( V × V ) )
296 290 295 sstrd ⊢ ( 𝑐 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) → 𝑐 ⊆ ( V × V ) )
297 79 296 syl ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) → 𝑐 ⊆ ( V × V ) )
298 df-rel ⊢ ( Rel 𝑐 ↔ 𝑐 ⊆ ( V × V ) )
299 297 298 sylibr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) → Rel 𝑐 )
300 1 289 15 2 299 19 17 50 gsummpt2d ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ dom 𝑐 ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ ( 𝑐 “ { 𝑗 } ) ↦ 𝐶 ) ) ) ) )
301 nfcv ⊢ Ⅎ 𝑗 dom 𝑐
302 237 a1i ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) → dom 𝑐 ∈ V )
303 278 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑗 ∈ dom 𝑐 ) ∧ 𝑘 ∈ ( 𝑐 “ { 𝑗 } ) ) → 𝜑 )
304 280 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑗 ∈ dom 𝑐 ) ∧ 𝑘 ∈ ( 𝑐 “ { 𝑗 } ) ) → 𝑗 ∈ 𝐴 )
305 79 adantr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑗 ∈ dom 𝑐 ) → 𝑐 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) )
306 imass1 ⊢ ( 𝑐 ⊆ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) → ( 𝑐 “ { 𝑗 } ) ⊆ ( ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) “ { 𝑗 } ) )
307 305 306 syl ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑗 ∈ dom 𝑐 ) → ( 𝑐 “ { 𝑗 } ) ⊆ ( ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) “ { 𝑗 } ) )
308 3 4 iunsnima ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → ( ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) “ { 𝑗 } ) = 𝐵 )
309 278 280 308 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑗 ∈ dom 𝑐 ) → ( ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) “ { 𝑗 } ) = 𝐵 )
310 307 309 sseqtrd ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑗 ∈ dom 𝑐 ) → ( 𝑐 “ { 𝑗 } ) ⊆ 𝐵 )
311 310 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑗 ∈ dom 𝑐 ) ∧ 𝑘 ∈ ( 𝑐 “ { 𝑗 } ) ) → 𝑘 ∈ 𝐵 )
312 303 304 311 5 syl12anc ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑗 ∈ dom 𝑐 ) ∧ 𝑘 ∈ ( 𝑐 “ { 𝑗 } ) ) → 𝐶 ∈ ( 0 [,] +∞ ) )
313 312 ralrimiva ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑗 ∈ dom 𝑐 ) → ∀ 𝑘 ∈ ( 𝑐 “ { 𝑗 } ) 𝐶 ∈ ( 0 [,] +∞ ) )
314 imaexg ⊢ ( 𝑐 ∈ V → ( 𝑐 “ { 𝑗 } ) ∈ V )
315 23 314 ax-mp ⊢ ( 𝑐 “ { 𝑗 } ) ∈ V
316 nfcv ⊢ Ⅎ 𝑘 ( 𝑐 “ { 𝑗 } )
317 316 esumcl ⊢ ( ( ( 𝑐 “ { 𝑗 } ) ∈ V ∧ ∀ 𝑘 ∈ ( 𝑐 “ { 𝑗 } ) 𝐶 ∈ ( 0 [,] +∞ ) ) → Σ* 𝑘 ∈ ( 𝑐 “ { 𝑗 } ) 𝐶 ∈ ( 0 [,] +∞ ) )
318 315 317 mpan ⊢ ( ∀ 𝑘 ∈ ( 𝑐 “ { 𝑗 } ) 𝐶 ∈ ( 0 [,] +∞ ) → Σ* 𝑘 ∈ ( 𝑐 “ { 𝑗 } ) 𝐶 ∈ ( 0 [,] +∞ ) )
319 313 318 syl ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑗 ∈ dom 𝑐 ) → Σ* 𝑘 ∈ ( 𝑐 “ { 𝑗 } ) 𝐶 ∈ ( 0 [,] +∞ ) )
320 nfv ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑗 ∈ dom 𝑐 )
321 278 280 4 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑗 ∈ dom 𝑐 ) → 𝐵 ∈ 𝑊 )
322 278 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑗 ∈ dom 𝑐 ) ∧ 𝑘 ∈ 𝐵 ) → 𝜑 )
323 280 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑗 ∈ dom 𝑐 ) ∧ 𝑘 ∈ 𝐵 ) → 𝑗 ∈ 𝐴 )
324 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑗 ∈ dom 𝑐 ) ∧ 𝑘 ∈ 𝐵 ) → 𝑘 ∈ 𝐵 )
325 322 323 324 5 syl12anc ⊢ ( ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑗 ∈ dom 𝑐 ) ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ( 0 [,] +∞ ) )
326 320 321 325 310 esummono ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑗 ∈ dom 𝑐 ) → Σ* 𝑘 ∈ ( 𝑐 “ { 𝑗 } ) 𝐶 ≤ Σ* 𝑘 ∈ 𝐵 𝐶 )
327 289 301 302 319 281 326 esumlef ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) → Σ* 𝑗 ∈ dom 𝑐 Σ* 𝑘 ∈ ( 𝑐 “ { 𝑗 } ) 𝐶 ≤ Σ* 𝑗 ∈ dom 𝑐 Σ* 𝑘 ∈ 𝐵 𝐶 )
328 19 242 syl ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) → dom 𝑐 ∈ Fin )
329 289 301 328 319 esumgsum ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) → Σ* 𝑗 ∈ dom 𝑐 Σ* 𝑘 ∈ ( 𝑐 “ { 𝑗 } ) 𝐶 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ dom 𝑐 ↦ Σ* 𝑘 ∈ ( 𝑐 “ { 𝑗 } ) 𝐶 ) ) )
330 19 adantr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑗 ∈ dom 𝑐 ) → 𝑐 ∈ Fin )
331 imafi2 ⊢ ( 𝑐 ∈ Fin → ( 𝑐 “ { 𝑗 } ) ∈ Fin )
332 330 331 syl ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑗 ∈ dom 𝑐 ) → ( 𝑐 “ { 𝑗 } ) ∈ Fin )
333 320 316 332 312 esumgsum ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑗 ∈ dom 𝑐 ) → Σ* 𝑘 ∈ ( 𝑐 “ { 𝑗 } ) 𝐶 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ ( 𝑐 “ { 𝑗 } ) ↦ 𝐶 ) ) )
334 289 333 mpteq2da ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) → ( 𝑗 ∈ dom 𝑐 ↦ Σ* 𝑘 ∈ ( 𝑐 “ { 𝑗 } ) 𝐶 ) = ( 𝑗 ∈ dom 𝑐 ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ ( 𝑐 “ { 𝑗 } ) ↦ 𝐶 ) ) ) )
335 334 oveq2d ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ dom 𝑐 ↦ Σ* 𝑘 ∈ ( 𝑐 “ { 𝑗 } ) 𝐶 ) ) = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ dom 𝑐 ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ ( 𝑐 “ { 𝑗 } ) ↦ 𝐶 ) ) ) ) )
336 329 335 eqtrd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) → Σ* 𝑗 ∈ dom 𝑐 Σ* 𝑘 ∈ ( 𝑐 “ { 𝑗 } ) 𝐶 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ dom 𝑐 ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ ( 𝑐 “ { 𝑗 } ) ↦ 𝐶 ) ) ) ) )
337 289 301 328 281 esumgsum ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) → Σ* 𝑗 ∈ dom 𝑐 Σ* 𝑘 ∈ 𝐵 𝐶 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ dom 𝑐 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) )
338 327 336 337 3brtr3d ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ dom 𝑐 ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑘 ∈ ( 𝑐 “ { 𝑗 } ) ↦ 𝐶 ) ) ) ) ≤ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ dom 𝑐 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) )
339 300 338 eqbrtrd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ≤ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ dom 𝑐 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) )
340 339 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ≤ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ dom 𝑐 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) )
341 340 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑠 < ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ≤ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ dom 𝑐 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) )
342 253 270 287 288 341 xrltletrd ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑠 < ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) → 𝑠 < ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ dom 𝑐 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) )
343 250 252 342 rspcedvd ⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑠 < ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) → ∃ 𝑡 ∈ ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) ) 𝑠 < 𝑡 )
344 343 adantllr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑠 ∈ ℝ* ) ∧ 𝑠 < sup ( ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) , ℝ* , < ) ) ∧ 𝑠 < ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) → ∃ 𝑡 ∈ ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) ) 𝑠 < 𝑡 )
345 218 221 222 344 syl21anc ⊢ ( ( ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ℝ* ∧ 𝑠 < sup ( ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) , ℝ* , < ) ) ) ∧ 𝑢 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ) ∧ 𝑠 < 𝑢 ) ∧ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ) ∧ 𝑢 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) → ∃ 𝑡 ∈ ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) ) 𝑠 < 𝑡 )
346 55 89 elrnmpti ⊢ ( 𝑢 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ↔ ∃ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) 𝑢 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) )
347 346 biimpi ⊢ ( 𝑢 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) → ∃ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) 𝑢 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) )
348 347 ad2antlr ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ℝ* ∧ 𝑠 < sup ( ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) , ℝ* , < ) ) ) ∧ 𝑢 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ) ∧ 𝑠 < 𝑢 ) → ∃ 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) 𝑢 = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) )
349 209 345 348 r19.29af ⊢ ( ( ( ( 𝜑 ∧ ( 𝑠 ∈ ℝ* ∧ 𝑠 < sup ( ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) , ℝ* , < ) ) ) ∧ 𝑢 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) ) ∧ 𝑠 < 𝑢 ) → ∃ 𝑡 ∈ ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) ) 𝑠 < 𝑡 )
350 7 134 suplub ⊢ ( 𝜑 → ( ( 𝑠 ∈ ℝ* ∧ 𝑠 < sup ( ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) , ℝ* , < ) ) → ∃ 𝑡 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) 𝑠 < 𝑡 ) )
351 350 imp ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ℝ* ∧ 𝑠 < sup ( ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) , ℝ* , < ) ) ) → ∃ 𝑡 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) 𝑠 < 𝑡 )
352 breq2 ⊢ ( 𝑡 = 𝑢 → ( 𝑠 < 𝑡 ↔ 𝑠 < 𝑢 ) )
353 352 cbvrexvw ⊢ ( ∃ 𝑡 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) 𝑠 < 𝑡 ↔ ∃ 𝑢 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) 𝑠 < 𝑢 )
354 351 353 sylib ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ℝ* ∧ 𝑠 < sup ( ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) , ℝ* , < ) ) ) → ∃ 𝑢 ∈ ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) 𝑠 < 𝑢 )
355 349 354 r19.29a ⊢ ( ( 𝜑 ∧ ( 𝑠 ∈ ℝ* ∧ 𝑠 < sup ( ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) , ℝ* , < ) ) ) → ∃ 𝑡 ∈ ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) ) 𝑠 < 𝑡 )
356 7 135 197 355 eqsupd ⊢ ( 𝜑 → sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) ) , ℝ* , < ) = sup ( ran ( 𝑐 ∈ ( 𝒫 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑧 ∈ 𝑐 ↦ 𝐹 ) ) ) , ℝ* , < ) )
357 nfcv ⊢ Ⅎ 𝑗 𝐴
358 eqidd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) = ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) )
359 28 357 3 161 358 esumval ⊢ ( 𝜑 → Σ* 𝑗 ∈ 𝐴 Σ* 𝑘 ∈ 𝐵 𝐶 = sup ( ran ( 𝑎 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( ( ℝ*𝑠 ↾s ( 0 [,] +∞ ) ) Σg ( 𝑗 ∈ 𝑎 ↦ Σ* 𝑘 ∈ 𝐵 𝐶 ) ) ) , ℝ* , < ) )
360 356 359 182 3eqtr4d ⊢ ( 𝜑 → Σ* 𝑗 ∈ 𝐴 Σ* 𝑘 ∈ 𝐵 𝐶 = Σ* 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐵 ) 𝐹 )