Metamath Proof Explorer

Theorem ntrneifv2

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

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

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 1 2 3 ntrneinex ⊢ ( 𝜑 → 𝑁 ∈ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) )
6 dff1o3 ⊢ ( 𝐹 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) ↔ ( 𝐹 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –onto→ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) ∧ Fun ◡ 𝐹 ) )
7 6 simprbi ⊢ ( 𝐹 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) → Fun ◡ 𝐹 )
8 7 adantr ⊢ ( ( 𝐹 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) ∧ 𝑁 ∈ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) ) → Fun ◡ 𝐹 )
9 df-rn ⊢ ran 𝐹 = dom ◡ 𝐹
10 f1ofo ⊢ ( 𝐹 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) → 𝐹 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –onto→ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) )
11 forn ⊢ ( 𝐹 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –onto→ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) → ran 𝐹 = ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) )
12 10 11 syl ⊢ ( 𝐹 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) → ran 𝐹 = ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) )
13 9 12 eqtr3id ⊢ ( 𝐹 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) → dom ◡ 𝐹 = ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) )
14 13 eleq2d ⊢ ( 𝐹 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) → ( 𝑁 ∈ dom ◡ 𝐹 ↔ 𝑁 ∈ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) ) )
15 14 biimpar ⊢ ( ( 𝐹 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) ∧ 𝑁 ∈ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) ) → 𝑁 ∈ dom ◡ 𝐹 )
16 8 15 jca ⊢ ( ( 𝐹 : ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) –1-1-onto→ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) ∧ 𝑁 ∈ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) ) → ( Fun ◡ 𝐹 ∧ 𝑁 ∈ dom ◡ 𝐹 ) )
17 4 5 16 syl2anc ⊢ ( 𝜑 → ( Fun ◡ 𝐹 ∧ 𝑁 ∈ dom ◡ 𝐹 ) )
18 funbrfvb ⊢ ( ( Fun ◡ 𝐹 ∧ 𝑁 ∈ dom ◡ 𝐹 ) → ( ( ◡ 𝐹 ‘ 𝑁 ) = 𝐼 ↔ 𝑁 ◡ 𝐹 𝐼 ) )
19 17 18 syl ⊢ ( 𝜑 → ( ( ◡ 𝐹 ‘ 𝑁 ) = 𝐼 ↔ 𝑁 ◡ 𝐹 𝐼 ) )
20 1 2 3 ntrneiiex ⊢ ( 𝜑 → 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
21 brcnvg ⊢ ( ( 𝑁 ∈ ( 𝒫 𝒫 𝐵 ↑m 𝐵 ) ∧ 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) → ( 𝑁 ◡ 𝐹 𝐼 ↔ 𝐼 𝐹 𝑁 ) )
22 5 20 21 syl2anc ⊢ ( 𝜑 → ( 𝑁 ◡ 𝐹 𝐼 ↔ 𝐼 𝐹 𝑁 ) )
23 19 22 bitrd ⊢ ( 𝜑 → ( ( ◡ 𝐹 ‘ 𝑁 ) = 𝐼 ↔ 𝐼 𝐹 𝑁 ) )
24 3 23 mpbird ⊢ ( 𝜑 → ( ◡ 𝐹 ‘ 𝑁 ) = 𝐼 )