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	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐶 ∈ ( 𝐴 𝑂 𝐵 ) ↔ ( 𝐶 ∈ ℝ* ∧ 𝐴 𝑅 𝐶 ∧ 𝐶 𝑆 𝐵 ) ) )