Metamath Proof Explorer

Theorem elkgen

Description: Value of the compact generator. (Contributed by Mario Carneiro, 20-Mar-2015)

		Ref	Expression
	Assertion	elkgen	$⊢ J \in TopOn (X) \to (A \in 𝑘Gen (J) \leftrightarrow (A \subseteq X \land \forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to A \cap k \in (J ↾_{𝑡} k))))$

Proof

Step	Hyp	Ref	Expression
1		kgenval	$⊢ J \in TopOn (X) \to 𝑘Gen (J) = \{x \in 𝒫 X \| \forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to x \cap k \in (J ↾_{𝑡} k))\}$
2	1	eleq2d	$⊢ J \in TopOn (X) \to (A \in 𝑘Gen (J) \leftrightarrow A \in \{x \in 𝒫 X \| \forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to x \cap k \in (J ↾_{𝑡} k))\})$
3		ineq1	$⊢ x = A \to x \cap k = A \cap k$
4	3	eleq1d	$⊢ x = A \to (x \cap k \in (J ↾_{𝑡} k) \leftrightarrow A \cap k \in (J ↾_{𝑡} k))$
5	4	imbi2d	$⊢ x = A \to ((J ↾_{𝑡} k \in Comp \to x \cap k \in (J ↾_{𝑡} k)) \leftrightarrow (J ↾_{𝑡} k \in Comp \to A \cap k \in (J ↾_{𝑡} k)))$
6	5	ralbidv	$⊢ x = A \to (\forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to x \cap k \in (J ↾_{𝑡} k)) \leftrightarrow \forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to A \cap k \in (J ↾_{𝑡} k)))$
7	6	elrab	$⊢ A \in \{x \in 𝒫 X \| \forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to x \cap k \in (J ↾_{𝑡} k))\} \leftrightarrow (A \in 𝒫 X \land \forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to A \cap k \in (J ↾_{𝑡} k)))$
8		toponmax	$⊢ J \in TopOn (X) \to X \in J$
9		elpw2g	$⊢ X \in J \to (A \in 𝒫 X \leftrightarrow A \subseteq X)$
10	8 9	syl	$⊢ J \in TopOn (X) \to (A \in 𝒫 X \leftrightarrow A \subseteq X)$
11	10	anbi1d	$⊢ J \in TopOn (X) \to ((A \in 𝒫 X \land \forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to A \cap k \in (J ↾_{𝑡} k))) \leftrightarrow (A \subseteq X \land \forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to A \cap k \in (J ↾_{𝑡} k))))$
12	7 11	bitrid	$⊢ J \in TopOn (X) \to (A \in \{x \in 𝒫 X \| \forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to x \cap k \in (J ↾_{𝑡} k))\} \leftrightarrow (A \subseteq X \land \forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to A \cap k \in (J ↾_{𝑡} k))))$
13	2 12	bitrd	$⊢ J \in TopOn (X) \to (A \in 𝑘Gen (J) \leftrightarrow (A \subseteq X \land \forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to A \cap k \in (J ↾_{𝑡} k))))$