Theorem esumiun 34429

Description: Sum over a nonnecessarily disjoint indexed union. The inequality is strict in the case where the sets B(x) overlap. (Contributed by Thierry Arnoux, 21-Sep-2019.)

Hypotheses

Ref	Expression
esumiun.0	⊢ (𝜑 → 𝐴 ∈ 𝑉)
esumiun.1	⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ 𝑊)
esumiun.2	⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞))

Assertion

Ref	Expression
esumiun	⊢ (𝜑 → Σ*𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝐶 ≤ Σ*𝑗 ∈ 𝐴Σ*𝑘 ∈ 𝐵𝐶)

Distinct variable groups:   𝐴,𝑗,𝑘   𝐵,𝑘   𝐶,𝑗   𝑗,𝑊,𝑘   𝜑,𝑗,𝑘

Allowed substitution hints:   𝐵(𝑗)   𝐶(𝑘)   𝑉(𝑗,𝑘)

Proof of Theorem esumiun

Dummy variables 𝑓 𝑙 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		esumiun.0	. . . 4 ⊢ (𝜑 → 𝐴 ∈ 𝑉)
2		esumiun.1	. . . 4 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → 𝐵 ∈ 𝑊)
3	1, 2	aciunf1 32949	. . 3 ⊢ (𝜑 → ∃𝑓(𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙))
4		f1f1orn 6833	. . . . . 6 ⊢ (𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) → 𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓)
5	4	anim1i 626	. . . . 5 ⊢ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) → (𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙))
6		f1f 6775	. . . . . . 7 ⊢ (𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) → 𝑓:∪ 𝑗 ∈ 𝐴 𝐵⟶∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
7	6	frnd 6715	. . . . . 6 ⊢ (𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) → ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
8	7	adantr 485	. . . . 5 ⊢ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) → ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
9	5, 8	jca 520	. . . 4 ⊢ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) → ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)))
10	9	eximi 1862	. . 3 ⊢ (∃𝑓(𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1→∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) → ∃𝑓((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)))
11	3, 10	syl 18	. 2 ⊢ (𝜑 → ∃𝑓((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)))
12		nfv 1941	. . . . . 6 ⊢ Ⅎ𝑧(𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)))
13		nfcv 2931	. . . . . 6 ⊢ Ⅎ𝑧𝐶
14		nfcsb1v 3885	. . . . . 6 ⊢ Ⅎ𝑘⦋(2nd ‘𝑧) / 𝑘⦌𝐶
15		nfcv 2931	. . . . . 6 ⊢ Ⅎ𝑧∪ 𝑗 ∈ 𝐴 𝐵
16		nfcv 2931	. . . . . 6 ⊢ Ⅎ𝑧ran 𝑓
17		nfcv 2931	. . . . . 6 ⊢ Ⅎ𝑧◡𝑓
18		csbeq1a 3875	. . . . . 6 ⊢ (𝑘 = (2nd ‘𝑧) → 𝐶 = ⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
19	2	ralrimiva 3163	. . . . . . . 8 ⊢ (𝜑 → ∀𝑗 ∈ 𝐴 𝐵 ∈ 𝑊)
20		iunexg 7960	. . . . . . . 8 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑗 ∈ 𝐴 𝐵 ∈ 𝑊) → ∪ 𝑗 ∈ 𝐴 𝐵 ∈ V)
21	1, 19, 20	syl2anc 595	. . . . . . 7 ⊢ (𝜑 → ∪ 𝑗 ∈ 𝐴 𝐵 ∈ V)
22	21	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) → ∪ 𝑗 ∈ 𝐴 𝐵 ∈ V)
23		simprl 782	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) → 𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓)
24		f1ocnv 6834	. . . . . . . 8 ⊢ (𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 → ◡𝑓:ran 𝑓–1-1-onto→∪ 𝑗 ∈ 𝐴 𝐵)
25	23, 24	syl 18	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) → ◡𝑓:ran 𝑓–1-1-onto→∪ 𝑗 ∈ 𝐴 𝐵)
26	25	adantrlr 735	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) → ◡𝑓:ran 𝑓–1-1-onto→∪ 𝑗 ∈ 𝐴 𝐵)
27		nfv 1941	. . . . . . . . 9 ⊢ Ⅎ𝑗𝜑
28		nfcv 2931	. . . . . . . . . . . 12 ⊢ Ⅎ𝑗𝑓
29		nfiu1 4996	. . . . . . . . . . . 12 ⊢ Ⅎ𝑗∪ 𝑗 ∈ 𝐴 𝐵
30	28	nfrn 5943	. . . . . . . . . . . 12 ⊢ Ⅎ𝑗ran 𝑓
31	28, 29, 30	nff1o 6819	. . . . . . . . . . 11 ⊢ Ⅎ𝑗 𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓
32		nfv 1941	. . . . . . . . . . . 12 ⊢ Ⅎ𝑗(2nd ‘(𝑓‘𝑙)) = 𝑙
33	29, 32	nfralw 3318	. . . . . . . . . . 11 ⊢ Ⅎ𝑗∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙
34	31, 33	nfan 1926	. . . . . . . . . 10 ⊢ Ⅎ𝑗(𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙)
35		nfcv 2931	. . . . . . . . . . 11 ⊢ Ⅎ𝑗ran 𝑓
36		nfiu1 4996	. . . . . . . . . . 11 ⊢ Ⅎ𝑗∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)
37	35, 36	nfss 3938	. . . . . . . . . 10 ⊢ Ⅎ𝑗ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)
38	34, 37	nfan 1926	. . . . . . . . 9 ⊢ Ⅎ𝑗((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
39	27, 38	nfan 1926	. . . . . . . 8 ⊢ Ⅎ𝑗(𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)))
40		nfv 1941	. . . . . . . 8 ⊢ Ⅎ𝑗 𝑧 ∈ ran 𝑓
41	39, 40	nfan 1926	. . . . . . 7 ⊢ Ⅎ𝑗((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓)
42		simpr 489	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) ∧ 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → (𝑓‘𝑘) = 𝑧)
43	42	fveq2d 6886	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) ∧ 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → (2nd ‘(𝑓‘𝑘)) = (2nd ‘𝑧))
44		simplr 780	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) ∧ 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵)
45		simp-4r 795	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) → ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)))
46	45	simpld 499	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) → (𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙))
47	46	simprd 500	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) → ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙)
48	47	ad2antrr 738	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) ∧ 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙)
49		2fveq3 6887	. . . . . . . . . . . . 13 ⊢ (𝑙 = 𝑘 → (2nd ‘(𝑓‘𝑙)) = (2nd ‘(𝑓‘𝑘)))
50		id 23	. . . . . . . . . . . . 13 ⊢ (𝑙 = 𝑘 → 𝑙 = 𝑘)
51	49, 50	eqeq12d 2785	. . . . . . . . . . . 12 ⊢ (𝑙 = 𝑘 → ((2nd ‘(𝑓‘𝑙)) = 𝑙 ↔ (2nd ‘(𝑓‘𝑘)) = 𝑘))
52	51	rspcva 3588	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) → (2nd ‘(𝑓‘𝑘)) = 𝑘)
53	44, 48, 52	syl2anc 595	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) ∧ 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → (2nd ‘(𝑓‘𝑘)) = 𝑘)
54	43, 53	eqtr3d 2806	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) ∧ 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → (2nd ‘𝑧) = 𝑘)
55	46	simpld 499	. . . . . . . . . . 11 ⊢ (((((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) → 𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓)
56	55	ad2antrr 738	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) ∧ 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → 𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓)
57		f1ocnvfv1 7275	. . . . . . . . . 10 ⊢ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) → (◡𝑓‘(𝑓‘𝑘)) = 𝑘)
58	56, 44, 57	syl2anc 595	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) ∧ 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → (◡𝑓‘(𝑓‘𝑘)) = 𝑘)
59	42	fveq2d 6886	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) ∧ 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → (◡𝑓‘(𝑓‘𝑘)) = (◡𝑓‘𝑧))
60	54, 58, 59	3eqtr2rd 2811	. . . . . . . 8 ⊢ (((((((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) ∧ 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → (◡𝑓‘𝑧) = (2nd ‘𝑧))
61		f1ofn 6822	. . . . . . . . . 10 ⊢ (𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 → 𝑓 Fn ∪ 𝑗 ∈ 𝐴 𝐵)
62	55, 61	syl 18	. . . . . . . . 9 ⊢ (((((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) → 𝑓 Fn ∪ 𝑗 ∈ 𝐴 𝐵)
63		simpllr 787	. . . . . . . . 9 ⊢ (((((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) → 𝑧 ∈ ran 𝑓)
64		fvelrnb 6942	. . . . . . . . . 10 ⊢ (𝑓 Fn ∪ 𝑗 ∈ 𝐴 𝐵 → (𝑧 ∈ ran 𝑓 ↔ ∃𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(𝑓‘𝑘) = 𝑧))
65	64	biimpa 481	. . . . . . . . 9 ⊢ ((𝑓 Fn ∪ 𝑗 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ran 𝑓) → ∃𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(𝑓‘𝑘) = 𝑧)
66	62, 63, 65	syl2anc 595	. . . . . . . 8 ⊢ (((((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) → ∃𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(𝑓‘𝑘) = 𝑧)
67	60, 66	r19.29a 3179	. . . . . . 7 ⊢ (((((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑗 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑗} × 𝐵)) → (◡𝑓‘𝑧) = (2nd ‘𝑧))
68		simprr 784	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) → ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
69	68	sselda 3945	. . . . . . . 8 ⊢ (((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) → 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
70		eliun 4964	. . . . . . . 8 ⊢ (𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ↔ ∃𝑗 ∈ 𝐴 𝑧 ∈ ({𝑗} × 𝐵))
71	69, 70	sylib 221	. . . . . . 7 ⊢ (((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) → ∃𝑗 ∈ 𝐴 𝑧 ∈ ({𝑗} × 𝐵))
72	41, 67, 71	r19.29af 3280	. . . . . 6 ⊢ (((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) → (◡𝑓‘𝑧) = (2nd ‘𝑧))
73		nfcv 2931	. . . . . . . . . 10 ⊢ Ⅎ𝑗𝑘
74	73, 29	nfel 2945	. . . . . . . . 9 ⊢ Ⅎ𝑗 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵
75	27, 74	nfan 1926	. . . . . . . 8 ⊢ Ⅎ𝑗(𝜑 ∧ 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵)
76		esumiun.2	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑗 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞))
77	76	adantllr 731	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) ∧ 𝑗 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ (0[,]+∞))
78		eliun 4964	. . . . . . . . 9 ⊢ (𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵 ↔ ∃𝑗 ∈ 𝐴 𝑘 ∈ 𝐵)
79	78	bilani 509	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) → ∃𝑗 ∈ 𝐴 𝑘 ∈ 𝐵)
80	75, 77, 79	r19.29af 3280	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) → 𝐶 ∈ (0[,]+∞))
81	80	adantlr 727	. . . . . 6 ⊢ (((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵) → 𝐶 ∈ (0[,]+∞))
82	12, 13, 14, 15, 16, 17, 18, 22, 26, 72, 81	esumf1o 34385	. . . . 5 ⊢ ((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) → Σ*𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝐶 = Σ*𝑧 ∈ ran 𝑓⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
83	82	eqcomd 2775	. . . 4 ⊢ ((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) → Σ*𝑧 ∈ ran 𝑓⦋(2nd ‘𝑧) / 𝑘⦌𝐶 = Σ*𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝐶)
84		vsnex 5407	. . . . . . . . . 10 ⊢ {𝑗} ∈ V
85	84	a1i 11	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → {𝑗} ∈ V)
86	85, 2	xpexd 7750	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ({𝑗} × 𝐵) ∈ V)
87	86	ralrimiva 3163	. . . . . . 7 ⊢ (𝜑 → ∀𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∈ V)
88		iunexg 7960	. . . . . . 7 ⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∈ V) → ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∈ V)
89	1, 87, 88	syl2anc 595	. . . . . 6 ⊢ (𝜑 → ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∈ V)
90	89	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) → ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) ∈ V)
91		nfcv 2931	. . . . . . . . 9 ⊢ Ⅎ𝑗𝑧
92	91, 36	nfel 2945	. . . . . . . 8 ⊢ Ⅎ𝑗 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)
93	27, 92	nfan 1926	. . . . . . 7 ⊢ Ⅎ𝑗(𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
94		nfcv 2931	. . . . . . . . 9 ⊢ Ⅎ𝑗(2nd ‘𝑧)
95		nfcv 2931	. . . . . . . . 9 ⊢ Ⅎ𝑗𝐶
96	94, 95	nfcsbw 3887	. . . . . . . 8 ⊢ Ⅎ𝑗⦋(2nd ‘𝑧) / 𝑘⦌𝐶
97		nfcv 2931	. . . . . . . 8 ⊢ Ⅎ𝑗(0[,]+∞)
98	96, 97	nfel 2945	. . . . . . 7 ⊢ Ⅎ𝑗⦋(2nd ‘𝑧) / 𝑘⦌𝐶 ∈ (0[,]+∞)
99		simprr 784	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) ∧ 𝑗 ∈ 𝐴) ∧ ((1st ‘𝑧) = 𝑗 ∧ (2nd ‘𝑧) ∈ 𝐵)) → (2nd ‘𝑧) ∈ 𝐵)
100		simplll 786	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) ∧ 𝑗 ∈ 𝐴) ∧ ((1st ‘𝑧) = 𝑗 ∧ (2nd ‘𝑧) ∈ 𝐵)) → 𝜑)
101		simplr 780	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) ∧ 𝑗 ∈ 𝐴) ∧ ((1st ‘𝑧) = 𝑗 ∧ (2nd ‘𝑧) ∈ 𝐵)) → 𝑗 ∈ 𝐴)
102	76	ralrimiva 3163	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑗 ∈ 𝐴) → ∀𝑘 ∈ 𝐵 𝐶 ∈ (0[,]+∞))
103	100, 101, 102	syl2anc 595	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) ∧ 𝑗 ∈ 𝐴) ∧ ((1st ‘𝑧) = 𝑗 ∧ (2nd ‘𝑧) ∈ 𝐵)) → ∀𝑘 ∈ 𝐵 𝐶 ∈ (0[,]+∞))
104		rspcsbela 4409	. . . . . . . 8 ⊢ (((2nd ‘𝑧) ∈ 𝐵 ∧ ∀𝑘 ∈ 𝐵 𝐶 ∈ (0[,]+∞)) → ⦋(2nd ‘𝑧) / 𝑘⦌𝐶 ∈ (0[,]+∞))
105	99, 103, 104	syl2anc 595	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) ∧ 𝑗 ∈ 𝐴) ∧ ((1st ‘𝑧) = 𝑗 ∧ (2nd ‘𝑧) ∈ 𝐵)) → ⦋(2nd ‘𝑧) / 𝑘⦌𝐶 ∈ (0[,]+∞))
106		xp1st 8018	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ ({𝑗} × 𝐵) → (1st ‘𝑧) ∈ {𝑗})
107		elsni 4611	. . . . . . . . . . . 12 ⊢ ((1st ‘𝑧) ∈ {𝑗} → (1st ‘𝑧) = 𝑗)
108	106, 107	syl 18	. . . . . . . . . . 11 ⊢ (𝑧 ∈ ({𝑗} × 𝐵) → (1st ‘𝑧) = 𝑗)
109		xp2nd 8019	. . . . . . . . . . 11 ⊢ (𝑧 ∈ ({𝑗} × 𝐵) → (2nd ‘𝑧) ∈ 𝐵)
110	108, 109	jca 520	. . . . . . . . . 10 ⊢ (𝑧 ∈ ({𝑗} × 𝐵) → ((1st ‘𝑧) = 𝑗 ∧ (2nd ‘𝑧) ∈ 𝐵))
111	110	reximi 3109	. . . . . . . . 9 ⊢ (∃𝑗 ∈ 𝐴 𝑧 ∈ ({𝑗} × 𝐵) → ∃𝑗 ∈ 𝐴 ((1st ‘𝑧) = 𝑗 ∧ (2nd ‘𝑧) ∈ 𝐵))
112	70, 111	sylbi 220	. . . . . . . 8 ⊢ (𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵) → ∃𝑗 ∈ 𝐴 ((1st ‘𝑧) = 𝑗 ∧ (2nd ‘𝑧) ∈ 𝐵))
113	112	adantl 486	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) → ∃𝑗 ∈ 𝐴 ((1st ‘𝑧) = 𝑗 ∧ (2nd ‘𝑧) ∈ 𝐵))
114	93, 98, 105, 113	r19.29af2 3279	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) → ⦋(2nd ‘𝑧) / 𝑘⦌𝐶 ∈ (0[,]+∞))
115	114	adantlr 727	. . . . 5 ⊢ (((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)) → ⦋(2nd ‘𝑧) / 𝑘⦌𝐶 ∈ (0[,]+∞))
116		simprr 784	. . . . . 6 ⊢ ((𝜑 ∧ (𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) → ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
117	116	adantrlr 735	. . . . 5 ⊢ ((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) → ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))
118	12, 90, 115, 117	esummono 34389	. . . 4 ⊢ ((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) → Σ*𝑧 ∈ ran 𝑓⦋(2nd ‘𝑧) / 𝑘⦌𝐶 ≤ Σ*𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
119	83, 118	eqbrtrrd 5139	. . 3 ⊢ ((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) → Σ*𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝐶 ≤ Σ*𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
120		vex 3467	. . . . . . . . 9 ⊢ 𝑗 ∈ V
121		vex 3467	. . . . . . . . 9 ⊢ 𝑘 ∈ V
122	120, 121	op2ndd 7997	. . . . . . . 8 ⊢ (𝑧 = ⟨𝑗, 𝑘⟩ → (2nd ‘𝑧) = 𝑘)
123	122	eqcomd 2775	. . . . . . 7 ⊢ (𝑧 = ⟨𝑗, 𝑘⟩ → 𝑘 = (2nd ‘𝑧))
124	123, 18	syl 18	. . . . . 6 ⊢ (𝑧 = ⟨𝑗, 𝑘⟩ → 𝐶 = ⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
125	124	eqcomd 2775	. . . . 5 ⊢ (𝑧 = ⟨𝑗, 𝑘⟩ → ⦋(2nd ‘𝑧) / 𝑘⦌𝐶 = 𝐶)
126	76	anasss 471	. . . . 5 ⊢ ((𝜑 ∧ (𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐵)) → 𝐶 ∈ (0[,]+∞))
127	14, 125, 1, 2, 126	esum2d 34428	. . . 4 ⊢ (𝜑 → Σ*𝑗 ∈ 𝐴Σ*𝑘 ∈ 𝐵𝐶 = Σ*𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
128	127	adantr 485	. . 3 ⊢ ((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) → Σ*𝑗 ∈ 𝐴Σ*𝑘 ∈ 𝐵𝐶 = Σ*𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵)⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
129	119, 128	breqtrrd 5143	. 2 ⊢ ((𝜑 ∧ ((𝑓:∪ 𝑗 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑗 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑗 ∈ 𝐴 ({𝑗} × 𝐵))) → Σ*𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝐶 ≤ Σ*𝑗 ∈ 𝐴Σ*𝑘 ∈ 𝐵𝐶)
130	11, 129	exlimddv 1962	1 ⊢ (𝜑 → Σ*𝑘 ∈ ∪ 𝑗 ∈ 𝐴 𝐵𝐶 ≤ Σ*𝑗 ∈ 𝐴Σ*𝑘 ∈ 𝐵𝐶)

Syntax hints:   → wi 4   ∧ wa 400   = wceq 1567  ∃wex 1806   ∈ wcel 2149  ∀wral 3085  ∃wrex 3095  Vcvv 3463  ⦋csb 3861   ⊆ wss 3913  {csn 4594  ⟨cop 4600  ∪ ciun 4960   class class class wbr 5113   × cxp 5660  ^◡ccnv 5661  ran crn 5663   Fn wfn 6532  –1-1→wf1 6534  –1-1-onto→wf1o 6536  ‘cfv 6537  (class class class)co 7411  1^st c1st 7984  2^nd c2nd 7985  0cc0 11100  +∞cpnf 11240   ≤ cle 11244  [,]cicc 13375  Σ^*cesum 34362

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-rep 5242  ax-sep 5261  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733  ax-reg 9554  ax-inf2 9610  ax-ac2 10447  ax-cnex 11156  ax-resscn 11157  ax-1cn 11158  ax-icn 11159  ax-addcl 11160  ax-addrcl 11161  ax-mulcl 11162  ax-mulrcl 11163  ax-mulcom 11164  ax-addass 11165  ax-mulass 11166  ax-distr 11167  ax-i2m1 11168  ax-1ne0 11169  ax-1rid 11170  ax-rnegex 11171  ax-rrecex 11172  ax-cnre 11173  ax-pre-lttri 11174  ax-pre-lttrn 11175  ax-pre-ltadd 11176  ax-pre-mulgt0 11177  ax-pre-sup 11178  ax-addf 11179  ax-mulf 11180

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-rmo 3376  df-reu 3377  df-rab 3424  df-v 3465  df-sbc 3754  df-csb 3862  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-pss 3933  df-nul 4295  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-tp 4599  df-op 4601  df-uni 4877  df-int 4917  df-iun 4962  df-iin 4963  df-br 5114  df-opab 5178  df-mpt 5197  df-tr 5223  df-id 5557  df-eprel 5562  df-po 5570  df-so 5571  df-fr 5615  df-se 5616  df-we 5617  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-isom 6546  df-riota 7368  df-ov 7414  df-oprab 7415  df-mpo 7416  df-of 7675  df-om 7863  df-1st 7986  df-2nd 7987  df-supp 8157  df-frecs 8278  df-wrecs 8309  df-recs 8358  df-rdg 8397  df-1o 8453  df-2o 8454  df-er 8694  df-map 8826  df-pm 8827  df-ixp 8896  df-en 8944  df-dom 8945  df-sdom 8946  df-fin 8947  df-fsupp 9322  df-fi 9371  df-sup 9402  df-inf 9403  df-oi 9472  df-r1 9736  df-rank 9737  df-card 9925  df-ac 10100  df-pnf 11245  df-mnf 11246  df-xr 11247  df-ltxr 11248  df-le 11249  df-sub 11443  df-neg 11444  df-div 11872  df-nn 12234  df-2 12303  df-3 12304  df-4 12305  df-5 12306  df-6 12307  df-7 12308  df-8 12309  df-9 12310  df-n0 12505  df-z 12592  df-dec 12712  df-uz 12863  df-q 12973  df-rp 13017  df-xneg 13137  df-xadd 13138  df-xmul 13139  df-ioo 13376  df-ioc 13377  df-ico 13378  df-icc 13379  df-fz 13536  df-fzo 13683  df-fl 13825  df-mod 13903  df-seq 14038  df-exp 14098  df-fac 14310  df-bc 14339  df-hash 14367  df-shft 15104  df-cj 15150  df-re 15151  df-im 15152  df-sqrt 15286  df-abs 15287  df-limsup 15522  df-clim 15539  df-rlim 15540  df-sum 15738  df-ef 16121  df-sin 16123  df-cos 16124  df-pi 16126  df-struct 17207  df-sets 17224  df-slot 17242  df-ndx 17254  df-base 17270  df-ress 17291  df-plusg 17323  df-mulr 17324  df-starv 17325  df-sca 17326  df-vsca 17327  df-ip 17328  df-tset 17329  df-ple 17330  df-ds 17332  df-unif 17333  df-hom 17334  df-cco 17335  df-rest 17475  df-topn 17476  df-0g 17494  df-gsum 17495  df-topgen 17496  df-pt 17497  df-prds 17500  df-ordt 17555  df-xrs 17556  df-qtop 17561  df-imas 17562  df-xps 17564  df-mre 17638  df-mrc 17639  df-acs 17641  df-ps 18622  df-tsr 18623  df-plusf 18697  df-mgm 18698  df-sgrp 18777  df-mnd 18793  df-mhm 18841  df-submnd 18842  df-grp 19003  df-minusg 19004  df-sbg 19005  df-mulg 19134  df-subg 19189  df-cntz 19387  df-cmn 19852  df-abl 19853  df-mgp 20217  df-rng 20231  df-ur 20264  df-ring 20317  df-cring 20318  df-subrng 20631  df-subrg 20655  df-abv 20890  df-lmod 20961  df-scaf 20962  df-sra 21272  df-rgmod 21273  df-psmet 21483  df-xmet 21484  df-met 21485  df-bl 21486  df-mopn 21487  df-fbas 21488  df-fg 21489  df-cnfld 21492  df-top 23020  df-topon 23037  df-topsp 23059  df-bases 23072  df-cld 23145  df-ntr 23146  df-cls 23147  df-nei 23224  df-lp 23262  df-perf 23263  df-cn 23353  df-cnp 23354  df-haus 23441  df-tx 23688  df-hmeo 23881  df-fil 23972  df-fm 24064  df-flim 24065  df-flf 24066  df-tmd 24198  df-tgp 24199  df-tsms 24253  df-trg 24286  df-xms 24446  df-ms 24447  df-tms 24448  df-nm 24708  df-ngp 24709  df-nrg 24711  df-nlm 24712  df-ii 25005  df-cncf 25006  df-limc 25994  df-dv 25995  df-log 26687  df-esum 34363

This theorem is referenced by:  omssubadd  34635