Metamath Proof Explorer

Theorem hoi2toco

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 hoi2toco.1 ⊢ Ⅎ k φ
hoi2toco.c ⊢ I = k ∈ X ⟼ A ⁡ k B ⁡ k
Assertion hoi2toco ⊢ φ → ⨉ k ∈ X . ∘ I ⁡ k = ⨉ k ∈ X A ⁡ k B ⁡ k

Proof

Step Hyp Ref Expression
1 hoi2toco.1 ⊢ Ⅎ k φ
2 hoi2toco.c ⊢ I = k ∈ X ⟼ A ⁡ k B ⁡ k
3 2 funmpt2 ⊢ Fun ⁡ I
4 3 a1i ⊢ φ → Fun ⁡ I
5 4 adantr ⊢ φ ∧ k ∈ X → Fun ⁡ I
6 simpr ⊢ φ ∧ k ∈ X → k ∈ X
7 2 dmeqi ⊢ dom ⁡ I = dom ⁡ k ∈ X ⟼ A ⁡ k B ⁡ k
8 7 a1i ⊢ φ → dom ⁡ I = dom ⁡ k ∈ X ⟼ A ⁡ k B ⁡ k
9 opex ⊢ A ⁡ k B ⁡ k ∈ V
10 9 2a1i ⊢ φ → k ∈ X → A ⁡ k B ⁡ k ∈ V
11 1 10 ralrimi ⊢ φ → ∀ k ∈ X A ⁡ k B ⁡ k ∈ V
12 dmmptg ⊢ ∀ k ∈ X A ⁡ k B ⁡ k ∈ V → dom ⁡ k ∈ X ⟼ A ⁡ k B ⁡ k = X
13 11 12 syl ⊢ φ → dom ⁡ k ∈ X ⟼ A ⁡ k B ⁡ k = X
14 8 13 eqtr2d ⊢ φ → X = dom ⁡ I
15 14 adantr ⊢ φ ∧ k ∈ X → X = dom ⁡ I
16 6 15 eleqtrd ⊢ φ ∧ k ∈ X → k ∈ dom ⁡ I
17 fvco ⊢ Fun ⁡ I ∧ k ∈ dom ⁡ I → . ∘ I ⁡ k = . ⁡ I ⁡ k
18 5 16 17 syl2anc ⊢ φ ∧ k ∈ X → . ∘ I ⁡ k = . ⁡ I ⁡ k
19 9 a1i ⊢ φ ∧ k ∈ X → A ⁡ k B ⁡ k ∈ V
20 2 fvmpt2 ⊢ k ∈ X ∧ A ⁡ k B ⁡ k ∈ V → I ⁡ k = A ⁡ k B ⁡ k
21 6 19 20 syl2anc ⊢ φ ∧ k ∈ X → I ⁡ k = A ⁡ k B ⁡ k
22 21 fveq2d ⊢ φ ∧ k ∈ X → . ⁡ I ⁡ k = . ⁡ A ⁡ k B ⁡ k
23 df-ov ⊢ A ⁡ k B ⁡ k = . ⁡ A ⁡ k B ⁡ k
24 23 eqcomi ⊢ . ⁡ A ⁡ k B ⁡ k = A ⁡ k B ⁡ k
25 24 a1i ⊢ φ ∧ k ∈ X → . ⁡ A ⁡ k B ⁡ k = A ⁡ k B ⁡ k
26 18 22 25 3eqtrd ⊢ φ ∧ k ∈ X → . ∘ I ⁡ k = A ⁡ k B ⁡ k
27 1 26 ixpeq2d ⊢ φ → ⨉ k ∈ X . ∘ I ⁡ k = ⨉ k ∈ X A ⁡ k B ⁡ k