Metamath Proof Explorer

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 syl5eq ⊢ ( 𝑓 = 𝐹 → 𝑆 = 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 𝑆 , ℝ* , < ) ∈ 𝑀 )