ist0cld

Description: The predicate "is a T_0 space", using closed sets. (Contributed by Thierry Arnoux, 16-Aug-2020)

	Ref	Expression
Hypotheses	ist0cls.1	$⊢ φ \to B = ⋃ J$
	ist0cls.2	$⊢ φ \to D = Clsd (J)$
Assertion	ist0cld	$⊢ φ \to (J \in Kol2 \leftrightarrow (J \in Top \land \forall x \in B \forall y \in B (\forall d \in D (x \in d \leftrightarrow y \in d) \to x = y)))$

Proof

Step	Hyp	Ref	Expression
1		ist0cls.1	$⊢ φ \to B = ⋃ J$
2		ist0cls.2	$⊢ φ \to D = Clsd (J)$
3		eqid	$⊢ ⋃ J = ⋃ J$
4	3	ist0	$⊢ J \in Kol2 \leftrightarrow (J \in Top \land \forall x \in ⋃ J \forall y \in ⋃ J (\forall o \in J (x \in o \leftrightarrow y \in o) \to x = y))$
5	4	simplbi	$⊢ J \in Kol2 \to J \in Top$
6	5	adantl	$⊢ (φ \land J \in Kol2) \to J \in Top$
7	4	baib	$⊢ J \in Top \to (J \in Kol2 \leftrightarrow \forall x \in ⋃ J \forall y \in ⋃ J (\forall o \in J (x \in o \leftrightarrow y \in o) \to x = y))$
8	7	adantl	$⊢ (φ \land J \in Top) \to (J \in Kol2 \leftrightarrow \forall x \in ⋃ J \forall y \in ⋃ J (\forall o \in J (x \in o \leftrightarrow y \in o) \to x = y))$
9	1	adantr	$⊢ (φ \land J \in Top) \to B = ⋃ J$
10	9	eqcomd	$⊢ (φ \land J \in Top) \to ⋃ J = B$
11	10	adantr	$⊢ ((φ \land J \in Top) \land x \in ⋃ J) \to ⋃ J = B$
12		simp-4r	$⊢ ((((φ \land J \in Top) \land x \in ⋃ J) \land y \in ⋃ J) \land o \in J) \to J \in Top$
13		uniexg	$⊢ J \in Top \to ⋃ J \in V$
14		difexg	$⊢ ⋃ J \in V \to ⋃ J ∖ o \in V$
15	12 13 14	3syl	$⊢ ((((φ \land J \in Top) \land x \in ⋃ J) \land y \in ⋃ J) \land o \in J) \to ⋃ J ∖ o \in V$
16	3	iscld	$⊢ J \in Top \to (d \in Clsd (J) \leftrightarrow (d \subseteq ⋃ J \land ⋃ J ∖ d \in J))$
17	16	adantl	$⊢ (φ \land J \in Top) \to (d \in Clsd (J) \leftrightarrow (d \subseteq ⋃ J \land ⋃ J ∖ d \in J))$
18	2	eleq2d	$⊢ φ \to (d \in D \leftrightarrow d \in Clsd (J))$
19	18	adantr	$⊢ (φ \land J \in Top) \to (d \in D \leftrightarrow d \in Clsd (J))$
20		simpr	$⊢ (((φ \land J \in Top) \land o \in J) \land d = ⋃ J ∖ o) \to d = ⋃ J ∖ o$
21		difssd	$⊢ (((φ \land J \in Top) \land o \in J) \land d = ⋃ J ∖ o) \to ⋃ J ∖ o \subseteq ⋃ J$
22	20 21	eqsstrd	$⊢ (((φ \land J \in Top) \land o \in J) \land d = ⋃ J ∖ o) \to d \subseteq ⋃ J$
23	22	r19.29an	$⊢ ((φ \land J \in Top) \land \exists o \in J d = ⋃ J ∖ o) \to d \subseteq ⋃ J$
24		simpr	$⊢ ((((φ \land J \in Top) \land d \subseteq ⋃ J) \land o \in J) \land d = ⋃ J ∖ o) \to d = ⋃ J ∖ o$
25	24	difeq2d	$⊢ ((((φ \land J \in Top) \land d \subseteq ⋃ J) \land o \in J) \land d = ⋃ J ∖ o) \to ⋃ J ∖ d = ⋃ J ∖ (⋃ J ∖ o)$
26	3	eltopss	$⊢ (J \in Top \land o \in J) \to o \subseteq ⋃ J$
27	26	ad5ant24	$⊢ ((((φ \land J \in Top) \land d \subseteq ⋃ J) \land o \in J) \land d = ⋃ J ∖ o) \to o \subseteq ⋃ J$
28		dfss4	$⊢ o \subseteq ⋃ J \leftrightarrow ⋃ J ∖ (⋃ J ∖ o) = o$
29	27 28	sylib	$⊢ ((((φ \land J \in Top) \land d \subseteq ⋃ J) \land o \in J) \land d = ⋃ J ∖ o) \to ⋃ J ∖ (⋃ J ∖ o) = o$
30		simplr	$⊢ ((((φ \land J \in Top) \land d \subseteq ⋃ J) \land o \in J) \land d = ⋃ J ∖ o) \to o \in J$
31	29 30	eqeltrd	$⊢ ((((φ \land J \in Top) \land d \subseteq ⋃ J) \land o \in J) \land d = ⋃ J ∖ o) \to ⋃ J ∖ (⋃ J ∖ o) \in J$
32	25 31	eqeltrd	$⊢ ((((φ \land J \in Top) \land d \subseteq ⋃ J) \land o \in J) \land d = ⋃ J ∖ o) \to ⋃ J ∖ d \in J$
33	32	r19.29an	$⊢ (((φ \land J \in Top) \land d \subseteq ⋃ J) \land \exists o \in J d = ⋃ J ∖ o) \to ⋃ J ∖ d \in J$
34		simpr	$⊢ (((φ \land J \in Top) \land d \subseteq ⋃ J) \land ⋃ J ∖ d \in J) \to ⋃ J ∖ d \in J$
35		simpr	$⊢ ((((φ \land J \in Top) \land d \subseteq ⋃ J) \land ⋃ J ∖ d \in J) \land o = ⋃ J ∖ d) \to o = ⋃ J ∖ d$
36	35	difeq2d	$⊢ ((((φ \land J \in Top) \land d \subseteq ⋃ J) \land ⋃ J ∖ d \in J) \land o = ⋃ J ∖ d) \to ⋃ J ∖ o = ⋃ J ∖ (⋃ J ∖ d)$
37	36	eqeq2d	$⊢ ((((φ \land J \in Top) \land d \subseteq ⋃ J) \land ⋃ J ∖ d \in J) \land o = ⋃ J ∖ d) \to (d = ⋃ J ∖ o \leftrightarrow d = ⋃ J ∖ (⋃ J ∖ d))$
38		simplr	$⊢ (((φ \land J \in Top) \land d \subseteq ⋃ J) \land ⋃ J ∖ d \in J) \to d \subseteq ⋃ J$
39		dfss4	$⊢ d \subseteq ⋃ J \leftrightarrow ⋃ J ∖ (⋃ J ∖ d) = d$
40	38 39	sylib	$⊢ (((φ \land J \in Top) \land d \subseteq ⋃ J) \land ⋃ J ∖ d \in J) \to ⋃ J ∖ (⋃ J ∖ d) = d$
41	40	eqcomd	$⊢ (((φ \land J \in Top) \land d \subseteq ⋃ J) \land ⋃ J ∖ d \in J) \to d = ⋃ J ∖ (⋃ J ∖ d)$
42	34 37 41	rspcedvd	$⊢ (((φ \land J \in Top) \land d \subseteq ⋃ J) \land ⋃ J ∖ d \in J) \to \exists o \in J d = ⋃ J ∖ o$
43	33 42	impbida	$⊢ ((φ \land J \in Top) \land d \subseteq ⋃ J) \to (\exists o \in J d = ⋃ J ∖ o \leftrightarrow ⋃ J ∖ d \in J)$
44	23 43	biadanid	$⊢ (φ \land J \in Top) \to (\exists o \in J d = ⋃ J ∖ o \leftrightarrow (d \subseteq ⋃ J \land ⋃ J ∖ d \in J))$
45	17 19 44	3bitr4d	$⊢ (φ \land J \in Top) \to (d \in D \leftrightarrow \exists o \in J d = ⋃ J ∖ o)$
46	45	ad2antrr	$⊢ (((φ \land J \in Top) \land x \in ⋃ J) \land y \in ⋃ J) \to (d \in D \leftrightarrow \exists o \in J d = ⋃ J ∖ o)$
47		simpr	$⊢ ((((φ \land J \in Top) \land x \in ⋃ J) \land y \in ⋃ J) \land d = ⋃ J ∖ o) \to d = ⋃ J ∖ o$
48	47	eleq2d	$⊢ ((((φ \land J \in Top) \land x \in ⋃ J) \land y \in ⋃ J) \land d = ⋃ J ∖ o) \to (x \in d \leftrightarrow x \in (⋃ J ∖ o))$
49		eldif	$⊢ x \in (⋃ J ∖ o) \leftrightarrow (x \in ⋃ J \land \neg x \in o)$
50	49	baib	$⊢ x \in ⋃ J \to (x \in (⋃ J ∖ o) \leftrightarrow \neg x \in o)$
51	50	ad3antlr	$⊢ ((((φ \land J \in Top) \land x \in ⋃ J) \land y \in ⋃ J) \land d = ⋃ J ∖ o) \to (x \in (⋃ J ∖ o) \leftrightarrow \neg x \in o)$
52	48 51	bitrd	$⊢ ((((φ \land J \in Top) \land x \in ⋃ J) \land y \in ⋃ J) \land d = ⋃ J ∖ o) \to (x \in d \leftrightarrow \neg x \in o)$
53	47	eleq2d	$⊢ ((((φ \land J \in Top) \land x \in ⋃ J) \land y \in ⋃ J) \land d = ⋃ J ∖ o) \to (y \in d \leftrightarrow y \in (⋃ J ∖ o))$
54		eldif	$⊢ y \in (⋃ J ∖ o) \leftrightarrow (y \in ⋃ J \land \neg y \in o)$
55	54	baib	$⊢ y \in ⋃ J \to (y \in (⋃ J ∖ o) \leftrightarrow \neg y \in o)$
56	55	ad2antlr	$⊢ ((((φ \land J \in Top) \land x \in ⋃ J) \land y \in ⋃ J) \land d = ⋃ J ∖ o) \to (y \in (⋃ J ∖ o) \leftrightarrow \neg y \in o)$
57	53 56	bitrd	$⊢ ((((φ \land J \in Top) \land x \in ⋃ J) \land y \in ⋃ J) \land d = ⋃ J ∖ o) \to (y \in d \leftrightarrow \neg y \in o)$
58	52 57	bibi12d	$⊢ ((((φ \land J \in Top) \land x \in ⋃ J) \land y \in ⋃ J) \land d = ⋃ J ∖ o) \to ((x \in d \leftrightarrow y \in d) \leftrightarrow (\neg x \in o \leftrightarrow \neg y \in o))$
59		notbi	$⊢ (x \in o \leftrightarrow y \in o) \leftrightarrow (\neg x \in o \leftrightarrow \neg y \in o)$
60	58 59	bitr4di	$⊢ ((((φ \land J \in Top) \land x \in ⋃ J) \land y \in ⋃ J) \land d = ⋃ J ∖ o) \to ((x \in d \leftrightarrow y \in d) \leftrightarrow (x \in o \leftrightarrow y \in o))$
61	15 46 60	ralxfr2d	$⊢ (((φ \land J \in Top) \land x \in ⋃ J) \land y \in ⋃ J) \to (\forall d \in D (x \in d \leftrightarrow y \in d) \leftrightarrow \forall o \in J (x \in o \leftrightarrow y \in o))$
62	61	bicomd	$⊢ (((φ \land J \in Top) \land x \in ⋃ J) \land y \in ⋃ J) \to (\forall o \in J (x \in o \leftrightarrow y \in o) \leftrightarrow \forall d \in D (x \in d \leftrightarrow y \in d))$
63	62	imbi1d	$⊢ (((φ \land J \in Top) \land x \in ⋃ J) \land y \in ⋃ J) \to ((\forall o \in J (x \in o \leftrightarrow y \in o) \to x = y) \leftrightarrow (\forall d \in D (x \in d \leftrightarrow y \in d) \to x = y))$
64	11 63	raleqbidva	$⊢ ((φ \land J \in Top) \land x \in ⋃ J) \to (\forall y \in ⋃ J (\forall o \in J (x \in o \leftrightarrow y \in o) \to x = y) \leftrightarrow \forall y \in B (\forall d \in D (x \in d \leftrightarrow y \in d) \to x = y))$
65	10 64	raleqbidva	$⊢ (φ \land J \in Top) \to (\forall x \in ⋃ J \forall y \in ⋃ J (\forall o \in J (x \in o \leftrightarrow y \in o) \to x = y) \leftrightarrow \forall x \in B \forall y \in B (\forall d \in D (x \in d \leftrightarrow y \in d) \to x = y))$
66	8 65	bitrd	$⊢ (φ \land J \in Top) \to (J \in Kol2 \leftrightarrow \forall x \in B \forall y \in B (\forall d \in D (x \in d \leftrightarrow y \in d) \to x = y))$
67	6 66	biadanid	$⊢ φ \to (J \in Kol2 \leftrightarrow (J \in Top \land \forall x \in B \forall y \in B (\forall d \in D (x \in d \leftrightarrow y \in d) \to x = y)))$

Metamath Proof Explorer

Theorem ist0cld

Proof