Theorem fsumiunle 32682

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.)

Hypotheses

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

Assertion

Ref	Expression
fsumiunle	⊢ (𝜑 → Σ𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝐶 ≤ Σ𝑥 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶)

Distinct variable groups:   𝐴,𝑘,𝑥   𝐵,𝑘   𝑥,𝐶   𝜑,𝑘,𝑥

Allowed substitution hints:   𝐵(𝑥)   𝐶(𝑘)

Proof of Theorem fsumiunle

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

Step	Hyp	Ref	Expression
1		fsumiunle.1	. . . 4 ⊢ (𝜑 → 𝐴 ∈ Fin)
2		fsumiunle.2	. . . 4 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐵 ∈ Fin)
3	1, 2	aciunf1 32535	. . 3 ⊢ (𝜑 → ∃𝑓(𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1→∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙))
4		f1f1orn 6849	. . . . . 6 ⊢ (𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1→∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) → 𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓)
5	4	anim1i 613	. . . . 5 ⊢ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1→∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) → (𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙))
6		f1f 6793	. . . . . . 7 ⊢ (𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1→∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) → 𝑓:∪ 𝑥 ∈ 𝐴 𝐵⟶∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))
7	6	frnd 6731	. . . . . 6 ⊢ (𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1→∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) → ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))
8	7	adantr 479	. . . . 5 ⊢ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1→∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) → ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))
9	5, 8	jca 510	. . . 4 ⊢ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1→∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) → ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)))
10	9	eximi 1829	. . 3 ⊢ (∃𝑓(𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1→∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) → ∃𝑓((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)))
11	3, 10	syl 17	. 2 ⊢ (𝜑 → ∃𝑓((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)))
12		csbeq1a 3903	. . . . . . 7 ⊢ (𝑘 = 𝑦 → 𝐶 = ⦋𝑦 / 𝑘⦌𝐶)
13		nfcv 2891	. . . . . . 7 ⊢ Ⅎ𝑦∪ 𝑥 ∈ 𝐴 𝐵
14		nfcv 2891	. . . . . . 7 ⊢ Ⅎ𝑘∪ 𝑥 ∈ 𝐴 𝐵
15		nfcv 2891	. . . . . . 7 ⊢ Ⅎ𝑦𝐶
16		nfcsb1v 3914	. . . . . . 7 ⊢ Ⅎ𝑘⦋𝑦 / 𝑘⦌𝐶
17	12, 13, 14, 15, 16	cbvsum 15682	. . . . . 6 ⊢ Σ𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝐶 = Σ𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵⦋𝑦 / 𝑘⦌𝐶
18		csbeq1 3892	. . . . . . 7 ⊢ (𝑦 = (2nd ‘𝑧) → ⦋𝑦 / 𝑘⦌𝐶 = ⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
19		snfi 9071	. . . . . . . . . . . 12 ⊢ {𝑥} ∈ Fin
20		xpfi 9346	. . . . . . . . . . . 12 ⊢ (({𝑥} ∈ Fin ∧ 𝐵 ∈ Fin) → ({𝑥} × 𝐵) ∈ Fin)
21	19, 2, 20	sylancr 585	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ({𝑥} × 𝐵) ∈ Fin)
22	21	ralrimiva 3135	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ∈ Fin)
23		iunfi 9371	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ∈ Fin) → ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ∈ Fin)
24	1, 22, 23	syl2anc 582	. . . . . . . . 9 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ∈ Fin)
25	24	adantr 479	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ∈ Fin)
26		simprr 771	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))
27	25, 26	ssfid 9295	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → ran 𝑓 ∈ Fin)
28		simprl 769	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → 𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓)
29		f1ocnv 6850	. . . . . . . . 9 ⊢ (𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 → ◡𝑓:ran 𝑓–1-1-onto→∪ 𝑥 ∈ 𝐴 𝐵)
30	28, 29	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → ◡𝑓:ran 𝑓–1-1-onto→∪ 𝑥 ∈ 𝐴 𝐵)
31	30	adantrlr 721	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → ◡𝑓:ran 𝑓–1-1-onto→∪ 𝑥 ∈ 𝐴 𝐵)
32		nfv 1909	. . . . . . . . . 10 ⊢ Ⅎ𝑥𝜑
33		nfcv 2891	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥𝑓
34		nfiu1 5031	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵
35	33	nfrn 5954	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥ran 𝑓
36	33, 34, 35	nff1o 6836	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥 𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓
37		nfv 1909	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(2nd ‘(𝑓‘𝑙)) = 𝑙
38	34, 37	nfralw 3298	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙
39	36, 38	nfan 1894	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙)
40		nfcv 2891	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥ran 𝑓
41		nfiu1 5031	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)
42	40, 41	nfss 3969	. . . . . . . . . . 11 ⊢ Ⅎ𝑥ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)
43	39, 42	nfan 1894	. . . . . . . . . 10 ⊢ Ⅎ𝑥((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))
44	32, 43	nfan 1894	. . . . . . . . 9 ⊢ Ⅎ𝑥(𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)))
45		nfv 1909	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑧 ∈ ran 𝑓
46	44, 45	nfan 1894	. . . . . . . 8 ⊢ Ⅎ𝑥((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓)
47		simpr 483	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → (𝑓‘𝑘) = 𝑧)
48	47	fveq2d 6900	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → (2nd ‘(𝑓‘𝑘)) = (2nd ‘𝑧))
49		simplr 767	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵)
50		simp-4r 782	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)))
51	50	simpld 493	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → (𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙))
52	51	simprd 494	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙)
53	52	ad2antrr 724	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙)
54		2fveq3 6901	. . . . . . . . . . . . . 14 ⊢ (𝑙 = 𝑘 → (2nd ‘(𝑓‘𝑙)) = (2nd ‘(𝑓‘𝑘)))
55		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑙 = 𝑘 → 𝑙 = 𝑘)
56	54, 55	eqeq12d 2741	. . . . . . . . . . . . 13 ⊢ (𝑙 = 𝑘 → ((2nd ‘(𝑓‘𝑙)) = 𝑙 ↔ (2nd ‘(𝑓‘𝑘)) = 𝑘))
57	56	rspcva 3604	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) → (2nd ‘(𝑓‘𝑘)) = 𝑘)
58	49, 53, 57	syl2anc 582	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → (2nd ‘(𝑓‘𝑘)) = 𝑘)
59	48, 58	eqtr3d 2767	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → (2nd ‘𝑧) = 𝑘)
60	51	simpld 493	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → 𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓)
61	60	ad2antrr 724	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → 𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓)
62		f1ocnvfv1 7285	. . . . . . . . . . 11 ⊢ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → (◡𝑓‘(𝑓‘𝑘)) = 𝑘)
63	61, 49, 62	syl2anc 582	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → (◡𝑓‘(𝑓‘𝑘)) = 𝑘)
64	47	fveq2d 6900	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → (◡𝑓‘(𝑓‘𝑘)) = (◡𝑓‘𝑧))
65	59, 63, 64	3eqtr2rd 2772	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → (◡𝑓‘𝑧) = (2nd ‘𝑧))
66		f1ofn 6839	. . . . . . . . . . 11 ⊢ (𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 → 𝑓 Fn ∪ 𝑥 ∈ 𝐴 𝐵)
67	60, 66	syl 17	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → 𝑓 Fn ∪ 𝑥 ∈ 𝐴 𝐵)
68		simpllr 774	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → 𝑧 ∈ ran 𝑓)
69		fvelrnb 6958	. . . . . . . . . . 11 ⊢ (𝑓 Fn ∪ 𝑥 ∈ 𝐴 𝐵 → (𝑧 ∈ ran 𝑓 ↔ ∃𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(𝑓‘𝑘) = 𝑧))
70	69	biimpa 475	. . . . . . . . . 10 ⊢ ((𝑓 Fn ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ran 𝑓) → ∃𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(𝑓‘𝑘) = 𝑧)
71	67, 68, 70	syl2anc 582	. . . . . . . . 9 ⊢ (((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → ∃𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(𝑓‘𝑘) = 𝑧)
72	65, 71	r19.29a 3151	. . . . . . . 8 ⊢ (((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → (◡𝑓‘𝑧) = (2nd ‘𝑧))
73	26	sselda 3976	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) → 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))
74		eliun 5001	. . . . . . . . 9 ⊢ (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ ∃𝑥 ∈ 𝐴 𝑧 ∈ ({𝑥} × 𝐵))
75	73, 74	sylib 217	. . . . . . . 8 ⊢ (((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) → ∃𝑥 ∈ 𝐴 𝑧 ∈ ({𝑥} × 𝐵))
76	46, 72, 75	r19.29af 3255	. . . . . . 7 ⊢ (((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) → (◡𝑓‘𝑧) = (2nd ‘𝑧))
77		nfv 1909	. . . . . . . . . 10 ⊢ Ⅎ𝑘(𝜑 ∧ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵)
78		nfcv 2891	. . . . . . . . . . 11 ⊢ Ⅎ𝑘ℂ
79	16, 78	nfel 2906	. . . . . . . . . 10 ⊢ Ⅎ𝑘⦋𝑦 / 𝑘⦌𝐶 ∈ ℂ
80	77, 79	nfim 1891	. . . . . . . . 9 ⊢ Ⅎ𝑘((𝜑 ∧ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → ⦋𝑦 / 𝑘⦌𝐶 ∈ ℂ)
81		eleq1w 2808	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑦 → (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵))
82	81	anbi2d 628	. . . . . . . . . 10 ⊢ (𝑘 = 𝑦 → ((𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ↔ (𝜑 ∧ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵)))
83	12	eleq1d 2810	. . . . . . . . . 10 ⊢ (𝑘 = 𝑦 → (𝐶 ∈ ℂ ↔ ⦋𝑦 / 𝑘⦌𝐶 ∈ ℂ))
84	82, 83	imbi12d 343	. . . . . . . . 9 ⊢ (𝑘 = 𝑦 → (((𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → 𝐶 ∈ ℂ) ↔ ((𝜑 ∧ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → ⦋𝑦 / 𝑘⦌𝐶 ∈ ℂ)))
85		nfcv 2891	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥𝑘
86	85, 34	nfel 2906	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵
87	32, 86	nfan 1894	. . . . . . . . . 10 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵)
88		fsumiunle.3	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℝ)
89	88	adantllr 717	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℝ)
90	89	recnd 11279	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ)
91		eliun 5001	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵)
92	91	biimpi 215	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → ∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵)
93	92	adantl 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → ∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵)
94	87, 90, 93	r19.29af 3255	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → 𝐶 ∈ ℂ)
95	80, 84, 94	chvarfv 2228	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → ⦋𝑦 / 𝑘⦌𝐶 ∈ ℂ)
96	95	adantlr 713	. . . . . . 7 ⊢ (((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → ⦋𝑦 / 𝑘⦌𝐶 ∈ ℂ)
97	18, 27, 31, 76, 96	fsumf1o 15710	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → Σ𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵⦋𝑦 / 𝑘⦌𝐶 = Σ𝑧 ∈ ran 𝑓⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
98	17, 97	eqtrid 2777	. . . . 5 ⊢ ((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → Σ𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝐶 = Σ𝑧 ∈ ran 𝑓⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
99	98	eqcomd 2731	. . . 4 ⊢ ((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → Σ𝑧 ∈ ran 𝑓⦋(2nd ‘𝑧) / 𝑘⦌𝐶 = Σ𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝐶)
100		nfcv 2891	. . . . . . . . 9 ⊢ Ⅎ𝑥𝑧
101	100, 41	nfel 2906	. . . . . . . 8 ⊢ Ⅎ𝑥 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)
102	32, 101	nfan 1894	. . . . . . 7 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))
103		xp2nd 8027	. . . . . . . . 9 ⊢ (𝑧 ∈ ({𝑥} × 𝐵) → (2nd ‘𝑧) ∈ 𝐵)
104	103	adantl 480	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → (2nd ‘𝑧) ∈ 𝐵)
105	88	ralrimiva 3135	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑘 ∈ 𝐵 𝐶 ∈ ℝ)
106	105	adantlr 713	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) ∧ 𝑥 ∈ 𝐴) → ∀𝑘 ∈ 𝐵 𝐶 ∈ ℝ)
107	106	adantr 479	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → ∀𝑘 ∈ 𝐵 𝐶 ∈ ℝ)
108		nfcsb1v 3914	. . . . . . . . . . 11 ⊢ Ⅎ𝑘⦋(2nd ‘𝑧) / 𝑘⦌𝐶
109	108	nfel1 2908	. . . . . . . . . 10 ⊢ Ⅎ𝑘⦋(2nd ‘𝑧) / 𝑘⦌𝐶 ∈ ℝ
110		csbeq1a 3903	. . . . . . . . . . 11 ⊢ (𝑘 = (2nd ‘𝑧) → 𝐶 = ⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
111	110	eleq1d 2810	. . . . . . . . . 10 ⊢ (𝑘 = (2nd ‘𝑧) → (𝐶 ∈ ℝ ↔ ⦋(2nd ‘𝑧) / 𝑘⦌𝐶 ∈ ℝ))
112	109, 111	rspc 3594	. . . . . . . . 9 ⊢ ((2nd ‘𝑧) ∈ 𝐵 → (∀𝑘 ∈ 𝐵 𝐶 ∈ ℝ → ⦋(2nd ‘𝑧) / 𝑘⦌𝐶 ∈ ℝ))
113	112	imp 405	. . . . . . . 8 ⊢ (((2nd ‘𝑧) ∈ 𝐵 ∧ ∀𝑘 ∈ 𝐵 𝐶 ∈ ℝ) → ⦋(2nd ‘𝑧) / 𝑘⦌𝐶 ∈ ℝ)
114	104, 107, 113	syl2anc 582	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → ⦋(2nd ‘𝑧) / 𝑘⦌𝐶 ∈ ℝ)
115	74	biimpi 215	. . . . . . . 8 ⊢ (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) → ∃𝑥 ∈ 𝐴 𝑧 ∈ ({𝑥} × 𝐵))
116	115	adantl 480	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) → ∃𝑥 ∈ 𝐴 𝑧 ∈ ({𝑥} × 𝐵))
117	102, 114, 116	r19.29af 3255	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) → ⦋(2nd ‘𝑧) / 𝑘⦌𝐶 ∈ ℝ)
118	117	adantlr 713	. . . . 5 ⊢ (((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) → ⦋(2nd ‘𝑧) / 𝑘⦌𝐶 ∈ ℝ)
119		xp1st 8026	. . . . . . . . . . 11 ⊢ (𝑧 ∈ ({𝑥} × 𝐵) → (1st ‘𝑧) ∈ {𝑥})
120		elsni 4647	. . . . . . . . . . 11 ⊢ ((1st ‘𝑧) ∈ {𝑥} → (1st ‘𝑧) = 𝑥)
121	119, 120	syl 17	. . . . . . . . . 10 ⊢ (𝑧 ∈ ({𝑥} × 𝐵) → (1st ‘𝑧) = 𝑥)
122	121, 103	jca 510	. . . . . . . . 9 ⊢ (𝑧 ∈ ({𝑥} × 𝐵) → ((1st ‘𝑧) = 𝑥 ∧ (2nd ‘𝑧) ∈ 𝐵))
123		simplll 773	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ ((1st ‘𝑧) = 𝑥 ∧ (2nd ‘𝑧) ∈ 𝐵)) → 𝜑)
124		simplr 767	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ ((1st ‘𝑧) = 𝑥 ∧ (2nd ‘𝑧) ∈ 𝐵)) → 𝑥 ∈ 𝐴)
125		fsumiunle.4	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 0 ≤ 𝐶)
126	125	ralrimiva 3135	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑘 ∈ 𝐵 0 ≤ 𝐶)
127	123, 124, 126	syl2anc 582	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ ((1st ‘𝑧) = 𝑥 ∧ (2nd ‘𝑧) ∈ 𝐵)) → ∀𝑘 ∈ 𝐵 0 ≤ 𝐶)
128	122, 127	sylan2 591	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → ∀𝑘 ∈ 𝐵 0 ≤ 𝐶)
129		nfcv 2891	. . . . . . . . . . 11 ⊢ Ⅎ𝑘0
130		nfcv 2891	. . . . . . . . . . 11 ⊢ Ⅎ𝑘 ≤
131	129, 130, 108	nfbr 5196	. . . . . . . . . 10 ⊢ Ⅎ𝑘0 ≤ ⦋(2nd ‘𝑧) / 𝑘⦌𝐶
132	110	breq2d 5161	. . . . . . . . . 10 ⊢ (𝑘 = (2nd ‘𝑧) → (0 ≤ 𝐶 ↔ 0 ≤ ⦋(2nd ‘𝑧) / 𝑘⦌𝐶))
133	131, 132	rspc 3594	. . . . . . . . 9 ⊢ ((2nd ‘𝑧) ∈ 𝐵 → (∀𝑘 ∈ 𝐵 0 ≤ 𝐶 → 0 ≤ ⦋(2nd ‘𝑧) / 𝑘⦌𝐶))
134	133	imp 405	. . . . . . . 8 ⊢ (((2nd ‘𝑧) ∈ 𝐵 ∧ ∀𝑘 ∈ 𝐵 0 ≤ 𝐶) → 0 ≤ ⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
135	104, 128, 134	syl2anc 582	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → 0 ≤ ⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
136	102, 135, 116	r19.29af 3255	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) → 0 ≤ ⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
137	136	adantlr 713	. . . . 5 ⊢ (((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) → 0 ≤ ⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
138	25, 118, 137, 26	fsumless 15783	. . . 4 ⊢ ((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → Σ𝑧 ∈ ran 𝑓⦋(2nd ‘𝑧) / 𝑘⦌𝐶 ≤ Σ𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
139	99, 138	eqbrtrrd 5173	. . 3 ⊢ ((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → Σ𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝐶 ≤ Σ𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
140		nfcv 2891	. . . . . . . 8 ⊢ Ⅎ𝑦𝐵
141		nfcv 2891	. . . . . . . 8 ⊢ Ⅎ𝑘𝐵
142	12, 140, 141, 15, 16	cbvsum 15682	. . . . . . 7 ⊢ Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑦 ∈ 𝐵 ⦋𝑦 / 𝑘⦌𝐶
143	142	a1i 11	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑦 ∈ 𝐵 ⦋𝑦 / 𝑘⦌𝐶)
144	143	sumeq2sdv 15691	. . . . 5 ⊢ (𝜑 → Σ𝑥 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑥 ∈ 𝐴 Σ𝑦 ∈ 𝐵 ⦋𝑦 / 𝑘⦌𝐶)
145		vex 3465	. . . . . . . . . 10 ⊢ 𝑥 ∈ V
146		vex 3465	. . . . . . . . . 10 ⊢ 𝑦 ∈ V
147	145, 146	op2ndd 8005	. . . . . . . . 9 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (2nd ‘𝑧) = 𝑦)
148	147	eqcomd 2731	. . . . . . . 8 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → 𝑦 = (2nd ‘𝑧))
149	148	csbeq1d 3893	. . . . . . 7 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ⦋𝑦 / 𝑘⦌𝐶 = ⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
150	149	eqcomd 2731	. . . . . 6 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ⦋(2nd ‘𝑧) / 𝑘⦌𝐶 = ⦋𝑦 / 𝑘⦌𝐶)
151		nfv 1909	. . . . . . . . 9 ⊢ Ⅎ𝑘((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵)
152	16	nfel1 2908	. . . . . . . . 9 ⊢ Ⅎ𝑘⦋𝑦 / 𝑘⦌𝐶 ∈ ℂ
153	151, 152	nfim 1891	. . . . . . . 8 ⊢ Ⅎ𝑘(((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → ⦋𝑦 / 𝑘⦌𝐶 ∈ ℂ)
154		eleq1w 2808	. . . . . . . . . 10 ⊢ (𝑘 = 𝑦 → (𝑘 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵))
155	154	anbi2d 628	. . . . . . . . 9 ⊢ (𝑘 = 𝑦 → (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) ↔ ((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵)))
156	155, 83	imbi12d 343	. . . . . . . 8 ⊢ (𝑘 = 𝑦 → ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ) ↔ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → ⦋𝑦 / 𝑘⦌𝐶 ∈ ℂ)))
157	88	recnd 11279	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ)
158	153, 156, 157	chvarfv 2228	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → ⦋𝑦 / 𝑘⦌𝐶 ∈ ℂ)
159	158	anasss 465	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → ⦋𝑦 / 𝑘⦌𝐶 ∈ ℂ)
160	150, 1, 2, 159	fsum2d 15758	. . . . 5 ⊢ (𝜑 → Σ𝑥 ∈ 𝐴 Σ𝑦 ∈ 𝐵 ⦋𝑦 / 𝑘⦌𝐶 = Σ𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
161	144, 160	eqtrd 2765	. . . 4 ⊢ (𝜑 → Σ𝑥 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
162	161	adantr 479	. . 3 ⊢ ((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → Σ𝑥 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
163	139, 162	breqtrrd 5177	. 2 ⊢ ((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → Σ𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝐶 ≤ Σ𝑥 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶)
164	11, 163	exlimddv 1930	1 ⊢ (𝜑 → Σ𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝐶 ≤ Σ𝑥 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶)

Syntax hints:   → wi 4   ∧ wa 394   = wceq 1533  ∃wex 1773   ∈ wcel 2098  ∀wral 3050  ∃wrex 3059  ⦋csb 3889   ⊆ wss 3944  {csn 4630  ⟨cop 4636  ∪ ciun 4997   class class class wbr 5149   × cxp 5676  ^◡ccnv 5677  ran crn 5679   Fn wfn 6544  –1-1→wf1 6546  –1-1-onto→wf1o 6548  ‘cfv 6549  1^st c1st 7992  2^nd c2nd 7993  Fincfn 8964  ℂcc 11143  ℝcr 11144  0cc0 11145   ≤ cle 11286  Σcsu 15673

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741  ax-reg 9622  ax-inf2 9671  ax-ac2 10493  ax-cnex 11201  ax-resscn 11202  ax-1cn 11203  ax-icn 11204  ax-addcl 11205  ax-addrcl 11206  ax-mulcl 11207  ax-mulrcl 11208  ax-mulcom 11209  ax-addass 11210  ax-mulass 11211  ax-distr 11212  ax-i2m1 11213  ax-1ne0 11214  ax-1rid 11215  ax-rnegex 11216  ax-rrecex 11217  ax-cnre 11218  ax-pre-lttri 11219  ax-pre-lttrn 11220  ax-pre-ltadd 11221  ax-pre-mulgt0 11222  ax-pre-sup 11223

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3363  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3964  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-int 4951  df-iun 4999  df-iin 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-se 5634  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-pred 6307  df-ord 6374  df-on 6375  df-lim 6376  df-suc 6377  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-isom 6558  df-riota 7375  df-ov 7422  df-oprab 7423  df-mpo 7424  df-om 7872  df-1st 7994  df-2nd 7995  df-frecs 8287  df-wrecs 8318  df-recs 8392  df-rdg 8431  df-1o 8487  df-er 8725  df-en 8965  df-dom 8966  df-sdom 8967  df-fin 8968  df-sup 9472  df-oi 9540  df-r1 9794  df-rank 9795  df-card 9969  df-ac 10146  df-pnf 11287  df-mnf 11288  df-xr 11289  df-ltxr 11290  df-le 11291  df-sub 11483  df-neg 11484  df-div 11909  df-nn 12251  df-2 12313  df-3 12314  df-n0 12511  df-z 12597  df-uz 12861  df-rp 13015  df-ico 13370  df-fz 13525  df-fzo 13668  df-seq 14008  df-exp 14068  df-hash 14331  df-cj 15087  df-re 15088  df-im 15089  df-sqrt 15223  df-abs 15224  df-clim 15473  df-sum 15674

This theorem is referenced by:  hgt750lema  34422