Description: A generic neighborhood space has 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 | gneispacern | ⊢ ( 𝐹 ∈ 𝐴 → ran 𝐹 ⊆ ( 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } ) ∖ { ∅ } ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | gneispace.a | ⊢ 𝐴 = { 𝑓 ∣ ( 𝑓 : dom 𝑓 ⟶ ( 𝒫 ( 𝒫 dom 𝑓 ∖ { ∅ } ) ∖ { ∅ } ) ∧ ∀ 𝑝 ∈ dom 𝑓 ∀ 𝑛 ∈ ( 𝑓 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝑓 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝑓 ‘ 𝑝 ) ) ) ) } | |
| 2 | 1 | gneispacef | ⊢ ( 𝐹 ∈ 𝐴 → 𝐹 : dom 𝐹 ⟶ ( 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } ) ∖ { ∅ } ) ) |
| 3 | 2 | frnd | ⊢ ( 𝐹 ∈ 𝐴 → ran 𝐹 ⊆ ( 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } ) ∖ { ∅ } ) ) |