Metamath Proof Explorer

Theorem neipeltop

Description: Lemma for neiptopreu . (Contributed by Thierry Arnoux, 6-Jan-2018)

Ref Expression
Hypothesis neiptop.o 
|- J = { a e. ~P X | A. p e. a a e. ( N ` p ) }
Assertion neipeltop 
|- ( C e. J <-> ( C C_ X /\ A. p e. C C e. ( N ` p ) ) )

Proof

Step Hyp Ref Expression
1 neiptop.o 
 |-  J = { a e. ~P X | A. p e. a a e. ( N ` p ) }
2 eleq1 
 |-  ( a = C -> ( a e. ( N ` p ) <-> C e. ( N ` p ) ) )
3 2 raleqbi1dv 
 |-  ( a = C -> ( A. p e. a a e. ( N ` p ) <-> A. p e. C C e. ( N ` p ) ) )
4 3 1 elrab2 
 |-  ( C e. J <-> ( C e. ~P X /\ A. p e. C C e. ( N ` p ) ) )
5 0ex 
 |-  (/) e. _V
6 eleq1 
 |-  ( C = (/) -> ( C e. _V <-> (/) e. _V ) )
7 5 6 mpbiri 
 |-  ( C = (/) -> C e. _V )
8 7 adantl 
 |-  ( ( A. p e. C C e. ( N ` p ) /\ C = (/) ) -> C e. _V )
9 elex 
 |-  ( C e. ( N ` p ) -> C e. _V )
10 9 ralimi 
 |-  ( A. p e. C C e. ( N ` p ) -> A. p e. C C e. _V )
11 r19.3rzv 
 |-  ( C =/= (/) -> ( C e. _V <-> A. p e. C C e. _V ) )
12 11 biimparc 
 |-  ( ( A. p e. C C e. _V /\ C =/= (/) ) -> C e. _V )
13 10 12 sylan 
 |-  ( ( A. p e. C C e. ( N ` p ) /\ C =/= (/) ) -> C e. _V )
14 8 13 pm2.61dane 
 |-  ( A. p e. C C e. ( N ` p ) -> C e. _V )
15 elpwg 
 |-  ( C e. _V -> ( C e. ~P X <-> C C_ X ) )
16 14 15 syl 
 |-  ( A. p e. C C e. ( N ` p ) -> ( C e. ~P X <-> C C_ X ) )
17 16 pm5.32ri 
 |-  ( ( C e. ~P X /\ A. p e. C C e. ( N ` p ) ) <-> ( C C_ X /\ A. p e. C C e. ( N ` p ) ) )
18 4 17 bitri 
 |-  ( C e. J <-> ( C C_ X /\ A. p e. C C e. ( N ` p ) ) )