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

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 ∈ a a ∈ N ⁡ p
Assertion neipeltop ⊢ C ∈ J ↔ C ⊆ X ∧ ∀ p ∈ C C ∈ N ⁡ p

Proof

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