Metamath Proof Explorer

Theorem hoicoto2

Description: The half-open interval expressed using a composition of a function into ( RR X. RR ) and using two distinct real-valued functions for the borders. (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses hoicoto2.i ⊢ φ → I : X ⟶ ℝ 2
hoicoto2.a ⊢ A = k ∈ X ⟼ 1 st ⁡ I ⁡ k
hoicoto2.b ⊢ B = k ∈ X ⟼ 2 nd ⁡ I ⁡ k
Assertion hoicoto2 ⊢ φ → ⨉ k ∈ X . ∘ I ⁡ k = ⨉ k ∈ X A ⁡ k B ⁡ k

Proof

Step Hyp Ref Expression
1 hoicoto2.i ⊢ φ → I : X ⟶ ℝ 2
2 hoicoto2.a ⊢ A = k ∈ X ⟼ 1 st ⁡ I ⁡ k
3 hoicoto2.b ⊢ B = k ∈ X ⟼ 2 nd ⁡ I ⁡ k
4 1 adantr ⊢ φ ∧ k ∈ X → I : X ⟶ ℝ 2
5 simpr ⊢ φ ∧ k ∈ X → k ∈ X
6 4 5 fvovco ⊢ φ ∧ k ∈ X → . ∘ I ⁡ k = 1 st ⁡ I ⁡ k 2 nd ⁡ I ⁡ k
7 1 ffvelrnda ⊢ φ ∧ k ∈ X → I ⁡ k ∈ ℝ 2
8 xp1st ⊢ I ⁡ k ∈ ℝ 2 → 1 st ⁡ I ⁡ k ∈ ℝ
9 7 8 syl ⊢ φ ∧ k ∈ X → 1 st ⁡ I ⁡ k ∈ ℝ
10 9 elexd ⊢ φ ∧ k ∈ X → 1 st ⁡ I ⁡ k ∈ V
11 2 fvmpt2 ⊢ k ∈ X ∧ 1 st ⁡ I ⁡ k ∈ V → A ⁡ k = 1 st ⁡ I ⁡ k
12 5 10 11 syl2anc ⊢ φ ∧ k ∈ X → A ⁡ k = 1 st ⁡ I ⁡ k
13 12 eqcomd ⊢ φ ∧ k ∈ X → 1 st ⁡ I ⁡ k = A ⁡ k
14 xp2nd ⊢ I ⁡ k ∈ ℝ 2 → 2 nd ⁡ I ⁡ k ∈ ℝ
15 7 14 syl ⊢ φ ∧ k ∈ X → 2 nd ⁡ I ⁡ k ∈ ℝ
16 15 elexd ⊢ φ ∧ k ∈ X → 2 nd ⁡ I ⁡ k ∈ V
17 3 fvmpt2 ⊢ k ∈ X ∧ 2 nd ⁡ I ⁡ k ∈ V → B ⁡ k = 2 nd ⁡ I ⁡ k
18 5 16 17 syl2anc ⊢ φ ∧ k ∈ X → B ⁡ k = 2 nd ⁡ I ⁡ k
19 18 eqcomd ⊢ φ ∧ k ∈ X → 2 nd ⁡ I ⁡ k = B ⁡ k
20 13 19 oveq12d ⊢ φ ∧ k ∈ X → 1 st ⁡ I ⁡ k 2 nd ⁡ I ⁡ k = A ⁡ k B ⁡ k
21 6 20 eqtrd ⊢ φ ∧ k ∈ X → . ∘ I ⁡ k = A ⁡ k B ⁡ k
22 21 ixpeq2dva ⊢ φ → ⨉ k ∈ X . ∘ I ⁡ k = ⨉ k ∈ X A ⁡ k B ⁡ k