Theorem gneispaceel2

Description: Every neighborhood of a point in a generic neighborhood space contains that point. (Contributed by RP, 15-Apr-2021)

	Ref	Expression
Hypothesis	gneispace.a	⊢ 𝐴 = { 𝑓 ∣ ( 𝑓 : dom 𝑓 ⟶ ( 𝒫 ( 𝒫 dom 𝑓 ∖ { ∅ } ) ∖ { ∅ } ) ∧ ∀ 𝑝 ∈ dom 𝑓 ∀ 𝑛 ∈ ( 𝑓 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝑓 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝑓 ‘ 𝑝 ) ) ) ) }
Assertion	gneispaceel2	⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑃 ∈ dom 𝐹 ∧ 𝑁 ∈ ( 𝐹 ‘ 𝑃 ) ) → 𝑃 ∈ 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		gneispace.a	⊢ 𝐴 = { 𝑓 ∣ ( 𝑓 : dom 𝑓 ⟶ ( 𝒫 ( 𝒫 dom 𝑓 ∖ { ∅ } ) ∖ { ∅ } ) ∧ ∀ 𝑝 ∈ dom 𝑓 ∀ 𝑛 ∈ ( 𝑓 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝑓 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝑓 ‘ 𝑝 ) ) ) ) }
2	1	gneispaceel	⊢ ( 𝐹 ∈ 𝐴 → ∀ 𝑝 ∈ dom 𝐹 ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) 𝑝 ∈ 𝑛 )
3		fveq2	⊢ ( 𝑝 = 𝑃 → ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑃 ) )
4		eleq1	⊢ ( 𝑝 = 𝑃 → ( 𝑝 ∈ 𝑛 ↔ 𝑃 ∈ 𝑛 ) )
5	3 4	raleqbidv	⊢ ( 𝑝 = 𝑃 → ( ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) 𝑝 ∈ 𝑛 ↔ ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑃 ) 𝑃 ∈ 𝑛 ) )
6	5	rspccv	⊢ ( ∀ 𝑝 ∈ dom 𝐹 ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) 𝑝 ∈ 𝑛 → ( 𝑃 ∈ dom 𝐹 → ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑃 ) 𝑃 ∈ 𝑛 ) )
7	2 6	syl	⊢ ( 𝐹 ∈ 𝐴 → ( 𝑃 ∈ dom 𝐹 → ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑃 ) 𝑃 ∈ 𝑛 ) )
8		eleq2	⊢ ( 𝑛 = 𝑁 → ( 𝑃 ∈ 𝑛 ↔ 𝑃 ∈ 𝑁 ) )
9	8	rspccv	⊢ ( ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑃 ) 𝑃 ∈ 𝑛 → ( 𝑁 ∈ ( 𝐹 ‘ 𝑃 ) → 𝑃 ∈ 𝑁 ) )
10	7 9	syl6	⊢ ( 𝐹 ∈ 𝐴 → ( 𝑃 ∈ dom 𝐹 → ( 𝑁 ∈ ( 𝐹 ‘ 𝑃 ) → 𝑃 ∈ 𝑁 ) ) )
11	10	3imp	⊢ ( ( 𝐹 ∈ 𝐴 ∧ 𝑃 ∈ dom 𝐹 ∧ 𝑁 ∈ ( 𝐹 ‘ 𝑃 ) ) → 𝑃 ∈ 𝑁 )