sge0pnffigt

Description: If the sum of nonnegative extended reals is +oo , then any real number can be dominated by finite subsums. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	sge0pnffigt.x	$⊢ φ \to X \in V$
	sge0pnffigt.f	$⊢ φ \to F : X ⟶ [0, +∞]$
	sge0pnffigt.pnf	$⊢ φ \to sum^(F) = +∞$
	sge0pnffigt.y	$⊢ φ \to Y \in ℝ$
Assertion	sge0pnffigt	$⊢ φ \to \exists x \in (𝒫 X \cap Fin) Y < sum^({F ↾}_{x})$

Proof

Step	Hyp	Ref	Expression
1		sge0pnffigt.x	$⊢ φ \to X \in V$
2		sge0pnffigt.f	$⊢ φ \to F : X ⟶ [0, +∞]$
3		sge0pnffigt.pnf	$⊢ φ \to sum^(F) = +∞$
4		sge0pnffigt.y	$⊢ φ \to Y \in ℝ$
5	1 2	sge0sup	$⊢ φ \to sum^(F) = sup (ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) ℝ^{*} <)$
6	5 3	eqtr3d	$⊢ φ \to sup (ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) ℝ^{*} <) = +∞$
7		vex	$⊢ x \in V$
8	7	a1i	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to x \in V$
9	2	adantr	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to F : X ⟶ [0, +∞]$
10		elpwinss	$⊢ x \in (𝒫 X \cap Fin) \to x \subseteq X$
11	10	adantl	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to x \subseteq X$
12	9 11	fssresd	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to ({F ↾}_{x}) : x ⟶ [0, +∞]$
13	8 12	sge0xrcl	$⊢ (φ \land x \in (𝒫 X \cap Fin)) \to sum^({F ↾}_{x}) \in ℝ^{*}$
14	13	ralrimiva	$⊢ φ \to \forall x \in (𝒫 X \cap Fin) sum^({F ↾}_{x}) \in ℝ^{*}$
15		eqid	$⊢ (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) = (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x}))$
16	15	rnmptss	$⊢ \forall x \in (𝒫 X \cap Fin) sum^({F ↾}_{x}) \in ℝ^{} \to ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) \subseteq ℝ^{}$
17	14 16	syl	$⊢ φ \to ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) \subseteq ℝ^{*}$
18		supxrunb2	$⊢ ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) \subseteq ℝ^{} \to (\forall y \in ℝ \exists z \in ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) y < z \leftrightarrow sup (ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) ℝ^{} <) = +∞)$
19	17 18	syl	$⊢ φ \to (\forall y \in ℝ \exists z \in ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) y < z \leftrightarrow sup (ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) ℝ^{*} <) = +∞)$
20	6 19	mpbird	$⊢ φ \to \forall y \in ℝ \exists z \in ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) y < z$
21		breq1	$⊢ y = Y \to (y < z \leftrightarrow Y < z)$
22	21	rexbidv	$⊢ y = Y \to (\exists z \in ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) y < z \leftrightarrow \exists z \in ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) Y < z)$
23	22	rspcva	$⊢ (Y \in ℝ \land \forall y \in ℝ \exists z \in ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) y < z) \to \exists z \in ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) Y < z$
24	4 20 23	syl2anc	$⊢ φ \to \exists z \in ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) Y < z$
25		vex	$⊢ z \in V$
26	15	elrnmpt	$⊢ z \in V \to (z \in ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) \leftrightarrow \exists x \in (𝒫 X \cap Fin) z = sum^({F ↾}_{x}))$
27	25 26	ax-mp	$⊢ z \in ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) \leftrightarrow \exists x \in (𝒫 X \cap Fin) z = sum^({F ↾}_{x})$
28	27	biimpi	$⊢ z \in ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) \to \exists x \in (𝒫 X \cap Fin) z = sum^({F ↾}_{x})$
29	28	3ad2ant2	$⊢ (φ \land z \in ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) \land Y < z) \to \exists x \in (𝒫 X \cap Fin) z = sum^({F ↾}_{x})$
30		nfv	$⊢ Ⅎ x φ$
31		nfcv	$⊢ \underline{Ⅎ} x z$
32		nfmpt1	$⊢ \underline{Ⅎ} x (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x}))$
33	32	nfrn	$⊢ \underline{Ⅎ} x ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x}))$
34	31 33	nfel	$⊢ Ⅎ x z \in ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x}))$
35		nfv	$⊢ Ⅎ x Y < z$
36	30 34 35	nf3an	$⊢ Ⅎ x (φ \land z \in ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) \land Y < z)$
37		simpl	$⊢ (Y < z \land z = sum^({F ↾}_{x})) \to Y < z$
38		simpr	$⊢ (Y < z \land z = sum^({F ↾}_{x})) \to z = sum^({F ↾}_{x})$
39	38	breq2d	$⊢ (Y < z \land z = sum^({F ↾}_{x})) \to (Y < z \leftrightarrow Y < sum^({F ↾}_{x}))$
40	37 39	mpbid	$⊢ (Y < z \land z = sum^({F ↾}_{x})) \to Y < sum^({F ↾}_{x})$
41	40	ex	$⊢ Y < z \to (z = sum^({F ↾}_{x}) \to Y < sum^({F ↾}_{x}))$
42	41	adantl	$⊢ (φ \land Y < z) \to (z = sum^({F ↾}_{x}) \to Y < sum^({F ↾}_{x}))$
43	42	a1d	$⊢ (φ \land Y < z) \to (x \in (𝒫 X \cap Fin) \to (z = sum^({F ↾}_{x}) \to Y < sum^({F ↾}_{x})))$
44	43	3adant2	$⊢ (φ \land z \in ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) \land Y < z) \to (x \in (𝒫 X \cap Fin) \to (z = sum^({F ↾}_{x}) \to Y < sum^({F ↾}_{x})))$
45	36 44	reximdai	$⊢ (φ \land z \in ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) \land Y < z) \to (\exists x \in (𝒫 X \cap Fin) z = sum^({F ↾}_{x}) \to \exists x \in (𝒫 X \cap Fin) Y < sum^({F ↾}_{x}))$
46	29 45	mpd	$⊢ (φ \land z \in ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) \land Y < z) \to \exists x \in (𝒫 X \cap Fin) Y < sum^({F ↾}_{x})$
47	46	3exp	$⊢ φ \to (z \in ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) \to (Y < z \to \exists x \in (𝒫 X \cap Fin) Y < sum^({F ↾}_{x})))$
48	47	rexlimdv	$⊢ φ \to (\exists z \in ran (x \in (𝒫 X \cap Fin) ⟼ sum^({F ↾}_{x})) Y < z \to \exists x \in (𝒫 X \cap Fin) Y < sum^({F ↾}_{x}))$
49	24 48	mpd	$⊢ φ \to \exists x \in (𝒫 X \cap Fin) Y < sum^({F ↾}_{x})$

Metamath Proof Explorer

Theorem sge0pnffigt

Proof