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	⊢ ( 𝐶 ∈ 𝐽 ↔ ( 𝐶 ⊆ 𝑋 ∧ ∀ 𝑝 ∈ 𝐶 𝐶 ∈ ( 𝑁 ‘ 𝑝 ) ) )