Theorem elovolmr

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

	Ref	Expression
Hypotheses	elovolm.1	⊢ 𝑀 = { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) }
	elovolmr.2	⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
Assertion	elovolmr	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐹 ) ) → sup ( ran 𝑆 , ℝ* , < ) ∈ 𝑀 )

Proof

Step	Hyp	Ref	Expression
1		elovolm.1	⊢ 𝑀 = { 𝑦 ∈ ℝ* ∣ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ 𝑦 = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) }
2		elovolmr.2	⊢ 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) )
3		elovolmlem	⊢ ( 𝐹 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ↔ 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) )
4		id	⊢ ( 𝑓 = 𝐹 → 𝑓 = 𝐹 )
5	4	eqcomd	⊢ ( 𝑓 = 𝐹 → 𝐹 = 𝑓 )
6	5	coeq2d	⊢ ( 𝑓 = 𝐹 → ( ( abs ∘ − ) ∘ 𝐹 ) = ( ( abs ∘ − ) ∘ 𝑓 ) )
7	6	seqeq3d	⊢ ( 𝑓 = 𝐹 → seq 1 ( + , ( ( abs ∘ − ) ∘ 𝐹 ) ) = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) )
8	2 7	eqtrid	⊢ ( 𝑓 = 𝐹 → 𝑆 = seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) )
9	8	rneqd	⊢ ( 𝑓 = 𝐹 → ran 𝑆 = ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) )
10	9	supeq1d	⊢ ( 𝑓 = 𝐹 → sup ( ran 𝑆 , ℝ* , < ) = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) )
11	10	biantrud	⊢ ( 𝑓 = 𝐹 → ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ↔ ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ sup ( ran 𝑆 , ℝ* , < ) = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) ) )
12		coeq2	⊢ ( 𝑓 = 𝐹 → ( (,) ∘ 𝑓 ) = ( (,) ∘ 𝐹 ) )
13	12	rneqd	⊢ ( 𝑓 = 𝐹 → ran ( (,) ∘ 𝑓 ) = ran ( (,) ∘ 𝐹 ) )
14	13	unieqd	⊢ ( 𝑓 = 𝐹 → ∪ ran ( (,) ∘ 𝑓 ) = ∪ ran ( (,) ∘ 𝐹 ) )
15	14	sseq2d	⊢ ( 𝑓 = 𝐹 → ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ↔ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐹 ) ) )
16	11 15	bitr3d	⊢ ( 𝑓 = 𝐹 → ( ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ sup ( ran 𝑆 , ℝ* , < ) = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) ↔ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐹 ) ) )
17	16	rspcev	⊢ ( ( 𝐹 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ∧ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐹 ) ) → ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ sup ( ran 𝑆 , ℝ* , < ) = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) )
18	3 17	sylanbr	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐹 ) ) → ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ sup ( ran 𝑆 , ℝ* , < ) = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) )
19	1	elovolm	⊢ ( sup ( ran 𝑆 , ℝ* , < ) ∈ 𝑀 ↔ ∃ 𝑓 ∈ ( ( ≤ ∩ ( ℝ × ℝ ) ) ↑m ℕ ) ( 𝐴 ⊆ ∪ ran ( (,) ∘ 𝑓 ) ∧ sup ( ran 𝑆 , ℝ* , < ) = sup ( ran seq 1 ( + , ( ( abs ∘ − ) ∘ 𝑓 ) ) , ℝ* , < ) ) )
20	18 19	sylibr	⊢ ( ( 𝐹 : ℕ ⟶ ( ≤ ∩ ( ℝ × ℝ ) ) ∧ 𝐴 ⊆ ∪ ran ( (,) ∘ 𝐹 ) ) → sup ( ran 𝑆 , ℝ* , < ) ∈ 𝑀 )