ordtopn3

Description: An open interval ( A , B ) is open. (Contributed by Mario Carneiro, 3-Sep-2015)

		Ref	Expression
	Hypothesis	ordttopon.3	$⊢ X = dom R$
	Assertion	ordtopn3	$⊢ (R \in V \land A \in X \land B \in X) \to \{x \in X \| (\neg x R A \land \neg B R x)\} \in ordTop (R)$

Step	Hyp	Ref	Expression
1		ordttopon.3	$⊢ X = dom R$
2		inrab	$⊢ \{x \in X \| \neg x R A\} \cap \{x \in X \| \neg B R x\} = \{x \in X \| (\neg x R A \land \neg B R x)\}$
3	1	ordttopon	$⊢ R \in V \to ordTop (R) \in TopOn (X)$
4	3	3ad2ant1	$⊢ (R \in V \land A \in X \land B \in X) \to ordTop (R) \in TopOn (X)$
5		topontop	$⊢ ordTop (R) \in TopOn (X) \to ordTop (R) \in Top$
6	4 5	syl	$⊢ (R \in V \land A \in X \land B \in X) \to ordTop (R) \in Top$
7	1	ordtopn1	$⊢ (R \in V \land A \in X) \to \{x \in X \| \neg x R A\} \in ordTop (R)$
8	7	3adant3	$⊢ (R \in V \land A \in X \land B \in X) \to \{x \in X \| \neg x R A\} \in ordTop (R)$
9	1	ordtopn2	$⊢ (R \in V \land B \in X) \to \{x \in X \| \neg B R x\} \in ordTop (R)$
10	9	3adant2	$⊢ (R \in V \land A \in X \land B \in X) \to \{x \in X \| \neg B R x\} \in ordTop (R)$
11		inopn	$⊢ (ordTop (R) \in Top \land \{x \in X \| \neg x R A\} \in ordTop (R) \land \{x \in X \| \neg B R x\} \in ordTop (R)) \to \{x \in X \| \neg x R A\} \cap \{x \in X \| \neg B R x\} \in ordTop (R)$
12	6 8 10 11	syl3anc	$⊢ (R \in V \land A \in X \land B \in X) \to \{x \in X \| \neg x R A\} \cap \{x \in X \| \neg B R x\} \in ordTop (R)$
13	2 12	eqeltrrid	$⊢ (R \in V \land A \in X \land B \in X) \to \{x \in X \| (\neg x R A \land \neg B R x)\} \in ordTop (R)$

Metamath Proof Explorer