Metamath Proof Explorer

Theorem fsumiunle

Description: Upper bound for a sum of nonnegative terms over an indexed union. The inequality may be strict if the indexed union is non-disjoint, since in the right hand side, a summand may be counted several times. (Contributed by Thierry Arnoux, 1-Jan-2021)

Ref Expression
Hypotheses fsumiunle.1 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
fsumiunle.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ Fin )
fsumiunle.3 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ℝ )
fsumiunle.4 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐵 ) → 0 ≤ 𝐶 )
Assertion fsumiunle ( 𝜑 → Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝐶 ≤ Σ 𝑥 ∈ 𝐴 Σ 𝑘 ∈ 𝐵 𝐶 )

Proof

Step Hyp Ref Expression
1 fsumiunle.1 ⊢ ( 𝜑 → 𝐴 ∈ Fin )
2 fsumiunle.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ Fin )
3 fsumiunle.3 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ℝ )
4 fsumiunle.4 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐵 ) → 0 ≤ 𝐶 )
5 1 2 aciunf1 ⊢ ( 𝜑 → ∃ 𝑓 ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1→ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) )
6 f1f1orn ⊢ ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1→ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) → 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 )
7 6 anim1i ⊢ ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1→ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) → ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) )
8 f1f ⊢ ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1→ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) → 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 ⟶ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) )
9 8 frnd ⊢ ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1→ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) → ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) )
10 9 adantr ⊢ ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1→ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) → ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) )
11 7 10 jca ⊢ ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1→ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) → ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) )
12 11 eximi ⊢ ( ∃ 𝑓 ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1→ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) → ∃ 𝑓 ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) )
13 5 12 syl ⊢ ( 𝜑 → ∃ 𝑓 ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) )
14 csbeq1a ⊢ ( 𝑘 = 𝑦 → 𝐶 = ⦋ 𝑦 / 𝑘 ⦌ 𝐶 )
15 nfcv ⊢ Ⅎ 𝑦 ∪ 𝑥 ∈ 𝐴 𝐵
16 nfcv ⊢ Ⅎ 𝑘 ∪ 𝑥 ∈ 𝐴 𝐵
17 nfcv ⊢ Ⅎ 𝑦 𝐶
18 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ 𝑦 / 𝑘 ⦌ 𝐶
19 14 15 16 17 18 cbvsum ⊢ Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝐶 = Σ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ⦋ 𝑦 / 𝑘 ⦌ 𝐶
20 csbeq1 ⊢ ( 𝑦 = ( 2nd ‘ 𝑧 ) → ⦋ 𝑦 / 𝑘 ⦌ 𝐶 = ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 )
21 snfi ⊢ { 𝑥 } ∈ Fin
22 xpfi ⊢ ( ( { 𝑥 } ∈ Fin ∧ 𝐵 ∈ Fin ) → ( { 𝑥 } × 𝐵 ) ∈ Fin )
23 21 2 22 sylancr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( { 𝑥 } × 𝐵 ) ∈ Fin )
24 23 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ∈ Fin )
25 iunfi ⊢ ( ( 𝐴 ∈ Fin ∧ ∀ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ∈ Fin ) → ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ∈ Fin )
26 1 24 25 syl2anc ⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ∈ Fin )
27 26 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ) → ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ∈ Fin )
28 simprr ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ) → ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) )
29 27 28 ssfid ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ) → ran 𝑓 ∈ Fin )
30 simprl ⊢ ( ( 𝜑 ∧ ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ) → 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 )
31 f1ocnv ⊢ ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 → ◡ 𝑓 : ran 𝑓 –1-1-onto→ ∪ 𝑥 ∈ 𝐴 𝐵 )
32 30 31 syl ⊢ ( ( 𝜑 ∧ ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ) → ◡ 𝑓 : ran 𝑓 –1-1-onto→ ∪ 𝑥 ∈ 𝐴 𝐵 )
33 32 adantrlr ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ) → ◡ 𝑓 : ran 𝑓 –1-1-onto→ ∪ 𝑥 ∈ 𝐴 𝐵 )
34 nfv ⊢ Ⅎ 𝑥 𝜑
35 nfcv ⊢ Ⅎ 𝑥 𝑓
36 nfiu1 ⊢ Ⅎ 𝑥 ∪ 𝑥 ∈ 𝐴 𝐵
37 35 nfrn ⊢ Ⅎ 𝑥 ran 𝑓
38 35 36 37 nff1o ⊢ Ⅎ 𝑥 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓
39 nfv ⊢ Ⅎ 𝑥 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙
40 36 39 nfralw ⊢ Ⅎ 𝑥 ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙
41 38 40 nfan ⊢ Ⅎ 𝑥 ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 )
42 nfcv ⊢ Ⅎ 𝑥 ran 𝑓
43 nfiu1 ⊢ Ⅎ 𝑥 ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 )
44 42 43 nfss ⊢ Ⅎ 𝑥 ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 )
45 41 44 nfan ⊢ Ⅎ 𝑥 ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) )
46 34 45 nfan ⊢ Ⅎ 𝑥 ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) )
47 nfv ⊢ Ⅎ 𝑥 𝑧 ∈ ran 𝑓
48 46 47 nfan ⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ) ∧ 𝑧 ∈ ran 𝑓 )
49 simpr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ) ∧ 𝑧 ∈ ran 𝑓 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑥 } × 𝐵 ) ) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( 𝑓 ‘ 𝑘 ) = 𝑧 ) → ( 𝑓 ‘ 𝑘 ) = 𝑧 )
50 49 fveq2d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ) ∧ 𝑧 ∈ ran 𝑓 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑥 } × 𝐵 ) ) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( 𝑓 ‘ 𝑘 ) = 𝑧 ) → ( 2nd ‘ ( 𝑓 ‘ 𝑘 ) ) = ( 2nd ‘ 𝑧 ) )
51 simplr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ) ∧ 𝑧 ∈ ran 𝑓 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑥 } × 𝐵 ) ) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( 𝑓 ‘ 𝑘 ) = 𝑧 ) → 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 )
52 simp-4r ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ) ∧ 𝑧 ∈ ran 𝑓 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑥 } × 𝐵 ) ) → ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) )
53 52 simpld ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ) ∧ 𝑧 ∈ ran 𝑓 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑥 } × 𝐵 ) ) → ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) )
54 53 simprd ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ) ∧ 𝑧 ∈ ran 𝑓 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑥 } × 𝐵 ) ) → ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 )
55 54 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ) ∧ 𝑧 ∈ ran 𝑓 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑥 } × 𝐵 ) ) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( 𝑓 ‘ 𝑘 ) = 𝑧 ) → ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 )
56 2fveq3 ⊢ ( 𝑙 = 𝑘 → ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = ( 2nd ‘ ( 𝑓 ‘ 𝑘 ) ) )
57 id ⊢ ( 𝑙 = 𝑘 → 𝑙 = 𝑘 )
58 56 57 eqeq12d ⊢ ( 𝑙 = 𝑘 → ( ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ↔ ( 2nd ‘ ( 𝑓 ‘ 𝑘 ) ) = 𝑘 ) )
59 58 rspcva ⊢ ( ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) → ( 2nd ‘ ( 𝑓 ‘ 𝑘 ) ) = 𝑘 )
60 51 55 59 syl2anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ) ∧ 𝑧 ∈ ran 𝑓 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑥 } × 𝐵 ) ) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( 𝑓 ‘ 𝑘 ) = 𝑧 ) → ( 2nd ‘ ( 𝑓 ‘ 𝑘 ) ) = 𝑘 )
61 50 60 eqtr3d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ) ∧ 𝑧 ∈ ran 𝑓 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑥 } × 𝐵 ) ) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( 𝑓 ‘ 𝑘 ) = 𝑧 ) → ( 2nd ‘ 𝑧 ) = 𝑘 )
62 53 simpld ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ) ∧ 𝑧 ∈ ran 𝑓 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑥 } × 𝐵 ) ) → 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 )
63 62 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ) ∧ 𝑧 ∈ ran 𝑓 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑥 } × 𝐵 ) ) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( 𝑓 ‘ 𝑘 ) = 𝑧 ) → 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 )
64 f1ocnvfv1 ⊢ ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → ( ◡ 𝑓 ‘ ( 𝑓 ‘ 𝑘 ) ) = 𝑘 )
65 63 51 64 syl2anc ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ) ∧ 𝑧 ∈ ran 𝑓 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑥 } × 𝐵 ) ) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( 𝑓 ‘ 𝑘 ) = 𝑧 ) → ( ◡ 𝑓 ‘ ( 𝑓 ‘ 𝑘 ) ) = 𝑘 )
66 49 fveq2d ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ) ∧ 𝑧 ∈ ran 𝑓 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑥 } × 𝐵 ) ) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( 𝑓 ‘ 𝑘 ) = 𝑧 ) → ( ◡ 𝑓 ‘ ( 𝑓 ‘ 𝑘 ) ) = ( ◡ 𝑓 ‘ 𝑧 ) )
67 61 65 66 3eqtr2rd ⊢ ( ( ( ( ( ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ) ∧ 𝑧 ∈ ran 𝑓 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑥 } × 𝐵 ) ) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ ( 𝑓 ‘ 𝑘 ) = 𝑧 ) → ( ◡ 𝑓 ‘ 𝑧 ) = ( 2nd ‘ 𝑧 ) )
68 f1ofn ⊢ ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 → 𝑓 Fn ∪ 𝑥 ∈ 𝐴 𝐵 )
69 62 68 syl ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ) ∧ 𝑧 ∈ ran 𝑓 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑥 } × 𝐵 ) ) → 𝑓 Fn ∪ 𝑥 ∈ 𝐴 𝐵 )
70 simpllr ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ) ∧ 𝑧 ∈ ran 𝑓 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑥 } × 𝐵 ) ) → 𝑧 ∈ ran 𝑓 )
71 fvelrnb ⊢ ( 𝑓 Fn ∪ 𝑥 ∈ 𝐴 𝐵 → ( 𝑧 ∈ ran 𝑓 ↔ ∃ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 𝑓 ‘ 𝑘 ) = 𝑧 ) )
72 71 biimpa ⊢ ( ( 𝑓 Fn ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ran 𝑓 ) → ∃ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 𝑓 ‘ 𝑘 ) = 𝑧 )
73 69 70 72 syl2anc ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ) ∧ 𝑧 ∈ ran 𝑓 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑥 } × 𝐵 ) ) → ∃ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 𝑓 ‘ 𝑘 ) = 𝑧 )
74 67 73 r19.29a ⊢ ( ( ( ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ) ∧ 𝑧 ∈ ran 𝑓 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑥 } × 𝐵 ) ) → ( ◡ 𝑓 ‘ 𝑧 ) = ( 2nd ‘ 𝑧 ) )
75 28 sselda ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ) ∧ 𝑧 ∈ ran 𝑓 ) → 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) )
76 eliun ⊢ ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ↔ ∃ 𝑥 ∈ 𝐴 𝑧 ∈ ( { 𝑥 } × 𝐵 ) )
77 75 76 sylib ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ) ∧ 𝑧 ∈ ran 𝑓 ) → ∃ 𝑥 ∈ 𝐴 𝑧 ∈ ( { 𝑥 } × 𝐵 ) )
78 48 74 77 r19.29af ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ) ∧ 𝑧 ∈ ran 𝑓 ) → ( ◡ 𝑓 ‘ 𝑧 ) = ( 2nd ‘ 𝑧 ) )
79 nfv ⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 )
80 nfcv ⊢ Ⅎ 𝑘 ℂ
81 18 80 nfel ⊢ Ⅎ 𝑘 ⦋ 𝑦 / 𝑘 ⦌ 𝐶 ∈ ℂ
82 79 81 nfim ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → ⦋ 𝑦 / 𝑘 ⦌ 𝐶 ∈ ℂ )
83 eleq1w ⊢ ( 𝑘 = 𝑦 → ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) )
84 83 anbi2d ⊢ ( 𝑘 = 𝑦 → ( ( 𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ↔ ( 𝜑 ∧ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ) )
85 14 eleq1d ⊢ ( 𝑘 = 𝑦 → ( 𝐶 ∈ ℂ ↔ ⦋ 𝑦 / 𝑘 ⦌ 𝐶 ∈ ℂ ) )
86 84 85 imbi12d ⊢ ( 𝑘 = 𝑦 → ( ( ( 𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → 𝐶 ∈ ℂ ) ↔ ( ( 𝜑 ∧ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → ⦋ 𝑦 / 𝑘 ⦌ 𝐶 ∈ ℂ ) ) )
87 nfcv ⊢ Ⅎ 𝑥 𝑘
88 87 36 nfel ⊢ Ⅎ 𝑥 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵
89 34 88 nfan ⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 )
90 3 adantllr ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ℝ )
91 90 recnd ⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ℂ )
92 eliun ⊢ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃ 𝑥 ∈ 𝐴 𝑘 ∈ 𝐵 )
93 92 biimpi ⊢ ( 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → ∃ 𝑥 ∈ 𝐴 𝑘 ∈ 𝐵 )
94 93 adantl ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝑘 ∈ 𝐵 )
95 89 91 94 r19.29af ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → 𝐶 ∈ ℂ )
96 82 86 95 chvarfv ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → ⦋ 𝑦 / 𝑘 ⦌ 𝐶 ∈ ℂ )
97 96 adantlr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ) ∧ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → ⦋ 𝑦 / 𝑘 ⦌ 𝐶 ∈ ℂ )
98 20 29 33 78 97 fsumf1o ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ) → Σ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ⦋ 𝑦 / 𝑘 ⦌ 𝐶 = Σ 𝑧 ∈ ran 𝑓 ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 )
99 19 98 syl5eq ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ) → Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝐶 = Σ 𝑧 ∈ ran 𝑓 ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 )
100 99 eqcomd ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ) → Σ 𝑧 ∈ ran 𝑓 ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 = Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝐶 )
101 nfcv ⊢ Ⅎ 𝑥 𝑧
102 101 43 nfel ⊢ Ⅎ 𝑥 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 )
103 34 102 nfan ⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) )
104 xp2nd ⊢ ( 𝑧 ∈ ( { 𝑥 } × 𝐵 ) → ( 2nd ‘ 𝑧 ) ∈ 𝐵 )
105 104 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑥 } × 𝐵 ) ) → ( 2nd ‘ 𝑧 ) ∈ 𝐵 )
106 3 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑘 ∈ 𝐵 𝐶 ∈ ℝ )
107 106 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑘 ∈ 𝐵 𝐶 ∈ ℝ )
108 107 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑥 } × 𝐵 ) ) → ∀ 𝑘 ∈ 𝐵 𝐶 ∈ ℝ )
109 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶
110 109 nfel1 ⊢ Ⅎ 𝑘 ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 ∈ ℝ
111 csbeq1a ⊢ ( 𝑘 = ( 2nd ‘ 𝑧 ) → 𝐶 = ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 )
112 111 eleq1d ⊢ ( 𝑘 = ( 2nd ‘ 𝑧 ) → ( 𝐶 ∈ ℝ ↔ ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 ∈ ℝ ) )
113 110 112 rspc ⊢ ( ( 2nd ‘ 𝑧 ) ∈ 𝐵 → ( ∀ 𝑘 ∈ 𝐵 𝐶 ∈ ℝ → ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 ∈ ℝ ) )
114 113 imp ⊢ ( ( ( 2nd ‘ 𝑧 ) ∈ 𝐵 ∧ ∀ 𝑘 ∈ 𝐵 𝐶 ∈ ℝ ) → ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 ∈ ℝ )
115 105 108 114 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑥 } × 𝐵 ) ) → ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 ∈ ℝ )
116 76 biimpi ⊢ ( 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝑧 ∈ ( { 𝑥 } × 𝐵 ) )
117 116 adantl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) → ∃ 𝑥 ∈ 𝐴 𝑧 ∈ ( { 𝑥 } × 𝐵 ) )
118 103 115 117 r19.29af ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) → ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 ∈ ℝ )
119 118 adantlr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ) ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) → ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 ∈ ℝ )
120 xp1st ⊢ ( 𝑧 ∈ ( { 𝑥 } × 𝐵 ) → ( 1st ‘ 𝑧 ) ∈ { 𝑥 } )
121 elsni ⊢ ( ( 1st ‘ 𝑧 ) ∈ { 𝑥 } → ( 1st ‘ 𝑧 ) = 𝑥 )
122 120 121 syl ⊢ ( 𝑧 ∈ ( { 𝑥 } × 𝐵 ) → ( 1st ‘ 𝑧 ) = 𝑥 )
123 122 104 jca ⊢ ( 𝑧 ∈ ( { 𝑥 } × 𝐵 ) → ( ( 1st ‘ 𝑧 ) = 𝑥 ∧ ( 2nd ‘ 𝑧 ) ∈ 𝐵 ) )
124 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( ( 1st ‘ 𝑧 ) = 𝑥 ∧ ( 2nd ‘ 𝑧 ) ∈ 𝐵 ) ) → 𝜑 )
125 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( ( 1st ‘ 𝑧 ) = 𝑥 ∧ ( 2nd ‘ 𝑧 ) ∈ 𝐵 ) ) → 𝑥 ∈ 𝐴 )
126 4 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑘 ∈ 𝐵 0 ≤ 𝐶 )
127 124 125 126 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( ( 1st ‘ 𝑧 ) = 𝑥 ∧ ( 2nd ‘ 𝑧 ) ∈ 𝐵 ) ) → ∀ 𝑘 ∈ 𝐵 0 ≤ 𝐶 )
128 123 127 sylan2 ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑥 } × 𝐵 ) ) → ∀ 𝑘 ∈ 𝐵 0 ≤ 𝐶 )
129 nfcv ⊢ Ⅎ 𝑘 0
130 nfcv ⊢ Ⅎ 𝑘 ≤
131 129 130 109 nfbr ⊢ Ⅎ 𝑘 0 ≤ ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶
132 111 breq2d ⊢ ( 𝑘 = ( 2nd ‘ 𝑧 ) → ( 0 ≤ 𝐶 ↔ 0 ≤ ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 ) )
133 131 132 rspc ⊢ ( ( 2nd ‘ 𝑧 ) ∈ 𝐵 → ( ∀ 𝑘 ∈ 𝐵 0 ≤ 𝐶 → 0 ≤ ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 ) )
134 133 imp ⊢ ( ( ( 2nd ‘ 𝑧 ) ∈ 𝐵 ∧ ∀ 𝑘 ∈ 𝐵 0 ≤ 𝐶 ) → 0 ≤ ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 )
135 105 128 134 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑥 } × 𝐵 ) ) → 0 ≤ ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 )
136 103 135 117 r19.29af ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) → 0 ≤ ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 )
137 136 adantlr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ) ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) → 0 ≤ ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 )
138 27 119 137 28 fsumless ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ) → Σ 𝑧 ∈ ran 𝑓 ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 ≤ Σ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 )
139 100 138 eqbrtrrd ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ) → Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝐶 ≤ Σ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 )
140 nfcv ⊢ Ⅎ 𝑦 𝐵
141 nfcv ⊢ Ⅎ 𝑘 𝐵
142 14 140 141 17 18 cbvsum ⊢ Σ 𝑘 ∈ 𝐵 𝐶 = Σ 𝑦 ∈ 𝐵 ⦋ 𝑦 / 𝑘 ⦌ 𝐶
143 142 a1i ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐵 𝐶 = Σ 𝑦 ∈ 𝐵 ⦋ 𝑦 / 𝑘 ⦌ 𝐶 )
144 143 sumeq2sdv ⊢ ( 𝜑 → Σ 𝑥 ∈ 𝐴 Σ 𝑘 ∈ 𝐵 𝐶 = Σ 𝑥 ∈ 𝐴 Σ 𝑦 ∈ 𝐵 ⦋ 𝑦 / 𝑘 ⦌ 𝐶 )
145 vex ⊢ 𝑥 ∈ V
146 vex ⊢ 𝑦 ∈ V
147 145 146 op2ndd ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 2nd ‘ 𝑧 ) = 𝑦 )
148 147 eqcomd ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → 𝑦 = ( 2nd ‘ 𝑧 ) )
149 148 csbeq1d ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ⦋ 𝑦 / 𝑘 ⦌ 𝐶 = ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 )
150 149 eqcomd ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 = ⦋ 𝑦 / 𝑘 ⦌ 𝐶 )
151 nfv ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 )
152 18 nfel1 ⊢ Ⅎ 𝑘 ⦋ 𝑦 / 𝑘 ⦌ 𝐶 ∈ ℂ
153 151 152 nfim ⊢ Ⅎ 𝑘 ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → ⦋ 𝑦 / 𝑘 ⦌ 𝐶 ∈ ℂ )
154 eleq1w ⊢ ( 𝑘 = 𝑦 → ( 𝑘 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵 ) )
155 154 anbi2d ⊢ ( 𝑘 = 𝑦 → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐵 ) ↔ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) ) )
156 155 85 imbi12d ⊢ ( 𝑘 = 𝑦 → ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ℂ ) ↔ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → ⦋ 𝑦 / 𝑘 ⦌ 𝐶 ∈ ℂ ) ) )
157 3 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ℂ )
158 153 156 157 chvarfv ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → ⦋ 𝑦 / 𝑘 ⦌ 𝐶 ∈ ℂ )
159 158 anasss ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → ⦋ 𝑦 / 𝑘 ⦌ 𝐶 ∈ ℂ )
160 150 1 2 159 fsum2d ⊢ ( 𝜑 → Σ 𝑥 ∈ 𝐴 Σ 𝑦 ∈ 𝐵 ⦋ 𝑦 / 𝑘 ⦌ 𝐶 = Σ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 )
161 144 160 eqtrd ⊢ ( 𝜑 → Σ 𝑥 ∈ 𝐴 Σ 𝑘 ∈ 𝐵 𝐶 = Σ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 )
162 161 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ) → Σ 𝑥 ∈ 𝐴 Σ 𝑘 ∈ 𝐵 𝐶 = Σ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 )
163 139 162 breqtrrd ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ) → Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝐶 ≤ Σ 𝑥 ∈ 𝐴 Σ 𝑘 ∈ 𝐵 𝐶 )
164 13 163 exlimddv ⊢ ( 𝜑 → Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝐶 ≤ Σ 𝑥 ∈ 𝐴 Σ 𝑘 ∈ 𝐵 𝐶 )