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 = U. J
	Assertion	iskgen3	\|- ( J e. ran kGen <-> ( J e. Top /\ A. x e. ~P X ( A. k e. ~P X ( ( J \|`t k ) e. Comp -> ( x i^i k ) e. ( J \|`t k ) ) -> x e. J ) ) )

Proof

Step	Hyp	Ref	Expression
1		iskgen3.1	\|- X = U. J
2		iskgen2	\|- ( J e. ran kGen <-> ( J e. Top /\ ( kGen ` J ) C_ J ) )
3	1	toptopon	\|- ( J e. Top <-> J e. ( TopOn ` X ) )
4		elkgen	\|- ( J e. ( TopOn ` X ) -> ( x e. ( kGen ` J ) <-> ( x C_ X /\ A. k e. ~P X ( ( J \|`t k ) e. Comp -> ( x i^i k ) e. ( J \|`t k ) ) ) ) )
5	3 4	sylbi	\|- ( J e. Top -> ( x e. ( kGen ` J ) <-> ( x C_ X /\ A. k e. ~P X ( ( J \|`t k ) e. Comp -> ( x i^i k ) e. ( J \|`t k ) ) ) ) )
6		vex	\|- x e. _V
7	6	elpw	\|- ( x e. ~P X <-> x C_ X )
8	7	anbi1i	\|- ( ( x e. ~P X /\ A. k e. ~P X ( ( J \|`t k ) e. Comp -> ( x i^i k ) e. ( J \|`t k ) ) ) <-> ( x C_ X /\ A. k e. ~P X ( ( J \|`t k ) e. Comp -> ( x i^i k ) e. ( J \|`t k ) ) ) )
9	5 8	bitr4di	\|- ( J e. Top -> ( x e. ( kGen ` J ) <-> ( x e. ~P X /\ A. k e. ~P X ( ( J \|`t k ) e. Comp -> ( x i^i k ) e. ( J \|`t k ) ) ) ) )
10	9	imbi1d	\|- ( J e. Top -> ( ( x e. ( kGen ` J ) -> x e. J ) <-> ( ( x e. ~P X /\ A. k e. ~P X ( ( J \|`t k ) e. Comp -> ( x i^i k ) e. ( J \|`t k ) ) ) -> x e. J ) ) )
11		impexp	\|- ( ( ( x e. ~P X /\ A. k e. ~P X ( ( J \|`t k ) e. Comp -> ( x i^i k ) e. ( J \|`t k ) ) ) -> x e. J ) <-> ( x e. ~P X -> ( A. k e. ~P X ( ( J \|`t k ) e. Comp -> ( x i^i k ) e. ( J \|`t k ) ) -> x e. J ) ) )
12	10 11	bitrdi	\|- ( J e. Top -> ( ( x e. ( kGen ` J ) -> x e. J ) <-> ( x e. ~P X -> ( A. k e. ~P X ( ( J \|`t k ) e. Comp -> ( x i^i k ) e. ( J \|`t k ) ) -> x e. J ) ) ) )
13	12	albidv	\|- ( J e. Top -> ( A. x ( x e. ( kGen ` J ) -> x e. J ) <-> A. x ( x e. ~P X -> ( A. k e. ~P X ( ( J \|`t k ) e. Comp -> ( x i^i k ) e. ( J \|`t k ) ) -> x e. J ) ) ) )
14		df-ss	\|- ( ( kGen ` J ) C_ J <-> A. x ( x e. ( kGen ` J ) -> x e. J ) )
15		df-ral	\|- ( A. x e. ~P X ( A. k e. ~P X ( ( J \|`t k ) e. Comp -> ( x i^i k ) e. ( J \|`t k ) ) -> x e. J ) <-> A. x ( x e. ~P X -> ( A. k e. ~P X ( ( J \|`t k ) e. Comp -> ( x i^i k ) e. ( J \|`t k ) ) -> x e. J ) ) )
16	13 14 15	3bitr4g	\|- ( J e. Top -> ( ( kGen ` J ) C_ J <-> A. x e. ~P X ( A. k e. ~P X ( ( J \|`t k ) e. Comp -> ( x i^i k ) e. ( J \|`t k ) ) -> x e. J ) ) )
17	16	pm5.32i	\|- ( ( J e. Top /\ ( kGen ` J ) C_ J ) <-> ( J e. Top /\ A. x e. ~P X ( A. k e. ~P X ( ( J \|`t k ) e. Comp -> ( x i^i k ) e. ( J \|`t k ) ) -> x e. J ) ) )
18	2 17	bitri	\|- ( J e. ran kGen <-> ( J e. Top /\ A. x e. ~P X ( A. k e. ~P X ( ( J \|`t k ) e. Comp -> ( x i^i k ) e. ( J \|`t k ) ) -> x e. J ) ) )