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

Proof

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

Metamath Proof Explorer

Theorem elixx3g

Proof