Metamath Proof Explorer

Theorem gneispace2

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 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

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 id ⊢ f = F → f = F
3 dmeq ⊢ f = F → dom ⁡ f = dom ⁡ F
4 3 pweqd ⊢ f = F → 𝒫 dom ⁡ f = 𝒫 dom ⁡ F
5 4 difeq1d ⊢ f = F → 𝒫 dom ⁡ f ∖ ∅ = 𝒫 dom ⁡ F ∖ ∅
6 5 pweqd ⊢ f = F → 𝒫 𝒫 dom ⁡ f ∖ ∅ = 𝒫 𝒫 dom ⁡ F ∖ ∅
7 6 difeq1d ⊢ f = F → 𝒫 𝒫 dom ⁡ f ∖ ∅ ∖ ∅ = 𝒫 𝒫 dom ⁡ F ∖ ∅ ∖ ∅
8 2 3 7 feq123d ⊢ f = F → f : dom ⁡ f ⟶ 𝒫 𝒫 dom ⁡ f ∖ ∅ ∖ ∅ ↔ F : dom ⁡ F ⟶ 𝒫 𝒫 dom ⁡ F ∖ ∅ ∖ ∅
9 fveq1 ⊢ f = F → f ⁡ p = F ⁡ p
10 9 eleq2d ⊢ f = F → s ∈ f ⁡ p ↔ s ∈ F ⁡ p
11 10 imbi2d ⊢ f = F → n ⊆ s → s ∈ f ⁡ p ↔ n ⊆ s → s ∈ F ⁡ p
12 4 11 raleqbidv ⊢ f = F → ∀ s ∈ 𝒫 dom ⁡ f n ⊆ s → s ∈ f ⁡ p ↔ ∀ s ∈ 𝒫 dom ⁡ F n ⊆ s → s ∈ F ⁡ p
13 12 anbi2d ⊢ f = F → p ∈ n ∧ ∀ s ∈ 𝒫 dom ⁡ f n ⊆ s → s ∈ f ⁡ p ↔ p ∈ n ∧ ∀ s ∈ 𝒫 dom ⁡ F n ⊆ s → s ∈ F ⁡ p
14 9 13 raleqbidv ⊢ f = F → ∀ n ∈ f ⁡ p p ∈ n ∧ ∀ s ∈ 𝒫 dom ⁡ f n ⊆ s → s ∈ f ⁡ p ↔ ∀ n ∈ F ⁡ p p ∈ n ∧ ∀ s ∈ 𝒫 dom ⁡ F n ⊆ s → s ∈ F ⁡ p
15 3 14 raleqbidv ⊢ f = F → ∀ p ∈ dom ⁡ f ∀ n ∈ f ⁡ p p ∈ n ∧ ∀ s ∈ 𝒫 dom ⁡ f n ⊆ s → s ∈ f ⁡ p ↔ ∀ p ∈ dom ⁡ F ∀ n ∈ F ⁡ p p ∈ n ∧ ∀ s ∈ 𝒫 dom ⁡ F n ⊆ s → s ∈ F ⁡ p
16 8 15 anbi12d ⊢ f = F → f : dom ⁡ f ⟶ 𝒫 𝒫 dom ⁡ f ∖ ∅ ∖ ∅ ∧ ∀ p ∈ dom ⁡ f ∀ n ∈ f ⁡ p p ∈ n ∧ ∀ s ∈ 𝒫 dom ⁡ f n ⊆ s → s ∈ f ⁡ p ↔ F : dom ⁡ F ⟶ 𝒫 𝒫 dom ⁡ F ∖ ∅ ∖ ∅ ∧ ∀ p ∈ dom ⁡ F ∀ n ∈ F ⁡ p p ∈ n ∧ ∀ s ∈ 𝒫 dom ⁡ F n ⊆ s → s ∈ F ⁡ p
17 16 1 elab2g ⊢ 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