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

Metamath Proof Explorer

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 ) =/= (/) ) ) ) )