istopclsd

Description: A closure function which satisfies sscls , clsidm , cls0 , and clsun defines a (unique) topology which it is the closure function on. (Contributed by Stefan O'Rear, 1-Feb-2015)

	Ref	Expression
Hypotheses	istopclsd.b	$⊢ φ \to B \in V$
	istopclsd.f	$⊢ φ \to F : 𝒫 B ⟶ 𝒫 B$
	istopclsd.e	$⊢ (φ \land x \subseteq B) \to x \subseteq F (x)$
	istopclsd.i	$⊢ (φ \land x \subseteq B) \to F (F (x)) = F (x)$
	istopclsd.z	$⊢ φ \to F (\emptyset) = \emptyset$
	istopclsd.u	$⊢ (φ \land x \subseteq B \land y \subseteq B) \to F (x \cup y) = F (x) \cup F (y)$
	istopclsd.j	$⊢ J = \{z \in 𝒫 B \| F (B ∖ z) = B ∖ z\}$
Assertion	istopclsd	$⊢ φ \to (J \in TopOn (B) \land cls (J) = F)$

Proof

Step	Hyp	Ref	Expression
1		istopclsd.b	$⊢ φ \to B \in V$
2		istopclsd.f	$⊢ φ \to F : 𝒫 B ⟶ 𝒫 B$
3		istopclsd.e	$⊢ (φ \land x \subseteq B) \to x \subseteq F (x)$
4		istopclsd.i	$⊢ (φ \land x \subseteq B) \to F (F (x)) = F (x)$
5		istopclsd.z	$⊢ φ \to F (\emptyset) = \emptyset$
6		istopclsd.u	$⊢ (φ \land x \subseteq B \land y \subseteq B) \to F (x \cup y) = F (x) \cup F (y)$
7		istopclsd.j	$⊢ J = \{z \in 𝒫 B \| F (B ∖ z) = B ∖ z\}$
8	2	ffnd	$⊢ φ \to F Fn 𝒫 B$
9	8	adantr	$⊢ (φ \land z \in 𝒫 B) \to F Fn 𝒫 B$
10		difss	$⊢ B ∖ z \subseteq B$
11		elpw2g	$⊢ B \in V \to (B ∖ z \in 𝒫 B \leftrightarrow B ∖ z \subseteq B)$
12	1 11	syl	$⊢ φ \to (B ∖ z \in 𝒫 B \leftrightarrow B ∖ z \subseteq B)$
13	10 12	mpbiri	$⊢ φ \to B ∖ z \in 𝒫 B$
14	13	adantr	$⊢ (φ \land z \in 𝒫 B) \to B ∖ z \in 𝒫 B$
15		fnelfp	$⊢ (F Fn 𝒫 B \land B ∖ z \in 𝒫 B) \to (B ∖ z \in dom (F \cap I) \leftrightarrow F (B ∖ z) = B ∖ z)$
16	9 14 15	syl2anc	$⊢ (φ \land z \in 𝒫 B) \to (B ∖ z \in dom (F \cap I) \leftrightarrow F (B ∖ z) = B ∖ z)$
17	16	bicomd	$⊢ (φ \land z \in 𝒫 B) \to (F (B ∖ z) = B ∖ z \leftrightarrow B ∖ z \in dom (F \cap I))$
18	17	rabbidva	$⊢ φ \to \{z \in 𝒫 B \| F (B ∖ z) = B ∖ z\} = \{z \in 𝒫 B \| B ∖ z \in dom (F \cap I)\}$
19	7 18	syl5eq	$⊢ φ \to J = \{z \in 𝒫 B \| B ∖ z \in dom (F \cap I)\}$
20		simp1	$⊢ (φ \land x \subseteq B \land y \subseteq x) \to φ$
21		simp2	$⊢ (φ \land x \subseteq B \land y \subseteq x) \to x \subseteq B$
22		simp3	$⊢ (φ \land x \subseteq B \land y \subseteq x) \to y \subseteq x$
23	22 21	sstrd	$⊢ (φ \land x \subseteq B \land y \subseteq x) \to y \subseteq B$
24	20 21 23 6	syl3anc	$⊢ (φ \land x \subseteq B \land y \subseteq x) \to F (x \cup y) = F (x) \cup F (y)$
25		ssequn2	$⊢ y \subseteq x \leftrightarrow x \cup y = x$
26	25	biimpi	$⊢ y \subseteq x \to x \cup y = x$
27	26	3ad2ant3	$⊢ (φ \land x \subseteq B \land y \subseteq x) \to x \cup y = x$
28	27	fveq2d	$⊢ (φ \land x \subseteq B \land y \subseteq x) \to F (x \cup y) = F (x)$
29	24 28	eqtr3d	$⊢ (φ \land x \subseteq B \land y \subseteq x) \to F (x) \cup F (y) = F (x)$
30		ssequn2	$⊢ F (y) \subseteq F (x) \leftrightarrow F (x) \cup F (y) = F (x)$
31	29 30	sylibr	$⊢ (φ \land x \subseteq B \land y \subseteq x) \to F (y) \subseteq F (x)$
32	1 2 3 31 4	ismrcd1	$⊢ φ \to dom (F \cap I) \in Moore (B)$
33		0elpw	$⊢ \emptyset \in 𝒫 B$
34		fnelfp	$⊢ (F Fn 𝒫 B \land \emptyset \in 𝒫 B) \to (\emptyset \in dom (F \cap I) \leftrightarrow F (\emptyset) = \emptyset)$
35	8 33 34	sylancl	$⊢ φ \to (\emptyset \in dom (F \cap I) \leftrightarrow F (\emptyset) = \emptyset)$
36	5 35	mpbird	$⊢ φ \to \emptyset \in dom (F \cap I)$
37		simp1	$⊢ (φ \land x \in dom (F \cap I) \land y \in dom (F \cap I)) \to φ$
38		inss1	$⊢ F \cap I \subseteq F$
39		dmss	$⊢ F \cap I \subseteq F \to dom (F \cap I) \subseteq dom F$
40	38 39	ax-mp	$⊢ dom (F \cap I) \subseteq dom F$
41	40 2	fssdm	$⊢ φ \to dom (F \cap I) \subseteq 𝒫 B$
42	41	3ad2ant1	$⊢ (φ \land x \in dom (F \cap I) \land y \in dom (F \cap I)) \to dom (F \cap I) \subseteq 𝒫 B$
43		simp2	$⊢ (φ \land x \in dom (F \cap I) \land y \in dom (F \cap I)) \to x \in dom (F \cap I)$
44	42 43	sseldd	$⊢ (φ \land x \in dom (F \cap I) \land y \in dom (F \cap I)) \to x \in 𝒫 B$
45	44	elpwid	$⊢ (φ \land x \in dom (F \cap I) \land y \in dom (F \cap I)) \to x \subseteq B$
46		simp3	$⊢ (φ \land x \in dom (F \cap I) \land y \in dom (F \cap I)) \to y \in dom (F \cap I)$
47	42 46	sseldd	$⊢ (φ \land x \in dom (F \cap I) \land y \in dom (F \cap I)) \to y \in 𝒫 B$
48	47	elpwid	$⊢ (φ \land x \in dom (F \cap I) \land y \in dom (F \cap I)) \to y \subseteq B$
49	37 45 48 6	syl3anc	$⊢ (φ \land x \in dom (F \cap I) \land y \in dom (F \cap I)) \to F (x \cup y) = F (x) \cup F (y)$
50	8	3ad2ant1	$⊢ (φ \land x \in dom (F \cap I) \land y \in dom (F \cap I)) \to F Fn 𝒫 B$
51		fnelfp	$⊢ (F Fn 𝒫 B \land x \in 𝒫 B) \to (x \in dom (F \cap I) \leftrightarrow F (x) = x)$
52	50 44 51	syl2anc	$⊢ (φ \land x \in dom (F \cap I) \land y \in dom (F \cap I)) \to (x \in dom (F \cap I) \leftrightarrow F (x) = x)$
53	43 52	mpbid	$⊢ (φ \land x \in dom (F \cap I) \land y \in dom (F \cap I)) \to F (x) = x$
54		fnelfp	$⊢ (F Fn 𝒫 B \land y \in 𝒫 B) \to (y \in dom (F \cap I) \leftrightarrow F (y) = y)$
55	50 47 54	syl2anc	$⊢ (φ \land x \in dom (F \cap I) \land y \in dom (F \cap I)) \to (y \in dom (F \cap I) \leftrightarrow F (y) = y)$
56	46 55	mpbid	$⊢ (φ \land x \in dom (F \cap I) \land y \in dom (F \cap I)) \to F (y) = y$
57	53 56	uneq12d	$⊢ (φ \land x \in dom (F \cap I) \land y \in dom (F \cap I)) \to F (x) \cup F (y) = x \cup y$
58	49 57	eqtrd	$⊢ (φ \land x \in dom (F \cap I) \land y \in dom (F \cap I)) \to F (x \cup y) = x \cup y$
59	45 48	unssd	$⊢ (φ \land x \in dom (F \cap I) \land y \in dom (F \cap I)) \to x \cup y \subseteq B$
60		vex	$⊢ x \in V$
61		vex	$⊢ y \in V$
62	60 61	unex	$⊢ x \cup y \in V$
63	62	elpw	$⊢ x \cup y \in 𝒫 B \leftrightarrow x \cup y \subseteq B$
64	59 63	sylibr	$⊢ (φ \land x \in dom (F \cap I) \land y \in dom (F \cap I)) \to x \cup y \in 𝒫 B$
65		fnelfp	$⊢ (F Fn 𝒫 B \land x \cup y \in 𝒫 B) \to (x \cup y \in dom (F \cap I) \leftrightarrow F (x \cup y) = x \cup y)$
66	50 64 65	syl2anc	$⊢ (φ \land x \in dom (F \cap I) \land y \in dom (F \cap I)) \to (x \cup y \in dom (F \cap I) \leftrightarrow F (x \cup y) = x \cup y)$
67	58 66	mpbird	$⊢ (φ \land x \in dom (F \cap I) \land y \in dom (F \cap I)) \to x \cup y \in dom (F \cap I)$
68		eqid	$⊢ \{z \in 𝒫 B \| B ∖ z \in dom (F \cap I)\} = \{z \in 𝒫 B \| B ∖ z \in dom (F \cap I)\}$
69	32 36 67 68	mretopd	$⊢ φ \to (\{z \in 𝒫 B \| B ∖ z \in dom (F \cap I)\} \in TopOn (B) \land dom (F \cap I) = Clsd (\{z \in 𝒫 B \| B ∖ z \in dom (F \cap I)\}))$
70	69	simpld	$⊢ φ \to \{z \in 𝒫 B \| B ∖ z \in dom (F \cap I)\} \in TopOn (B)$
71	19 70	eqeltrd	$⊢ φ \to J \in TopOn (B)$
72		topontop	$⊢ J \in TopOn (B) \to J \in Top$
73	71 72	syl	$⊢ φ \to J \in Top$
74		eqid	$⊢ mrCls (Clsd (J)) = mrCls (Clsd (J))$
75	74	mrccls	$⊢ J \in Top \to cls (J) = mrCls (Clsd (J))$
76	73 75	syl	$⊢ φ \to cls (J) = mrCls (Clsd (J))$
77	69	simprd	$⊢ φ \to dom (F \cap I) = Clsd (\{z \in 𝒫 B \| B ∖ z \in dom (F \cap I)\})$
78	19	fveq2d	$⊢ φ \to Clsd (J) = Clsd (\{z \in 𝒫 B \| B ∖ z \in dom (F \cap I)\})$
79	77 78	eqtr4d	$⊢ φ \to dom (F \cap I) = Clsd (J)$
80	79	fveq2d	$⊢ φ \to mrCls (dom (F \cap I)) = mrCls (Clsd (J))$
81	76 80	eqtr4d	$⊢ φ \to cls (J) = mrCls (dom (F \cap I))$
82	1 2 3 31 4	ismrcd2	$⊢ φ \to F = mrCls (dom (F \cap I))$
83	81 82	eqtr4d	$⊢ φ \to cls (J) = F$
84	71 83	jca	$⊢ φ \to (J \in TopOn (B) \land cls (J) = F)$

Metamath Proof Explorer

Theorem istopclsd

Proof