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

Metamath Proof Explorer

Theorem elixx3g

Proof