Theorem hoidifhspval

Description: D is a function that returns the representation of the left side of the difference of a half-open interval and a half-space. Used in Lemma 115F of Fremlin1 p. 31 . (Contributed by Glauco Siliprandi, 24-Dec-2020)

	Ref	Expression
Hypotheses	hoidifhspval.d	⊢ 𝐷 = ( 𝑥 ∈ ℝ ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑋 ) ↦ ( 𝑘 ∈ 𝑋 ↦ if ( 𝑘 = 𝐾 , if ( 𝑥 ≤ ( 𝑎 ‘ 𝑘 ) , ( 𝑎 ‘ 𝑘 ) , 𝑥 ) , ( 𝑎 ‘ 𝑘 ) ) ) ) )
	hoidifhspval.y	⊢ ( 𝜑 → 𝑌 ∈ ℝ )
Assertion	hoidifhspval	⊢ ( 𝜑 → ( 𝐷 ‘ 𝑌 ) = ( 𝑎 ∈ ( ℝ ↑m 𝑋 ) ↦ ( 𝑘 ∈ 𝑋 ↦ if ( 𝑘 = 𝐾 , if ( 𝑌 ≤ ( 𝑎 ‘ 𝑘 ) , ( 𝑎 ‘ 𝑘 ) , 𝑌 ) , ( 𝑎 ‘ 𝑘 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		hoidifhspval.d	⊢ 𝐷 = ( 𝑥 ∈ ℝ ↦ ( 𝑎 ∈ ( ℝ ↑m 𝑋 ) ↦ ( 𝑘 ∈ 𝑋 ↦ if ( 𝑘 = 𝐾 , if ( 𝑥 ≤ ( 𝑎 ‘ 𝑘 ) , ( 𝑎 ‘ 𝑘 ) , 𝑥 ) , ( 𝑎 ‘ 𝑘 ) ) ) ) )
2		hoidifhspval.y	⊢ ( 𝜑 → 𝑌 ∈ ℝ )
3		breq1	⊢ ( 𝑥 = 𝑌 → ( 𝑥 ≤ ( 𝑎 ‘ 𝑘 ) ↔ 𝑌 ≤ ( 𝑎 ‘ 𝑘 ) ) )
4		id	⊢ ( 𝑥 = 𝑌 → 𝑥 = 𝑌 )
5	3 4	ifbieq2d	⊢ ( 𝑥 = 𝑌 → if ( 𝑥 ≤ ( 𝑎 ‘ 𝑘 ) , ( 𝑎 ‘ 𝑘 ) , 𝑥 ) = if ( 𝑌 ≤ ( 𝑎 ‘ 𝑘 ) , ( 𝑎 ‘ 𝑘 ) , 𝑌 ) )
6	5	ifeq1d	⊢ ( 𝑥 = 𝑌 → if ( 𝑘 = 𝐾 , if ( 𝑥 ≤ ( 𝑎 ‘ 𝑘 ) , ( 𝑎 ‘ 𝑘 ) , 𝑥 ) , ( 𝑎 ‘ 𝑘 ) ) = if ( 𝑘 = 𝐾 , if ( 𝑌 ≤ ( 𝑎 ‘ 𝑘 ) , ( 𝑎 ‘ 𝑘 ) , 𝑌 ) , ( 𝑎 ‘ 𝑘 ) ) )
7	6	mpteq2dv	⊢ ( 𝑥 = 𝑌 → ( 𝑘 ∈ 𝑋 ↦ if ( 𝑘 = 𝐾 , if ( 𝑥 ≤ ( 𝑎 ‘ 𝑘 ) , ( 𝑎 ‘ 𝑘 ) , 𝑥 ) , ( 𝑎 ‘ 𝑘 ) ) ) = ( 𝑘 ∈ 𝑋 ↦ if ( 𝑘 = 𝐾 , if ( 𝑌 ≤ ( 𝑎 ‘ 𝑘 ) , ( 𝑎 ‘ 𝑘 ) , 𝑌 ) , ( 𝑎 ‘ 𝑘 ) ) ) )
8	7	mpteq2dv	⊢ ( 𝑥 = 𝑌 → ( 𝑎 ∈ ( ℝ ↑m 𝑋 ) ↦ ( 𝑘 ∈ 𝑋 ↦ if ( 𝑘 = 𝐾 , if ( 𝑥 ≤ ( 𝑎 ‘ 𝑘 ) , ( 𝑎 ‘ 𝑘 ) , 𝑥 ) , ( 𝑎 ‘ 𝑘 ) ) ) ) = ( 𝑎 ∈ ( ℝ ↑m 𝑋 ) ↦ ( 𝑘 ∈ 𝑋 ↦ if ( 𝑘 = 𝐾 , if ( 𝑌 ≤ ( 𝑎 ‘ 𝑘 ) , ( 𝑎 ‘ 𝑘 ) , 𝑌 ) , ( 𝑎 ‘ 𝑘 ) ) ) ) )
9		ovex	⊢ ( ℝ ↑m 𝑋 ) ∈ V
10	9	mptex	⊢ ( 𝑎 ∈ ( ℝ ↑m 𝑋 ) ↦ ( 𝑘 ∈ 𝑋 ↦ if ( 𝑘 = 𝐾 , if ( 𝑌 ≤ ( 𝑎 ‘ 𝑘 ) , ( 𝑎 ‘ 𝑘 ) , 𝑌 ) , ( 𝑎 ‘ 𝑘 ) ) ) ) ∈ V
11	10	a1i	⊢ ( 𝜑 → ( 𝑎 ∈ ( ℝ ↑m 𝑋 ) ↦ ( 𝑘 ∈ 𝑋 ↦ if ( 𝑘 = 𝐾 , if ( 𝑌 ≤ ( 𝑎 ‘ 𝑘 ) , ( 𝑎 ‘ 𝑘 ) , 𝑌 ) , ( 𝑎 ‘ 𝑘 ) ) ) ) ∈ V )
12	1 8 2 11	fvmptd3	⊢ ( 𝜑 → ( 𝐷 ‘ 𝑌 ) = ( 𝑎 ∈ ( ℝ ↑m 𝑋 ) ↦ ( 𝑘 ∈ 𝑋 ↦ if ( 𝑘 = 𝐾 , if ( 𝑌 ≤ ( 𝑎 ‘ 𝑘 ) , ( 𝑎 ‘ 𝑘 ) , 𝑌 ) , ( 𝑎 ‘ 𝑘 ) ) ) ) )