elovolmr

Description: Sufficient condition for elementhood in the set M . (Contributed by Mario Carneiro, 16-Mar-2014)

	Ref	Expression
Hypotheses	elovolm.1	$⊢ M = \{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\}$
	elovolmr.2	$⊢ S = seq 1 (+ ((abs \circ -) \circ F))$
Assertion	elovolmr	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land A \subseteq ⋃ ran ((.) \circ F)) \to sup (ran S ℝ^{*} <) \in M$

Proof

Step	Hyp	Ref	Expression
1		elovolm.1	$⊢ M = \{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\}$
2		elovolmr.2	$⊢ S = seq 1 (+ ((abs \circ -) \circ F))$
3		elovolmlem	$⊢ F \in ({(\leq \cap ℝ^{2})}^{ℕ}) \leftrightarrow F : ℕ ⟶ \leq \cap ℝ^{2}$
4		id	$⊢ f = F \to f = F$
5	4	eqcomd	$⊢ f = F \to F = f$
6	5	coeq2d	$⊢ f = F \to (abs \circ -) \circ F = (abs \circ -) \circ f$
7	6	seqeq3d	$⊢ f = F \to seq 1 (+ ((abs \circ -) \circ F)) = seq 1 (+ ((abs \circ -) \circ f))$
8	2 7	syl5eq	$⊢ f = F \to S = seq 1 (+ ((abs \circ -) \circ f))$
9	8	rneqd	$⊢ f = F \to ran S = ran seq 1 (+ ((abs \circ -) \circ f))$
10	9	supeq1d	$⊢ f = F \to sup (ran S ℝ^{} <) = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <)$
11	10	biantrud	$⊢ f = F \to (A \subseteq ⋃ ran ((.) \circ f) \leftrightarrow (A \subseteq ⋃ ran ((.) \circ f) \land sup (ran S ℝ^{} <) = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <)))$
12		coeq2	$⊢ f = F \to (.) \circ f = (.) \circ F$
13	12	rneqd	$⊢ f = F \to ran ((.) \circ f) = ran ((.) \circ F)$
14	13	unieqd	$⊢ f = F \to ⋃ ran ((.) \circ f) = ⋃ ran ((.) \circ F)$
15	14	sseq2d	$⊢ f = F \to (A \subseteq ⋃ ran ((.) \circ f) \leftrightarrow A \subseteq ⋃ ran ((.) \circ F))$
16	11 15	bitr3d	$⊢ f = F \to ((A \subseteq ⋃ ran ((.) \circ f) \land sup (ran S ℝ^{} <) = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <)) \leftrightarrow A \subseteq ⋃ ran ((.) \circ F))$
17	16	rspcev	$⊢ (F \in ({(\leq \cap ℝ^{2})}^{ℕ}) \land A \subseteq ⋃ ran ((.) \circ F)) \to \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land sup (ran S ℝ^{} <) = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))$
18	3 17	sylanbr	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land A \subseteq ⋃ ran ((.) \circ F)) \to \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land sup (ran S ℝ^{} <) = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))$
19	1	elovolm	$⊢ sup (ran S ℝ^{} <) \in M \leftrightarrow \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ f) \land sup (ran S ℝ^{} <) = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{*} <))$
20	18 19	sylibr	$⊢ (F : ℕ ⟶ \leq \cap ℝ^{2} \land A \subseteq ⋃ ran ((.) \circ F)) \to sup (ran S ℝ^{*} <) \in M$

Metamath Proof Explorer

Theorem elovolmr

Proof