Metamath Proof Explorer

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 ⊢ A = f | f : dom ⁡ f ⟶ 𝒫 𝒫 dom ⁡ f ∖ ∅ ∖ ∅ ∧ ∀ p ∈ dom ⁡ f ∀ n ∈ f ⁡ p p ∈ n ∧ ∀ s ∈ 𝒫 dom ⁡ f n ⊆ s → s ∈ f ⁡ p
Assertion gneispacef2 ⊢ F ∈ A → F : dom ⁡ F ⟶ 𝒫 𝒫 dom ⁡ F

Proof

Step Hyp Ref Expression
1 gneispace.a ⊢ A = f | f : dom ⁡ f ⟶ 𝒫 𝒫 dom ⁡ f ∖ ∅ ∖ ∅ ∧ ∀ p ∈ dom ⁡ f ∀ n ∈ f ⁡ p p ∈ n ∧ ∀ s ∈ 𝒫 dom ⁡ f n ⊆ s → s ∈ f ⁡ p
2 elex ⊢ F ∈ A → F ∈ V
3 1 gneispace ⊢ F ∈ V → F ∈ A ↔ Fun ⁡ F ∧ ran ⁡ F ⊆ 𝒫 𝒫 dom ⁡ F ∧ ∀ p ∈ dom ⁡ F F ⁡ p ≠ ∅ ∧ ∀ n ∈ F ⁡ p p ∈ n ∧ ∀ s ∈ 𝒫 dom ⁡ F n ⊆ s → s ∈ F ⁡ p
4 2 3 syl ⊢ F ∈ A → F ∈ A ↔ Fun ⁡ F ∧ ran ⁡ F ⊆ 𝒫 𝒫 dom ⁡ F ∧ ∀ p ∈ dom ⁡ F F ⁡ p ≠ ∅ ∧ ∀ n ∈ F ⁡ p p ∈ n ∧ ∀ s ∈ 𝒫 dom ⁡ F n ⊆ s → s ∈ F ⁡ p
5 4 ibi ⊢ F ∈ A → Fun ⁡ F ∧ ran ⁡ F ⊆ 𝒫 𝒫 dom ⁡ F ∧ ∀ p ∈ dom ⁡ F F ⁡ p ≠ ∅ ∧ ∀ n ∈ F ⁡ p p ∈ n ∧ ∀ s ∈ 𝒫 dom ⁡ F n ⊆ s → s ∈ F ⁡ p
6 simp1 ⊢ Fun ⁡ F ∧ ran ⁡ F ⊆ 𝒫 𝒫 dom ⁡ F ∧ ∀ p ∈ dom ⁡ F F ⁡ p ≠ ∅ ∧ ∀ n ∈ F ⁡ p p ∈ n ∧ ∀ s ∈ 𝒫 dom ⁡ F n ⊆ s → s ∈ F ⁡ p → Fun ⁡ F
7 6 funfnd ⊢ Fun ⁡ F ∧ ran ⁡ F ⊆ 𝒫 𝒫 dom ⁡ F ∧ ∀ p ∈ dom ⁡ F F ⁡ p ≠ ∅ ∧ ∀ n ∈ F ⁡ p p ∈ n ∧ ∀ s ∈ 𝒫 dom ⁡ F n ⊆ s → s ∈ F ⁡ p → F Fn dom ⁡ F
8 simp2 ⊢ Fun ⁡ F ∧ ran ⁡ F ⊆ 𝒫 𝒫 dom ⁡ F ∧ ∀ p ∈ dom ⁡ F F ⁡ p ≠ ∅ ∧ ∀ n ∈ F ⁡ p p ∈ n ∧ ∀ s ∈ 𝒫 dom ⁡ F n ⊆ s → s ∈ F ⁡ p → ran ⁡ F ⊆ 𝒫 𝒫 dom ⁡ F
9 df-f ⊢ F : dom ⁡ F ⟶ 𝒫 𝒫 dom ⁡ F ↔ F Fn dom ⁡ F ∧ ran ⁡ F ⊆ 𝒫 𝒫 dom ⁡ F
10 7 8 9 sylanbrc ⊢ Fun ⁡ F ∧ ran ⁡ F ⊆ 𝒫 𝒫 dom ⁡ F ∧ ∀ p ∈ dom ⁡ F F ⁡ p ≠ ∅ ∧ ∀ n ∈ F ⁡ p p ∈ n ∧ ∀ s ∈ 𝒫 dom ⁡ F n ⊆ s → s ∈ F ⁡ p → F : dom ⁡ F ⟶ 𝒫 𝒫 dom ⁡ F
11 5 10 syl ⊢ F ∈ A → F : dom ⁡ F ⟶ 𝒫 𝒫 dom ⁡ F