ist1-2

Description: An alternate characterization of T_1 spaces. (Contributed by Jeff Hankins, 31-Jan-2010) (Proof shortened by Mario Carneiro, 24-Aug-2015)

		Ref	Expression
	Assertion	ist1-2	$⊢ J \in TopOn (X) \to (J \in Fre \leftrightarrow \forall x \in X \forall y \in X (\forall o \in J (x \in o \to y \in o) \to x = y))$

Proof

Step	Hyp	Ref	Expression
1		topontop	$⊢ J \in TopOn (X) \to J \in Top$
2		eqid	$⊢ ⋃ J = ⋃ J$
3	2	ist1	$⊢ J \in Fre \leftrightarrow (J \in Top \land \forall y \in ⋃ J \{y\} \in Clsd (J))$
4	3	baib	$⊢ J \in Top \to (J \in Fre \leftrightarrow \forall y \in ⋃ J \{y\} \in Clsd (J))$
5	1 4	syl	$⊢ J \in TopOn (X) \to (J \in Fre \leftrightarrow \forall y \in ⋃ J \{y\} \in Clsd (J))$
6		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
7	6	raleqdv	$⊢ J \in TopOn (X) \to (\forall y \in X \{y\} \in Clsd (J) \leftrightarrow \forall y \in ⋃ J \{y\} \in Clsd (J))$
8	1	adantr	$⊢ (J \in TopOn (X) \land y \in X) \to J \in Top$
9		eltop2	$⊢ J \in Top \to (⋃ J ∖ \{y\} \in J \leftrightarrow \forall x \in (⋃ J ∖ \{y\}) \exists o \in J (x \in o \land o \subseteq ⋃ J ∖ \{y\}))$
10	8 9	syl	$⊢ (J \in TopOn (X) \land y \in X) \to (⋃ J ∖ \{y\} \in J \leftrightarrow \forall x \in (⋃ J ∖ \{y\}) \exists o \in J (x \in o \land o \subseteq ⋃ J ∖ \{y\}))$
11	6	eleq2d	$⊢ J \in TopOn (X) \to (y \in X \leftrightarrow y \in ⋃ J)$
12	11	biimpa	$⊢ (J \in TopOn (X) \land y \in X) \to y \in ⋃ J$
13	12	snssd	$⊢ (J \in TopOn (X) \land y \in X) \to \{y\} \subseteq ⋃ J$
14	2	iscld2	$⊢ (J \in Top \land \{y\} \subseteq ⋃ J) \to (\{y\} \in Clsd (J) \leftrightarrow ⋃ J ∖ \{y\} \in J)$
15	8 13 14	syl2anc	$⊢ (J \in TopOn (X) \land y \in X) \to (\{y\} \in Clsd (J) \leftrightarrow ⋃ J ∖ \{y\} \in J)$
16	6	adantr	$⊢ (J \in TopOn (X) \land y \in X) \to X = ⋃ J$
17	16	eleq2d	$⊢ (J \in TopOn (X) \land y \in X) \to (x \in X \leftrightarrow x \in ⋃ J)$
18	17	imbi1d	$⊢ (J \in TopOn (X) \land y \in X) \to ((x \in X \to (x \neq y \to \exists o \in J (x \in o \land o \subseteq ⋃ J ∖ \{y\}))) \leftrightarrow (x \in ⋃ J \to (x \neq y \to \exists o \in J (x \in o \land o \subseteq ⋃ J ∖ \{y\}))))$
19		con1b	$⊢ (\neg x = y \to \exists o \in J (x \in o \land o \subseteq ⋃ J ∖ \{y\})) \leftrightarrow (\neg \exists o \in J (x \in o \land o \subseteq ⋃ J ∖ \{y\}) \to x = y)$
20		df-ne	$⊢ x \neq y \leftrightarrow \neg x = y$
21	20	imbi1i	$⊢ (x \neq y \to \exists o \in J (x \in o \land o \subseteq ⋃ J ∖ \{y\})) \leftrightarrow (\neg x = y \to \exists o \in J (x \in o \land o \subseteq ⋃ J ∖ \{y\}))$
22		disjsn	$⊢ o \cap \{y\} = \emptyset \leftrightarrow \neg y \in o$
23		elssuni	$⊢ o \in J \to o \subseteq ⋃ J$
24		reldisj	$⊢ o \subseteq ⋃ J \to (o \cap \{y\} = \emptyset \leftrightarrow o \subseteq ⋃ J ∖ \{y\})$
25	23 24	syl	$⊢ o \in J \to (o \cap \{y\} = \emptyset \leftrightarrow o \subseteq ⋃ J ∖ \{y\})$
26	22 25	bitr3id	$⊢ o \in J \to (\neg y \in o \leftrightarrow o \subseteq ⋃ J ∖ \{y\})$
27	26	anbi2d	$⊢ o \in J \to ((x \in o \land \neg y \in o) \leftrightarrow (x \in o \land o \subseteq ⋃ J ∖ \{y\}))$
28	27	rexbiia	$⊢ \exists o \in J (x \in o \land \neg y \in o) \leftrightarrow \exists o \in J (x \in o \land o \subseteq ⋃ J ∖ \{y\})$
29		rexanali	$⊢ \exists o \in J (x \in o \land \neg y \in o) \leftrightarrow \neg \forall o \in J (x \in o \to y \in o)$
30	28 29	bitr3i	$⊢ \exists o \in J (x \in o \land o \subseteq ⋃ J ∖ \{y\}) \leftrightarrow \neg \forall o \in J (x \in o \to y \in o)$
31	30	con2bii	$⊢ \forall o \in J (x \in o \to y \in o) \leftrightarrow \neg \exists o \in J (x \in o \land o \subseteq ⋃ J ∖ \{y\})$
32	31	imbi1i	$⊢ (\forall o \in J (x \in o \to y \in o) \to x = y) \leftrightarrow (\neg \exists o \in J (x \in o \land o \subseteq ⋃ J ∖ \{y\}) \to x = y)$
33	19 21 32	3bitr4ri	$⊢ (\forall o \in J (x \in o \to y \in o) \to x = y) \leftrightarrow (x \neq y \to \exists o \in J (x \in o \land o \subseteq ⋃ J ∖ \{y\}))$
34	33	imbi2i	$⊢ (x \in X \to (\forall o \in J (x \in o \to y \in o) \to x = y)) \leftrightarrow (x \in X \to (x \neq y \to \exists o \in J (x \in o \land o \subseteq ⋃ J ∖ \{y\})))$
35		eldifsn	$⊢ x \in (⋃ J ∖ \{y\}) \leftrightarrow (x \in ⋃ J \land x \neq y)$
36	35	imbi1i	$⊢ (x \in (⋃ J ∖ \{y\}) \to \exists o \in J (x \in o \land o \subseteq ⋃ J ∖ \{y\})) \leftrightarrow ((x \in ⋃ J \land x \neq y) \to \exists o \in J (x \in o \land o \subseteq ⋃ J ∖ \{y\}))$
37		impexp	$⊢ ((x \in ⋃ J \land x \neq y) \to \exists o \in J (x \in o \land o \subseteq ⋃ J ∖ \{y\})) \leftrightarrow (x \in ⋃ J \to (x \neq y \to \exists o \in J (x \in o \land o \subseteq ⋃ J ∖ \{y\})))$
38	36 37	bitri	$⊢ (x \in (⋃ J ∖ \{y\}) \to \exists o \in J (x \in o \land o \subseteq ⋃ J ∖ \{y\})) \leftrightarrow (x \in ⋃ J \to (x \neq y \to \exists o \in J (x \in o \land o \subseteq ⋃ J ∖ \{y\})))$
39	18 34 38	3bitr4g	$⊢ (J \in TopOn (X) \land y \in X) \to ((x \in X \to (\forall o \in J (x \in o \to y \in o) \to x = y)) \leftrightarrow (x \in (⋃ J ∖ \{y\}) \to \exists o \in J (x \in o \land o \subseteq ⋃ J ∖ \{y\})))$
40	39	ralbidv2	$⊢ (J \in TopOn (X) \land y \in X) \to (\forall x \in X (\forall o \in J (x \in o \to y \in o) \to x = y) \leftrightarrow \forall x \in (⋃ J ∖ \{y\}) \exists o \in J (x \in o \land o \subseteq ⋃ J ∖ \{y\}))$
41	10 15 40	3bitr4d	$⊢ (J \in TopOn (X) \land y \in X) \to (\{y\} \in Clsd (J) \leftrightarrow \forall x \in X (\forall o \in J (x \in o \to y \in o) \to x = y))$
42	41	ralbidva	$⊢ J \in TopOn (X) \to (\forall y \in X \{y\} \in Clsd (J) \leftrightarrow \forall y \in X \forall x \in X (\forall o \in J (x \in o \to y \in o) \to x = y))$
43		ralcom	$⊢ \forall y \in X \forall x \in X (\forall o \in J (x \in o \to y \in o) \to x = y) \leftrightarrow \forall x \in X \forall y \in X (\forall o \in J (x \in o \to y \in o) \to x = y)$
44	42 43	bitrdi	$⊢ J \in TopOn (X) \to (\forall y \in X \{y\} \in Clsd (J) \leftrightarrow \forall x \in X \forall y \in X (\forall o \in J (x \in o \to y \in o) \to x = y))$
45	5 7 44	3bitr2d	$⊢ J \in TopOn (X) \to (J \in Fre \leftrightarrow \forall x \in X \forall y \in X (\forall o \in J (x \in o \to y \in o) \to x = y))$

Metamath Proof Explorer

Theorem ist1-2

Proof