This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 𝑂 𝐵 ) = { 𝑧 ∈ ℝ* ∣ ( 𝐴 𝑅 𝑧 ∧ 𝑧 𝑆 𝐵 ) } )