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 ⊢ 𝐽 = { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑝 ∈ 𝑎 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) }
Assertion neipeltop ( 𝐶 ∈ 𝐽 ↔ ( 𝐶 ⊆ 𝑋 ∧ ∀ 𝑝 ∈ 𝐶 𝐶 ∈ ( 𝑁 ‘ 𝑝 ) ) )

Proof

Step Hyp Ref Expression
1 neiptop.o ⊢ 𝐽 = { 𝑎 ∈ 𝒫 𝑋 ∣ ∀ 𝑝 ∈ 𝑎 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) }
2 eleq1 ⊢ ( 𝑎 = 𝐶 → ( 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ↔ 𝐶 ∈ ( 𝑁 ‘ 𝑝 ) ) )
3 2 raleqbi1dv ⊢ ( 𝑎 = 𝐶 → ( ∀ 𝑝 ∈ 𝑎 𝑎 ∈ ( 𝑁 ‘ 𝑝 ) ↔ ∀ 𝑝 ∈ 𝐶 𝐶 ∈ ( 𝑁 ‘ 𝑝 ) ) )
4 3 1 elrab2 ⊢ ( 𝐶 ∈ 𝐽 ↔ ( 𝐶 ∈ 𝒫 𝑋 ∧ ∀ 𝑝 ∈ 𝐶 𝐶 ∈ ( 𝑁 ‘ 𝑝 ) ) )
5 0ex ⊢ ∅ ∈ V
6 eleq1 ⊢ ( 𝐶 = ∅ → ( 𝐶 ∈ V ↔ ∅ ∈ V ) )
7 5 6 mpbiri ⊢ ( 𝐶 = ∅ → 𝐶 ∈ V )
8 7 adantl ⊢ ( ( ∀ 𝑝 ∈ 𝐶 𝐶 ∈ ( 𝑁 ‘ 𝑝 ) ∧ 𝐶 = ∅ ) → 𝐶 ∈ V )
9 elex ⊢ ( 𝐶 ∈ ( 𝑁 ‘ 𝑝 ) → 𝐶 ∈ V )
10 9 ralimi ⊢ ( ∀ 𝑝 ∈ 𝐶 𝐶 ∈ ( 𝑁 ‘ 𝑝 ) → ∀ 𝑝 ∈ 𝐶 𝐶 ∈ V )
11 r19.3rzv ⊢ ( 𝐶 ≠ ∅ → ( 𝐶 ∈ V ↔ ∀ 𝑝 ∈ 𝐶 𝐶 ∈ V ) )
12 11 biimparc ⊢ ( ( ∀ 𝑝 ∈ 𝐶 𝐶 ∈ V ∧ 𝐶 ≠ ∅ ) → 𝐶 ∈ V )
13 10 12 sylan ⊢ ( ( ∀ 𝑝 ∈ 𝐶 𝐶 ∈ ( 𝑁 ‘ 𝑝 ) ∧ 𝐶 ≠ ∅ ) → 𝐶 ∈ V )
14 8 13 pm2.61dane ⊢ ( ∀ 𝑝 ∈ 𝐶 𝐶 ∈ ( 𝑁 ‘ 𝑝 ) → 𝐶 ∈ V )
15 elpwg ⊢ ( 𝐶 ∈ V → ( 𝐶 ∈ 𝒫 𝑋 ↔ 𝐶 ⊆ 𝑋 ) )
16 14 15 syl ⊢ ( ∀ 𝑝 ∈ 𝐶 𝐶 ∈ ( 𝑁 ‘ 𝑝 ) → ( 𝐶 ∈ 𝒫 𝑋 ↔ 𝐶 ⊆ 𝑋 ) )
17 16 pm5.32ri ⊢ ( ( 𝐶 ∈ 𝒫 𝑋 ∧ ∀ 𝑝 ∈ 𝐶 𝐶 ∈ ( 𝑁 ‘ 𝑝 ) ) ↔ ( 𝐶 ⊆ 𝑋 ∧ ∀ 𝑝 ∈ 𝐶 𝐶 ∈ ( 𝑁 ‘ 𝑝 ) ) )
18 4 17 bitri ⊢ ( 𝐶 ∈ 𝐽 ↔ ( 𝐶 ⊆ 𝑋 ∧ ∀ 𝑝 ∈ 𝐶 𝐶 ∈ ( 𝑁 ‘ 𝑝 ) ) )