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