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 ( 𝜑𝐼 : 𝑋 ⟶ ( ℝ × ℝ ) )
hoicoto2.a 𝐴 = ( 𝑘𝑋 ↦ ( 1st ‘ ( 𝐼𝑘 ) ) )
hoicoto2.b 𝐵 = ( 𝑘𝑋 ↦ ( 2nd ‘ ( 𝐼𝑘 ) ) )
Assertion hoicoto2 ( 𝜑X 𝑘𝑋 ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) = X 𝑘𝑋 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) )

Proof

Step Hyp Ref Expression
1 hoicoto2.i ( 𝜑𝐼 : 𝑋 ⟶ ( ℝ × ℝ ) )
2 hoicoto2.a 𝐴 = ( 𝑘𝑋 ↦ ( 1st ‘ ( 𝐼𝑘 ) ) )
3 hoicoto2.b 𝐵 = ( 𝑘𝑋 ↦ ( 2nd ‘ ( 𝐼𝑘 ) ) )
4 1 adantr ( ( 𝜑𝑘𝑋 ) → 𝐼 : 𝑋 ⟶ ( ℝ × ℝ ) )
5 simpr ( ( 𝜑𝑘𝑋 ) → 𝑘𝑋 )
6 4 5 fvovco ( ( 𝜑𝑘𝑋 ) → ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) = ( ( 1st ‘ ( 𝐼𝑘 ) ) [,) ( 2nd ‘ ( 𝐼𝑘 ) ) ) )
7 1 ffvelrnda ( ( 𝜑𝑘𝑋 ) → ( 𝐼𝑘 ) ∈ ( ℝ × ℝ ) )
8 xp1st ( ( 𝐼𝑘 ) ∈ ( ℝ × ℝ ) → ( 1st ‘ ( 𝐼𝑘 ) ) ∈ ℝ )
9 7 8 syl ( ( 𝜑𝑘𝑋 ) → ( 1st ‘ ( 𝐼𝑘 ) ) ∈ ℝ )
10 9 elexd ( ( 𝜑𝑘𝑋 ) → ( 1st ‘ ( 𝐼𝑘 ) ) ∈ V )
11 2 fvmpt2 ( ( 𝑘𝑋 ∧ ( 1st ‘ ( 𝐼𝑘 ) ) ∈ V ) → ( 𝐴𝑘 ) = ( 1st ‘ ( 𝐼𝑘 ) ) )
12 5 10 11 syl2anc ( ( 𝜑𝑘𝑋 ) → ( 𝐴𝑘 ) = ( 1st ‘ ( 𝐼𝑘 ) ) )
13 12 eqcomd ( ( 𝜑𝑘𝑋 ) → ( 1st ‘ ( 𝐼𝑘 ) ) = ( 𝐴𝑘 ) )
14 xp2nd ( ( 𝐼𝑘 ) ∈ ( ℝ × ℝ ) → ( 2nd ‘ ( 𝐼𝑘 ) ) ∈ ℝ )
15 7 14 syl ( ( 𝜑𝑘𝑋 ) → ( 2nd ‘ ( 𝐼𝑘 ) ) ∈ ℝ )
16 15 elexd ( ( 𝜑𝑘𝑋 ) → ( 2nd ‘ ( 𝐼𝑘 ) ) ∈ V )
17 3 fvmpt2 ( ( 𝑘𝑋 ∧ ( 2nd ‘ ( 𝐼𝑘 ) ) ∈ V ) → ( 𝐵𝑘 ) = ( 2nd ‘ ( 𝐼𝑘 ) ) )
18 5 16 17 syl2anc ( ( 𝜑𝑘𝑋 ) → ( 𝐵𝑘 ) = ( 2nd ‘ ( 𝐼𝑘 ) ) )
19 18 eqcomd ( ( 𝜑𝑘𝑋 ) → ( 2nd ‘ ( 𝐼𝑘 ) ) = ( 𝐵𝑘 ) )
20 13 19 oveq12d ( ( 𝜑𝑘𝑋 ) → ( ( 1st ‘ ( 𝐼𝑘 ) ) [,) ( 2nd ‘ ( 𝐼𝑘 ) ) ) = ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) )
21 6 20 eqtrd ( ( 𝜑𝑘𝑋 ) → ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) = ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) )
22 21 ixpeq2dva ( 𝜑X 𝑘𝑋 ( ( [,) ∘ 𝐼 ) ‘ 𝑘 ) = X 𝑘𝑋 ( ( 𝐴𝑘 ) [,) ( 𝐵𝑘 ) ) )