Theorem fsumiunle 31725

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 31579	. . 3 ⊢ (𝜑 → ∃𝑓(𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1→∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙))
4		f1f1orn 6795	. . . . . 6 ⊢ (𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1→∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) → 𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓)
5	4	anim1i 615	. . . . 5 ⊢ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1→∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) → (𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙))
6		f1f 6738	. . . . . . 7 ⊢ (𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1→∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) → 𝑓:∪ 𝑥 ∈ 𝐴 𝐵⟶∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))
7	6	frnd 6676	. . . . . 6 ⊢ (𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1→∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) → ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))
8	7	adantr 481	. . . . 5 ⊢ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1→∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) → ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))
9	5, 8	jca 512	. . . 4 ⊢ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1→∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) → ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)))
10	9	eximi 1837	. . 3 ⊢ (∃𝑓(𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1→∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) → ∃𝑓((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)))
11	3, 10	syl 17	. 2 ⊢ (𝜑 → ∃𝑓((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)))
12		csbeq1a 3869	. . . . . . 7 ⊢ (𝑘 = 𝑦 → 𝐶 = ⦋𝑦 / 𝑘⦌𝐶)
13		nfcv 2907	. . . . . . 7 ⊢ Ⅎ𝑦∪ 𝑥 ∈ 𝐴 𝐵
14		nfcv 2907	. . . . . . 7 ⊢ Ⅎ𝑘∪ 𝑥 ∈ 𝐴 𝐵
15		nfcv 2907	. . . . . . 7 ⊢ Ⅎ𝑦𝐶
16		nfcsb1v 3880	. . . . . . 7 ⊢ Ⅎ𝑘⦋𝑦 / 𝑘⦌𝐶
17	12, 13, 14, 15, 16	cbvsum 15580	. . . . . 6 ⊢ Σ𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝐶 = Σ𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵⦋𝑦 / 𝑘⦌𝐶
18		csbeq1 3858	. . . . . . 7 ⊢ (𝑦 = (2nd ‘𝑧) → ⦋𝑦 / 𝑘⦌𝐶 = ⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
19		snfi 8988	. . . . . . . . . . . 12 ⊢ {𝑥} ∈ Fin
20		xpfi 9261	. . . . . . . . . . . 12 ⊢ (({𝑥} ∈ Fin ∧ 𝐵 ∈ Fin) → ({𝑥} × 𝐵) ∈ Fin)
21	19, 2, 20	sylancr 587	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ({𝑥} × 𝐵) ∈ Fin)
22	21	ralrimiva 3143	. . . . . . . . . 10 ⊢ (𝜑 → ∀𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ∈ Fin)
23		iunfi 9284	. . . . . . . . . 10 ⊢ ((𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ∈ Fin) → ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ∈ Fin)
24	1, 22, 23	syl2anc 584	. . . . . . . . 9 ⊢ (𝜑 → ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ∈ Fin)
25	24	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ∈ Fin)
26		simprr 771	. . . . . . . 8 ⊢ ((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))
27	25, 26	ssfid 9211	. . . . . . 7 ⊢ ((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → ran 𝑓 ∈ Fin)
28		simprl 769	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → 𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓)
29		f1ocnv 6796	. . . . . . . . 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 1917	. . . . . . . . . 10 ⊢ Ⅎ𝑥𝜑
33		nfcv 2907	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥𝑓
34		nfiu1 4988	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 𝐵
35	33	nfrn 5907	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥ran 𝑓
36	33, 34, 35	nff1o 6782	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥 𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓
37		nfv 1917	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑥(2nd ‘(𝑓‘𝑙)) = 𝑙
38	34, 37	nfralw 3294	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙
39	36, 38	nfan 1902	. . . . . . . . . . 11 ⊢ Ⅎ𝑥(𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙)
40		nfcv 2907	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥ran 𝑓
41		nfiu1 4988	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)
42	40, 41	nfss 3936	. . . . . . . . . . 11 ⊢ Ⅎ𝑥ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)
43	39, 42	nfan 1902	. . . . . . . . . 10 ⊢ Ⅎ𝑥((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))
44	32, 43	nfan 1902	. . . . . . . . 9 ⊢ Ⅎ𝑥(𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)))
45		nfv 1917	. . . . . . . . 9 ⊢ Ⅎ𝑥 𝑧 ∈ ran 𝑓
46	44, 45	nfan 1902	. . . . . . . 8 ⊢ Ⅎ𝑥((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓)
47		simpr 485	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → (𝑓‘𝑘) = 𝑧)
48	47	fveq2d 6846	. . . . . . . . . . 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 495	. . . . . . . . . . . . . 14 ⊢ (((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → (𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙))
52	51	simprd 496	. . . . . . . . . . . . 13 ⊢ (((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙)
53	52	ad2antrr 724	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙)
54		2fveq3 6847	. . . . . . . . . . . . . 14 ⊢ (𝑙 = 𝑘 → (2nd ‘(𝑓‘𝑙)) = (2nd ‘(𝑓‘𝑘)))
55		id 22	. . . . . . . . . . . . . 14 ⊢ (𝑙 = 𝑘 → 𝑙 = 𝑘)
56	54, 55	eqeq12d 2752	. . . . . . . . . . . . 13 ⊢ (𝑙 = 𝑘 → ((2nd ‘(𝑓‘𝑙)) = 𝑙 ↔ (2nd ‘(𝑓‘𝑘)) = 𝑘))
57	56	rspcva 3579	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) → (2nd ‘(𝑓‘𝑘)) = 𝑘)
58	49, 53, 57	syl2anc 584	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → (2nd ‘(𝑓‘𝑘)) = 𝑘)
59	48, 58	eqtr3d 2778	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → (2nd ‘𝑧) = 𝑘)
60	51	simpld 495	. . . . . . . . . . . 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 7222	. . . . . . . . . . 11 ⊢ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → (◡𝑓‘(𝑓‘𝑘)) = 𝑘)
63	61, 49, 62	syl2anc 584	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → (◡𝑓‘(𝑓‘𝑘)) = 𝑘)
64	47	fveq2d 6846	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → (◡𝑓‘(𝑓‘𝑘)) = (◡𝑓‘𝑧))
65	59, 63, 64	3eqtr2rd 2783	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ (𝑓‘𝑘) = 𝑧) → (◡𝑓‘𝑧) = (2nd ‘𝑧))
66		f1ofn 6785	. . . . . . . . . . 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 6903	. . . . . . . . . . 11 ⊢ (𝑓 Fn ∪ 𝑥 ∈ 𝐴 𝐵 → (𝑧 ∈ ran 𝑓 ↔ ∃𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(𝑓‘𝑘) = 𝑧))
70	69	biimpa 477	. . . . . . . . . 10 ⊢ ((𝑓 Fn ∪ 𝑥 ∈ 𝐴 𝐵 ∧ 𝑧 ∈ ran 𝑓) → ∃𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(𝑓‘𝑘) = 𝑧)
71	67, 68, 70	syl2anc 584	. . . . . . . . 9 ⊢ (((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → ∃𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(𝑓‘𝑘) = 𝑧)
72	65, 71	r19.29a 3159	. . . . . . . 8 ⊢ (((((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → (◡𝑓‘𝑧) = (2nd ‘𝑧))
73	26	sselda 3944	. . . . . . . . 9 ⊢ (((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) → 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))
74		eliun 4958	. . . . . . . . 9 ⊢ (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) ↔ ∃𝑥 ∈ 𝐴 𝑧 ∈ ({𝑥} × 𝐵))
75	73, 74	sylib 217	. . . . . . . 8 ⊢ (((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) → ∃𝑥 ∈ 𝐴 𝑧 ∈ ({𝑥} × 𝐵))
76	46, 72, 75	r19.29af 3251	. . . . . . 7 ⊢ (((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ran 𝑓) → (◡𝑓‘𝑧) = (2nd ‘𝑧))
77		nfv 1917	. . . . . . . . . 10 ⊢ Ⅎ𝑘(𝜑 ∧ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵)
78		nfcv 2907	. . . . . . . . . . 11 ⊢ Ⅎ𝑘ℂ
79	16, 78	nfel 2921	. . . . . . . . . 10 ⊢ Ⅎ𝑘⦋𝑦 / 𝑘⦌𝐶 ∈ ℂ
80	77, 79	nfim 1899	. . . . . . . . 9 ⊢ Ⅎ𝑘((𝜑 ∧ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → ⦋𝑦 / 𝑘⦌𝐶 ∈ ℂ)
81		eleq1w 2820	. . . . . . . . . . 11 ⊢ (𝑘 = 𝑦 → (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵))
82	81	anbi2d 629	. . . . . . . . . 10 ⊢ (𝑘 = 𝑦 → ((𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ↔ (𝜑 ∧ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵)))
83	12	eleq1d 2822	. . . . . . . . . 10 ⊢ (𝑘 = 𝑦 → (𝐶 ∈ ℂ ↔ ⦋𝑦 / 𝑘⦌𝐶 ∈ ℂ))
84	82, 83	imbi12d 344	. . . . . . . . 9 ⊢ (𝑘 = 𝑦 → (((𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → 𝐶 ∈ ℂ) ↔ ((𝜑 ∧ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → ⦋𝑦 / 𝑘⦌𝐶 ∈ ℂ)))
85		nfcv 2907	. . . . . . . . . . . 12 ⊢ Ⅎ𝑥𝑘
86	85, 34	nfel 2921	. . . . . . . . . . 11 ⊢ Ⅎ𝑥 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵
87	32, 86	nfan 1902	. . . . . . . . . 10 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵)
88		fsumiunle.3	. . . . . . . . . . . 12 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℝ)
89	88	adantllr 717	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℝ)
90	89	recnd 11183	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ)
91		eliun 4958	. . . . . . . . . . . 12 ⊢ (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 ↔ ∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵)
92	91	biimpi 215	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵 → ∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵)
93	92	adantl 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → ∃𝑥 ∈ 𝐴 𝑘 ∈ 𝐵)
94	87, 90, 93	r19.29af 3251	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → 𝐶 ∈ ℂ)
95	80, 84, 94	chvarfv 2233	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → ⦋𝑦 / 𝑘⦌𝐶 ∈ ℂ)
96	95	adantlr 713	. . . . . . 7 ⊢ (((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵) → ⦋𝑦 / 𝑘⦌𝐶 ∈ ℂ)
97	18, 27, 31, 76, 96	fsumf1o 15608	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → Σ𝑦 ∈ ∪ 𝑥 ∈ 𝐴 𝐵⦋𝑦 / 𝑘⦌𝐶 = Σ𝑧 ∈ ran 𝑓⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
98	17, 97	eqtrid 2788	. . . . 5 ⊢ ((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → Σ𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝐶 = Σ𝑧 ∈ ran 𝑓⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
99	98	eqcomd 2742	. . . 4 ⊢ ((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → Σ𝑧 ∈ ran 𝑓⦋(2nd ‘𝑧) / 𝑘⦌𝐶 = Σ𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝐶)
100		nfcv 2907	. . . . . . . . 9 ⊢ Ⅎ𝑥𝑧
101	100, 41	nfel 2921	. . . . . . . 8 ⊢ Ⅎ𝑥 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)
102	32, 101	nfan 1902	. . . . . . 7 ⊢ Ⅎ𝑥(𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))
103		xp2nd 7954	. . . . . . . . 9 ⊢ (𝑧 ∈ ({𝑥} × 𝐵) → (2nd ‘𝑧) ∈ 𝐵)
104	103	adantl 482	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → (2nd ‘𝑧) ∈ 𝐵)
105	88	ralrimiva 3143	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑘 ∈ 𝐵 𝐶 ∈ ℝ)
106	105	adantlr 713	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) ∧ 𝑥 ∈ 𝐴) → ∀𝑘 ∈ 𝐵 𝐶 ∈ ℝ)
107	106	adantr 481	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → ∀𝑘 ∈ 𝐵 𝐶 ∈ ℝ)
108		nfcsb1v 3880	. . . . . . . . . . 11 ⊢ Ⅎ𝑘⦋(2nd ‘𝑧) / 𝑘⦌𝐶
109	108	nfel1 2923	. . . . . . . . . 10 ⊢ Ⅎ𝑘⦋(2nd ‘𝑧) / 𝑘⦌𝐶 ∈ ℝ
110		csbeq1a 3869	. . . . . . . . . . 11 ⊢ (𝑘 = (2nd ‘𝑧) → 𝐶 = ⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
111	110	eleq1d 2822	. . . . . . . . . 10 ⊢ (𝑘 = (2nd ‘𝑧) → (𝐶 ∈ ℝ ↔ ⦋(2nd ‘𝑧) / 𝑘⦌𝐶 ∈ ℝ))
112	109, 111	rspc 3569	. . . . . . . . 9 ⊢ ((2nd ‘𝑧) ∈ 𝐵 → (∀𝑘 ∈ 𝐵 𝐶 ∈ ℝ → ⦋(2nd ‘𝑧) / 𝑘⦌𝐶 ∈ ℝ))
113	112	imp 407	. . . . . . . 8 ⊢ (((2nd ‘𝑧) ∈ 𝐵 ∧ ∀𝑘 ∈ 𝐵 𝐶 ∈ ℝ) → ⦋(2nd ‘𝑧) / 𝑘⦌𝐶 ∈ ℝ)
114	104, 107, 113	syl2anc 584	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → ⦋(2nd ‘𝑧) / 𝑘⦌𝐶 ∈ ℝ)
115	74	biimpi 215	. . . . . . . 8 ⊢ (𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵) → ∃𝑥 ∈ 𝐴 𝑧 ∈ ({𝑥} × 𝐵))
116	115	adantl 482	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) → ∃𝑥 ∈ 𝐴 𝑧 ∈ ({𝑥} × 𝐵))
117	102, 114, 116	r19.29af 3251	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) → ⦋(2nd ‘𝑧) / 𝑘⦌𝐶 ∈ ℝ)
118	117	adantlr 713	. . . . 5 ⊢ (((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) → ⦋(2nd ‘𝑧) / 𝑘⦌𝐶 ∈ ℝ)
119		xp1st 7953	. . . . . . . . . . 11 ⊢ (𝑧 ∈ ({𝑥} × 𝐵) → (1st ‘𝑧) ∈ {𝑥})
120		elsni 4603	. . . . . . . . . . 11 ⊢ ((1st ‘𝑧) ∈ {𝑥} → (1st ‘𝑧) = 𝑥)
121	119, 120	syl 17	. . . . . . . . . 10 ⊢ (𝑧 ∈ ({𝑥} × 𝐵) → (1st ‘𝑧) = 𝑥)
122	121, 103	jca 512	. . . . . . . . 9 ⊢ (𝑧 ∈ ({𝑥} × 𝐵) → ((1st ‘𝑧) = 𝑥 ∧ (2nd ‘𝑧) ∈ 𝐵))
123		simplll 773	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ ((1st ‘𝑧) = 𝑥 ∧ (2nd ‘𝑧) ∈ 𝐵)) → 𝜑)
124		simplr 767	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ ((1st ‘𝑧) = 𝑥 ∧ (2nd ‘𝑧) ∈ 𝐵)) → 𝑥 ∈ 𝐴)
125		fsumiunle.4	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 0 ≤ 𝐶)
126	125	ralrimiva 3143	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → ∀𝑘 ∈ 𝐵 0 ≤ 𝐶)
127	123, 124, 126	syl2anc 584	. . . . . . . . 9 ⊢ ((((𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ ((1st ‘𝑧) = 𝑥 ∧ (2nd ‘𝑧) ∈ 𝐵)) → ∀𝑘 ∈ 𝐵 0 ≤ 𝐶)
128	122, 127	sylan2 593	. . . . . . . 8 ⊢ ((((𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → ∀𝑘 ∈ 𝐵 0 ≤ 𝐶)
129		nfcv 2907	. . . . . . . . . . 11 ⊢ Ⅎ𝑘0
130		nfcv 2907	. . . . . . . . . . 11 ⊢ Ⅎ𝑘 ≤
131	129, 130, 108	nfbr 5152	. . . . . . . . . 10 ⊢ Ⅎ𝑘0 ≤ ⦋(2nd ‘𝑧) / 𝑘⦌𝐶
132	110	breq2d 5117	. . . . . . . . . 10 ⊢ (𝑘 = (2nd ‘𝑧) → (0 ≤ 𝐶 ↔ 0 ≤ ⦋(2nd ‘𝑧) / 𝑘⦌𝐶))
133	131, 132	rspc 3569	. . . . . . . . 9 ⊢ ((2nd ‘𝑧) ∈ 𝐵 → (∀𝑘 ∈ 𝐵 0 ≤ 𝐶 → 0 ≤ ⦋(2nd ‘𝑧) / 𝑘⦌𝐶))
134	133	imp 407	. . . . . . . 8 ⊢ (((2nd ‘𝑧) ∈ 𝐵 ∧ ∀𝑘 ∈ 𝐵 0 ≤ 𝐶) → 0 ≤ ⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
135	104, 128, 134	syl2anc 584	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) ∧ 𝑥 ∈ 𝐴) ∧ 𝑧 ∈ ({𝑥} × 𝐵)) → 0 ≤ ⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
136	102, 135, 116	r19.29af 3251	. . . . . 6 ⊢ ((𝜑 ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) → 0 ≤ ⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
137	136	adantlr 713	. . . . 5 ⊢ (((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) ∧ 𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)) → 0 ≤ ⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
138	25, 118, 137, 26	fsumless 15681	. . . 4 ⊢ ((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → Σ𝑧 ∈ ran 𝑓⦋(2nd ‘𝑧) / 𝑘⦌𝐶 ≤ Σ𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
139	99, 138	eqbrtrrd 5129	. . 3 ⊢ ((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → Σ𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝐶 ≤ Σ𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
140		nfcv 2907	. . . . . . . 8 ⊢ Ⅎ𝑦𝐵
141		nfcv 2907	. . . . . . . 8 ⊢ Ⅎ𝑘𝐵
142	12, 140, 141, 15, 16	cbvsum 15580	. . . . . . 7 ⊢ Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑦 ∈ 𝐵 ⦋𝑦 / 𝑘⦌𝐶
143	142	a1i 11	. . . . . 6 ⊢ (𝜑 → Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑦 ∈ 𝐵 ⦋𝑦 / 𝑘⦌𝐶)
144	143	sumeq2sdv 15589	. . . . 5 ⊢ (𝜑 → Σ𝑥 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑥 ∈ 𝐴 Σ𝑦 ∈ 𝐵 ⦋𝑦 / 𝑘⦌𝐶)
145		vex 3449	. . . . . . . . . 10 ⊢ 𝑥 ∈ V
146		vex 3449	. . . . . . . . . 10 ⊢ 𝑦 ∈ V
147	145, 146	op2ndd 7932	. . . . . . . . 9 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → (2nd ‘𝑧) = 𝑦)
148	147	eqcomd 2742	. . . . . . . 8 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → 𝑦 = (2nd ‘𝑧))
149	148	csbeq1d 3859	. . . . . . 7 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ⦋𝑦 / 𝑘⦌𝐶 = ⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
150	149	eqcomd 2742	. . . . . 6 ⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ⦋(2nd ‘𝑧) / 𝑘⦌𝐶 = ⦋𝑦 / 𝑘⦌𝐶)
151		nfv 1917	. . . . . . . . 9 ⊢ Ⅎ𝑘((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵)
152	16	nfel1 2923	. . . . . . . . 9 ⊢ Ⅎ𝑘⦋𝑦 / 𝑘⦌𝐶 ∈ ℂ
153	151, 152	nfim 1899	. . . . . . . 8 ⊢ Ⅎ𝑘(((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → ⦋𝑦 / 𝑘⦌𝐶 ∈ ℂ)
154		eleq1w 2820	. . . . . . . . . 10 ⊢ (𝑘 = 𝑦 → (𝑘 ∈ 𝐵 ↔ 𝑦 ∈ 𝐵))
155	154	anbi2d 629	. . . . . . . . 9 ⊢ (𝑘 = 𝑦 → (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) ↔ ((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵)))
156	155, 83	imbi12d 344	. . . . . . . 8 ⊢ (𝑘 = 𝑦 → ((((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ) ↔ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → ⦋𝑦 / 𝑘⦌𝐶 ∈ ℂ)))
157	88	recnd 11183	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑘 ∈ 𝐵) → 𝐶 ∈ ℂ)
158	153, 156, 157	chvarfv 2233	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑥 ∈ 𝐴) ∧ 𝑦 ∈ 𝐵) → ⦋𝑦 / 𝑘⦌𝐶 ∈ ℂ)
159	158	anasss 467	. . . . . 6 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵)) → ⦋𝑦 / 𝑘⦌𝐶 ∈ ℂ)
160	150, 1, 2, 159	fsum2d 15656	. . . . 5 ⊢ (𝜑 → Σ𝑥 ∈ 𝐴 Σ𝑦 ∈ 𝐵 ⦋𝑦 / 𝑘⦌𝐶 = Σ𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
161	144, 160	eqtrd 2776	. . . 4 ⊢ (𝜑 → Σ𝑥 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
162	161	adantr 481	. . 3 ⊢ ((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → Σ𝑥 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶 = Σ𝑧 ∈ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵)⦋(2nd ‘𝑧) / 𝑘⦌𝐶)
163	139, 162	breqtrrd 5133	. 2 ⊢ ((𝜑 ∧ ((𝑓:∪ 𝑥 ∈ 𝐴 𝐵–1-1-onto→ran 𝑓 ∧ ∀𝑙 ∈ ∪ 𝑥 ∈ 𝐴 𝐵(2nd ‘(𝑓‘𝑙)) = 𝑙) ∧ ran 𝑓 ⊆ ∪ 𝑥 ∈ 𝐴 ({𝑥} × 𝐵))) → Σ𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝐶 ≤ Σ𝑥 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶)
164	11, 163	exlimddv 1938	1 ⊢ (𝜑 → Σ𝑘 ∈ ∪ 𝑥 ∈ 𝐴 𝐵𝐶 ≤ Σ𝑥 ∈ 𝐴 Σ𝑘 ∈ 𝐵 𝐶)

Syntax hints:   → wi 4   ∧ wa 396   = wceq 1541  ∃wex 1781   ∈ wcel 2106  ∀wral 3064  ∃wrex 3073  ⦋csb 3855   ⊆ wss 3910  {csn 4586  ⟨cop 4592  ∪ ciun 4954   class class class wbr 5105   × cxp 5631  ^◡ccnv 5632  ran crn 5634   Fn wfn 6491  –1-1→wf1 6493  –1-1-onto→wf1o 6495  ‘cfv 6496  1^st c1st 7919  2^nd c2nd 7920  Fincfn 8883  ℂcc 11049  ℝcr 11050  0cc0 11051   ≤ cle 11190  Σcsu 15570

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-reg 9528  ax-inf2 9577  ax-ac2 10399  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128  ax-pre-sup 11129

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-iin 4957  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-se 5589  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-isom 6505  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-er 8648  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-sup 9378  df-oi 9446  df-r1 9700  df-rank 9701  df-card 9875  df-ac 10052  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-div 11813  df-nn 12154  df-2 12216  df-3 12217  df-n0 12414  df-z 12500  df-uz 12764  df-rp 12916  df-ico 13270  df-fz 13425  df-fzo 13568  df-seq 13907  df-exp 13968  df-hash 14231  df-cj 14984  df-re 14985  df-im 14986  df-sqrt 15120  df-abs 15121  df-clim 15370  df-sum 15571

This theorem is referenced by:  hgt750lema  33270