This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iskgen3

Description: Derive the usual definition of "compactly generated". A topology is compactly generated if every subset of X that is open in every compact subset is open. (Contributed by Mario Carneiro, 20-Mar-2015)

		Ref	Expression
	Hypothesis	iskgen3.1	$⊢ X = ⋃ J$
	Assertion	iskgen3	$⊢ J \in ran 𝑘Gen \leftrightarrow (J \in Top \land \forall x \in 𝒫 X (\forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to x \cap k \in (J ↾_{𝑡} k)) \to x \in J))$

Proof

Step	Hyp	Ref	Expression
1		iskgen3.1	$⊢ X = ⋃ J$
2		iskgen2	$⊢ J \in ran 𝑘Gen \leftrightarrow (J \in Top \land 𝑘Gen (J) \subseteq J)$
3	1	toptopon	$⊢ J \in Top \leftrightarrow J \in TopOn (X)$
4		elkgen	$⊢ J \in TopOn (X) \to (x \in 𝑘Gen (J) \leftrightarrow (x \subseteq X \land \forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to x \cap k \in (J ↾_{𝑡} k))))$
5	3 4	sylbi	$⊢ J \in Top \to (x \in 𝑘Gen (J) \leftrightarrow (x \subseteq X \land \forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to x \cap k \in (J ↾_{𝑡} k))))$
6		vex	$⊢ x \in V$
7	6	elpw	$⊢ x \in 𝒫 X \leftrightarrow x \subseteq X$
8	7	anbi1i	$⊢ (x \in 𝒫 X \land \forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to x \cap k \in (J ↾_{𝑡} k))) \leftrightarrow (x \subseteq X \land \forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to x \cap k \in (J ↾_{𝑡} k)))$
9	5 8	bitr4di	$⊢ J \in Top \to (x \in 𝑘Gen (J) \leftrightarrow (x \in 𝒫 X \land \forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to x \cap k \in (J ↾_{𝑡} k))))$
10	9	imbi1d	$⊢ J \in Top \to ((x \in 𝑘Gen (J) \to x \in J) \leftrightarrow ((x \in 𝒫 X \land \forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to x \cap k \in (J ↾_{𝑡} k))) \to x \in J))$
11		impexp	$⊢ ((x \in 𝒫 X \land \forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to x \cap k \in (J ↾_{𝑡} k))) \to x \in J) \leftrightarrow (x \in 𝒫 X \to (\forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to x \cap k \in (J ↾_{𝑡} k)) \to x \in J))$
12	10 11	bitrdi	$⊢ J \in Top \to ((x \in 𝑘Gen (J) \to x \in J) \leftrightarrow (x \in 𝒫 X \to (\forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to x \cap k \in (J ↾_{𝑡} k)) \to x \in J)))$
13	12	albidv	$⊢ J \in Top \to (\forall x (x \in 𝑘Gen (J) \to x \in J) \leftrightarrow \forall x (x \in 𝒫 X \to (\forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to x \cap k \in (J ↾_{𝑡} k)) \to x \in J)))$
14		df-ss	$⊢ 𝑘Gen (J) \subseteq J \leftrightarrow \forall x (x \in 𝑘Gen (J) \to x \in J)$
15		df-ral	$⊢ \forall x \in 𝒫 X (\forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to x \cap k \in (J ↾_{𝑡} k)) \to x \in J) \leftrightarrow \forall x (x \in 𝒫 X \to (\forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to x \cap k \in (J ↾_{𝑡} k)) \to x \in J))$
16	13 14 15	3bitr4g	$⊢ J \in Top \to (𝑘Gen (J) \subseteq J \leftrightarrow \forall x \in 𝒫 X (\forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to x \cap k \in (J ↾_{𝑡} k)) \to x \in J))$
17	16	pm5.32i	$⊢ (J \in Top \land 𝑘Gen (J) \subseteq J) \leftrightarrow (J \in Top \land \forall x \in 𝒫 X (\forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to x \cap k \in (J ↾_{𝑡} k)) \to x \in J))$
18	2 17	bitri	$⊢ J \in ran 𝑘Gen \leftrightarrow (J \in Top \land \forall x \in 𝒫 X (\forall k \in 𝒫 X (J ↾_{𝑡} k \in Comp \to x \cap k \in (J ↾_{𝑡} k)) \to x \in J))$