Metamath Proof Explorer

Theorem ordtcld2

Description: An upward ray [ P , +oo ) is closed. (Contributed by Mario Carneiro, 3-Sep-2015)

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

Proof

Step	Hyp	Ref	Expression
1		ordttopon.3	$⊢ X = dom R$
2		ssrab2	$⊢ \{x \in X \| P R x\} \subseteq X$
3	1	ordttopon	$⊢ R \in V \to ordTop (R) \in TopOn (X)$
4	3	adantr	$⊢ (R \in V \land P \in X) \to ordTop (R) \in TopOn (X)$
5		toponuni	$⊢ ordTop (R) \in TopOn (X) \to X = ⋃ ordTop (R)$
6	4 5	syl	$⊢ (R \in V \land P \in X) \to X = ⋃ ordTop (R)$
7	2 6	sseqtrid	$⊢ (R \in V \land P \in X) \to \{x \in X \| P R x\} \subseteq ⋃ ordTop (R)$
8		notrab	$⊢ X ∖ \{x \in X \| P R x\} = \{x \in X \| \neg P R x\}$
9	6	difeq1d	$⊢ (R \in V \land P \in X) \to X ∖ \{x \in X \| P R x\} = ⋃ ordTop (R) ∖ \{x \in X \| P R x\}$
10	8 9	eqtr3id	$⊢ (R \in V \land P \in X) \to \{x \in X \| \neg P R x\} = ⋃ ordTop (R) ∖ \{x \in X \| P R x\}$
11	1	ordtopn2	$⊢ (R \in V \land P \in X) \to \{x \in X \| \neg P R x\} \in ordTop (R)$
12	10 11	eqeltrrd	$⊢ (R \in V \land P \in X) \to ⋃ ordTop (R) ∖ \{x \in X \| P R x\} \in ordTop (R)$
13		topontop	$⊢ ordTop (R) \in TopOn (X) \to ordTop (R) \in Top$
14		eqid	$⊢ ⋃ ordTop (R) = ⋃ ordTop (R)$
15	14	iscld	$⊢ ordTop (R) \in Top \to (\{x \in X \| P R x\} \in Clsd (ordTop (R)) \leftrightarrow (\{x \in X \| P R x\} \subseteq ⋃ ordTop (R) \land ⋃ ordTop (R) ∖ \{x \in X \| P R x\} \in ordTop (R)))$
16	4 13 15	3syl	$⊢ (R \in V \land P \in X) \to (\{x \in X \| P R x\} \in Clsd (ordTop (R)) \leftrightarrow (\{x \in X \| P R x\} \subseteq ⋃ ordTop (R) \land ⋃ ordTop (R) ∖ \{x \in X \| P R x\} \in ordTop (R)))$
17	7 12 16	mpbir2and	$⊢ (R \in V \land P \in X) \to \{x \in X \| P R x\} \in Clsd (ordTop (R))$