Theorem ovolshftlem2

Description: Lemma for ovolshft . (Contributed by Mario Carneiro, 22-Mar-2014)

	Ref	Expression
Hypotheses	ovolshft.1	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
	ovolshft.2	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
	ovolshft.3	⊢ ( 𝜑 → 𝐵 = { 𝑥 ∈ ℝ ∣ ( 𝑥 − 𝐶 ) ∈ 𝐴 } )
	ovolshft.4	⊢ 𝑀 = { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐵 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) }
Assertion	ovolshftlem2	⊢ ( 𝜑 → { 𝑧 ∈ ℝ* ∣ ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑧 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ) } ⊆ 𝑀 )

Proof

Step	Hyp	Ref	Expression
1		ovolshft.1	⊢ ( 𝜑 → 𝐴 ⊆ ℝ )
2		ovolshft.2	⊢ ( 𝜑 → 𝐶 ∈ ℝ )
3		ovolshft.3	⊢ ( 𝜑 → 𝐵 = { 𝑥 ∈ ℝ ∣ ( 𝑥 − 𝐶 ) ∈ 𝐴 } )
4		ovolshft.4	⊢ 𝑀 = { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐵 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) }
5	1	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ* ) ∧ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ) ∧ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ) → 𝐴 ⊆ ℝ )
6	2	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ* ) ∧ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ) ∧ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ) → 𝐶 ∈ ℝ )
7	3	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ* ) ∧ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ) ∧ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ) → 𝐵 = { 𝑥 ∈ ℝ ∣ ( 𝑥 − 𝐶 ) ∈ 𝐴 } )
8		eqid	⊢ seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) )
9		2fveq3	⊢ ( 𝑚 = 𝑛 → ( 1st ‘ ( 𝑔 ‘ 𝑚 ) ) = ( 1st ‘ ( 𝑔 ‘ 𝑛 ) ) )
10	9	oveq1d	⊢ ( 𝑚 = 𝑛 → ( ( 1st ‘ ( 𝑔 ‘ 𝑚 ) ) + 𝐶 ) = ( ( 1st ‘ ( 𝑔 ‘ 𝑛 ) ) + 𝐶 ) )
11		2fveq3	⊢ ( 𝑚 = 𝑛 → ( 2nd ‘ ( 𝑔 ‘ 𝑚 ) ) = ( 2nd ‘ ( 𝑔 ‘ 𝑛 ) ) )
12	11	oveq1d	⊢ ( 𝑚 = 𝑛 → ( ( 2nd ‘ ( 𝑔 ‘ 𝑚 ) ) + 𝐶 ) = ( ( 2nd ‘ ( 𝑔 ‘ 𝑛 ) ) + 𝐶 ) )
13	10 12	opeq12d	⊢ ( 𝑚 = 𝑛 → ⟨ ( ( 1st ‘ ( 𝑔 ‘ 𝑚 ) ) + 𝐶 ) , ( ( 2nd ‘ ( 𝑔 ‘ 𝑚 ) ) + 𝐶 ) ⟩ = ⟨ ( ( 1st ‘ ( 𝑔 ‘ 𝑛 ) ) + 𝐶 ) , ( ( 2nd ‘ ( 𝑔 ‘ 𝑛 ) ) + 𝐶 ) ⟩ )
14	13	cbvmptv	⊢ ( 𝑚 ∈ ℕ ↦ ⟨ ( ( 1st ‘ ( 𝑔 ‘ 𝑚 ) ) + 𝐶 ) , ( ( 2nd ‘ ( 𝑔 ‘ 𝑚 ) ) + 𝐶 ) ⟩ ) = ( 𝑛 ∈ ℕ ↦ ⟨ ( ( 1st ‘ ( 𝑔 ‘ 𝑛 ) ) + 𝐶 ) , ( ( 2nd ‘ ( 𝑔 ‘ 𝑛 ) ) + 𝐶 ) ⟩ )
15		simplr	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ* ) ∧ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ) ∧ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ) → 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) )
16		elovolmlem	⊢ ( 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ↔ 𝑔 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
17	15 16	sylib	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ* ) ∧ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ) ∧ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ) → 𝑔 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
18		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ* ) ∧ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ) ∧ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ) → 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) )
19	5 6 7 4 8 14 17 18	ovolshftlem1	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ* ) ∧ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ) ∧ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ) → sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ∈ 𝑀 )
20		eleq1a	⊢ ( sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ∈ 𝑀 → ( 𝑧 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) → 𝑧 ∈ 𝑀 ) )
21	19 20	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ* ) ∧ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ) ∧ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ) → ( 𝑧 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) → 𝑧 ∈ 𝑀 ) )
22	21	expimpd	⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ ℝ* ) ∧ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ) → ( ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑧 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ) → 𝑧 ∈ 𝑀 ) )
23	22	rexlimdva	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ℝ* ) → ( ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑧 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ) → 𝑧 ∈ 𝑀 ) )
24	23	ralrimiva	⊢ ( 𝜑 → ∀ 𝑧 ∈ ℝ* ( ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑧 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ) → 𝑧 ∈ 𝑀 ) )
25		rabss	⊢ ( { 𝑧 ∈ ℝ* ∣ ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑧 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ) } ⊆ 𝑀 ↔ ∀ 𝑧 ∈ ℝ* ( ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑧 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ) → 𝑧 ∈ 𝑀 ) )
26	24 25	sylibr	⊢ ( 𝜑 → { 𝑧 ∈ ℝ* ∣ ∃ 𝑔 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑔 ) ∧ 𝑧 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑔 ) ) , ℝ* , < ) ) } ⊆ 𝑀 )