tgdom

Description: A space has no more open sets than subsets of a basis. (Contributed by Stefan O'Rear, 22-Feb-2015) (Revised by Mario Carneiro, 9-Apr-2015)

		Ref	Expression
	Assertion	tgdom	$⊢ B \in V \to topGen (B) ≼ 𝒫 B$

Proof

Step	Hyp	Ref	Expression
1		pwexg	$⊢ B \in V \to 𝒫 B \in V$
2		inss1	$⊢ B \cap 𝒫 x \subseteq B$
3		vpwex	$⊢ 𝒫 x \in V$
4	3	inex2	$⊢ B \cap 𝒫 x \in V$
5	4	elpw	$⊢ B \cap 𝒫 x \in 𝒫 B \leftrightarrow B \cap 𝒫 x \subseteq B$
6	2 5	mpbir	$⊢ B \cap 𝒫 x \in 𝒫 B$
7	6	a1i	$⊢ x \in topGen (B) \to B \cap 𝒫 x \in 𝒫 B$
8		unieq	$⊢ B \cap 𝒫 x = B \cap 𝒫 y \to ⋃ (B \cap 𝒫 x) = ⋃ (B \cap 𝒫 y)$
9	8	adantl	$⊢ ((x \in topGen (B) \land y \in topGen (B)) \land B \cap 𝒫 x = B \cap 𝒫 y) \to ⋃ (B \cap 𝒫 x) = ⋃ (B \cap 𝒫 y)$
10		eltg4i	$⊢ x \in topGen (B) \to x = ⋃ (B \cap 𝒫 x)$
11	10	ad2antrr	$⊢ ((x \in topGen (B) \land y \in topGen (B)) \land B \cap 𝒫 x = B \cap 𝒫 y) \to x = ⋃ (B \cap 𝒫 x)$
12		eltg4i	$⊢ y \in topGen (B) \to y = ⋃ (B \cap 𝒫 y)$
13	12	ad2antlr	$⊢ ((x \in topGen (B) \land y \in topGen (B)) \land B \cap 𝒫 x = B \cap 𝒫 y) \to y = ⋃ (B \cap 𝒫 y)$
14	9 11 13	3eqtr4d	$⊢ ((x \in topGen (B) \land y \in topGen (B)) \land B \cap 𝒫 x = B \cap 𝒫 y) \to x = y$
15	14	ex	$⊢ (x \in topGen (B) \land y \in topGen (B)) \to (B \cap 𝒫 x = B \cap 𝒫 y \to x = y)$
16		pweq	$⊢ x = y \to 𝒫 x = 𝒫 y$
17	16	ineq2d	$⊢ x = y \to B \cap 𝒫 x = B \cap 𝒫 y$
18	15 17	impbid1	$⊢ (x \in topGen (B) \land y \in topGen (B)) \to (B \cap 𝒫 x = B \cap 𝒫 y \leftrightarrow x = y)$
19	7 18	dom2	$⊢ 𝒫 B \in V \to topGen (B) ≼ 𝒫 B$
20	1 19	syl	$⊢ B \in V \to topGen (B) ≼ 𝒫 B$

Metamath Proof Explorer

Theorem tgdom

Proof