kqcldsat

Description: Any closed set is saturated with respect to the topological indistinguishability map (in the terminology of qtoprest ). (Contributed by Mario Carneiro, 25-Aug-2015)

		Ref	Expression
	Hypothesis	kqval.2	$⊢ F = (x \in X ⟼ \{y \in J \| x \in y\})$
	Assertion	kqcldsat	$⊢ (J \in TopOn (X) \land U \in Clsd (J)) \to F^{-1} [F [U]] = U$

Proof

Step	Hyp	Ref	Expression
1		kqval.2	$⊢ F = (x \in X ⟼ \{y \in J \| x \in y\})$
2	1	kqffn	$⊢ J \in TopOn (X) \to F Fn X$
3		elpreima	$⊢ F Fn X \to (z \in F^{-1} [F [U]] \leftrightarrow (z \in X \land F (z) \in F [U]))$
4	2 3	syl	$⊢ J \in TopOn (X) \to (z \in F^{-1} [F [U]] \leftrightarrow (z \in X \land F (z) \in F [U]))$
5	4	adantr	$⊢ (J \in TopOn (X) \land U \in Clsd (J)) \to (z \in F^{-1} [F [U]] \leftrightarrow (z \in X \land F (z) \in F [U]))$
6		noel	$⊢ \neg F (z) \in \emptyset$
7		elin	$⊢ F (z) \in (F [U] \cap F [X ∖ U]) \leftrightarrow (F (z) \in F [U] \land F (z) \in F [X ∖ U])$
8		incom	$⊢ F [U] \cap F [X ∖ U] = F [X ∖ U] \cap F [U]$
9		eqid	$⊢ ⋃ J = ⋃ J$
10	9	cldss	$⊢ U \in Clsd (J) \to U \subseteq ⋃ J$
11	10	adantl	$⊢ (J \in TopOn (X) \land U \in Clsd (J)) \to U \subseteq ⋃ J$
12		fndm	$⊢ F Fn X \to dom F = X$
13	2 12	syl	$⊢ J \in TopOn (X) \to dom F = X$
14		toponuni	$⊢ J \in TopOn (X) \to X = ⋃ J$
15	13 14	eqtrd	$⊢ J \in TopOn (X) \to dom F = ⋃ J$
16	15	adantr	$⊢ (J \in TopOn (X) \land U \in Clsd (J)) \to dom F = ⋃ J$
17	11 16	sseqtrrd	$⊢ (J \in TopOn (X) \land U \in Clsd (J)) \to U \subseteq dom F$
18	13	adantr	$⊢ (J \in TopOn (X) \land U \in Clsd (J)) \to dom F = X$
19	17 18	sseqtrd	$⊢ (J \in TopOn (X) \land U \in Clsd (J)) \to U \subseteq X$
20	19	adantr	$⊢ ((J \in TopOn (X) \land U \in Clsd (J)) \land z \in X) \to U \subseteq X$
21		dfss4	$⊢ U \subseteq X \leftrightarrow X ∖ (X ∖ U) = U$
22	20 21	sylib	$⊢ ((J \in TopOn (X) \land U \in Clsd (J)) \land z \in X) \to X ∖ (X ∖ U) = U$
23	22	imaeq2d	$⊢ ((J \in TopOn (X) \land U \in Clsd (J)) \land z \in X) \to F [X ∖ (X ∖ U)] = F [U]$
24	23	ineq2d	$⊢ ((J \in TopOn (X) \land U \in Clsd (J)) \land z \in X) \to F [X ∖ U] \cap F [X ∖ (X ∖ U)] = F [X ∖ U] \cap F [U]$
25		simpll	$⊢ ((J \in TopOn (X) \land U \in Clsd (J)) \land z \in X) \to J \in TopOn (X)$
26	14	adantr	$⊢ (J \in TopOn (X) \land U \in Clsd (J)) \to X = ⋃ J$
27	26	difeq1d	$⊢ (J \in TopOn (X) \land U \in Clsd (J)) \to X ∖ U = ⋃ J ∖ U$
28	9	cldopn	$⊢ U \in Clsd (J) \to ⋃ J ∖ U \in J$
29	28	adantl	$⊢ (J \in TopOn (X) \land U \in Clsd (J)) \to ⋃ J ∖ U \in J$
30	27 29	eqeltrd	$⊢ (J \in TopOn (X) \land U \in Clsd (J)) \to X ∖ U \in J$
31	30	adantr	$⊢ ((J \in TopOn (X) \land U \in Clsd (J)) \land z \in X) \to X ∖ U \in J$
32	1	kqdisj	$⊢ (J \in TopOn (X) \land X ∖ U \in J) \to F [X ∖ U] \cap F [X ∖ (X ∖ U)] = \emptyset$
33	25 31 32	syl2anc	$⊢ ((J \in TopOn (X) \land U \in Clsd (J)) \land z \in X) \to F [X ∖ U] \cap F [X ∖ (X ∖ U)] = \emptyset$
34	24 33	eqtr3d	$⊢ ((J \in TopOn (X) \land U \in Clsd (J)) \land z \in X) \to F [X ∖ U] \cap F [U] = \emptyset$
35	8 34	syl5eq	$⊢ ((J \in TopOn (X) \land U \in Clsd (J)) \land z \in X) \to F [U] \cap F [X ∖ U] = \emptyset$
36	35	eleq2d	$⊢ ((J \in TopOn (X) \land U \in Clsd (J)) \land z \in X) \to (F (z) \in (F [U] \cap F [X ∖ U]) \leftrightarrow F (z) \in \emptyset)$
37	7 36	bitr3id	$⊢ ((J \in TopOn (X) \land U \in Clsd (J)) \land z \in X) \to ((F (z) \in F [U] \land F (z) \in F [X ∖ U]) \leftrightarrow F (z) \in \emptyset)$
38	6 37	mtbiri	$⊢ ((J \in TopOn (X) \land U \in Clsd (J)) \land z \in X) \to \neg (F (z) \in F [U] \land F (z) \in F [X ∖ U])$
39		imnan	$⊢ (F (z) \in F [U] \to \neg F (z) \in F [X ∖ U]) \leftrightarrow \neg (F (z) \in F [U] \land F (z) \in F [X ∖ U])$
40	38 39	sylibr	$⊢ ((J \in TopOn (X) \land U \in Clsd (J)) \land z \in X) \to (F (z) \in F [U] \to \neg F (z) \in F [X ∖ U])$
41		eldif	$⊢ z \in (X ∖ U) \leftrightarrow (z \in X \land \neg z \in U)$
42	41	baibr	$⊢ z \in X \to (\neg z \in U \leftrightarrow z \in (X ∖ U))$
43	42	adantl	$⊢ ((J \in TopOn (X) \land U \in Clsd (J)) \land z \in X) \to (\neg z \in U \leftrightarrow z \in (X ∖ U))$
44		simpr	$⊢ ((J \in TopOn (X) \land U \in Clsd (J)) \land z \in X) \to z \in X$
45	1	kqfvima	$⊢ (J \in TopOn (X) \land X ∖ U \in J \land z \in X) \to (z \in (X ∖ U) \leftrightarrow F (z) \in F [X ∖ U])$
46	25 31 44 45	syl3anc	$⊢ ((J \in TopOn (X) \land U \in Clsd (J)) \land z \in X) \to (z \in (X ∖ U) \leftrightarrow F (z) \in F [X ∖ U])$
47	43 46	bitrd	$⊢ ((J \in TopOn (X) \land U \in Clsd (J)) \land z \in X) \to (\neg z \in U \leftrightarrow F (z) \in F [X ∖ U])$
48	47	con1bid	$⊢ ((J \in TopOn (X) \land U \in Clsd (J)) \land z \in X) \to (\neg F (z) \in F [X ∖ U] \leftrightarrow z \in U)$
49	40 48	sylibd	$⊢ ((J \in TopOn (X) \land U \in Clsd (J)) \land z \in X) \to (F (z) \in F [U] \to z \in U)$
50	49	expimpd	$⊢ (J \in TopOn (X) \land U \in Clsd (J)) \to ((z \in X \land F (z) \in F [U]) \to z \in U)$
51	5 50	sylbid	$⊢ (J \in TopOn (X) \land U \in Clsd (J)) \to (z \in F^{-1} [F [U]] \to z \in U)$
52	51	ssrdv	$⊢ (J \in TopOn (X) \land U \in Clsd (J)) \to F^{-1} [F [U]] \subseteq U$
53		sseqin2	$⊢ U \subseteq dom F \leftrightarrow dom F \cap U = U$
54	17 53	sylib	$⊢ (J \in TopOn (X) \land U \in Clsd (J)) \to dom F \cap U = U$
55		dminss	$⊢ dom F \cap U \subseteq F^{-1} [F [U]]$
56	54 55	eqsstrrdi	$⊢ (J \in TopOn (X) \land U \in Clsd (J)) \to U \subseteq F^{-1} [F [U]]$
57	52 56	eqssd	$⊢ (J \in TopOn (X) \land U \in Clsd (J)) \to F^{-1} [F [U]] = U$

Metamath Proof Explorer

Theorem kqcldsat

Proof