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 ⊢ Ⅎ 𝑘 𝜑
hoi2toco.c ⊢ 𝐼 = ( 𝑘 ∈ 𝑋 ↦ ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ )
Assertion hoi2toco ( 𝜑 → X 𝑘 ∈ 𝑋 ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) = X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) )

Proof

Step Hyp Ref Expression
1 hoi2toco.1 ⊢ Ⅎ 𝑘 𝜑
2 hoi2toco.c ⊢ 𝐼 = ( 𝑘 ∈ 𝑋 ↦ ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ )
3 2 funmpt2 ⊢ Fun 𝐼
4 3 a1i ⊢ ( 𝜑 → Fun 𝐼 )
5 4 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → Fun 𝐼 )
6 simpr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝑘 ∈ 𝑋 )
7 2 dmeqi ⊢ dom 𝐼 = dom ( 𝑘 ∈ 𝑋 ↦ ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ )
8 7 a1i ⊢ ( 𝜑 → dom 𝐼 = dom ( 𝑘 ∈ 𝑋 ↦ ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ ) )
9 opex ⊢ ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ ∈ V
10 9 2a1i ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑋 → ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ ∈ V ) )
11 1 10 ralrimi ⊢ ( 𝜑 → ∀ 𝑘 ∈ 𝑋 ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ ∈ V )
12 dmmptg ⊢ ( ∀ 𝑘 ∈ 𝑋 ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ ∈ V → dom ( 𝑘 ∈ 𝑋 ↦ ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ ) = 𝑋 )
13 11 12 syl ⊢ ( 𝜑 → dom ( 𝑘 ∈ 𝑋 ↦ ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ ) = 𝑋 )
14 8 13 eqtr2d ⊢ ( 𝜑 → 𝑋 = dom 𝐼 )
15 14 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝑋 = dom 𝐼 )
16 6 15 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → 𝑘 ∈ dom 𝐼 )
17 fvco ⊢ ( ( Fun 𝐼 ∧ 𝑘 ∈ dom 𝐼 ) → ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) = ( [,) ‘ ( 𝐼 ‘ 𝑘 ) ) )
18 5 16 17 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) = ( [,) ‘ ( 𝐼 ‘ 𝑘 ) ) )
19 9 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ ∈ V )
20 2 fvmpt2 ⊢ ( ( 𝑘 ∈ 𝑋 ∧ ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ ∈ V ) → ( 𝐼 ‘ 𝑘 ) = ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ )
21 6 19 20 syl2anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( 𝐼 ‘ 𝑘 ) = ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ )
22 21 fveq2d ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( [,) ‘ ( 𝐼 ‘ 𝑘 ) ) = ( [,) ‘ ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ ) )
23 df-ov ⊢ ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) = ( [,) ‘ ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ )
24 23 eqcomi ⊢ ( [,) ‘ ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ ) = ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) )
25 24 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( [,) ‘ ⟨ ( 𝐴 ‘ 𝑘 ) , ( 𝐵 ‘ 𝑘 ) ⟩ ) = ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) )
26 18 22 25 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑋 ) → ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) = ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) )
27 1 26 ixpeq2d ⊢ ( 𝜑 → X 𝑘 ∈ 𝑋 ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) = X 𝑘 ∈ 𝑋 ( ( 𝐴 ‘ 𝑘 ) [,) ( 𝐵 ‘ 𝑘 ) ) )