isr0

Description: The property " J is an R_0 space". A space is R_0 if any two topologically distinguishable points are separated (there is an open set containing each one and disjoint from the other). Or in contraposition, if every open set which contains x also contains y , so there is no separation, then x and y are members of the same open sets. We have chosen not to give this definition a name, because it turns out that a space is R_0 if and only if its Kolmogorov quotient is T_1, so that is what we prove here. (Contributed by Mario Carneiro, 25-Aug-2015)

		Ref	Expression
	Hypothesis	kqval.2	$⊢ F = (x \in X ⟼ \{y \in J \| x \in y\})$
	Assertion	isr0	$⊢ J \in TopOn (X) \to (KQ (J) \in Fre \leftrightarrow \forall z \in X \forall w \in X (\forall o \in J (z \in o \to w \in o) \to \forall o \in J (z \in o \leftrightarrow w \in o)))$

Proof

Step	Hyp	Ref	Expression
1		kqval.2	$⊢ F = (x \in X ⟼ \{y \in J \| x \in y\})$
2	1	kqid	$⊢ J \in TopOn (X) \to F \in (J Cn KQ (J))$
3	2	ad2antrr	$⊢ ((J \in TopOn (X) \land KQ (J) \in Fre) \land (z \in X \land w \in X)) \to F \in (J Cn KQ (J))$
4		cnima	$⊢ (F \in (J Cn KQ (J)) \land v \in KQ (J)) \to F^{-1} [v] \in J$
5	3 4	sylan	$⊢ (((J \in TopOn (X) \land KQ (J) \in Fre) \land (z \in X \land w \in X)) \land v \in KQ (J)) \to F^{-1} [v] \in J$
6		eleq2	$⊢ o = F^{-1} [v] \to (z \in o \leftrightarrow z \in F^{-1} [v])$
7		eleq2	$⊢ o = F^{-1} [v] \to (w \in o \leftrightarrow w \in F^{-1} [v])$
8	6 7	imbi12d	$⊢ o = F^{-1} [v] \to ((z \in o \to w \in o) \leftrightarrow (z \in F^{-1} [v] \to w \in F^{-1} [v]))$
9	8	rspcv	$⊢ F^{-1} [v] \in J \to (\forall o \in J (z \in o \to w \in o) \to (z \in F^{-1} [v] \to w \in F^{-1} [v]))$
10	5 9	syl	$⊢ (((J \in TopOn (X) \land KQ (J) \in Fre) \land (z \in X \land w \in X)) \land v \in KQ (J)) \to (\forall o \in J (z \in o \to w \in o) \to (z \in F^{-1} [v] \to w \in F^{-1} [v]))$
11	1	kqffn	$⊢ J \in TopOn (X) \to F Fn X$
12	11	ad2antrr	$⊢ ((J \in TopOn (X) \land KQ (J) \in Fre) \land (z \in X \land w \in X)) \to F Fn X$
13	12	adantr	$⊢ (((J \in TopOn (X) \land KQ (J) \in Fre) \land (z \in X \land w \in X)) \land v \in KQ (J)) \to F Fn X$
14		fnfun	$⊢ F Fn X \to Fun F$
15	13 14	syl	$⊢ (((J \in TopOn (X) \land KQ (J) \in Fre) \land (z \in X \land w \in X)) \land v \in KQ (J)) \to Fun F$
16		simprl	$⊢ ((J \in TopOn (X) \land KQ (J) \in Fre) \land (z \in X \land w \in X)) \to z \in X$
17	16	adantr	$⊢ (((J \in TopOn (X) \land KQ (J) \in Fre) \land (z \in X \land w \in X)) \land v \in KQ (J)) \to z \in X$
18	13	fndmd	$⊢ (((J \in TopOn (X) \land KQ (J) \in Fre) \land (z \in X \land w \in X)) \land v \in KQ (J)) \to dom F = X$
19	17 18	eleqtrrd	$⊢ (((J \in TopOn (X) \land KQ (J) \in Fre) \land (z \in X \land w \in X)) \land v \in KQ (J)) \to z \in dom F$
20		fvimacnv	$⊢ (Fun F \land z \in dom F) \to (F (z) \in v \leftrightarrow z \in F^{-1} [v])$
21	15 19 20	syl2anc	$⊢ (((J \in TopOn (X) \land KQ (J) \in Fre) \land (z \in X \land w \in X)) \land v \in KQ (J)) \to (F (z) \in v \leftrightarrow z \in F^{-1} [v])$
22		simprr	$⊢ ((J \in TopOn (X) \land KQ (J) \in Fre) \land (z \in X \land w \in X)) \to w \in X$
23	22	adantr	$⊢ (((J \in TopOn (X) \land KQ (J) \in Fre) \land (z \in X \land w \in X)) \land v \in KQ (J)) \to w \in X$
24	23 18	eleqtrrd	$⊢ (((J \in TopOn (X) \land KQ (J) \in Fre) \land (z \in X \land w \in X)) \land v \in KQ (J)) \to w \in dom F$
25		fvimacnv	$⊢ (Fun F \land w \in dom F) \to (F (w) \in v \leftrightarrow w \in F^{-1} [v])$
26	15 24 25	syl2anc	$⊢ (((J \in TopOn (X) \land KQ (J) \in Fre) \land (z \in X \land w \in X)) \land v \in KQ (J)) \to (F (w) \in v \leftrightarrow w \in F^{-1} [v])$
27	21 26	imbi12d	$⊢ (((J \in TopOn (X) \land KQ (J) \in Fre) \land (z \in X \land w \in X)) \land v \in KQ (J)) \to ((F (z) \in v \to F (w) \in v) \leftrightarrow (z \in F^{-1} [v] \to w \in F^{-1} [v]))$
28	10 27	sylibrd	$⊢ (((J \in TopOn (X) \land KQ (J) \in Fre) \land (z \in X \land w \in X)) \land v \in KQ (J)) \to (\forall o \in J (z \in o \to w \in o) \to (F (z) \in v \to F (w) \in v))$
29	28	ralrimdva	$⊢ ((J \in TopOn (X) \land KQ (J) \in Fre) \land (z \in X \land w \in X)) \to (\forall o \in J (z \in o \to w \in o) \to \forall v \in KQ (J) (F (z) \in v \to F (w) \in v))$
30		simplr	$⊢ ((J \in TopOn (X) \land KQ (J) \in Fre) \land (z \in X \land w \in X)) \to KQ (J) \in Fre$
31		fnfvelrn	$⊢ (F Fn X \land z \in X) \to F (z) \in ran F$
32	12 16 31	syl2anc	$⊢ ((J \in TopOn (X) \land KQ (J) \in Fre) \land (z \in X \land w \in X)) \to F (z) \in ran F$
33	1	kqtopon	$⊢ J \in TopOn (X) \to KQ (J) \in TopOn (ran F)$
34	33	ad2antrr	$⊢ ((J \in TopOn (X) \land KQ (J) \in Fre) \land (z \in X \land w \in X)) \to KQ (J) \in TopOn (ran F)$
35		toponuni	$⊢ KQ (J) \in TopOn (ran F) \to ran F = ⋃ KQ (J)$
36	34 35	syl	$⊢ ((J \in TopOn (X) \land KQ (J) \in Fre) \land (z \in X \land w \in X)) \to ran F = ⋃ KQ (J)$
37	32 36	eleqtrd	$⊢ ((J \in TopOn (X) \land KQ (J) \in Fre) \land (z \in X \land w \in X)) \to F (z) \in ⋃ KQ (J)$
38		fnfvelrn	$⊢ (F Fn X \land w \in X) \to F (w) \in ran F$
39	12 22 38	syl2anc	$⊢ ((J \in TopOn (X) \land KQ (J) \in Fre) \land (z \in X \land w \in X)) \to F (w) \in ran F$
40	39 36	eleqtrd	$⊢ ((J \in TopOn (X) \land KQ (J) \in Fre) \land (z \in X \land w \in X)) \to F (w) \in ⋃ KQ (J)$
41		eqid	$⊢ ⋃ KQ (J) = ⋃ KQ (J)$
42	41	t1sep2	$⊢ (KQ (J) \in Fre \land F (z) \in ⋃ KQ (J) \land F (w) \in ⋃ KQ (J)) \to (\forall v \in KQ (J) (F (z) \in v \to F (w) \in v) \to F (z) = F (w))$
43	30 37 40 42	syl3anc	$⊢ ((J \in TopOn (X) \land KQ (J) \in Fre) \land (z \in X \land w \in X)) \to (\forall v \in KQ (J) (F (z) \in v \to F (w) \in v) \to F (z) = F (w))$
44	29 43	syld	$⊢ ((J \in TopOn (X) \land KQ (J) \in Fre) \land (z \in X \land w \in X)) \to (\forall o \in J (z \in o \to w \in o) \to F (z) = F (w))$
45	1	kqfeq	$⊢ (J \in TopOn (X) \land z \in X \land w \in X) \to (F (z) = F (w) \leftrightarrow \forall y \in J (z \in y \leftrightarrow w \in y))$
46		eleq2	$⊢ o = y \to (z \in o \leftrightarrow z \in y)$
47		eleq2	$⊢ o = y \to (w \in o \leftrightarrow w \in y)$
48	46 47	bibi12d	$⊢ o = y \to ((z \in o \leftrightarrow w \in o) \leftrightarrow (z \in y \leftrightarrow w \in y))$
49	48	cbvralvw	$⊢ \forall o \in J (z \in o \leftrightarrow w \in o) \leftrightarrow \forall y \in J (z \in y \leftrightarrow w \in y)$
50	45 49	bitr4di	$⊢ (J \in TopOn (X) \land z \in X \land w \in X) \to (F (z) = F (w) \leftrightarrow \forall o \in J (z \in o \leftrightarrow w \in o))$
51	50	3expb	$⊢ (J \in TopOn (X) \land (z \in X \land w \in X)) \to (F (z) = F (w) \leftrightarrow \forall o \in J (z \in o \leftrightarrow w \in o))$
52	51	adantlr	$⊢ ((J \in TopOn (X) \land KQ (J) \in Fre) \land (z \in X \land w \in X)) \to (F (z) = F (w) \leftrightarrow \forall o \in J (z \in o \leftrightarrow w \in o))$
53	44 52	sylibd	$⊢ ((J \in TopOn (X) \land KQ (J) \in Fre) \land (z \in X \land w \in X)) \to (\forall o \in J (z \in o \to w \in o) \to \forall o \in J (z \in o \leftrightarrow w \in o))$
54	53	ralrimivva	$⊢ (J \in TopOn (X) \land KQ (J) \in Fre) \to \forall z \in X \forall w \in X (\forall o \in J (z \in o \to w \in o) \to \forall o \in J (z \in o \leftrightarrow w \in o))$
55	54	ex	$⊢ J \in TopOn (X) \to (KQ (J) \in Fre \to \forall z \in X \forall w \in X (\forall o \in J (z \in o \to w \in o) \to \forall o \in J (z \in o \leftrightarrow w \in o)))$
56	1	kqopn	$⊢ (J \in TopOn (X) \land o \in J) \to F [o] \in KQ (J)$
57	56	ad4ant14	$⊢ (((J \in TopOn (X) \land z \in X) \land w \in X) \land o \in J) \to F [o] \in KQ (J)$
58		eleq2	$⊢ v = F [o] \to (F (z) \in v \leftrightarrow F (z) \in F [o])$
59		eleq2	$⊢ v = F [o] \to (F (w) \in v \leftrightarrow F (w) \in F [o])$
60	58 59	imbi12d	$⊢ v = F [o] \to ((F (z) \in v \to F (w) \in v) \leftrightarrow (F (z) \in F [o] \to F (w) \in F [o]))$
61	60	rspcv	$⊢ F [o] \in KQ (J) \to (\forall v \in KQ (J) (F (z) \in v \to F (w) \in v) \to (F (z) \in F [o] \to F (w) \in F [o]))$
62	57 61	syl	$⊢ (((J \in TopOn (X) \land z \in X) \land w \in X) \land o \in J) \to (\forall v \in KQ (J) (F (z) \in v \to F (w) \in v) \to (F (z) \in F [o] \to F (w) \in F [o]))$
63	1	kqfvima	$⊢ (J \in TopOn (X) \land o \in J \land z \in X) \to (z \in o \leftrightarrow F (z) \in F [o])$
64	63	3expa	$⊢ ((J \in TopOn (X) \land o \in J) \land z \in X) \to (z \in o \leftrightarrow F (z) \in F [o])$
65	64	an32s	$⊢ ((J \in TopOn (X) \land z \in X) \land o \in J) \to (z \in o \leftrightarrow F (z) \in F [o])$
66	65	adantlr	$⊢ (((J \in TopOn (X) \land z \in X) \land w \in X) \land o \in J) \to (z \in o \leftrightarrow F (z) \in F [o])$
67	1	kqfvima	$⊢ (J \in TopOn (X) \land o \in J \land w \in X) \to (w \in o \leftrightarrow F (w) \in F [o])$
68	67	3expa	$⊢ ((J \in TopOn (X) \land o \in J) \land w \in X) \to (w \in o \leftrightarrow F (w) \in F [o])$
69	68	an32s	$⊢ ((J \in TopOn (X) \land w \in X) \land o \in J) \to (w \in o \leftrightarrow F (w) \in F [o])$
70	69	adantllr	$⊢ (((J \in TopOn (X) \land z \in X) \land w \in X) \land o \in J) \to (w \in o \leftrightarrow F (w) \in F [o])$
71	66 70	imbi12d	$⊢ (((J \in TopOn (X) \land z \in X) \land w \in X) \land o \in J) \to ((z \in o \to w \in o) \leftrightarrow (F (z) \in F [o] \to F (w) \in F [o]))$
72	62 71	sylibrd	$⊢ (((J \in TopOn (X) \land z \in X) \land w \in X) \land o \in J) \to (\forall v \in KQ (J) (F (z) \in v \to F (w) \in v) \to (z \in o \to w \in o))$
73	72	ralrimdva	$⊢ ((J \in TopOn (X) \land z \in X) \land w \in X) \to (\forall v \in KQ (J) (F (z) \in v \to F (w) \in v) \to \forall o \in J (z \in o \to w \in o))$
74	1	kqfval	$⊢ (J \in TopOn (X) \land z \in X) \to F (z) = \{y \in J \| z \in y\}$
75	74	adantr	$⊢ ((J \in TopOn (X) \land z \in X) \land w \in X) \to F (z) = \{y \in J \| z \in y\}$
76	1	kqfval	$⊢ (J \in TopOn (X) \land w \in X) \to F (w) = \{y \in J \| w \in y\}$
77	76	adantlr	$⊢ ((J \in TopOn (X) \land z \in X) \land w \in X) \to F (w) = \{y \in J \| w \in y\}$
78	75 77	eqeq12d	$⊢ ((J \in TopOn (X) \land z \in X) \land w \in X) \to (F (z) = F (w) \leftrightarrow \{y \in J \| z \in y\} = \{y \in J \| w \in y\})$
79		rabbi	$⊢ \forall y \in J (z \in y \leftrightarrow w \in y) \leftrightarrow \{y \in J \| z \in y\} = \{y \in J \| w \in y\}$
80	49 79	bitri	$⊢ \forall o \in J (z \in o \leftrightarrow w \in o) \leftrightarrow \{y \in J \| z \in y\} = \{y \in J \| w \in y\}$
81	78 80	bitr4di	$⊢ ((J \in TopOn (X) \land z \in X) \land w \in X) \to (F (z) = F (w) \leftrightarrow \forall o \in J (z \in o \leftrightarrow w \in o))$
82	81	biimprd	$⊢ ((J \in TopOn (X) \land z \in X) \land w \in X) \to (\forall o \in J (z \in o \leftrightarrow w \in o) \to F (z) = F (w))$
83	73 82	imim12d	$⊢ ((J \in TopOn (X) \land z \in X) \land w \in X) \to ((\forall o \in J (z \in o \to w \in o) \to \forall o \in J (z \in o \leftrightarrow w \in o)) \to (\forall v \in KQ (J) (F (z) \in v \to F (w) \in v) \to F (z) = F (w)))$
84	83	ralimdva	$⊢ (J \in TopOn (X) \land z \in X) \to (\forall w \in X (\forall o \in J (z \in o \to w \in o) \to \forall o \in J (z \in o \leftrightarrow w \in o)) \to \forall w \in X (\forall v \in KQ (J) (F (z) \in v \to F (w) \in v) \to F (z) = F (w)))$
85	84	ralimdva	$⊢ J \in TopOn (X) \to (\forall z \in X \forall w \in X (\forall o \in J (z \in o \to w \in o) \to \forall o \in J (z \in o \leftrightarrow w \in o)) \to \forall z \in X \forall w \in X (\forall v \in KQ (J) (F (z) \in v \to F (w) \in v) \to F (z) = F (w)))$
86		eleq1	$⊢ a = F (z) \to (a \in v \leftrightarrow F (z) \in v)$
87	86	imbi1d	$⊢ a = F (z) \to ((a \in v \to b \in v) \leftrightarrow (F (z) \in v \to b \in v))$
88	87	ralbidv	$⊢ a = F (z) \to (\forall v \in KQ (J) (a \in v \to b \in v) \leftrightarrow \forall v \in KQ (J) (F (z) \in v \to b \in v))$
89		eqeq1	$⊢ a = F (z) \to (a = b \leftrightarrow F (z) = b)$
90	88 89	imbi12d	$⊢ a = F (z) \to ((\forall v \in KQ (J) (a \in v \to b \in v) \to a = b) \leftrightarrow (\forall v \in KQ (J) (F (z) \in v \to b \in v) \to F (z) = b))$
91	90	ralbidv	$⊢ a = F (z) \to (\forall b \in ran F (\forall v \in KQ (J) (a \in v \to b \in v) \to a = b) \leftrightarrow \forall b \in ran F (\forall v \in KQ (J) (F (z) \in v \to b \in v) \to F (z) = b))$
92	91	ralrn	$⊢ F Fn X \to (\forall a \in ran F \forall b \in ran F (\forall v \in KQ (J) (a \in v \to b \in v) \to a = b) \leftrightarrow \forall z \in X \forall b \in ran F (\forall v \in KQ (J) (F (z) \in v \to b \in v) \to F (z) = b))$
93		eleq1	$⊢ b = F (w) \to (b \in v \leftrightarrow F (w) \in v)$
94	93	imbi2d	$⊢ b = F (w) \to ((F (z) \in v \to b \in v) \leftrightarrow (F (z) \in v \to F (w) \in v))$
95	94	ralbidv	$⊢ b = F (w) \to (\forall v \in KQ (J) (F (z) \in v \to b \in v) \leftrightarrow \forall v \in KQ (J) (F (z) \in v \to F (w) \in v))$
96		eqeq2	$⊢ b = F (w) \to (F (z) = b \leftrightarrow F (z) = F (w))$
97	95 96	imbi12d	$⊢ b = F (w) \to ((\forall v \in KQ (J) (F (z) \in v \to b \in v) \to F (z) = b) \leftrightarrow (\forall v \in KQ (J) (F (z) \in v \to F (w) \in v) \to F (z) = F (w)))$
98	97	ralrn	$⊢ F Fn X \to (\forall b \in ran F (\forall v \in KQ (J) (F (z) \in v \to b \in v) \to F (z) = b) \leftrightarrow \forall w \in X (\forall v \in KQ (J) (F (z) \in v \to F (w) \in v) \to F (z) = F (w)))$
99	98	ralbidv	$⊢ F Fn X \to (\forall z \in X \forall b \in ran F (\forall v \in KQ (J) (F (z) \in v \to b \in v) \to F (z) = b) \leftrightarrow \forall z \in X \forall w \in X (\forall v \in KQ (J) (F (z) \in v \to F (w) \in v) \to F (z) = F (w)))$
100	92 99	bitrd	$⊢ F Fn X \to (\forall a \in ran F \forall b \in ran F (\forall v \in KQ (J) (a \in v \to b \in v) \to a = b) \leftrightarrow \forall z \in X \forall w \in X (\forall v \in KQ (J) (F (z) \in v \to F (w) \in v) \to F (z) = F (w)))$
101	11 100	syl	$⊢ J \in TopOn (X) \to (\forall a \in ran F \forall b \in ran F (\forall v \in KQ (J) (a \in v \to b \in v) \to a = b) \leftrightarrow \forall z \in X \forall w \in X (\forall v \in KQ (J) (F (z) \in v \to F (w) \in v) \to F (z) = F (w)))$
102	85 101	sylibrd	$⊢ J \in TopOn (X) \to (\forall z \in X \forall w \in X (\forall o \in J (z \in o \to w \in o) \to \forall o \in J (z \in o \leftrightarrow w \in o)) \to \forall a \in ran F \forall b \in ran F (\forall v \in KQ (J) (a \in v \to b \in v) \to a = b))$
103		ist1-2	$⊢ KQ (J) \in TopOn (ran F) \to (KQ (J) \in Fre \leftrightarrow \forall a \in ran F \forall b \in ran F (\forall v \in KQ (J) (a \in v \to b \in v) \to a = b))$
104	33 103	syl	$⊢ J \in TopOn (X) \to (KQ (J) \in Fre \leftrightarrow \forall a \in ran F \forall b \in ran F (\forall v \in KQ (J) (a \in v \to b \in v) \to a = b))$
105	102 104	sylibrd	$⊢ J \in TopOn (X) \to (\forall z \in X \forall w \in X (\forall o \in J (z \in o \to w \in o) \to \forall o \in J (z \in o \leftrightarrow w \in o)) \to KQ (J) \in Fre)$
106	55 105	impbid	$⊢ J \in TopOn (X) \to (KQ (J) \in Fre \leftrightarrow \forall z \in X \forall w \in X (\forall o \in J (z \in o \to w \in o) \to \forall o \in J (z \in o \leftrightarrow w \in o)))$

Metamath Proof Explorer

Theorem isr0

Proof