Theorem fsumiunle 32741

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 32574	. . 3 ⊢ (𝜑 → ∃𝑓(𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1→∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙))
4		f1f1orn 6825	. . . . . 6 ⊢ (𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1→∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) → 𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓)
5	4	anim1i 615	. . . . 5 ⊢ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1→∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) → (𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙))
6		f1f 6770	. . . . . . 7 ⊢ (𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1→∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) → 𝑓:∪ 𝑥 ∈ 𝐴 𝐵⟶∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))
7	6	frnd 6710	. . . . . 6 ⊢ (𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1→∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) → ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))
8	7	adantr 480	. . . . 5 ⊢ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1→∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) → ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))
9	5, 8	jca 511	. . . 4 ⊢ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1→∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) → ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)))
10	9	eximi 1834	. . 3 ⊢ (∃𝑓(𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1→∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) → ∃𝑓((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)))
11	3, 10	syl 17	. 2 ⊢ (𝜑 → ∃𝑓((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)))
12		csbeq1a 3886	. . . . . . 7 ⊢ (𝑘 = 𝑦 → 𝐶 = ⦋𝑦 / 𝑘⦌𝐶)
13		nfcv 2897	. . . . . . 7 ⊢ Ⅎ𝑦𝐶
14		nfcsb1v 3896	. . . . . . 7 ⊢ Ⅎ𝑘⦋𝑦 / 𝑘⦌𝐶
15	12, 13, 14	cbvsum 15698	. . . . . 6 ⊢ Σ𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝐶 = Σ𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵⦋𝑦 / 𝑘⦌𝐶
16		csbeq1 3875	. . . . . . 7 ⊢ (𝑦 = (2nd ‘𝑧) → ⦋𝑦 / 𝑘⦌𝐶 = ⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
17		snfi 9051	. . . . . . . . . . . 12 ⊢ {𝑥} ∈ Fin
18		xpfi 9324	. . . . . . . . . . . 12 ⊢ (({𝑥} ∈ Fin ∧ 𝐵 ∈ Fin) → ({𝑥} × 𝐵) ∈ Fin)
19	17, 2, 18	sylancr 587	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ({𝑥} × 𝐵) ∈ Fin)
20	19	ralrimiva 3130	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ∈ Fin)
21		iunfi 9349	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ∈ Fin) → ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ∈ Fin)
22	1, 20, 21	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ∈ Fin)
23	22	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ∈ Fin)
24		simprr 772	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))
25	23, 24	ssfid 9267	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → ran 𝑓 ∈ Fin)
26		simprl 770	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → 𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓)
27		f1ocnv 6826	. . . . . . . . 9 ⊢ (𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 → ◡𝑓:ran 𝑓–1-1-onto→∪ 𝑥 ∈ 𝐴 𝐵)
28	26, 27	syl 17	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → ◡𝑓:ran 𝑓–1-1-onto→∪ 𝑥 ∈ 𝐴 𝐵)
29	28	adantrlr 723	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → ◡𝑓:ran 𝑓–1-1-onto→∪ 𝑥 ∈ 𝐴 𝐵)
30		nfv 1913	. . . . . . . . . 10 ⊢ Ⅎ𝑥𝜑
31		nfcv 2897	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥𝑓
32		nfiu1 5000	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵
33	31	nfrn 5929	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥ran 𝑓
34	31, 32, 33	nff1o 6812	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥 𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓
35		nfv 1913	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(2nd ‘(𝑓‘𝑙)) = 𝑙
36	32, 35	nfralw 3289	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙
37	34, 36	nfan 1898	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙)
38		nfcv 2897	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥ran 𝑓
39		nfiu1 5000	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)
40	38, 39	nfss 3949	. . . . . . . . . . 11 ⊢ Ⅎ𝑥ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)
41	37, 40	nfan 1898	. . . . . . . . . 10 ⊢ Ⅎ𝑥((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))
42	30, 41	nfan 1898	. . . . . . . . 9 ⊢ Ⅎ𝑥(𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)))
43		nfv 1913	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑧 ∈ ran 𝑓
44	42, 43	nfan 1898	. . . . . . . 8 ⊢ Ⅎ𝑥((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓)
45		simpr 484	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → (𝑓‘𝑘) = 𝑧)
46	45	fveq2d 6876	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → (2nd ‘(𝑓‘𝑘)) = (2nd ‘𝑧))
47		simplr 768	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵)
48		simp-4r 783	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)))
49	48	simpld 494	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → (𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙))
50	49	simprd 495	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙)
51	50	ad2antrr 726	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙)
52		2fveq3 6877	. . . . . . . . . . . . . 14 ⊢ (𝑙 = 𝑘 → (2nd ‘(𝑓‘𝑙)) = (2nd ‘(𝑓‘𝑘)))
53		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑙 = 𝑘 → 𝑙 = 𝑘)
54	52, 53	eqeq12d 2750	. . . . . . . . . . . . 13 ⊢ (𝑙 = 𝑘 → ((2nd ‘(𝑓‘𝑙)) = 𝑙 ↔ (2nd ‘(𝑓‘𝑘)) = 𝑘))
55	54	rspcva 3597	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) → (2nd ‘(𝑓‘𝑘)) = 𝑘)
56	47, 51, 55	syl2anc 584	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → (2nd ‘(𝑓‘𝑘)) = 𝑘)
57	46, 56	eqtr3d 2771	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → (2nd ‘𝑧) = 𝑘)
58	49	simpld 494	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → 𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓)
59	58	ad2antrr 726	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → 𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓)
60		f1ocnvfv1 7264	. . . . . . . . . . 11 ⊢ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → (◡𝑓‘(𝑓‘𝑘)) = 𝑘)
61	59, 47, 60	syl2anc 584	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → (◡𝑓‘(𝑓‘𝑘)) = 𝑘)
62	45	fveq2d 6876	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → (◡𝑓‘(𝑓‘𝑘)) = (◡𝑓‘𝑧))
63	57, 61, 62	3eqtr2rd 2776	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → (◡𝑓‘𝑧) = (2nd ‘𝑧))
64		f1ofn 6815	. . . . . . . . . . 11 ⊢ (𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 → 𝑓 Fn ∪ 𝑥 ∈ 𝐴 𝐵)
65	58, 64	syl 17	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → 𝑓 Fn ∪ 𝑥 ∈ 𝐴 𝐵)
66		simpllr 775	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → 𝑧 ∈ ran 𝑓)
67		fvelrnb 6935	. . . . . . . . . . 11 ⊢ (𝑓 Fn ∪ 𝑥 ∈ 𝐴 𝐵 → (𝑧 ∈ ran 𝑓 ↔ ∃𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(𝑓‘𝑘) = 𝑧))
68	67	biimpa 476	. . . . . . . . . 10 ⊢ ((𝑓 Fn ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ran 𝑓) → ∃𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(𝑓‘𝑘) = 𝑧)
69	65, 66, 68	syl2anc 584	. . . . . . . . 9 ⊢ (((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → ∃𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(𝑓‘𝑘) = 𝑧)
70	63, 69	r19.29a 3146	. . . . . . . 8 ⊢ (((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → (◡𝑓‘𝑧) = (2nd ‘𝑧))
71	24	sselda 3956	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) → 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))
72		eliun 4968	. . . . . . . . 9 ⊢ (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ ∃𝑥 ∈ 𝐴 𝑧 ∈ ({𝑥} × 𝐵))
73	71, 72	sylib 218	. . . . . . . 8 ⊢ (((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) → ∃𝑥 ∈ 𝐴 𝑧 ∈ ({𝑥} × 𝐵))
74	44, 70, 73	r19.29af 3249	. . . . . . 7 ⊢ (((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) → (◡𝑓‘𝑧) = (2nd ‘𝑧))
75		nfv 1913	. . . . . . . . . 10 ⊢ Ⅎ𝑘(𝜑 ∧ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵)
76		nfcv 2897	. . . . . . . . . . 11 ⊢ Ⅎ𝑘ℂ
77	14, 76	nfel 2912	. . . . . . . . . 10 ⊢ Ⅎ𝑘⦋𝑦 / 𝑘⦌𝐶 ∈ ℂ
78	75, 77	nfim 1895	. . . . . . . . 9 ⊢ Ⅎ𝑘((𝜑 ∧ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → ⦋𝑦 / 𝑘⦌𝐶 ∈ ℂ)
79		eleq1w 2816	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑦 → (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵))
80	79	anbi2d 630	. . . . . . . . . 10 ⊢ (𝑘 = 𝑦 → ((𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ↔ (𝜑 ∧ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵)))
81	12	eleq1d 2818	. . . . . . . . . 10 ⊢ (𝑘 = 𝑦 → (𝐶 ∈ ℂ ↔ ⦋𝑦 / 𝑘⦌𝐶 ∈ ℂ))
82	80, 81	imbi12d 344	. . . . . . . . 9 ⊢ (𝑘 = 𝑦 → (((𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → 𝐶 ∈ ℂ) ↔ ((𝜑 ∧ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → ⦋𝑦 / 𝑘⦌𝐶 ∈ ℂ)))
83		nfcv 2897	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥𝑘
84	83, 32	nfel 2912	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵
85	30, 84	nfan 1898	. . . . . . . . . 10 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵)
86		fsumiunle.3	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℝ)
87	86	adantllr 719	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℝ)
88	87	recnd 11255	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ)
89		eliun 4968	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵)
90	89	biimpi 216	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → ∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵)
91	90	adantl 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → ∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵)
92	85, 88, 91	r19.29af 3249	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → 𝐶 ∈ ℂ)
93	78, 82, 92	chvarfv 2239	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → ⦋𝑦 / 𝑘⦌𝐶 ∈ ℂ)
94	93	adantlr 715	. . . . . . 7 ⊢ (((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → ⦋𝑦 / 𝑘⦌𝐶 ∈ ℂ)
95	16, 25, 29, 74, 94	fsumf1o 15726	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → Σ𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵⦋𝑦 / 𝑘⦌𝐶 = Σ𝑧 ∈ ran 𝑓⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
96	15, 95	eqtrid 2781	. . . . 5 ⊢ ((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → Σ𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝐶 = Σ𝑧 ∈ ran 𝑓⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
97	96	eqcomd 2740	. . . 4 ⊢ ((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → Σ𝑧 ∈ ran 𝑓⦋(2nd ‘𝑧) / 𝑘⦌𝐶 = Σ𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝐶)
98		nfcv 2897	. . . . . . . . 9 ⊢ Ⅎ𝑥𝑧
99	98, 39	nfel 2912	. . . . . . . 8 ⊢ Ⅎ𝑥 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)
100	30, 99	nfan 1898	. . . . . . 7 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))
101		xp2nd 8015	. . . . . . . . 9 ⊢ (𝑧 ∈ ({𝑥} × 𝐵) → (2nd ‘𝑧) ∈ 𝐵)
102	101	adantl 481	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → (2nd ‘𝑧) ∈ 𝐵)
103	86	ralrimiva 3130	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑘 ∈ 𝐵 𝐶 ∈ ℝ)
104	103	adantlr 715	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) ∧ 𝑥 ∈ 𝐴) → ∀𝑘 ∈ 𝐵 𝐶 ∈ ℝ)
105	104	adantr 480	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → ∀𝑘 ∈ 𝐵 𝐶 ∈ ℝ)
106		nfcsb1v 3896	. . . . . . . . . . 11 ⊢ Ⅎ𝑘⦋(2nd ‘𝑧) / 𝑘⦌𝐶
107	106	nfel1 2914	. . . . . . . . . 10 ⊢ Ⅎ𝑘⦋(2nd ‘𝑧) / 𝑘⦌𝐶 ∈ ℝ
108		csbeq1a 3886	. . . . . . . . . . 11 ⊢ (𝑘 = (2nd ‘𝑧) → 𝐶 = ⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
109	108	eleq1d 2818	. . . . . . . . . 10 ⊢ (𝑘 = (2nd ‘𝑧) → (𝐶 ∈ ℝ ↔ ⦋(2nd ‘𝑧) / 𝑘⦌𝐶 ∈ ℝ))
110	107, 109	rspc 3587	. . . . . . . . 9 ⊢ ((2nd ‘𝑧) ∈ 𝐵 → (∀𝑘 ∈ 𝐵 𝐶 ∈ ℝ → ⦋(2nd ‘𝑧) / 𝑘⦌𝐶 ∈ ℝ))
111	110	imp 406	. . . . . . . 8 ⊢ (((2nd ‘𝑧) ∈ 𝐵 ∧ ∀𝑘 ∈ 𝐵 𝐶 ∈ ℝ) → ⦋(2nd ‘𝑧) / 𝑘⦌𝐶 ∈ ℝ)
112	102, 105, 111	syl2anc 584	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → ⦋(2nd ‘𝑧) / 𝑘⦌𝐶 ∈ ℝ)
113	72	biimpi 216	. . . . . . . 8 ⊢ (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) → ∃𝑥 ∈ 𝐴 𝑧 ∈ ({𝑥} × 𝐵))
114	113	adantl 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) → ∃𝑥 ∈ 𝐴 𝑧 ∈ ({𝑥} × 𝐵))
115	100, 112, 114	r19.29af 3249	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) → ⦋(2nd ‘𝑧) / 𝑘⦌𝐶 ∈ ℝ)
116	115	adantlr 715	. . . . 5 ⊢ (((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) → ⦋(2nd ‘𝑧) / 𝑘⦌𝐶 ∈ ℝ)
117		xp1st 8014	. . . . . . . . . . 11 ⊢ (𝑧 ∈ ({𝑥} × 𝐵) → (1st ‘𝑧) ∈ {𝑥})
118		elsni 4616	. . . . . . . . . . 11 ⊢ ((1st ‘𝑧) ∈ {𝑥} → (1st ‘𝑧) = 𝑥)
119	117, 118	syl 17	. . . . . . . . . 10 ⊢ (𝑧 ∈ ({𝑥} × 𝐵) → (1st ‘𝑧) = 𝑥)
120	119, 101	jca 511	. . . . . . . . 9 ⊢ (𝑧 ∈ ({𝑥} × 𝐵) → ((1st ‘𝑧) = 𝑥 ∧ (2nd ‘𝑧) ∈ 𝐵))
121		simplll 774	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ ((1st ‘𝑧) = 𝑥 ∧ (2nd ‘𝑧) ∈ 𝐵)) → 𝜑)
122		simplr 768	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ ((1st ‘𝑧) = 𝑥 ∧ (2nd ‘𝑧) ∈ 𝐵)) → 𝑥 ∈ 𝐴)
123		fsumiunle.4	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 0 ≤ 𝐶)
124	123	ralrimiva 3130	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑘 ∈ 𝐵 0 ≤ 𝐶)
125	121, 122, 124	syl2anc 584	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ ((1st ‘𝑧) = 𝑥 ∧ (2nd ‘𝑧) ∈ 𝐵)) → ∀𝑘 ∈ 𝐵 0 ≤ 𝐶)
126	120, 125	sylan2 593	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → ∀𝑘 ∈ 𝐵 0 ≤ 𝐶)
127		nfcv 2897	. . . . . . . . . . 11 ⊢ Ⅎ𝑘0
128		nfcv 2897	. . . . . . . . . . 11 ⊢ Ⅎ𝑘 ≤
129	127, 128, 106	nfbr 5163	. . . . . . . . . 10 ⊢ Ⅎ𝑘0 ≤ ⦋(2nd ‘𝑧) / 𝑘⦌𝐶
130	108	breq2d 5128	. . . . . . . . . 10 ⊢ (𝑘 = (2nd ‘𝑧) → (0 ≤ 𝐶 ↔ 0 ≤ ⦋(2nd ‘𝑧) / 𝑘⦌𝐶))
131	129, 130	rspc 3587	. . . . . . . . 9 ⊢ ((2nd ‘𝑧) ∈ 𝐵 → (∀𝑘 ∈ 𝐵 0 ≤ 𝐶 → 0 ≤ ⦋(2nd ‘𝑧) / 𝑘⦌𝐶))
132	131	imp 406	. . . . . . . 8 ⊢ (((2nd ‘𝑧) ∈ 𝐵 ∧ ∀𝑘 ∈ 𝐵 0 ≤ 𝐶) → 0 ≤ ⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
133	102, 126, 132	syl2anc 584	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → 0 ≤ ⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
134	100, 133, 114	r19.29af 3249	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) → 0 ≤ ⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
135	134	adantlr 715	. . . . 5 ⊢ (((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) → 0 ≤ ⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
136	23, 116, 135, 24	fsumless 15799	. . . 4 ⊢ ((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → Σ𝑧 ∈ ran 𝑓⦋(2nd ‘𝑧) / 𝑘⦌𝐶 ≤ Σ𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
137	97, 136	eqbrtrrd 5140	. . 3 ⊢ ((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → Σ𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝐶 ≤ Σ𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
138	12, 13, 14	cbvsum 15698	. . . . . . 7 ⊢ Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑦 ∈ 𝐵 ⦋𝑦 / 𝑘⦌𝐶
139	138	a1i 11	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑦 ∈ 𝐵 ⦋𝑦 / 𝑘⦌𝐶)
140	139	sumeq2sdv 15706	. . . . 5 ⊢ (𝜑 → Σ𝑥 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑥 ∈ 𝐴 Σ𝑦 ∈ 𝐵 ⦋𝑦 / 𝑘⦌𝐶)
141		vex 3461	. . . . . . . . . 10 ⊢ 𝑥 ∈ V
142		vex 3461	. . . . . . . . . 10 ⊢ 𝑦 ∈ V
143	141, 142	op2ndd 7993	. . . . . . . . 9 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (2nd ‘𝑧) = 𝑦)
144	143	eqcomd 2740	. . . . . . . 8 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → 𝑦 = (2nd ‘𝑧))
145	144	csbeq1d 3876	. . . . . . 7 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ⦋𝑦 / 𝑘⦌𝐶 = ⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
146	145	eqcomd 2740	. . . . . 6 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ⦋(2nd ‘𝑧) / 𝑘⦌𝐶 = ⦋𝑦 / 𝑘⦌𝐶)
147		nfv 1913	. . . . . . . . 9 ⊢ Ⅎ𝑘((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵)
148	14	nfel1 2914	. . . . . . . . 9 ⊢ Ⅎ𝑘⦋𝑦 / 𝑘⦌𝐶 ∈ ℂ
149	147, 148	nfim 1895	. . . . . . . 8 ⊢ Ⅎ𝑘(((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → ⦋𝑦 / 𝑘⦌𝐶 ∈ ℂ)
150		eleq1w 2816	. . . . . . . . . 10 ⊢ (𝑘 = 𝑦 → (𝑘 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵))
151	150	anbi2d 630	. . . . . . . . 9 ⊢ (𝑘 = 𝑦 → (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) ↔ ((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵)))
152	151, 81	imbi12d 344	. . . . . . . 8 ⊢ (𝑘 = 𝑦 → ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ) ↔ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → ⦋𝑦 / 𝑘⦌𝐶 ∈ ℂ)))
153	86	recnd 11255	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ)
154	149, 152, 153	chvarfv 2239	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → ⦋𝑦 / 𝑘⦌𝐶 ∈ ℂ)
155	154	anasss 466	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → ⦋𝑦 / 𝑘⦌𝐶 ∈ ℂ)
156	146, 1, 2, 155	fsum2d 15774	. . . . 5 ⊢ (𝜑 → Σ𝑥 ∈ 𝐴 Σ𝑦 ∈ 𝐵 ⦋𝑦 / 𝑘⦌𝐶 = Σ𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
157	140, 156	eqtrd 2769	. . . 4 ⊢ (𝜑 → Σ𝑥 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
158	157	adantr 480	. . 3 ⊢ ((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → Σ𝑥 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
159	137, 158	breqtrrd 5144	. 2 ⊢ ((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → Σ𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝐶 ≤ Σ𝑥 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶)
160	11, 159	exlimddv 1934	1 ⊢ (𝜑 → Σ𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝐶 ≤ Σ𝑥 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1539  ∃wex 1778   ∈ wcel 2107  ∀wral 3050  ∃wrex 3059  ⦋csb 3872   ⊆ wss 3924  {csn 4599  ⟨cop 4605  ∪ ciun 4964   class class class wbr 5116   × cxp 5649  ^◡ccnv 5650  ran crn 5652   Fn wfn 6522  –1-1→wf1 6524  –1-1-onto→wf1o 6526  ‘cfv 6527  1^st c1st 7980  2^nd c2nd 7981  Fincfn 8953  ℂcc 11119  ℝcr 11120  0cc0 11121   ≤ cle 11262  Σcsu 15689

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2706  ax-rep 5246  ax-sep 5263  ax-nul 5273  ax-pow 5332  ax-pr 5399  ax-un 7723  ax-reg 9598  ax-inf2 9647  ax-ac2 10469  ax-cnex 11177  ax-resscn 11178  ax-1cn 11179  ax-icn 11180  ax-addcl 11181  ax-addrcl 11182  ax-mulcl 11183  ax-mulrcl 11184  ax-mulcom 11185  ax-addass 11186  ax-mulass 11187  ax-distr 11188  ax-i2m1 11189  ax-1ne0 11190  ax-1rid 11191  ax-rnegex 11192  ax-rrecex 11193  ax-cnre 11194  ax-pre-lttri 11195  ax-pre-lttrn 11196  ax-pre-ltadd 11197  ax-pre-mulgt0 11198  ax-pre-sup 11199

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2808  df-nfc 2884  df-ne 2932  df-nel 3036  df-ral 3051  df-rex 3060  df-rmo 3357  df-reu 3358  df-rab 3414  df-v 3459  df-sbc 3764  df-csb 3873  df-dif 3927  df-un 3929  df-in 3931  df-ss 3941  df-pss 3944  df-nul 4307  df-if 4499  df-pw 4575  df-sn 4600  df-pr 4602  df-op 4606  df-uni 4881  df-int 4920  df-iun 4966  df-iin 4967  df-br 5117  df-opab 5179  df-mpt 5199  df-tr 5227  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-se 5604  df-we 5605  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-pred 6287  df-ord 6352  df-on 6353  df-lim 6354  df-suc 6355  df-iota 6480  df-fun 6529  df-fn 6530  df-f 6531  df-f1 6532  df-fo 6533  df-f1o 6534  df-fv 6535  df-isom 6536  df-riota 7356  df-ov 7402  df-oprab 7403  df-mpo 7404  df-om 7856  df-1st 7982  df-2nd 7983  df-frecs 8274  df-wrecs 8305  df-recs 8379  df-rdg 8418  df-1o 8474  df-er 8713  df-en 8954  df-dom 8955  df-sdom 8956  df-fin 8957  df-sup 9448  df-oi 9516  df-r1 9770  df-rank 9771  df-card 9945  df-ac 10122  df-pnf 11263  df-mnf 11264  df-xr 11265  df-ltxr 11266  df-le 11267  df-sub 11460  df-neg 11461  df-div 11887  df-nn 12233  df-2 12295  df-3 12296  df-n0 12494  df-z 12581  df-uz 12845  df-rp 13001  df-ico 13359  df-fz 13514  df-fzo 13661  df-seq 14009  df-exp 14069  df-hash 14337  df-cj 15105  df-re 15106  df-im 15107  df-sqrt 15241  df-abs 15242  df-clim 15491  df-sum 15690

This theorem is referenced by:  hgt750lema  34610