eltg2b

Description: Membership in a topology generated by a basis. (Contributed by Mario Carneiro, 17-Jun-2014) (Revised by Mario Carneiro, 10-Jan-2015)

		Ref	Expression
	Assertion	eltg2b	$⊢ B \in V \to (A \in topGen (B) \leftrightarrow \forall x \in A \exists y \in B (x \in y \land y \subseteq A))$

Step	Hyp	Ref	Expression
1		eltg2	$⊢ B \in V \to (A \in topGen (B) \leftrightarrow (A \subseteq ⋃ B \land \forall x \in A \exists y \in B (x \in y \land y \subseteq A)))$
2		simpl	$⊢ (x \in y \land y \subseteq A) \to x \in y$
3	2	reximi	$⊢ \exists y \in B (x \in y \land y \subseteq A) \to \exists y \in B x \in y$
4		eluni2	$⊢ x \in ⋃ B \leftrightarrow \exists y \in B x \in y$
5	3 4	sylibr	$⊢ \exists y \in B (x \in y \land y \subseteq A) \to x \in ⋃ B$
6	5	ralimi	$⊢ \forall x \in A \exists y \in B (x \in y \land y \subseteq A) \to \forall x \in A x \in ⋃ B$
7		dfss3	$⊢ A \subseteq ⋃ B \leftrightarrow \forall x \in A x \in ⋃ B$
8	6 7	sylibr	$⊢ \forall x \in A \exists y \in B (x \in y \land y \subseteq A) \to A \subseteq ⋃ B$
9	8	pm4.71ri	$⊢ \forall x \in A \exists y \in B (x \in y \land y \subseteq A) \leftrightarrow (A \subseteq ⋃ B \land \forall x \in A \exists y \in B (x \in y \land y \subseteq A))$
10	1 9	bitr4di	$⊢ B \in V \to (A \in topGen (B) \leftrightarrow \forall x \in A \exists y \in B (x \in y \land y \subseteq A))$

Metamath Proof Explorer