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 bilani ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → ∃ 𝑥 ∈ 𝐴 𝑘 ∈ 𝐵 )
92 87 89 91 r19.29af ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → 𝐶 ∈ ℂ )
93 80 84 92 chvarfv ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → ⦋ 𝑦 / 𝑘 ⦌ 𝐶 ∈ ℂ )
94 93 adantlr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ) ∧ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ) → ⦋ 𝑦 / 𝑘 ⦌ 𝐶 ∈ ℂ )
95 18 27 31 76 94 fsumf1o ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ) → Σ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ⦋ 𝑦 / 𝑘 ⦌ 𝐶 = Σ 𝑧 ∈ ran 𝑓 ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 )
96 17 95 eqtrid ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ) → Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝐶 = Σ 𝑧 ∈ ran 𝑓 ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 )
97 96 eqcomd ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ) → Σ 𝑧 ∈ ran 𝑓 ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 = Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝐶 )
98 nfcv ⊢ Ⅎ 𝑥 𝑧
99 98 41 nfel ⊢ Ⅎ 𝑥 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 )
100 32 99 nfan ⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) )
101 xp2nd ⊢ ( 𝑧 ∈ ( { 𝑥 } × 𝐵 ) → ( 2nd ‘ 𝑧 ) ∈ 𝐵 )
102 101 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑥 } × 𝐵 ) ) → ( 2nd ‘ 𝑧 ) ∈ 𝐵 )
103 3 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑘 ∈ 𝐵 𝐶 ∈ ℝ )
104 103 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑘 ∈ 𝐵 𝐶 ∈ ℝ )
105 104 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑥 } × 𝐵 ) ) → ∀ 𝑘 ∈ 𝐵 𝐶 ∈ ℝ )
106 nfcsb1v ⊢ Ⅎ 𝑘 ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶
107 106 nfel1 ⊢ Ⅎ 𝑘 ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 ∈ ℝ
108 csbeq1a ⊢ ( 𝑘 = ( 2nd ‘ 𝑧 ) → 𝐶 = ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 )
109 108 eleq1d ⊢ ( 𝑘 = ( 2nd ‘ 𝑧 ) → ( 𝐶 ∈ ℝ ↔ ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 ∈ ℝ ) )
110 107 109 rspc ⊢ ( ( 2nd ‘ 𝑧 ) ∈ 𝐵 → ( ∀ 𝑘 ∈ 𝐵 𝐶 ∈ ℝ → ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 ∈ ℝ ) )
111 110 imp ⊢ ( ( ( 2nd ‘ 𝑧 ) ∈ 𝐵 ∧ ∀ 𝑘 ∈ 𝐵 𝐶 ∈ ℝ ) → ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 ∈ ℝ )
112 102 105 111 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑥 } × 𝐵 ) ) → ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 ∈ ℝ )
113 74 bilani ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) → ∃ 𝑥 ∈ 𝐴 𝑧 ∈ ( { 𝑥 } × 𝐵 ) )
114 100 112 113 r19.29af ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) → ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 ∈ ℝ )
115 114 adantlr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ) ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) → ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 ∈ ℝ )
116 xp1st ⊢ ( 𝑧 ∈ ( { 𝑥 } × 𝐵 ) → ( 1st ‘ 𝑧 ) ∈ { 𝑥 } )
117 elsni ⊢ ( ( 1st ‘ 𝑧 ) ∈ { 𝑥 } → ( 1st ‘ 𝑧 ) = 𝑥 )
118 116 117 syl ⊢ ( 𝑧 ∈ ( { 𝑥 } × 𝐵 ) → ( 1st ‘ 𝑧 ) = 𝑥 )
119 118 101 jca ⊢ ( 𝑧 ∈ ( { 𝑥 } × 𝐵 ) → ( ( 1st ‘ 𝑧 ) = 𝑥 ∧ ( 2nd ‘ 𝑧 ) ∈ 𝐵 ) )
120 simplll ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( ( 1st ‘ 𝑧 ) = 𝑥 ∧ ( 2nd ‘ 𝑧 ) ∈ 𝐵 ) ) → 𝜑 )
121 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( ( 1st ‘ 𝑧 ) = 𝑥 ∧ ( 2nd ‘ 𝑧 ) ∈ 𝐵 ) ) → 𝑥 ∈ 𝐴 )
122 4 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑘 ∈ 𝐵 0 ≤ 𝐶 )
123 120 121 122 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( ( 1st ‘ 𝑧 ) = 𝑥 ∧ ( 2nd ‘ 𝑧 ) ∈ 𝐵 ) ) → ∀ 𝑘 ∈ 𝐵 0 ≤ 𝐶 )
124 119 123 sylan2 ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑥 } × 𝐵 ) ) → ∀ 𝑘 ∈ 𝐵 0 ≤ 𝐶 )
125 nfcv ⊢ Ⅎ 𝑘 0
126 nfcv ⊢ Ⅎ 𝑘 ≤
127 125 126 106 nfbr ⊢ Ⅎ 𝑘 0 ≤ ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶
128 108 breq2d ⊢ ( 𝑘 = ( 2nd ‘ 𝑧 ) → ( 0 ≤ 𝐶 ↔ 0 ≤ ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 ) )
129 127 128 rspc ⊢ ( ( 2nd ‘ 𝑧 ) ∈ 𝐵 → ( ∀ 𝑘 ∈ 𝐵 0 ≤ 𝐶 → 0 ≤ ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 ) )
130 129 imp ⊢ ( ( ( 2nd ‘ 𝑧 ) ∈ 𝐵 ∧ ∀ 𝑘 ∈ 𝐵 0 ≤ 𝐶 ) → 0 ≤ ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 )
131 102 124 130 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑧 ∈ ( { 𝑥 } × 𝐵 ) ) → 0 ≤ ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 )
132 100 131 113 r19.29af ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) → 0 ≤ ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 )
133 132 adantlr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ) ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) → 0 ≤ ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 )
134 25 115 133 26 fsumless ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ) → Σ 𝑧 ∈ ran 𝑓 ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 ≤ Σ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 )
135 97 134 eqbrtrrd ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ) → Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝐶 ≤ Σ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 )
136 14 15 16 cbvsum ⊢ Σ 𝑘 ∈ 𝐵 𝐶 = Σ 𝑦 ∈ 𝐵 ⦋ 𝑦 / 𝑘 ⦌ 𝐶
137 136 a1i ⊢ ( 𝜑 → Σ 𝑘 ∈ 𝐵 𝐶 = Σ 𝑦 ∈ 𝐵 ⦋ 𝑦 / 𝑘 ⦌ 𝐶 )
138 137 sumeq2sdv ⊢ ( 𝜑 → Σ 𝑥 ∈ 𝐴 Σ 𝑘 ∈ 𝐵 𝐶 = Σ 𝑥 ∈ 𝐴 Σ 𝑦 ∈ 𝐵 ⦋ 𝑦 / 𝑘 ⦌ 𝐶 )
139 vex ⊢ 𝑥 ∈ V
140 vex ⊢ 𝑦 ∈ V
141 139 140 op2ndd ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 2nd ‘ 𝑧 ) = 𝑦 )
142 141 eqcomd ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → 𝑦 = ( 2nd ‘ 𝑧 ) )
143 142 csbeq1d ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ⦋ 𝑦 / 𝑘 ⦌ 𝐶 = ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 )
144 143 eqcomd ⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 = ⦋ 𝑦 / 𝑘 ⦌ 𝐶 )
145 nfv ⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 )
146 16 nfel1 ⊢ Ⅎ 𝑘 ⦋ 𝑦 / 𝑘 ⦌ 𝐶 ∈ ℂ
147 145 146 nfim ⊢ Ⅎ 𝑘 ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → ⦋ 𝑦 / 𝑘 ⦌ 𝐶 ∈ ℂ )
148 eleq1w ⊢ ( 𝑘 = 𝑦 → ( 𝑘 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵 ) )
149 148 anbi2d ⊢ ( 𝑘 = 𝑦 → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐵 ) ↔ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) ) )
150 149 83 imbi12d ⊢ ( 𝑘 = 𝑦 → ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ℂ ) ↔ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → ⦋ 𝑦 / 𝑘 ⦌ 𝐶 ∈ ℂ ) ) )
151 3 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑘 ∈ 𝐵 ) → 𝐶 ∈ ℂ )
152 147 150 151 chvarfv ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ) → ⦋ 𝑦 / 𝑘 ⦌ 𝐶 ∈ ℂ )
153 152 anasss ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ) → ⦋ 𝑦 / 𝑘 ⦌ 𝐶 ∈ ℂ )
154 144 1 2 153 fsum2d ⊢ ( 𝜑 → Σ 𝑥 ∈ 𝐴 Σ 𝑦 ∈ 𝐵 ⦋ 𝑦 / 𝑘 ⦌ 𝐶 = Σ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 )
155 138 154 eqtrd ⊢ ( 𝜑 → Σ 𝑥 ∈ 𝐴 Σ 𝑘 ∈ 𝐵 𝐶 = Σ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 )
156 155 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ) → Σ 𝑥 ∈ 𝐴 Σ 𝑘 ∈ 𝐵 𝐶 = Σ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ⦋ ( 2nd ‘ 𝑧 ) / 𝑘 ⦌ 𝐶 )
157 135 156 breqtrrd ⊢ ( ( 𝜑 ∧ ( ( 𝑓 : ∪ 𝑥 ∈ 𝐴 𝐵 –1-1-onto→ ran 𝑓 ∧ ∀ 𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ( 2nd ‘ ( 𝑓 ‘ 𝑙 ) ) = 𝑙 ) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ( { 𝑥 } × 𝐵 ) ) ) → Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝐶 ≤ Σ 𝑥 ∈ 𝐴 Σ 𝑘 ∈ 𝐵 𝐶 )
158 13 157 exlimddv ⊢ ( 𝜑 → Σ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 𝐶 ≤ Σ 𝑥 ∈ 𝐴 Σ 𝑘 ∈ 𝐵 𝐶 )