Theorem gneispacef2

Description: A generic neighborhood space is a function with a range that is a subset of the powerset of the powerset of its domain. (Contributed by RP, 15-Apr-2021)

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

Proof

Step	Hyp	Ref	Expression
1		gneispace.a	⊢ 𝐴 = { 𝑓 ∣ ( 𝑓 : dom 𝑓 ⟶ ( 𝒫 ( 𝒫 dom 𝑓 ∖ { ∅ } ) ∖ { ∅ } ) ∧ ∀ 𝑝 ∈ dom 𝑓 ∀ 𝑛 ∈ ( 𝑓 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝑓 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝑓 ‘ 𝑝 ) ) ) ) }
2		elex	⊢ ( 𝐹 ∈ 𝐴 → 𝐹 ∈ V )
3	1	gneispace	⊢ ( 𝐹 ∈ V → ( 𝐹 ∈ 𝐴 ↔ ( Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀ 𝑝 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑝 ) ≠ ∅ ∧ ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) ) ) )
4	2 3	syl	⊢ ( 𝐹 ∈ 𝐴 → ( 𝐹 ∈ 𝐴 ↔ ( Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀ 𝑝 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑝 ) ≠ ∅ ∧ ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) ) ) )
5	4	ibi	⊢ ( 𝐹 ∈ 𝐴 → ( Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀ 𝑝 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑝 ) ≠ ∅ ∧ ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) ) )
6		simp1	⊢ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀ 𝑝 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑝 ) ≠ ∅ ∧ ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) ) → Fun 𝐹 )
7	6	funfnd	⊢ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀ 𝑝 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑝 ) ≠ ∅ ∧ ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) ) → 𝐹 Fn dom 𝐹 )
8		simp2	⊢ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀ 𝑝 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑝 ) ≠ ∅ ∧ ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) ) → ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 )
9		df-f	⊢ ( 𝐹 : dom 𝐹 ⟶ 𝒫 𝒫 dom 𝐹 ↔ ( 𝐹 Fn dom 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ) )
10	7 8 9	sylanbrc	⊢ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ 𝒫 𝒫 dom 𝐹 ∧ ∀ 𝑝 ∈ dom 𝐹 ( ( 𝐹 ‘ 𝑝 ) ≠ ∅ ∧ ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) ) → 𝐹 : dom 𝐹 ⟶ 𝒫 𝒫 dom 𝐹 )
11	5 10	syl	⊢ ( 𝐹 ∈ 𝐴 → 𝐹 : dom 𝐹 ⟶ 𝒫 𝒫 dom 𝐹 )