Metamath Proof Explorer

Theorem ntrclscls00

Description: If (pseudo-)interior and (pseudo-)closure functions are related by the duality operator then conditions equal to claiming that the closure of the empty set is the empty set hold equally. (Contributed by RP, 1-Jun-2021)

Ref Expression
Hypotheses ntrcls.o ⊢ 𝑂 = ( 𝑖 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑖 ↑m 𝒫 𝑖 ) ↦ ( 𝑗 ∈ 𝒫 𝑖 ↦ ( 𝑖 ∖ ( 𝑘 ‘ ( 𝑖 ∖ 𝑗 ) ) ) ) ) )
ntrcls.d ⊢ 𝐷 = ( 𝑂 ‘ 𝐵 )
ntrcls.r ⊢ ( 𝜑 → 𝐼 𝐷 𝐾 )
Assertion ntrclscls00 ( 𝜑 → ( ( 𝐼 ‘ 𝐵 ) = 𝐵 ↔ ( 𝐾 ‘ ∅ ) = ∅ ) )

Proof

Step Hyp Ref Expression
1 ntrcls.o ⊢ 𝑂 = ( 𝑖 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑖 ↑m 𝒫 𝑖 ) ↦ ( 𝑗 ∈ 𝒫 𝑖 ↦ ( 𝑖 ∖ ( 𝑘 ‘ ( 𝑖 ∖ 𝑗 ) ) ) ) ) )
2 ntrcls.d ⊢ 𝐷 = ( 𝑂 ‘ 𝐵 )
3 ntrcls.r ⊢ ( 𝜑 → 𝐼 𝐷 𝐾 )
4 1 2 3 ntrclsfv1 ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐼 ) = 𝐾 )
5 4 fveq1d ⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝐼 ) ‘ ∅ ) = ( 𝐾 ‘ ∅ ) )
6 2 3 ntrclsbex ⊢ ( 𝜑 → 𝐵 ∈ V )
7 1 2 3 ntrclsiex ⊢ ( 𝜑 → 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
8 eqid ⊢ ( 𝐷 ‘ 𝐼 ) = ( 𝐷 ‘ 𝐼 )
9 0elpw ⊢ ∅ ∈ 𝒫 𝐵
10 9 a1i ⊢ ( 𝜑 → ∅ ∈ 𝒫 𝐵 )
11 eqid ⊢ ( ( 𝐷 ‘ 𝐼 ) ‘ ∅ ) = ( ( 𝐷 ‘ 𝐼 ) ‘ ∅ )
12 1 2 6 7 8 10 11 dssmapfv3d ⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝐼 ) ‘ ∅ ) = ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ ∅ ) ) ) )
13 5 12 eqtr3d ⊢ ( 𝜑 → ( 𝐾 ‘ ∅ ) = ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ ∅ ) ) ) )
14 dif0 ⊢ ( 𝐵 ∖ ∅ ) = 𝐵
15 14 fveq2i ⊢ ( 𝐼 ‘ ( 𝐵 ∖ ∅ ) ) = ( 𝐼 ‘ 𝐵 )
16 id ⊢ ( ( 𝐼 ‘ 𝐵 ) = 𝐵 → ( 𝐼 ‘ 𝐵 ) = 𝐵 )
17 15 16 syl5eq ⊢ ( ( 𝐼 ‘ 𝐵 ) = 𝐵 → ( 𝐼 ‘ ( 𝐵 ∖ ∅ ) ) = 𝐵 )
18 17 difeq2d ⊢ ( ( 𝐼 ‘ 𝐵 ) = 𝐵 → ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ ∅ ) ) ) = ( 𝐵 ∖ 𝐵 ) )
19 difid ⊢ ( 𝐵 ∖ 𝐵 ) = ∅
20 18 19 eqtrdi ⊢ ( ( 𝐼 ‘ 𝐵 ) = 𝐵 → ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ ∅ ) ) ) = ∅ )
21 13 20 sylan9eq ⊢ ( ( 𝜑 ∧ ( 𝐼 ‘ 𝐵 ) = 𝐵 ) → ( 𝐾 ‘ ∅ ) = ∅ )
22 pwidg ⊢ ( 𝐵 ∈ V → 𝐵 ∈ 𝒫 𝐵 )
23 6 22 syl ⊢ ( 𝜑 → 𝐵 ∈ 𝒫 𝐵 )
24 1 2 3 23 ntrclsfv ⊢ ( 𝜑 → ( 𝐼 ‘ 𝐵 ) = ( 𝐵 ∖ ( 𝐾 ‘ ( 𝐵 ∖ 𝐵 ) ) ) )
25 19 fveq2i ⊢ ( 𝐾 ‘ ( 𝐵 ∖ 𝐵 ) ) = ( 𝐾 ‘ ∅ )
26 id ⊢ ( ( 𝐾 ‘ ∅ ) = ∅ → ( 𝐾 ‘ ∅ ) = ∅ )
27 25 26 syl5eq ⊢ ( ( 𝐾 ‘ ∅ ) = ∅ → ( 𝐾 ‘ ( 𝐵 ∖ 𝐵 ) ) = ∅ )
28 27 difeq2d ⊢ ( ( 𝐾 ‘ ∅ ) = ∅ → ( 𝐵 ∖ ( 𝐾 ‘ ( 𝐵 ∖ 𝐵 ) ) ) = ( 𝐵 ∖ ∅ ) )
29 28 14 eqtrdi ⊢ ( ( 𝐾 ‘ ∅ ) = ∅ → ( 𝐵 ∖ ( 𝐾 ‘ ( 𝐵 ∖ 𝐵 ) ) ) = 𝐵 )
30 24 29 sylan9eq ⊢ ( ( 𝜑 ∧ ( 𝐾 ‘ ∅ ) = ∅ ) → ( 𝐼 ‘ 𝐵 ) = 𝐵 )
31 21 30 impbida ⊢ ( 𝜑 → ( ( 𝐼 ‘ 𝐵 ) = 𝐵 ↔ ( 𝐾 ‘ ∅ ) = ∅ ) )