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 O = i V k 𝒫 i 𝒫 i j 𝒫 i i k i j
ntrcls.d D = O B
ntrcls.r φ I D K
Assertion ntrclscls00 φ I B = B K =

Proof

Step Hyp Ref Expression
1 ntrcls.o O = i V k 𝒫 i 𝒫 i j 𝒫 i i k i j
2 ntrcls.d D = O B
3 ntrcls.r φ I D K
4 1 2 3 ntrclsfv1 φ D I = K
5 4 fveq1d φ D I = K
6 2 3 ntrclsbex φ B V
7 1 2 3 ntrclsiex φ I 𝒫 B 𝒫 B
8 eqid D I = D I
9 0elpw 𝒫 B
10 9 a1i φ 𝒫 B
11 eqid D I = D I
12 1 2 6 7 8 10 11 dssmapfv3d φ D I = B I B
13 5 12 eqtr3d φ K = B I B
14 dif0 B = B
15 14 fveq2i I B = I B
16 id I B = B I B = B
17 15 16 syl5eq I B = B I B = B
18 17 difeq2d I B = B B I B = B B
19 difid B B =
20 18 19 syl6eq I B = B B I B =
21 13 20 sylan9eq φ I B = B K =
22 pwidg B V B 𝒫 B
23 6 22 syl φ B 𝒫 B
24 1 2 3 23 ntrclsfv φ I B = B K B B
25 19 fveq2i K B B = K
26 id K = K =
27 25 26 syl5eq K = K B B =
28 27 difeq2d K = B K B B = B
29 28 14 syl6eq K = B K B B = B
30 24 29 sylan9eq φ K = I B = B
31 21 30 impbida φ I B = B K =