Theorem elcls2

Description: Membership in a closure. (Contributed by NM, 5-Mar-2007)

	Ref	Expression
Hypothesis	clscld.1	|- X = U. J
Assertion	elcls2	|- ( ( J e. Top /\ S C_ X ) -> ( P e. ( ( cls ` J ) ` S ) <-> ( P e. X /\ A. x e. J ( P e. x -> ( x i^i S ) =/= (/) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		clscld.1	|- X = U. J
2	1	clsss3	|- ( ( J e. Top /\ S C_ X ) -> ( ( cls ` J ) ` S ) C_ X )
3		ssel	|- ( ( ( cls ` J ) ` S ) C_ X -> ( P e. ( ( cls ` J ) ` S ) -> P e. X ) )
4	3	pm4.71rd	|- ( ( ( cls ` J ) ` S ) C_ X -> ( P e. ( ( cls ` J ) ` S ) <-> ( P e. X /\ P e. ( ( cls ` J ) ` S ) ) ) )
5	2 4	syl	|- ( ( J e. Top /\ S C_ X ) -> ( P e. ( ( cls ` J ) ` S ) <-> ( P e. X /\ P e. ( ( cls ` J ) ` S ) ) ) )
6	1	elcls	|- ( ( J e. Top /\ S C_ X /\ P e. X ) -> ( P e. ( ( cls ` J ) ` S ) <-> A. x e. J ( P e. x -> ( x i^i S ) =/= (/) ) ) )
7	6	3expa	|- ( ( ( J e. Top /\ S C_ X ) /\ P e. X ) -> ( P e. ( ( cls ` J ) ` S ) <-> A. x e. J ( P e. x -> ( x i^i S ) =/= (/) ) ) )
8	7	pm5.32da	|- ( ( J e. Top /\ S C_ X ) -> ( ( P e. X /\ P e. ( ( cls ` J ) ` S ) ) <-> ( P e. X /\ A. x e. J ( P e. x -> ( x i^i S ) =/= (/) ) ) ) )
9	5 8	bitrd	|- ( ( J e. Top /\ S C_ X ) -> ( P e. ( ( cls ` J ) ` S ) <-> ( P e. X /\ A. x e. J ( P e. x -> ( x i^i S ) =/= (/) ) ) ) )