eltg3

Description: Membership in a topology generated by a basis. (Contributed by NM, 15-Jul-2006) (Proof shortened by Mario Carneiro, 30-Aug-2015)

		Ref	Expression
	Assertion	eltg3	$⊢ B \in V \to (A \in topGen (B) \leftrightarrow \exists x (x \subseteq B \land A = ⋃ x))$

Step	Hyp	Ref	Expression
1		elfvdm	$⊢ A \in topGen (B) \to B \in dom topGen$
2		inex1g	$⊢ B \in dom topGen \to B \cap 𝒫 A \in V$
3	1 2	syl	$⊢ A \in topGen (B) \to B \cap 𝒫 A \in V$
4		eltg4i	$⊢ A \in topGen (B) \to A = ⋃ (B \cap 𝒫 A)$
5		inss1	$⊢ B \cap 𝒫 A \subseteq B$
6		sseq1	$⊢ x = B \cap 𝒫 A \to (x \subseteq B \leftrightarrow B \cap 𝒫 A \subseteq B)$
7	5 6	mpbiri	$⊢ x = B \cap 𝒫 A \to x \subseteq B$
8	7	biantrurd	$⊢ x = B \cap 𝒫 A \to (A = ⋃ x \leftrightarrow (x \subseteq B \land A = ⋃ x))$
9		unieq	$⊢ x = B \cap 𝒫 A \to ⋃ x = ⋃ (B \cap 𝒫 A)$
10	9	eqeq2d	$⊢ x = B \cap 𝒫 A \to (A = ⋃ x \leftrightarrow A = ⋃ (B \cap 𝒫 A))$
11	8 10	bitr3d	$⊢ x = B \cap 𝒫 A \to ((x \subseteq B \land A = ⋃ x) \leftrightarrow A = ⋃ (B \cap 𝒫 A))$
12	3 4 11	spcedv	$⊢ A \in topGen (B) \to \exists x (x \subseteq B \land A = ⋃ x)$
13		eltg3i	$⊢ (B \in V \land x \subseteq B) \to ⋃ x \in topGen (B)$
14		eleq1	$⊢ A = ⋃ x \to (A \in topGen (B) \leftrightarrow ⋃ x \in topGen (B))$
15	13 14	syl5ibrcom	$⊢ (B \in V \land x \subseteq B) \to (A = ⋃ x \to A \in topGen (B))$
16	15	expimpd	$⊢ B \in V \to ((x \subseteq B \land A = ⋃ x) \to A \in topGen (B))$
17	16	exlimdv	$⊢ B \in V \to (\exists x (x \subseteq B \land A = ⋃ x) \to A \in topGen (B))$
18	12 17	impbid2	$⊢ B \in V \to (A \in topGen (B) \leftrightarrow \exists x (x \subseteq B \land A = ⋃ x))$

Metamath Proof Explorer