Theorem ntrneifv1

Description: If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, F , then the function value of F is the neighborhood function. (Contributed by RP, 29-May-2021)

	Ref	Expression
Hypotheses	ntrnei.o	⊢ 𝑂 = ( 𝑖 ∈ V , 𝑗 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑗 ↑m 𝑖 ) ↦ ( 𝑙 ∈ 𝑗 ↦ { 𝑚 ∈ 𝑖 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) ) )
	ntrnei.f	⊢ 𝐹 = ( 𝒫 𝐵 𝑂 𝐵 )
	ntrnei.r	⊢ ( 𝜑 → 𝐼 𝐹 𝑁 )
Assertion	ntrneifv1	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐼 ) = 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		ntrnei.o	⊢ 𝑂 = ( 𝑖 ∈ V , 𝑗 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑗 ↑m 𝑖 ) ↦ ( 𝑙 ∈ 𝑗 ↦ { 𝑚 ∈ 𝑖 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) ) )
2		ntrnei.f	⊢ 𝐹 = ( 𝒫 𝐵 𝑂 𝐵 )
3		ntrnei.r	⊢ ( 𝜑 → 𝐼 𝐹 𝑁 )
4	1 2 3	ntrneif1o	⊢ ( 𝜑 → 𝐹 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) )
5		f1ofn	⊢ ( 𝐹 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) → 𝐹 Fn ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
6	4 5	syl	⊢ ( 𝜑 → 𝐹 Fn ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
7	1 2 3	ntrneiiex	⊢ ( 𝜑 → 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
8	6 7	jca	⊢ ( 𝜑 → ( 𝐹 Fn ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ∧ 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) )
9		fnfun	⊢ ( 𝐹 Fn ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) → Fun 𝐹 )
10	9	adantr	⊢ ( ( 𝐹 Fn ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ∧ 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) → Fun 𝐹 )
11		fndm	⊢ ( 𝐹 Fn ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) → dom 𝐹 = ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
12	11	eleq2d	⊢ ( 𝐹 Fn ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) → ( 𝐼 ∈ dom 𝐹 ↔ 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) )
13	12	biimpar	⊢ ( ( 𝐹 Fn ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ∧ 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) → 𝐼 ∈ dom 𝐹 )
14	10 13	jca	⊢ ( ( 𝐹 Fn ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ∧ 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) → ( Fun 𝐹 ∧ 𝐼 ∈ dom 𝐹 ) )
15		funbrfvb	⊢ ( ( Fun 𝐹 ∧ 𝐼 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝐼 ) = 𝑁 ↔ 𝐼 𝐹 𝑁 ) )
16	8 14 15	3syl	⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝐼 ) = 𝑁 ↔ 𝐼 𝐹 𝑁 ) )
17	3 16	mpbird	⊢ ( 𝜑 → ( 𝐹 ‘ 𝐼 ) = 𝑁 )