# Metamath Proof Explorer

## 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 ${⊢}{O}=\left({x}\in {ℝ}^{*},{y}\in {ℝ}^{*}⟼\left\{{z}\in {ℝ}^{*}|\left({x}{R}{z}\wedge {z}{S}{y}\right)\right\}\right)$
Assertion elixx3g ${⊢}{C}\in \left({A}{O}{B}\right)↔\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}{R}{C}\wedge {C}{S}{B}\right)\right)$

### Proof

Step Hyp Ref Expression
1 ixx.1 ${⊢}{O}=\left({x}\in {ℝ}^{*},{y}\in {ℝ}^{*}⟼\left\{{z}\in {ℝ}^{*}|\left({x}{R}{z}\wedge {z}{S}{y}\right)\right\}\right)$
2 anass ${⊢}\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}{R}{C}\wedge {C}{S}{B}\right)\right)↔\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge \left({C}\in {ℝ}^{*}\wedge \left({A}{R}{C}\wedge {C}{S}{B}\right)\right)\right)$
3 df-3an ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)↔\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge {C}\in {ℝ}^{*}\right)$
4 3 anbi1i ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}{R}{C}\wedge {C}{S}{B}\right)\right)↔\left(\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}{R}{C}\wedge {C}{S}{B}\right)\right)$
5 1 elixx1 ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left({C}\in \left({A}{O}{B}\right)↔\left({C}\in {ℝ}^{*}\wedge {A}{R}{C}\wedge {C}{S}{B}\right)\right)$
6 3anass ${⊢}\left({C}\in {ℝ}^{*}\wedge {A}{R}{C}\wedge {C}{S}{B}\right)↔\left({C}\in {ℝ}^{*}\wedge \left({A}{R}{C}\wedge {C}{S}{B}\right)\right)$
7 ibar ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left(\left({C}\in {ℝ}^{*}\wedge \left({A}{R}{C}\wedge {C}{S}{B}\right)\right)↔\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge \left({C}\in {ℝ}^{*}\wedge \left({A}{R}{C}\wedge {C}{S}{B}\right)\right)\right)\right)$
8 6 7 syl5bb ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left(\left({C}\in {ℝ}^{*}\wedge {A}{R}{C}\wedge {C}{S}{B}\right)↔\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge \left({C}\in {ℝ}^{*}\wedge \left({A}{R}{C}\wedge {C}{S}{B}\right)\right)\right)\right)$
9 5 8 bitrd ${⊢}\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left({C}\in \left({A}{O}{B}\right)↔\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge \left({C}\in {ℝ}^{*}\wedge \left({A}{R}{C}\wedge {C}{S}{B}\right)\right)\right)\right)$
10 1 ixxf ${⊢}{O}:{ℝ}^{*}×{ℝ}^{*}⟶𝒫{ℝ}^{*}$
11 10 fdmi ${⊢}\mathrm{dom}{O}={ℝ}^{*}×{ℝ}^{*}$
12 11 ndmov ${⊢}¬\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to {A}{O}{B}=\varnothing$
13 12 eleq2d ${⊢}¬\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left({C}\in \left({A}{O}{B}\right)↔{C}\in \varnothing \right)$
14 noel ${⊢}¬{C}\in \varnothing$
15 14 pm2.21i ${⊢}{C}\in \varnothing \to \left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)$
16 simpl ${⊢}\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge \left({C}\in {ℝ}^{*}\wedge \left({A}{R}{C}\wedge {C}{S}{B}\right)\right)\right)\to \left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)$
17 15 16 pm5.21ni ${⊢}¬\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left({C}\in \varnothing ↔\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge \left({C}\in {ℝ}^{*}\wedge \left({A}{R}{C}\wedge {C}{S}{B}\right)\right)\right)\right)$
18 13 17 bitrd ${⊢}¬\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\to \left({C}\in \left({A}{O}{B}\right)↔\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge \left({C}\in {ℝ}^{*}\wedge \left({A}{R}{C}\wedge {C}{S}{B}\right)\right)\right)\right)$
19 9 18 pm2.61i ${⊢}{C}\in \left({A}{O}{B}\right)↔\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\right)\wedge \left({C}\in {ℝ}^{*}\wedge \left({A}{R}{C}\wedge {C}{S}{B}\right)\right)\right)$
20 2 4 19 3bitr4ri ${⊢}{C}\in \left({A}{O}{B}\right)↔\left(\left({A}\in {ℝ}^{*}\wedge {B}\in {ℝ}^{*}\wedge {C}\in {ℝ}^{*}\right)\wedge \left({A}{R}{C}\wedge {C}{S}{B}\right)\right)$