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

Metamath Proof Explorer

Theorem elkgen

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

		Ref	Expression
	Assertion	elkgen	\|- ( J e. ( TopOn ` X ) -> ( A e. ( kGen ` J ) <-> ( A C_ X /\ A. k e. ~P X ( ( J \|`t k ) e. Comp -> ( A i^i k ) e. ( J \|`t k ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		kgenval	\|- ( J e. ( TopOn ` X ) -> ( kGen ` J ) = { x e. ~P X \| A. k e. ~P X ( ( J \|`t k ) e. Comp -> ( x i^i k ) e. ( J \|`t k ) ) } )
2	1	eleq2d	\|- ( J e. ( TopOn ` X ) -> ( A e. ( kGen ` J ) <-> A e. { x e. ~P X \| A. k e. ~P X ( ( J \|`t k ) e. Comp -> ( x i^i k ) e. ( J \|`t k ) ) } ) )
3		ineq1	\|- ( x = A -> ( x i^i k ) = ( A i^i k ) )
4	3	eleq1d	\|- ( x = A -> ( ( x i^i k ) e. ( J \|`t k ) <-> ( A i^i k ) e. ( J \|`t k ) ) )
5	4	imbi2d	\|- ( x = A -> ( ( ( J \|`t k ) e. Comp -> ( x i^i k ) e. ( J \|`t k ) ) <-> ( ( J \|`t k ) e. Comp -> ( A i^i k ) e. ( J \|`t k ) ) ) )
6	5	ralbidv	\|- ( x = A -> ( A. k e. ~P X ( ( J \|`t k ) e. Comp -> ( x i^i k ) e. ( J \|`t k ) ) <-> A. k e. ~P X ( ( J \|`t k ) e. Comp -> ( A i^i k ) e. ( J \|`t k ) ) ) )
7	6	elrab	\|- ( A e. { x e. ~P X \| A. k e. ~P X ( ( J \|`t k ) e. Comp -> ( x i^i k ) e. ( J \|`t k ) ) } <-> ( A e. ~P X /\ A. k e. ~P X ( ( J \|`t k ) e. Comp -> ( A i^i k ) e. ( J \|`t k ) ) ) )
8		toponmax	\|- ( J e. ( TopOn ` X ) -> X e. J )
9		elpw2g	\|- ( X e. J -> ( A e. ~P X <-> A C_ X ) )
10	8 9	syl	\|- ( J e. ( TopOn ` X ) -> ( A e. ~P X <-> A C_ X ) )
11	10	anbi1d	\|- ( J e. ( TopOn ` X ) -> ( ( A e. ~P X /\ A. k e. ~P X ( ( J \|`t k ) e. Comp -> ( A i^i k ) e. ( J \|`t k ) ) ) <-> ( A C_ X /\ A. k e. ~P X ( ( J \|`t k ) e. Comp -> ( A i^i k ) e. ( J \|`t k ) ) ) ) )
12	7 11	bitrid	\|- ( J e. ( TopOn ` X ) -> ( A e. { x e. ~P X \| A. k e. ~P X ( ( J \|`t k ) e. Comp -> ( x i^i k ) e. ( J \|`t k ) ) } <-> ( A C_ X /\ A. k e. ~P X ( ( J \|`t k ) e. Comp -> ( A i^i k ) e. ( J \|`t k ) ) ) ) )
13	2 12	bitrd	\|- ( J e. ( TopOn ` X ) -> ( A e. ( kGen ` J ) <-> ( A C_ X /\ A. k e. ~P X ( ( J \|`t k ) e. Comp -> ( A i^i k ) e. ( J \|`t k ) ) ) ) )