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

Metamath Proof Explorer

Theorem elixx1

Description: Membership in an interval of extended reals. (Contributed by Mario Carneiro, 3-Nov-2013)

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

Proof

Step Hyp Ref Expression
1 ixx.1 ⊢ 𝑂 = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑆 𝑦 ) } )
2 1 ixxval ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 𝑂 𝐵 ) = { 𝑧 ∈ ℝ* ∣ ( 𝐴 𝑅 𝑧 ∧ 𝑧 𝑆 𝐵 ) } )
3 2 eleq2d ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐶 ∈ ( 𝐴 𝑂 𝐵 ) ↔ 𝐶 ∈ { 𝑧 ∈ ℝ* ∣ ( 𝐴 𝑅 𝑧 ∧ 𝑧 𝑆 𝐵 ) } ) )
4 breq2 ⊢ ( 𝑧 = 𝐶 → ( 𝐴 𝑅 𝑧 ↔ 𝐴 𝑅 𝐶 ) )
5 breq1 ⊢ ( 𝑧 = 𝐶 → ( 𝑧 𝑆 𝐵 ↔ 𝐶 𝑆 𝐵 ) )
6 4 5 anbi12d ⊢ ( 𝑧 = 𝐶 → ( ( 𝐴 𝑅 𝑧 ∧ 𝑧 𝑆 𝐵 ) ↔ ( 𝐴 𝑅 𝐶 ∧ 𝐶 𝑆 𝐵 ) ) )
7 6 elrab ⊢ ( 𝐶 ∈ { 𝑧 ∈ ℝ* ∣ ( 𝐴 𝑅 𝑧 ∧ 𝑧 𝑆 𝐵 ) } ↔ ( 𝐶 ∈ ℝ* ∧ ( 𝐴 𝑅 𝐶 ∧ 𝐶 𝑆 𝐵 ) ) )
8 3anass ⊢ ( ( 𝐶 ∈ ℝ* ∧ 𝐴 𝑅 𝐶 ∧ 𝐶 𝑆 𝐵 ) ↔ ( 𝐶 ∈ ℝ* ∧ ( 𝐴 𝑅 𝐶 ∧ 𝐶 𝑆 𝐵 ) ) )
9 7 8 bitr4i ⊢ ( 𝐶 ∈ { 𝑧 ∈ ℝ* ∣ ( 𝐴 𝑅 𝑧 ∧ 𝑧 𝑆 𝐵 ) } ↔ ( 𝐶 ∈ ℝ* ∧ 𝐴 𝑅 𝐶 ∧ 𝐶 𝑆 𝐵 ) )
10 3 9 bitrdi ⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐶 ∈ ( 𝐴 𝑂 𝐵 ) ↔ ( 𝐶 ∈ ℝ* ∧ 𝐴 𝑅 𝐶 ∧ 𝐶 𝑆 𝐵 ) ) )