tgidm

Description: The topology generator function is idempotent. (Contributed by NM, 18-Jul-2006) (Revised by Mario Carneiro, 2-Sep-2015)

		Ref	Expression
	Assertion	tgidm	$⊢ B \in V \to topGen (topGen (B)) = topGen (B)$

Proof

Step	Hyp	Ref	Expression
1		fvex	$⊢ topGen (B) \in V$
2		eltg3	$⊢ topGen (B) \in V \to (x \in topGen (topGen (B)) \leftrightarrow \exists y (y \subseteq topGen (B) \land x = ⋃ y))$
3	1 2	ax-mp	$⊢ x \in topGen (topGen (B)) \leftrightarrow \exists y (y \subseteq topGen (B) \land x = ⋃ y)$
4		uniiun	$⊢ ⋃ y = ⋃_{z \in y} z$
5		simpr	$⊢ (B \in V \land y \subseteq topGen (B)) \to y \subseteq topGen (B)$
6	5	sselda	$⊢ ((B \in V \land y \subseteq topGen (B)) \land z \in y) \to z \in topGen (B)$
7		eltg4i	$⊢ z \in topGen (B) \to z = ⋃ (B \cap 𝒫 z)$
8	6 7	syl	$⊢ ((B \in V \land y \subseteq topGen (B)) \land z \in y) \to z = ⋃ (B \cap 𝒫 z)$
9	8	iuneq2dv	$⊢ (B \in V \land y \subseteq topGen (B)) \to ⋃_{z \in y} z = ⋃_{z \in y} ⋃ (B \cap 𝒫 z)$
10	4 9	syl5eq	$⊢ (B \in V \land y \subseteq topGen (B)) \to ⋃ y = ⋃_{z \in y} ⋃ (B \cap 𝒫 z)$
11		iuncom4	$⊢ ⋃_{z \in y} ⋃ (B \cap 𝒫 z) = ⋃ ⋃_{z \in y} (B \cap 𝒫 z)$
12	10 11	eqtrdi	$⊢ (B \in V \land y \subseteq topGen (B)) \to ⋃ y = ⋃ ⋃_{z \in y} (B \cap 𝒫 z)$
13		inss1	$⊢ B \cap 𝒫 z \subseteq B$
14	13	rgenw	$⊢ \forall z \in y B \cap 𝒫 z \subseteq B$
15		iunss	$⊢ ⋃_{z \in y} (B \cap 𝒫 z) \subseteq B \leftrightarrow \forall z \in y B \cap 𝒫 z \subseteq B$
16	14 15	mpbir	$⊢ ⋃_{z \in y} (B \cap 𝒫 z) \subseteq B$
17	16	a1i	$⊢ y \subseteq topGen (B) \to ⋃_{z \in y} (B \cap 𝒫 z) \subseteq B$
18		eltg3i	$⊢ (B \in V \land ⋃_{z \in y} (B \cap 𝒫 z) \subseteq B) \to ⋃ ⋃_{z \in y} (B \cap 𝒫 z) \in topGen (B)$
19	17 18	sylan2	$⊢ (B \in V \land y \subseteq topGen (B)) \to ⋃ ⋃_{z \in y} (B \cap 𝒫 z) \in topGen (B)$
20	12 19	eqeltrd	$⊢ (B \in V \land y \subseteq topGen (B)) \to ⋃ y \in topGen (B)$
21		eleq1	$⊢ x = ⋃ y \to (x \in topGen (B) \leftrightarrow ⋃ y \in topGen (B))$
22	20 21	syl5ibrcom	$⊢ (B \in V \land y \subseteq topGen (B)) \to (x = ⋃ y \to x \in topGen (B))$
23	22	expimpd	$⊢ B \in V \to ((y \subseteq topGen (B) \land x = ⋃ y) \to x \in topGen (B))$
24	23	exlimdv	$⊢ B \in V \to (\exists y (y \subseteq topGen (B) \land x = ⋃ y) \to x \in topGen (B))$
25	3 24	syl5bi	$⊢ B \in V \to (x \in topGen (topGen (B)) \to x \in topGen (B))$
26	25	ssrdv	$⊢ B \in V \to topGen (topGen (B)) \subseteq topGen (B)$
27		bastg	$⊢ B \in V \to B \subseteq topGen (B)$
28		tgss	$⊢ (topGen (B) \in V \land B \subseteq topGen (B)) \to topGen (B) \subseteq topGen (topGen (B))$
29	1 27 28	sylancr	$⊢ B \in V \to topGen (B) \subseteq topGen (topGen (B))$
30	26 29	eqssd	$⊢ B \in V \to topGen (topGen (B)) = topGen (B)$

Metamath Proof Explorer

Theorem tgidm

Proof