Theorem elixx3g

Description: Membership in a set of open intervals of extended reals. We use the fact that an operation's value is empty outside of its domain to show A e. RR* and B e. RR* . (Contributed by Mario Carneiro, 3-Nov-2013)

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

Proof

Step	Hyp	Ref	Expression
1		ixx.1	⊢ 𝑂 = ( 𝑥 ∈ ℝ* , 𝑦 ∈ ℝ* ↦ { 𝑧 ∈ ℝ* ∣ ( 𝑥 𝑅 𝑧 ∧ 𝑧 𝑆 𝑦 ) } )
2		anass	⊢ ( ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑅 𝐶 ∧ 𝐶 𝑆 𝐵 ) ) ↔ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐶 ∈ ℝ* ∧ ( 𝐴 𝑅 𝐶 ∧ 𝐶 𝑆 𝐵 ) ) ) )
3		df-3an	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ↔ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝐶 ∈ ℝ* ) )
4	3	anbi1i	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑅 𝐶 ∧ 𝐶 𝑆 𝐵 ) ) ↔ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑅 𝐶 ∧ 𝐶 𝑆 𝐵 ) ) )
5	1	elixx1	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐶 ∈ ( 𝐴 𝑂 𝐵 ) ↔ ( 𝐶 ∈ ℝ* ∧ 𝐴 𝑅 𝐶 ∧ 𝐶 𝑆 𝐵 ) ) )
6		3anass	⊢ ( ( 𝐶 ∈ ℝ* ∧ 𝐴 𝑅 𝐶 ∧ 𝐶 𝑆 𝐵 ) ↔ ( 𝐶 ∈ ℝ* ∧ ( 𝐴 𝑅 𝐶 ∧ 𝐶 𝑆 𝐵 ) ) )
7		ibar	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐶 ∈ ℝ* ∧ ( 𝐴 𝑅 𝐶 ∧ 𝐶 𝑆 𝐵 ) ) ↔ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐶 ∈ ℝ* ∧ ( 𝐴 𝑅 𝐶 ∧ 𝐶 𝑆 𝐵 ) ) ) ) )
8	6 7	bitrid	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( ( 𝐶 ∈ ℝ* ∧ 𝐴 𝑅 𝐶 ∧ 𝐶 𝑆 𝐵 ) ↔ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐶 ∈ ℝ* ∧ ( 𝐴 𝑅 𝐶 ∧ 𝐶 𝑆 𝐵 ) ) ) ) )
9	5 8	bitrd	⊢ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐶 ∈ ( 𝐴 𝑂 𝐵 ) ↔ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐶 ∈ ℝ* ∧ ( 𝐴 𝑅 𝐶 ∧ 𝐶 𝑆 𝐵 ) ) ) ) )
10	1	ixxf	⊢ 𝑂 : ( ℝ* × ℝ* ) ⟶ 𝒫 ℝ*
11	10	fdmi	⊢ dom 𝑂 = ( ℝ* × ℝ* )
12	11	ndmov	⊢ ( ¬ ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐴 𝑂 𝐵 ) = ∅ )
13	12	eleq2d	⊢ ( ¬ ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐶 ∈ ( 𝐴 𝑂 𝐵 ) ↔ 𝐶 ∈ ∅ ) )
14		noel	⊢ ¬ 𝐶 ∈ ∅
15	14	pm2.21i	⊢ ( 𝐶 ∈ ∅ → ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) )
16		simpl	⊢ ( ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐶 ∈ ℝ* ∧ ( 𝐴 𝑅 𝐶 ∧ 𝐶 𝑆 𝐵 ) ) ) → ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) )
17	15 16	pm5.21ni	⊢ ( ¬ ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐶 ∈ ∅ ↔ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐶 ∈ ℝ* ∧ ( 𝐴 𝑅 𝐶 ∧ 𝐶 𝑆 𝐵 ) ) ) ) )
18	13 17	bitrd	⊢ ( ¬ ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) → ( 𝐶 ∈ ( 𝐴 𝑂 𝐵 ) ↔ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐶 ∈ ℝ* ∧ ( 𝐴 𝑅 𝐶 ∧ 𝐶 𝑆 𝐵 ) ) ) ) )
19	9 18	pm2.61i	⊢ ( 𝐶 ∈ ( 𝐴 𝑂 𝐵 ) ↔ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ) ∧ ( 𝐶 ∈ ℝ* ∧ ( 𝐴 𝑅 𝐶 ∧ 𝐶 𝑆 𝐵 ) ) ) )
20	2 4 19	3bitr4ri	⊢ ( 𝐶 ∈ ( 𝐴 𝑂 𝐵 ) ↔ ( ( 𝐴 ∈ ℝ* ∧ 𝐵 ∈ ℝ* ∧ 𝐶 ∈ ℝ* ) ∧ ( 𝐴 𝑅 𝐶 ∧ 𝐶 𝑆 𝐵 ) ) )