ordtopn2

Description: A downward ray ( -oo , P ) is open. (Contributed by Mario Carneiro, 3-Sep-2015)

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

Proof

Step	Hyp	Ref	Expression
1		ordttopon.3	$⊢ X = dom R$
2		eqid	$⊢ ran (y \in X ⟼ \{x \in X \| \neg x R y\}) = ran (y \in X ⟼ \{x \in X \| \neg x R y\})$
3		eqid	$⊢ ran (y \in X ⟼ \{x \in X \| \neg y R x\}) = ran (y \in X ⟼ \{x \in X \| \neg y R x\})$
4	1 2 3	ordtuni	$⊢ R \in V \to X = ⋃ (\{X\} \cup (ran (y \in X ⟼ \{x \in X \| \neg x R y\}) \cup ran (y \in X ⟼ \{x \in X \| \neg y R x\})))$
5	4	adantr	$⊢ (R \in V \land P \in X) \to X = ⋃ (\{X\} \cup (ran (y \in X ⟼ \{x \in X \| \neg x R y\}) \cup ran (y \in X ⟼ \{x \in X \| \neg y R x\})))$
6		dmexg	$⊢ R \in V \to dom R \in V$
7	1 6	eqeltrid	$⊢ R \in V \to X \in V$
8	7	adantr	$⊢ (R \in V \land P \in X) \to X \in V$
9	5 8	eqeltrrd	$⊢ (R \in V \land P \in X) \to ⋃ (\{X\} \cup (ran (y \in X ⟼ \{x \in X \| \neg x R y\}) \cup ran (y \in X ⟼ \{x \in X \| \neg y R x\}))) \in V$
10		uniexb	$⊢ \{X\} \cup (ran (y \in X ⟼ \{x \in X \| \neg x R y\}) \cup ran (y \in X ⟼ \{x \in X \| \neg y R x\})) \in V \leftrightarrow ⋃ (\{X\} \cup (ran (y \in X ⟼ \{x \in X \| \neg x R y\}) \cup ran (y \in X ⟼ \{x \in X \| \neg y R x\}))) \in V$
11	9 10	sylibr	$⊢ (R \in V \land P \in X) \to \{X\} \cup (ran (y \in X ⟼ \{x \in X \| \neg x R y\}) \cup ran (y \in X ⟼ \{x \in X \| \neg y R x\})) \in V$
12		ssfii	$⊢ \{X\} \cup (ran (y \in X ⟼ \{x \in X \| \neg x R y\}) \cup ran (y \in X ⟼ \{x \in X \| \neg y R x\})) \in V \to \{X\} \cup (ran (y \in X ⟼ \{x \in X \| \neg x R y\}) \cup ran (y \in X ⟼ \{x \in X \| \neg y R x\})) \subseteq fi (\{X\} \cup (ran (y \in X ⟼ \{x \in X \| \neg x R y\}) \cup ran (y \in X ⟼ \{x \in X \| \neg y R x\})))$
13	11 12	syl	$⊢ (R \in V \land P \in X) \to \{X\} \cup (ran (y \in X ⟼ \{x \in X \| \neg x R y\}) \cup ran (y \in X ⟼ \{x \in X \| \neg y R x\})) \subseteq fi (\{X\} \cup (ran (y \in X ⟼ \{x \in X \| \neg x R y\}) \cup ran (y \in X ⟼ \{x \in X \| \neg y R x\})))$
14		fibas	$⊢ fi (\{X\} \cup (ran (y \in X ⟼ \{x \in X \| \neg x R y\}) \cup ran (y \in X ⟼ \{x \in X \| \neg y R x\}))) \in TopBases$
15		bastg	$⊢ fi (\{X\} \cup (ran (y \in X ⟼ \{x \in X \| \neg x R y\}) \cup ran (y \in X ⟼ \{x \in X \| \neg y R x\}))) \in TopBases \to fi (\{X\} \cup (ran (y \in X ⟼ \{x \in X \| \neg x R y\}) \cup ran (y \in X ⟼ \{x \in X \| \neg y R x\}))) \subseteq topGen (fi (\{X\} \cup (ran (y \in X ⟼ \{x \in X \| \neg x R y\}) \cup ran (y \in X ⟼ \{x \in X \| \neg y R x\}))))$
16	14 15	ax-mp	$⊢ fi (\{X\} \cup (ran (y \in X ⟼ \{x \in X \| \neg x R y\}) \cup ran (y \in X ⟼ \{x \in X \| \neg y R x\}))) \subseteq topGen (fi (\{X\} \cup (ran (y \in X ⟼ \{x \in X \| \neg x R y\}) \cup ran (y \in X ⟼ \{x \in X \| \neg y R x\}))))$
17	13 16	sstrdi	$⊢ (R \in V \land P \in X) \to \{X\} \cup (ran (y \in X ⟼ \{x \in X \| \neg x R y\}) \cup ran (y \in X ⟼ \{x \in X \| \neg y R x\})) \subseteq topGen (fi (\{X\} \cup (ran (y \in X ⟼ \{x \in X \| \neg x R y\}) \cup ran (y \in X ⟼ \{x \in X \| \neg y R x\}))))$
18	1 2 3	ordtval	$⊢ R \in V \to ordTop (R) = topGen (fi (\{X\} \cup (ran (y \in X ⟼ \{x \in X \| \neg x R y\}) \cup ran (y \in X ⟼ \{x \in X \| \neg y R x\}))))$
19	18	adantr	$⊢ (R \in V \land P \in X) \to ordTop (R) = topGen (fi (\{X\} \cup (ran (y \in X ⟼ \{x \in X \| \neg x R y\}) \cup ran (y \in X ⟼ \{x \in X \| \neg y R x\}))))$
20	17 19	sseqtrrd	$⊢ (R \in V \land P \in X) \to \{X\} \cup (ran (y \in X ⟼ \{x \in X \| \neg x R y\}) \cup ran (y \in X ⟼ \{x \in X \| \neg y R x\})) \subseteq ordTop (R)$
21		ssun2	$⊢ ran (y \in X ⟼ \{x \in X \| \neg x R y\}) \cup ran (y \in X ⟼ \{x \in X \| \neg y R x\}) \subseteq \{X\} \cup (ran (y \in X ⟼ \{x \in X \| \neg x R y\}) \cup ran (y \in X ⟼ \{x \in X \| \neg y R x\}))$
22		ssun2	$⊢ ran (y \in X ⟼ \{x \in X \| \neg y R x\}) \subseteq ran (y \in X ⟼ \{x \in X \| \neg x R y\}) \cup ran (y \in X ⟼ \{x \in X \| \neg y R x\})$
23		simpr	$⊢ (R \in V \land P \in X) \to P \in X$
24		eqidd	$⊢ (R \in V \land P \in X) \to \{x \in X \| \neg P R x\} = \{x \in X \| \neg P R x\}$
25		breq1	$⊢ y = P \to (y R x \leftrightarrow P R x)$
26	25	notbid	$⊢ y = P \to (\neg y R x \leftrightarrow \neg P R x)$
27	26	rabbidv	$⊢ y = P \to \{x \in X \| \neg y R x\} = \{x \in X \| \neg P R x\}$
28	27	rspceeqv	$⊢ (P \in X \land \{x \in X \| \neg P R x\} = \{x \in X \| \neg P R x\}) \to \exists y \in X \{x \in X \| \neg P R x\} = \{x \in X \| \neg y R x\}$
29	23 24 28	syl2anc	$⊢ (R \in V \land P \in X) \to \exists y \in X \{x \in X \| \neg P R x\} = \{x \in X \| \neg y R x\}$
30		rabexg	$⊢ X \in V \to \{x \in X \| \neg P R x\} \in V$
31		eqid	$⊢ (y \in X ⟼ \{x \in X \| \neg y R x\}) = (y \in X ⟼ \{x \in X \| \neg y R x\})$
32	31	elrnmpt	$⊢ \{x \in X \| \neg P R x\} \in V \to (\{x \in X \| \neg P R x\} \in ran (y \in X ⟼ \{x \in X \| \neg y R x\}) \leftrightarrow \exists y \in X \{x \in X \| \neg P R x\} = \{x \in X \| \neg y R x\})$
33	8 30 32	3syl	$⊢ (R \in V \land P \in X) \to (\{x \in X \| \neg P R x\} \in ran (y \in X ⟼ \{x \in X \| \neg y R x\}) \leftrightarrow \exists y \in X \{x \in X \| \neg P R x\} = \{x \in X \| \neg y R x\})$
34	29 33	mpbird	$⊢ (R \in V \land P \in X) \to \{x \in X \| \neg P R x\} \in ran (y \in X ⟼ \{x \in X \| \neg y R x\})$
35	22 34	sselid	$⊢ (R \in V \land P \in X) \to \{x \in X \| \neg P R x\} \in (ran (y \in X ⟼ \{x \in X \| \neg x R y\}) \cup ran (y \in X ⟼ \{x \in X \| \neg y R x\}))$
36	21 35	sselid	$⊢ (R \in V \land P \in X) \to \{x \in X \| \neg P R x\} \in (\{X\} \cup (ran (y \in X ⟼ \{x \in X \| \neg x R y\}) \cup ran (y \in X ⟼ \{x \in X \| \neg y R x\})))$
37	20 36	sseldd	$⊢ (R \in V \land P \in X) \to \{x \in X \| \neg P R x\} \in ordTop (R)$

Metamath Proof Explorer

Theorem ordtopn2

Proof