Theorem gneispacess2

Description: All supersets of a neighborhood of a point (limited to the domain of the neighborhood space) are also neighborhoods of that point. (Contributed by RP, 15-Apr-2021)

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

Proof

Step	Hyp	Ref	Expression
1		gneispace.a	⊢ 𝐴 = { 𝑓 ∣ ( 𝑓 : dom 𝑓 ⟶ ( 𝒫 ( 𝒫 dom 𝑓 ∖ { ∅ } ) ∖ { ∅ } ) ∧ ∀ 𝑝 ∈ dom 𝑓 ∀ 𝑛 ∈ ( 𝑓 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝑓 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝑓 ‘ 𝑝 ) ) ) ) }
2	1	gneispacess	⊢ ( 𝐹 ∈ 𝐴 → ∀ 𝑝 ∈ dom 𝐹 ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) )
3		fveq2	⊢ ( 𝑝 = 𝑃 → ( 𝐹 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑃 ) )
4	3	eleq2d	⊢ ( 𝑝 = 𝑃 → ( 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ↔ 𝑠 ∈ ( 𝐹 ‘ 𝑃 ) ) )
5	4	imbi2d	⊢ ( 𝑝 = 𝑃 → ( ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ↔ ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑃 ) ) ) )
6	5	ralbidv	⊢ ( 𝑝 = 𝑃 → ( ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ↔ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑃 ) ) ) )
7	3 6	raleqbidv	⊢ ( 𝑝 = 𝑃 → ( ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ↔ ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑃 ) ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑃 ) ) ) )
8	7	rspccv	⊢ ( ∀ 𝑝 ∈ dom 𝐹 ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) → ( 𝑃 ∈ dom 𝐹 → ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑃 ) ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑃 ) ) ) )
9	2 8	syl	⊢ ( 𝐹 ∈ 𝐴 → ( 𝑃 ∈ dom 𝐹 → ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑃 ) ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑃 ) ) ) )
10		sseq1	⊢ ( 𝑛 = 𝑁 → ( 𝑛 ⊆ 𝑠 ↔ 𝑁 ⊆ 𝑠 ) )
11	10	imbi1d	⊢ ( 𝑛 = 𝑁 → ( ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑃 ) ) ↔ ( 𝑁 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑃 ) ) ) )
12	11	ralbidv	⊢ ( 𝑛 = 𝑁 → ( ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑃 ) ) ↔ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑁 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑃 ) ) ) )
13	12	rspccv	⊢ ( ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑃 ) ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑃 ) ) → ( 𝑁 ∈ ( 𝐹 ‘ 𝑃 ) → ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑁 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑃 ) ) ) )
14		sseq2	⊢ ( 𝑠 = 𝑆 → ( 𝑁 ⊆ 𝑠 ↔ 𝑁 ⊆ 𝑆 ) )
15		eleq1	⊢ ( 𝑠 = 𝑆 → ( 𝑠 ∈ ( 𝐹 ‘ 𝑃 ) ↔ 𝑆 ∈ ( 𝐹 ‘ 𝑃 ) ) )
16	14 15	imbi12d	⊢ ( 𝑠 = 𝑆 → ( ( 𝑁 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑃 ) ) ↔ ( 𝑁 ⊆ 𝑆 → 𝑆 ∈ ( 𝐹 ‘ 𝑃 ) ) ) )
17	16	rspccv	⊢ ( ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑁 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑃 ) ) → ( 𝑆 ∈ 𝒫 dom 𝐹 → ( 𝑁 ⊆ 𝑆 → 𝑆 ∈ ( 𝐹 ‘ 𝑃 ) ) ) )
18	13 17	syl6	⊢ ( ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑃 ) ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑃 ) ) → ( 𝑁 ∈ ( 𝐹 ‘ 𝑃 ) → ( 𝑆 ∈ 𝒫 dom 𝐹 → ( 𝑁 ⊆ 𝑆 → 𝑆 ∈ ( 𝐹 ‘ 𝑃 ) ) ) ) )
19	18	3impd	⊢ ( ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑃 ) ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑃 ) ) → ( ( 𝑁 ∈ ( 𝐹 ‘ 𝑃 ) ∧ 𝑆 ∈ 𝒫 dom 𝐹 ∧ 𝑁 ⊆ 𝑆 ) → 𝑆 ∈ ( 𝐹 ‘ 𝑃 ) ) )
20	9 19	syl6	⊢ ( 𝐹 ∈ 𝐴 → ( 𝑃 ∈ dom 𝐹 → ( ( 𝑁 ∈ ( 𝐹 ‘ 𝑃 ) ∧ 𝑆 ∈ 𝒫 dom 𝐹 ∧ 𝑁 ⊆ 𝑆 ) → 𝑆 ∈ ( 𝐹 ‘ 𝑃 ) ) ) )
21	20	imp31	⊢ ( ( ( 𝐹 ∈ 𝐴 ∧ 𝑃 ∈ dom 𝐹 ) ∧ ( 𝑁 ∈ ( 𝐹 ‘ 𝑃 ) ∧ 𝑆 ∈ 𝒫 dom 𝐹 ∧ 𝑁 ⊆ 𝑆 ) ) → 𝑆 ∈ ( 𝐹 ‘ 𝑃 ) )