Metamath Proof Explorer

Theorem neipeltop

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

Ref Expression
Hypothesis neiptop.o ⊢J=a∈𝒫X|∀p∈aa∈N⁡p
Assertion neipeltop ⊢C∈J↔C⊆X∧∀p∈CC∈N⁡p

Proof

Step Hyp Ref Expression
1 neiptop.o ⊢J=a∈𝒫X|∀p∈aa∈N⁡p
2 eleq1 ⊢a=C→a∈N⁡p↔C∈N⁡p
3 2 raleqbi1dv ⊢a=C→∀p∈aa∈N⁡p↔∀p∈CC∈N⁡p
4 3 1 elrab2 ⊢C∈J↔C∈𝒫X∧∀p∈CC∈N⁡p
5 0ex ⊢∅∈V
6 eleq1 ⊢C=∅→C∈V↔∅∈V
7 5 6 mpbiri ⊢C=∅→C∈V
8 7 adantl ⊢∀p∈CC∈N⁡p∧C=∅→C∈V
9 elex ⊢C∈N⁡p→C∈V
10 9 ralimi ⊢∀p∈CC∈N⁡p→∀p∈CC∈V
11 r19.3rzv ⊢C≠∅→C∈V↔∀p∈CC∈V
12 11 biimparc ⊢∀p∈CC∈V∧C≠∅→C∈V
13 10 12 sylan ⊢∀p∈CC∈N⁡p∧C≠∅→C∈V
14 8 13 pm2.61dane ⊢∀p∈CC∈N⁡p→C∈V
15 elpwg ⊢C∈V→C∈𝒫X↔C⊆X
16 14 15 syl ⊢∀p∈CC∈N⁡p→C∈𝒫X↔C⊆X
17 16 pm5.32ri ⊢C∈𝒫X∧∀p∈CC∈N⁡p↔C⊆X∧∀p∈CC∈N⁡p
18 4 17 bitri ⊢C∈J↔C⊆X∧∀p∈CC∈N⁡p