Theorem ixxval

Description: Value of the interval function. (Contributed by Mario Carneiro, 3-Nov-2013)

	Ref	Expression
Hypothesis	ixx.1	⊢ 𝑂 = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑆 𝑦 ) } )
Assertion	ixxval	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 𝑂 𝐵 ) = { 𝑧 ∈ ℝ* ∣ ( 𝐴 𝑅 𝑧 ∧ 𝑧 𝑆 𝐵 ) } )

Proof

Step	Hyp	Ref	Expression
1		ixx.1	⊢ 𝑂 = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑆 𝑦 ) } )
2		breq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 𝑅 𝑧 ↔ 𝐴 𝑅 𝑧 ) )
3	2	anbi1d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑆 𝑦 ) ↔ ( 𝐴 𝑅 𝑧 ∧ 𝑧 𝑆 𝑦 ) ) )
4	3	rabbidv	⊢ ( 𝑥 = 𝐴 → { 𝑧 ∈ ℝ* ∣ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑆 𝑦 ) } = { 𝑧 ∈ ℝ* ∣ ( 𝐴 𝑅 𝑧 ∧ 𝑧 𝑆 𝑦 ) } )
5		breq2	⊢ ( 𝑦 = 𝐵 → ( 𝑧 𝑆 𝑦 ↔ 𝑧 𝑆 𝐵 ) )
6	5	anbi2d	⊢ ( 𝑦 = 𝐵 → ( ( 𝐴 𝑅 𝑧 ∧ 𝑧 𝑆 𝑦 ) ↔ ( 𝐴 𝑅 𝑧 ∧ 𝑧 𝑆 𝐵 ) ) )
7	6	rabbidv	⊢ ( 𝑦 = 𝐵 → { 𝑧 ∈ ℝ* ∣ ( 𝐴 𝑅 𝑧 ∧ 𝑧 𝑆 𝑦 ) } = { 𝑧 ∈ ℝ* ∣ ( 𝐴 𝑅 𝑧 ∧ 𝑧 𝑆 𝐵 ) } )
8		xrex	⊢ ℝ* ∈ V
9	8	rabex	⊢ { 𝑧 ∈ ℝ* ∣ ( 𝐴 𝑅 𝑧 ∧ 𝑧 𝑆 𝐵 ) } ∈ V
10	4 7 1 9	ovmpo	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 𝑂 𝐵 ) = { 𝑧 ∈ ℝ* ∣ ( 𝐴 𝑅 𝑧 ∧ 𝑧 𝑆 𝐵 ) } )