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

Proof

Step	Hyp	Ref	Expression
1		gneispace.a	⊢ 𝐴 = { 𝑓 ∣ ( 𝑓 : dom 𝑓 ⟶ ( 𝒫 ( 𝒫 dom 𝑓 ∖ { ∅ } ) ∖ { ∅ } ) ∧ ∀ 𝑝 ∈ dom 𝑓 ∀ 𝑛 ∈ ( 𝑓 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝑓 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝑓 ‘ 𝑝 ) ) ) ) }
2		id	⊢ ( 𝑓 = 𝐹 → 𝑓 = 𝐹 )
3		dmeq	⊢ ( 𝑓 = 𝐹 → dom 𝑓 = dom 𝐹 )
4	3	pweqd	⊢ ( 𝑓 = 𝐹 → 𝒫 dom 𝑓 = 𝒫 dom 𝐹 )
5	4	difeq1d	⊢ ( 𝑓 = 𝐹 → ( 𝒫 dom 𝑓 ∖ { ∅ } ) = ( 𝒫 dom 𝐹 ∖ { ∅ } ) )
6	5	pweqd	⊢ ( 𝑓 = 𝐹 → 𝒫 ( 𝒫 dom 𝑓 ∖ { ∅ } ) = 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } ) )
7	6	difeq1d	⊢ ( 𝑓 = 𝐹 → ( 𝒫 ( 𝒫 dom 𝑓 ∖ { ∅ } ) ∖ { ∅ } ) = ( 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } ) ∖ { ∅ } ) )
8	2 3 7	feq123d	⊢ ( 𝑓 = 𝐹 → ( 𝑓 : dom 𝑓 ⟶ ( 𝒫 ( 𝒫 dom 𝑓 ∖ { ∅ } ) ∖ { ∅ } ) ↔ 𝐹 : dom 𝐹 ⟶ ( 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } ) ∖ { ∅ } ) ) )
9		fveq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 ‘ 𝑝 ) = ( 𝐹 ‘ 𝑝 ) )
10	9	eleq2d	⊢ ( 𝑓 = 𝐹 → ( 𝑠 ∈ ( 𝑓 ‘ 𝑝 ) ↔ 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) )
11	10	imbi2d	⊢ ( 𝑓 = 𝐹 → ( ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝑓 ‘ 𝑝 ) ) ↔ ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) )
12	4 11	raleqbidv	⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑠 ∈ 𝒫 dom 𝑓 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝑓 ‘ 𝑝 ) ) ↔ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) )
13	12	anbi2d	⊢ ( 𝑓 = 𝐹 → ( ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝑓 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝑓 ‘ 𝑝 ) ) ) ↔ ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) )
14	9 13	raleqbidv	⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑛 ∈ ( 𝑓 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝑓 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝑓 ‘ 𝑝 ) ) ) ↔ ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) )
15	3 14	raleqbidv	⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑝 ∈ dom 𝑓 ∀ 𝑛 ∈ ( 𝑓 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝑓 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝑓 ‘ 𝑝 ) ) ) ↔ ∀ 𝑝 ∈ dom 𝐹 ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) )
16	8 15	anbi12d	⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 : dom 𝑓 ⟶ ( 𝒫 ( 𝒫 dom 𝑓 ∖ { ∅ } ) ∖ { ∅ } ) ∧ ∀ 𝑝 ∈ dom 𝑓 ∀ 𝑛 ∈ ( 𝑓 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝑓 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝑓 ‘ 𝑝 ) ) ) ) ↔ ( 𝐹 : dom 𝐹 ⟶ ( 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } ) ∖ { ∅ } ) ∧ ∀ 𝑝 ∈ dom 𝐹 ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) ) )
17	16 1	elab2g	⊢ ( 𝐹 ∈ 𝑉 → ( 𝐹 ∈ 𝐴 ↔ ( 𝐹 : dom 𝐹 ⟶ ( 𝒫 ( 𝒫 dom 𝐹 ∖ { ∅ } ) ∖ { ∅ } ) ∧ ∀ 𝑝 ∈ dom 𝐹 ∀ 𝑛 ∈ ( 𝐹 ‘ 𝑝 ) ( 𝑝 ∈ 𝑛 ∧ ∀ 𝑠 ∈ 𝒫 dom 𝐹 ( 𝑛 ⊆ 𝑠 → 𝑠 ∈ ( 𝐹 ‘ 𝑝 ) ) ) ) ) )