ovolshftlem2

	Ref	Expression
Hypotheses	ovolshft.1	$⊢ φ \to A \subseteq ℝ$
	ovolshft.2	$⊢ φ \to C \in ℝ$
	ovolshft.3	$⊢ φ \to B = \{x \in ℝ \| x - C \in A\}$
	ovolshft.4	$⊢ M = \{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (B \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\}$
Assertion	ovolshftlem2	$⊢ φ \to \{z \in ℝ^{} \| \exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land z = sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <))\} \subseteq M$

Proof

Step	Hyp	Ref	Expression
1		ovolshft.1	$⊢ φ \to A \subseteq ℝ$
2		ovolshft.2	$⊢ φ \to C \in ℝ$
3		ovolshft.3	$⊢ φ \to B = \{x \in ℝ \| x - C \in A\}$
4		ovolshft.4	$⊢ M = \{y \in ℝ^{} \| \exists f \in ({(\leq \cap ℝ^{2})}^{ℕ}) (B \subseteq ⋃ ran ((.) \circ f) \land y = sup (ran seq 1 (+ ((abs \circ -) \circ f)) ℝ^{} <))\}$
5	1	ad3antrrr	$⊢ (((φ \land z \in ℝ^{*}) \land g \in ({(\leq \cap ℝ^{2})}^{ℕ})) \land A \subseteq ⋃ ran ((.) \circ g)) \to A \subseteq ℝ$
6	2	ad3antrrr	$⊢ (((φ \land z \in ℝ^{*}) \land g \in ({(\leq \cap ℝ^{2})}^{ℕ})) \land A \subseteq ⋃ ran ((.) \circ g)) \to C \in ℝ$
7	3	ad3antrrr	$⊢ (((φ \land z \in ℝ^{*}) \land g \in ({(\leq \cap ℝ^{2})}^{ℕ})) \land A \subseteq ⋃ ran ((.) \circ g)) \to B = \{x \in ℝ \| x - C \in A\}$
8		eqid	$⊢ seq 1 (+ ((abs \circ -) \circ g)) = seq 1 (+ ((abs \circ -) \circ g))$
9		2fveq3	$⊢ m = n \to 1^{st} (g (m)) = 1^{st} (g (n))$
10	9	oveq1d	$⊢ m = n \to 1^{st} (g (m)) + C = 1^{st} (g (n)) + C$
11		2fveq3	$⊢ m = n \to 2^{nd} (g (m)) = 2^{nd} (g (n))$
12	11	oveq1d	$⊢ m = n \to 2^{nd} (g (m)) + C = 2^{nd} (g (n)) + C$
13	10 12	opeq12d	$⊢ m = n \to ⟨1^{st} (g (m)) + C, 2^{nd} (g (m)) + C⟩ = ⟨1^{st} (g (n)) + C, 2^{nd} (g (n)) + C⟩$
14	13	cbvmptv	$⊢ (m \in ℕ ⟼ ⟨1^{st} (g (m)) + C, 2^{nd} (g (m)) + C⟩) = (n \in ℕ ⟼ ⟨1^{st} (g (n)) + C, 2^{nd} (g (n)) + C⟩)$
15		simplr	$⊢ (((φ \land z \in ℝ^{*}) \land g \in ({(\leq \cap ℝ^{2})}^{ℕ})) \land A \subseteq ⋃ ran ((.) \circ g)) \to g \in ({(\leq \cap ℝ^{2})}^{ℕ})$
16		elovolmlem	$⊢ g \in ({(\leq \cap ℝ^{2})}^{ℕ}) \leftrightarrow g : ℕ ⟶ \leq \cap ℝ^{2}$
17	15 16	sylib	$⊢ (((φ \land z \in ℝ^{*}) \land g \in ({(\leq \cap ℝ^{2})}^{ℕ})) \land A \subseteq ⋃ ran ((.) \circ g)) \to g : ℕ ⟶ \leq \cap ℝ^{2}$
18		simpr	$⊢ (((φ \land z \in ℝ^{*}) \land g \in ({(\leq \cap ℝ^{2})}^{ℕ})) \land A \subseteq ⋃ ran ((.) \circ g)) \to A \subseteq ⋃ ran ((.) \circ g)$
19	5 6 7 4 8 14 17 18	ovolshftlem1	$⊢ (((φ \land z \in ℝ^{}) \land g \in ({(\leq \cap ℝ^{2})}^{ℕ})) \land A \subseteq ⋃ ran ((.) \circ g)) \to sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <) \in M$
20		eleq1a	$⊢ sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <) \in M \to (z = sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <) \to z \in M)$
21	19 20	syl	$⊢ (((φ \land z \in ℝ^{}) \land g \in ({(\leq \cap ℝ^{2})}^{ℕ})) \land A \subseteq ⋃ ran ((.) \circ g)) \to (z = sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <) \to z \in M)$
22	21	expimpd	$⊢ ((φ \land z \in ℝ^{}) \land g \in ({(\leq \cap ℝ^{2})}^{ℕ})) \to ((A \subseteq ⋃ ran ((.) \circ g) \land z = sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <)) \to z \in M)$
23	22	rexlimdva	$⊢ (φ \land z \in ℝ^{}) \to (\exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land z = sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <)) \to z \in M)$
24	23	ralrimiva	$⊢ φ \to \forall z \in ℝ^{} (\exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land z = sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <)) \to z \in M)$
25		rabss	$⊢ \{z \in ℝ^{} \| \exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land z = sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <))\} \subseteq M \leftrightarrow \forall z \in ℝ^{} (\exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land z = sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <)) \to z \in M)$
26	24 25	sylibr	$⊢ φ \to \{z \in ℝ^{} \| \exists g \in ({(\leq \cap ℝ^{2})}^{ℕ}) (A \subseteq ⋃ ran ((.) \circ g) \land z = sup (ran seq 1 (+ ((abs \circ -) \circ g)) ℝ^{} <))\} \subseteq M$

Metamath Proof Explorer

Theorem ovolshftlem2

Proof