Metamath Proof Explorer

Theorem gneispace3

Description: The predicate that F is a (generic) Seifert and Threlfall neighborhood space. (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 gneispace3 ⊢ F ∈ V → F ∈ A ↔ Fun ⁡ F ∧ ran ⁡ F ⊆ 𝒫 𝒫 dom ⁡ F ∖ ∅ ∖ ∅ ∧ ∀ p ∈ dom ⁡ F ∀ n ∈ F ⁡ p p ∈ n ∧ ∀ s ∈ 𝒫 dom ⁡ F n ⊆ s → s ∈ F ⁡ p

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 1 gneispace2 ⊢ F ∈ V → F ∈ A ↔ F : dom ⁡ F ⟶ 𝒫 𝒫 dom ⁡ F ∖ ∅ ∖ ∅ ∧ ∀ p ∈ dom ⁡ F ∀ n ∈ F ⁡ p p ∈ n ∧ ∀ s ∈ 𝒫 dom ⁡ F n ⊆ s → s ∈ F ⁡ p
3 df-f ⊢ F : dom ⁡ F ⟶ 𝒫 𝒫 dom ⁡ F ∖ ∅ ∖ ∅ ↔ F Fn dom ⁡ F ∧ ran ⁡ F ⊆ 𝒫 𝒫 dom ⁡ F ∖ ∅ ∖ ∅
4 funfn ⊢ Fun ⁡ F ↔ F Fn dom ⁡ F
5 4 anbi1i ⊢ Fun ⁡ F ∧ ran ⁡ F ⊆ 𝒫 𝒫 dom ⁡ F ∖ ∅ ∖ ∅ ↔ F Fn dom ⁡ F ∧ ran ⁡ F ⊆ 𝒫 𝒫 dom ⁡ F ∖ ∅ ∖ ∅
6 3 5 bitr4i ⊢ F : dom ⁡ F ⟶ 𝒫 𝒫 dom ⁡ F ∖ ∅ ∖ ∅ ↔ Fun ⁡ F ∧ ran ⁡ F ⊆ 𝒫 𝒫 dom ⁡ F ∖ ∅ ∖ ∅
7 6 anbi1i ⊢ F : dom ⁡ F ⟶ 𝒫 𝒫 dom ⁡ F ∖ ∅ ∖ ∅ ∧ ∀ p ∈ dom ⁡ F ∀ n ∈ F ⁡ p p ∈ n ∧ ∀ s ∈ 𝒫 dom ⁡ F n ⊆ s → s ∈ F ⁡ p ↔ Fun ⁡ F ∧ ran ⁡ F ⊆ 𝒫 𝒫 dom ⁡ F ∖ ∅ ∖ ∅ ∧ ∀ p ∈ dom ⁡ F ∀ n ∈ F ⁡ p p ∈ n ∧ ∀ s ∈ 𝒫 dom ⁡ F n ⊆ s → s ∈ F ⁡ p
8 2 7 bitrdi ⊢ F ∈ V → F ∈ A ↔ Fun ⁡ F ∧ ran ⁡ F ⊆ 𝒫 𝒫 dom ⁡ F ∖ ∅ ∖ ∅ ∧ ∀ p ∈ dom ⁡ F ∀ n ∈ F ⁡ p p ∈ n ∧ ∀ s ∈ 𝒫 dom ⁡ F n ⊆ s → s ∈ F ⁡ p