Theorem fsumiunle 33033

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 32867	. . 3 ⊢ (𝜑 → ∃𝑓(𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1→∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙))
4		f1f1orn 6820	. . . . . 6 ⊢ (𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1→∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) → 𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓)
5	4	anim1i 624	. . . . 5 ⊢ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1→∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) → (𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙))
6		f1f 6762	. . . . . . 7 ⊢ (𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1→∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) → 𝑓:∪ 𝑥 ∈ 𝐴 𝐵⟶∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))
7	6	frnd 6702	. . . . . 6 ⊢ (𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1→∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) → ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))
8	7	adantr 484	. . . . 5 ⊢ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1→∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) → ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))
9	5, 8	jca 519	. . . 4 ⊢ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1→∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) → ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)))
10	9	eximi 1857	. . 3 ⊢ (∃𝑓(𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1→∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) → ∃𝑓((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)))
11	3, 10	syl 17	. 2 ⊢ (𝜑 → ∃𝑓((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)))
12		csbeq1a 3868	. . . . . . 7 ⊢ (𝑘 = 𝑦 → 𝐶 = ⦋𝑦 / 𝑘⦌𝐶)
13		nfcv 2926	. . . . . . 7 ⊢ Ⅎ𝑦𝐶
14		nfcsb1v 3878	. . . . . . 7 ⊢ Ⅎ𝑘⦋𝑦 / 𝑘⦌𝐶
15	12, 13, 14	cbvsum 15724	. . . . . 6 ⊢ Σ𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝐶 = Σ𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵⦋𝑦 / 𝑘⦌𝐶
16		csbeq1 3857	. . . . . . 7 ⊢ (𝑦 = (2nd ‘𝑧) → ⦋𝑦 / 𝑘⦌𝐶 = ⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
17		snfi 9026	. . . . . . . . . . . 12 ⊢ {𝑥} ∈ Fin
18		xpfi 9266	. . . . . . . . . . . 12 ⊢ (({𝑥} ∈ Fin ∧ 𝐵 ∈ Fin) → ({𝑥} × 𝐵) ∈ Fin)
19	17, 2, 18	sylancr 596	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ({𝑥} × 𝐵) ∈ Fin)
20	19	ralrimiva 3156	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ∈ Fin)
21		iunfi 9288	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ∈ Fin) → ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ∈ Fin)
22	1, 20, 21	syl2anc 593	. . . . . . . . 9 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ∈ Fin)
23	22	adantr 484	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ∈ Fin)
24		simprr 782	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))
25	23, 24	ssfid 9215	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → ran 𝑓 ∈ Fin)
26		simprl 780	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → 𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓)
27		f1ocnv 6821	. . . . . . . . 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 733	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → ◡𝑓:ran 𝑓–1-1-onto→∪ 𝑥 ∈ 𝐴 𝐵)
30		nfv 1936	. . . . . . . . . 10 ⊢ Ⅎ𝑥𝜑
31		nfcv 2926	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥𝑓
32		nfiu1 4987	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵
33	31	nfrn 5930	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥ran 𝑓
34	31, 32, 33	nff1o 6806	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥 𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓
35		nfv 1936	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(2nd ‘(𝑓‘𝑙)) = 𝑙
36	32, 35	nfralw 3311	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙
37	34, 36	nfan 1921	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙)
38		nfcv 2926	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥ran 𝑓
39		nfiu1 4987	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)
40	38, 39	nfss 3931	. . . . . . . . . . 11 ⊢ Ⅎ𝑥ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)
41	37, 40	nfan 1921	. . . . . . . . . 10 ⊢ Ⅎ𝑥((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))
42	30, 41	nfan 1921	. . . . . . . . 9 ⊢ Ⅎ𝑥(𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)))
43		nfv 1936	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑧 ∈ ran 𝑓
44	42, 43	nfan 1921	. . . . . . . 8 ⊢ Ⅎ𝑥((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓)
45		simpr 488	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → (𝑓‘𝑘) = 𝑧)
46	45	fveq2d 6873	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → (2nd ‘(𝑓‘𝑘)) = (2nd ‘𝑧))
47		simplr 778	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵)
48		simp-4r 793	. . . . . . . . . . . . . . 15 ⊢ (((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)))
49	48	simpld 498	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → (𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙))
50	49	simprd 499	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙)
51	50	ad2antrr 736	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙)
52		2fveq3 6874	. . . . . . . . . . . . . 14 ⊢ (𝑙 = 𝑘 → (2nd ‘(𝑓‘𝑙)) = (2nd ‘(𝑓‘𝑘)))
53		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑙 = 𝑘 → 𝑙 = 𝑘)
54	52, 53	eqeq12d 2780	. . . . . . . . . . . . 13 ⊢ (𝑙 = 𝑘 → ((2nd ‘(𝑓‘𝑙)) = 𝑙 ↔ (2nd ‘(𝑓‘𝑘)) = 𝑘))
55	54	rspcva 3581	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) → (2nd ‘(𝑓‘𝑘)) = 𝑘)
56	47, 51, 55	syl2anc 593	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → (2nd ‘(𝑓‘𝑘)) = 𝑘)
57	46, 56	eqtr3d 2801	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → (2nd ‘𝑧) = 𝑘)
58	49	simpld 498	. . . . . . . . . . . 12 ⊢ (((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → 𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓)
59	58	ad2antrr 736	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → 𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓)
60		f1ocnvfv1 7262	. . . . . . . . . . 11 ⊢ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → (◡𝑓‘(𝑓‘𝑘)) = 𝑘)
61	59, 47, 60	syl2anc 593	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → (◡𝑓‘(𝑓‘𝑘)) = 𝑘)
62	45	fveq2d 6873	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → (◡𝑓‘(𝑓‘𝑘)) = (◡𝑓‘𝑧))
63	57, 61, 62	3eqtr2rd 2806	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → (◡𝑓‘𝑧) = (2nd ‘𝑧))
64		f1ofn 6809	. . . . . . . . . . 11 ⊢ (𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 → 𝑓 Fn ∪ 𝑥 ∈ 𝐴 𝐵)
65	58, 64	syl 17	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → 𝑓 Fn ∪ 𝑥 ∈ 𝐴 𝐵)
66		simpllr 785	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → 𝑧 ∈ ran 𝑓)
67		fvelrnb 6929	. . . . . . . . . . 11 ⊢ (𝑓 Fn ∪ 𝑥 ∈ 𝐴 𝐵 → (𝑧 ∈ ran 𝑓 ↔ ∃𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(𝑓‘𝑘) = 𝑧))
68	67	biimpa 480	. . . . . . . . . 10 ⊢ ((𝑓 Fn ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ran 𝑓) → ∃𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(𝑓‘𝑘) = 𝑧)
69	65, 66, 68	syl2anc 593	. . . . . . . . 9 ⊢ (((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → ∃𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(𝑓‘𝑘) = 𝑧)
70	63, 69	r19.29a 3172	. . . . . . . 8 ⊢ (((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → (◡𝑓‘𝑧) = (2nd ‘𝑧))
71	24	sselda 3938	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) → 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))
72		eliun 4955	. . . . . . . . 9 ⊢ (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ ∃𝑥 ∈ 𝐴 𝑧 ∈ ({𝑥} × 𝐵))
73	71, 72	sylib 220	. . . . . . . 8 ⊢ (((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) → ∃𝑥 ∈ 𝐴 𝑧 ∈ ({𝑥} × 𝐵))
74	44, 70, 73	r19.29af 3273	. . . . . . 7 ⊢ (((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) → (◡𝑓‘𝑧) = (2nd ‘𝑧))
75		nfv 1936	. . . . . . . . . 10 ⊢ Ⅎ𝑘(𝜑 ∧ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵)
76		nfcv 2926	. . . . . . . . . . 11 ⊢ Ⅎ𝑘ℂ
77	14, 76	nfel 2940	. . . . . . . . . 10 ⊢ Ⅎ𝑘⦋𝑦 / 𝑘⦌𝐶 ∈ ℂ
78	75, 77	nfim 1918	. . . . . . . . 9 ⊢ Ⅎ𝑘((𝜑 ∧ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → ⦋𝑦 / 𝑘⦌𝐶 ∈ ℂ)
79		eleq1w 2847	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑦 → (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵))
80	79	anbi2d 639	. . . . . . . . . 10 ⊢ (𝑘 = 𝑦 → ((𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ↔ (𝜑 ∧ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵)))
81	12	eleq1d 2849	. . . . . . . . . 10 ⊢ (𝑘 = 𝑦 → (𝐶 ∈ ℂ ↔ ⦋𝑦 / 𝑘⦌𝐶 ∈ ℂ))
82	80, 81	imbi12d 346	. . . . . . . . 9 ⊢ (𝑘 = 𝑦 → (((𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → 𝐶 ∈ ℂ) ↔ ((𝜑 ∧ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → ⦋𝑦 / 𝑘⦌𝐶 ∈ ℂ)))
83		nfcv 2926	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥𝑘
84	83, 32	nfel 2940	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵
85	30, 84	nfan 1921	. . . . . . . . . 10 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵)
86		fsumiunle.3	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℝ)
87	86	adantllr 729	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℝ)
88	87	recnd 11212	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ)
89		eliun 4955	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵)
90	89	bilani 508	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → ∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵)
91	85, 88, 90	r19.29af 3273	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → 𝐶 ∈ ℂ)
92	78, 82, 91	chvarfv 2277	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → ⦋𝑦 / 𝑘⦌𝐶 ∈ ℂ)
93	92	adantlr 725	. . . . . . 7 ⊢ (((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → ⦋𝑦 / 𝑘⦌𝐶 ∈ ℂ)
94	16, 25, 29, 74, 93	fsumf1o 15752	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → Σ𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵⦋𝑦 / 𝑘⦌𝐶 = Σ𝑧 ∈ ran 𝑓⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
95	15, 94	eqtrid 2811	. . . . 5 ⊢ ((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → Σ𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝐶 = Σ𝑧 ∈ ran 𝑓⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
96	95	eqcomd 2770	. . . 4 ⊢ ((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → Σ𝑧 ∈ ran 𝑓⦋(2nd ‘𝑧) / 𝑘⦌𝐶 = Σ𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝐶)
97		nfcv 2926	. . . . . . . . 9 ⊢ Ⅎ𝑥𝑧
98	97, 39	nfel 2940	. . . . . . . 8 ⊢ Ⅎ𝑥 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)
99	30, 98	nfan 1921	. . . . . . 7 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))
100		xp2nd 8005	. . . . . . . . 9 ⊢ (𝑧 ∈ ({𝑥} × 𝐵) → (2nd ‘𝑧) ∈ 𝐵)
101	100	adantl 485	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → (2nd ‘𝑧) ∈ 𝐵)
102	86	ralrimiva 3156	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑘 ∈ 𝐵 𝐶 ∈ ℝ)
103	102	adantlr 725	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) ∧ 𝑥 ∈ 𝐴) → ∀𝑘 ∈ 𝐵 𝐶 ∈ ℝ)
104	103	adantr 484	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → ∀𝑘 ∈ 𝐵 𝐶 ∈ ℝ)
105		nfcsb1v 3878	. . . . . . . . . . 11 ⊢ Ⅎ𝑘⦋(2nd ‘𝑧) / 𝑘⦌𝐶
106	105	nfel1 2942	. . . . . . . . . 10 ⊢ Ⅎ𝑘⦋(2nd ‘𝑧) / 𝑘⦌𝐶 ∈ ℝ
107		csbeq1a 3868	. . . . . . . . . . 11 ⊢ (𝑘 = (2nd ‘𝑧) → 𝐶 = ⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
108	107	eleq1d 2849	. . . . . . . . . 10 ⊢ (𝑘 = (2nd ‘𝑧) → (𝐶 ∈ ℝ ↔ ⦋(2nd ‘𝑧) / 𝑘⦌𝐶 ∈ ℝ))
109	106, 108	rspc 3571	. . . . . . . . 9 ⊢ ((2nd ‘𝑧) ∈ 𝐵 → (∀𝑘 ∈ 𝐵 𝐶 ∈ ℝ → ⦋(2nd ‘𝑧) / 𝑘⦌𝐶 ∈ ℝ))
110	109	imp 410	. . . . . . . 8 ⊢ (((2nd ‘𝑧) ∈ 𝐵 ∧ ∀𝑘 ∈ 𝐵 𝐶 ∈ ℝ) → ⦋(2nd ‘𝑧) / 𝑘⦌𝐶 ∈ ℝ)
111	101, 104, 110	syl2anc 593	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → ⦋(2nd ‘𝑧) / 𝑘⦌𝐶 ∈ ℝ)
112	72	bilani 508	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) → ∃𝑥 ∈ 𝐴 𝑧 ∈ ({𝑥} × 𝐵))
113	99, 111, 112	r19.29af 3273	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) → ⦋(2nd ‘𝑧) / 𝑘⦌𝐶 ∈ ℝ)
114	113	adantlr 725	. . . . 5 ⊢ (((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) → ⦋(2nd ‘𝑧) / 𝑘⦌𝐶 ∈ ℝ)
115		xp1st 8004	. . . . . . . . . . 11 ⊢ (𝑧 ∈ ({𝑥} × 𝐵) → (1st ‘𝑧) ∈ {𝑥})
116		elsni 4601	. . . . . . . . . . 11 ⊢ ((1st ‘𝑧) ∈ {𝑥} → (1st ‘𝑧) = 𝑥)
117	115, 116	syl 17	. . . . . . . . . 10 ⊢ (𝑧 ∈ ({𝑥} × 𝐵) → (1st ‘𝑧) = 𝑥)
118	117, 100	jca 519	. . . . . . . . 9 ⊢ (𝑧 ∈ ({𝑥} × 𝐵) → ((1st ‘𝑧) = 𝑥 ∧ (2nd ‘𝑧) ∈ 𝐵))
119		simplll 784	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ ((1st ‘𝑧) = 𝑥 ∧ (2nd ‘𝑧) ∈ 𝐵)) → 𝜑)
120		simplr 778	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ ((1st ‘𝑧) = 𝑥 ∧ (2nd ‘𝑧) ∈ 𝐵)) → 𝑥 ∈ 𝐴)
121		fsumiunle.4	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 0 ≤ 𝐶)
122	121	ralrimiva 3156	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑘 ∈ 𝐵 0 ≤ 𝐶)
123	119, 120, 122	syl2anc 593	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ ((1st ‘𝑧) = 𝑥 ∧ (2nd ‘𝑧) ∈ 𝐵)) → ∀𝑘 ∈ 𝐵 0 ≤ 𝐶)
124	118, 123	sylan2 602	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → ∀𝑘 ∈ 𝐵 0 ≤ 𝐶)
125		nfcv 2926	. . . . . . . . . . 11 ⊢ Ⅎ𝑘0
126		nfcv 2926	. . . . . . . . . . 11 ⊢ Ⅎ𝑘 ≤
127	125, 126, 105	nfbr 5149	. . . . . . . . . 10 ⊢ Ⅎ𝑘0 ≤ ⦋(2nd ‘𝑧) / 𝑘⦌𝐶
128	107	breq2d 5114	. . . . . . . . . 10 ⊢ (𝑘 = (2nd ‘𝑧) → (0 ≤ 𝐶 ↔ 0 ≤ ⦋(2nd ‘𝑧) / 𝑘⦌𝐶))
129	127, 128	rspc 3571	. . . . . . . . 9 ⊢ ((2nd ‘𝑧) ∈ 𝐵 → (∀𝑘 ∈ 𝐵 0 ≤ 𝐶 → 0 ≤ ⦋(2nd ‘𝑧) / 𝑘⦌𝐶))
130	129	imp 410	. . . . . . . 8 ⊢ (((2nd ‘𝑧) ∈ 𝐵 ∧ ∀𝑘 ∈ 𝐵 0 ≤ 𝐶) → 0 ≤ ⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
131	101, 124, 130	syl2anc 593	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → 0 ≤ ⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
132	99, 131, 112	r19.29af 3273	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) → 0 ≤ ⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
133	132	adantlr 725	. . . . 5 ⊢ (((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) → 0 ≤ ⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
134	23, 114, 133, 24	fsumless 15826	. . . 4 ⊢ ((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → Σ𝑧 ∈ ran 𝑓⦋(2nd ‘𝑧) / 𝑘⦌𝐶 ≤ Σ𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
135	96, 134	eqbrtrrd 5126	. . 3 ⊢ ((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → Σ𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝐶 ≤ Σ𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
136	12, 13, 14	cbvsum 15724	. . . . . . 7 ⊢ Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑦 ∈ 𝐵 ⦋𝑦 / 𝑘⦌𝐶
137	136	a1i 11	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑦 ∈ 𝐵 ⦋𝑦 / 𝑘⦌𝐶)
138	137	sumeq2sdv 15732	. . . . 5 ⊢ (𝜑 → Σ𝑥 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑥 ∈ 𝐴 Σ𝑦 ∈ 𝐵 ⦋𝑦 / 𝑘⦌𝐶)
139		vex 3460	. . . . . . . . . 10 ⊢ 𝑥 ∈ V
140		vex 3460	. . . . . . . . . 10 ⊢ 𝑦 ∈ V
141	139, 140	op2ndd 7983	. . . . . . . . 9 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (2nd ‘𝑧) = 𝑦)
142	141	eqcomd 2770	. . . . . . . 8 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → 𝑦 = (2nd ‘𝑧))
143	142	csbeq1d 3858	. . . . . . 7 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ⦋𝑦 / 𝑘⦌𝐶 = ⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
144	143	eqcomd 2770	. . . . . 6 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ⦋(2nd ‘𝑧) / 𝑘⦌𝐶 = ⦋𝑦 / 𝑘⦌𝐶)
145		nfv 1936	. . . . . . . . 9 ⊢ Ⅎ𝑘((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵)
146	14	nfel1 2942	. . . . . . . . 9 ⊢ Ⅎ𝑘⦋𝑦 / 𝑘⦌𝐶 ∈ ℂ
147	145, 146	nfim 1918	. . . . . . . 8 ⊢ Ⅎ𝑘(((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → ⦋𝑦 / 𝑘⦌𝐶 ∈ ℂ)
148		eleq1w 2847	. . . . . . . . . 10 ⊢ (𝑘 = 𝑦 → (𝑘 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵))
149	148	anbi2d 639	. . . . . . . . 9 ⊢ (𝑘 = 𝑦 → (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) ↔ ((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵)))
150	149, 81	imbi12d 346	. . . . . . . 8 ⊢ (𝑘 = 𝑦 → ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ) ↔ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → ⦋𝑦 / 𝑘⦌𝐶 ∈ ℂ)))
151	86	recnd 11212	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ)
152	147, 150, 151	chvarfv 2277	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → ⦋𝑦 / 𝑘⦌𝐶 ∈ ℂ)
153	152	anasss 470	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → ⦋𝑦 / 𝑘⦌𝐶 ∈ ℂ)
154	144, 1, 2, 153	fsum2d 15800	. . . . 5 ⊢ (𝜑 → Σ𝑥 ∈ 𝐴 Σ𝑦 ∈ 𝐵 ⦋𝑦 / 𝑘⦌𝐶 = Σ𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
155	138, 154	eqtrd 2799	. . . 4 ⊢ (𝜑 → Σ𝑥 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
156	155	adantr 484	. . 3 ⊢ ((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → Σ𝑥 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
157	135, 156	breqtrrd 5130	. 2 ⊢ ((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → Σ𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝐶 ≤ Σ𝑥 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶)
158	11, 157	exlimddv 1957	1 ⊢ (𝜑 → Σ𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝐶 ≤ Σ𝑥 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶)

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1562  ∃wex 1801   ∈ wcel 2144  ∀wral 3078  ∃wrex 3088  ⦋csb 3854   ⊆ wss 3906  {csn 4584  ⟨cop 4590  ∪ ciun 4951   class class class wbr 5102   × cxp 5647  ^◡ccnv 5648  ran crn 5650   Fn wfn 6518  –1-1→wf1 6520  –1-1-onto→wf1o 6522  ‘cfv 6523  1^st c1st 7970  2^nd c2nd 7971  Fincfn 8929  ℂcc 11073  ℝcr 11074  0cc0 11075   ≤ cle 11219  Σcsu 15715

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1817  ax-4 1831  ax-5 1932  ax-6 1989  ax-7 2030  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2214  ax-ext 2736  ax-rep 5229  ax-sep 5248  ax-nul 5258  ax-pow 5324  ax-pr 5392  ax-un 7720  ax-reg 9542  ax-inf2 9598  ax-ac2 10422  ax-cnex 11131  ax-resscn 11132  ax-1cn 11133  ax-icn 11134  ax-addcl 11135  ax-addrcl 11136  ax-mulcl 11137  ax-mulrcl 11138  ax-mulcom 11139  ax-addass 11140  ax-mulass 11141  ax-distr 11142  ax-i2m1 11143  ax-1ne0 11144  ax-1rid 11145  ax-rnegex 11146  ax-rrecex 11147  ax-cnre 11148  ax-pre-lttri 11149  ax-pre-lttrn 11150  ax-pre-ltadd 11151  ax-pre-mulgt0 11152  ax-pre-sup 11153

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3or 1100  df-3an 1101  df-tru 1565  df-fal 1575  df-ex 1802  df-nf 1806  df-sb 2093  df-mo 2568  df-eu 2598  df-clab 2743  df-cleq 2756  df-clel 2839  df-nfc 2913  df-ne 2960  df-nel 3064  df-ral 3079  df-rex 3089  df-rmo 3369  df-reu 3370  df-rab 3417  df-v 3458  df-sbc 3747  df-csb 3855  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-pss 3926  df-nul 4288  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-int 4908  df-iun 4953  df-iin 4954  df-br 5103  df-opab 5165  df-mpt 5184  df-tr 5210  df-id 5544  df-eprel 5549  df-po 5557  df-so 5558  df-fr 5602  df-se 5603  df-we 5604  df-xp 5655  df-rel 5656  df-cnv 5657  df-co 5658  df-dm 5659  df-rn 5660  df-res 5661  df-ima 5662  df-pred 6290  df-ord 6351  df-on 6352  df-lim 6353  df-suc 6354  df-iota 6479  df-fun 6525  df-fn 6526  df-f 6527  df-f1 6528  df-fo 6529  df-f1o 6530  df-fv 6531  df-isom 6532  df-riota 7355  df-ov 7401  df-oprab 7402  df-mpo 7403  df-om 7849  df-1st 7972  df-2nd 7973  df-frecs 8264  df-wrecs 8295  df-recs 8344  df-rdg 8383  df-1o 8439  df-er 8680  df-en 8930  df-dom 8931  df-sdom 8932  df-fin 8933  df-sup 9390  df-oi 9460  df-r1 9724  df-rank 9725  df-card 9899  df-ac 10074  df-pnf 11220  df-mnf 11221  df-xr 11222  df-ltxr 11223  df-le 11224  df-sub 11418  df-neg 11419  df-div 11847  df-nn 12213  df-2 12282  df-3 12283  df-n0 12484  df-z 12571  df-uz 12842  df-rp 12996  df-ico 13357  df-fz 13515  df-fzo 13662  df-seq 14017  df-exp 14077  df-hash 14346  df-cj 15128  df-re 15129  df-im 15130  df-sqrt 15264  df-abs 15265  df-clim 15517  df-sum 15716

This theorem is referenced by:  hgt750lema  34953