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	⊢ 𝐴 = { 𝑓 ∣ ( 𝑓 : dom 𝑓 ⟶ ( 𝒫 ( 𝒫 dom 𝑓 ∖ { ∅ } ) ∖ { ∅ } ) ∧ ∀ 𝑝 ∈ dom 𝑓 ∀ 𝑛 ∈ ( 𝑓 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝑓 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝑓 ‘ 𝑝 ) ) ) ) }
Assertion	gneispace3	⊢ ( 𝐹 ∈ 𝑉 → ( 𝐹 ∈ 𝐴 ↔ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ ( 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } ) ∖ { ∅ } ) ) ∧ ∀ 𝑝 ∈ dom 𝐹 ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		gneispace.a	⊢ 𝐴 = { 𝑓 ∣ ( 𝑓 : dom 𝑓 ⟶ ( 𝒫 ( 𝒫 dom 𝑓 ∖ { ∅ } ) ∖ { ∅ } ) ∧ ∀ 𝑝 ∈ dom 𝑓 ∀ 𝑛 ∈ ( 𝑓 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝑓 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝑓 ‘ 𝑝 ) ) ) ) }
2	1	gneispace2	⊢ ( 𝐹 ∈ 𝑉 → ( 𝐹 ∈ 𝐴 ↔ ( 𝐹 : dom 𝐹 ⟶ ( 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } ) ∖ { ∅ } ) ∧ ∀ 𝑝 ∈ dom 𝐹 ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) ) )
3		df-f	⊢ ( 𝐹 : dom 𝐹 ⟶ ( 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } ) ∖ { ∅ } ) ↔ ( 𝐹 Fn dom 𝐹 ∧ ran 𝐹 ⊆ ( 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } ) ∖ { ∅ } ) ) )
4		funfn	⊢ ( Fun 𝐹 ↔ 𝐹 Fn dom 𝐹 )
5	4	anbi1i	⊢ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ ( 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } ) ∖ { ∅ } ) ) ↔ ( 𝐹 Fn dom 𝐹 ∧ ran 𝐹 ⊆ ( 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } ) ∖ { ∅ } ) ) )
6	3 5	bitr4i	⊢ ( 𝐹 : dom 𝐹 ⟶ ( 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } ) ∖ { ∅ } ) ↔ ( Fun 𝐹 ∧ ran 𝐹 ⊆ ( 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } ) ∖ { ∅ } ) ) )
7	6	anbi1i	⊢ ( ( 𝐹 : dom 𝐹 ⟶ ( 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } ) ∖ { ∅ } ) ∧ ∀ 𝑝 ∈ dom 𝐹 ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) ↔ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ ( 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } ) ∖ { ∅ } ) ) ∧ ∀ 𝑝 ∈ dom 𝐹 ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) )
8	2 7	bitrdi	⊢ ( 𝐹 ∈ 𝑉 → ( 𝐹 ∈ 𝐴 ↔ ( ( Fun 𝐹 ∧ ran 𝐹 ⊆ ( 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } ) ∖ { ∅ } ) ) ∧ ∀ 𝑝 ∈ dom 𝐹 ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) ) )