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