ordtcld3

Description: A closed interval [ A , B ] is closed. (Contributed by Mario Carneiro, 3-Sep-2015)

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

Step	Hyp	Ref	Expression
1		ordttopon.3	$⊢ X = dom R$
2		inrab	$⊢ \{x \in X \| A R x\} \cap \{x \in X \| x R B\} = \{x \in X \| (A R x \land x R B)\}$
3	1	ordtcld2	$⊢ (R \in V \land A \in X) \to \{x \in X \| A R x\} \in Clsd (ordTop (R))$
4	3	3adant3	$⊢ (R \in V \land A \in X \land B \in X) \to \{x \in X \| A R x\} \in Clsd (ordTop (R))$
5	1	ordtcld1	$⊢ (R \in V \land B \in X) \to \{x \in X \| x R B\} \in Clsd (ordTop (R))$
6		incld	$⊢ (\{x \in X \| A R x\} \in Clsd (ordTop (R)) \land \{x \in X \| x R B\} \in Clsd (ordTop (R))) \to \{x \in X \| A R x\} \cap \{x \in X \| x R B\} \in Clsd (ordTop (R))$
7	4 5 6	3imp3i2an	$⊢ (R \in V \land A \in X \land B \in X) \to \{x \in X \| A R x\} \cap \{x \in X \| x R B\} \in Clsd (ordTop (R))$
8	2 7	eqeltrrid	$⊢ (R \in V \land A \in X \land B \in X) \to \{x \in X \| (A R x \land x R B)\} \in Clsd (ordTop (R))$

Metamath Proof Explorer