Theorem ntrneibex

Description: If (pseudo-)interior and (pseudo-)neighborhood functions are related by the operator, F , then the base set exists. (Contributed by RP, 29-May-2021)

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

Proof

Step	Hyp	Ref	Expression
1		ntrnei.o	⊢ 𝑂 = ( 𝑖 ∈ V , 𝑗 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑗 ↑m 𝑖 ) ↦ ( 𝑙 ∈ 𝑗 ↦ { 𝑚 ∈ 𝑖 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) ) )
2		ntrnei.f	⊢ 𝐹 = ( 𝒫 𝐵 𝑂 𝐵 )
3		ntrnei.r	⊢ ( 𝜑 → 𝐼 𝐹 𝑁 )
4		oveq2	⊢ ( 𝑖 = 𝑎 → ( 𝒫 𝑗 ↑m 𝑖 ) = ( 𝒫 𝑗 ↑m 𝑎 ) )
5		rabeq	⊢ ( 𝑖 = 𝑎 → { 𝑚 ∈ 𝑖 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } = { 𝑚 ∈ 𝑎 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } )
6	5	mpteq2dv	⊢ ( 𝑖 = 𝑎 → ( 𝑙 ∈ 𝑗 ↦ { 𝑚 ∈ 𝑖 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) = ( 𝑙 ∈ 𝑗 ↦ { 𝑚 ∈ 𝑎 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) )
7	4 6	mpteq12dv	⊢ ( 𝑖 = 𝑎 → ( 𝑘 ∈ ( 𝒫 𝑗 ↑m 𝑖 ) ↦ ( 𝑙 ∈ 𝑗 ↦ { 𝑚 ∈ 𝑖 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) ) = ( 𝑘 ∈ ( 𝒫 𝑗 ↑m 𝑎 ) ↦ ( 𝑙 ∈ 𝑗 ↦ { 𝑚 ∈ 𝑎 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) ) )
8		pweq	⊢ ( 𝑗 = 𝑏 → 𝒫 𝑗 = 𝒫 𝑏 )
9	8	oveq1d	⊢ ( 𝑗 = 𝑏 → ( 𝒫 𝑗 ↑m 𝑎 ) = ( 𝒫 𝑏 ↑m 𝑎 ) )
10		mpteq1	⊢ ( 𝑗 = 𝑏 → ( 𝑙 ∈ 𝑗 ↦ { 𝑚 ∈ 𝑎 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) = ( 𝑙 ∈ 𝑏 ↦ { 𝑚 ∈ 𝑎 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) )
11	9 10	mpteq12dv	⊢ ( 𝑗 = 𝑏 → ( 𝑘 ∈ ( 𝒫 𝑗 ↑m 𝑎 ) ↦ ( 𝑙 ∈ 𝑗 ↦ { 𝑚 ∈ 𝑎 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) ) = ( 𝑘 ∈ ( 𝒫 𝑏 ↑m 𝑎 ) ↦ ( 𝑙 ∈ 𝑏 ↦ { 𝑚 ∈ 𝑎 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) ) )
12	7 11	cbvmpov	⊢ ( 𝑖 ∈ V , 𝑗 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑗 ↑m 𝑖 ) ↦ ( 𝑙 ∈ 𝑗 ↦ { 𝑚 ∈ 𝑖 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) ) ) = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑏 ↑m 𝑎 ) ↦ ( 𝑙 ∈ 𝑏 ↦ { 𝑚 ∈ 𝑎 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) ) )
13	1 12	eqtri	⊢ 𝑂 = ( 𝑎 ∈ V , 𝑏 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑏 ↑m 𝑎 ) ↦ ( 𝑙 ∈ 𝑏 ↦ { 𝑚 ∈ 𝑎 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) ) )
14	2	a1i	⊢ ( 𝜑 → 𝐹 = ( 𝒫 𝐵 𝑂 𝐵 ) )
15	13 3 14	brovmptimex2	⊢ ( 𝜑 → 𝐵 ∈ V )