Metamath Proof Explorer

Theorem ntrclsk4

Description: Idempotence of the interior function is equivalent to idempotence of the closure function. (Contributed by RP, 10-Jul-2021)

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

Proof

Step Hyp Ref Expression
1 ntrcls.o ⊢ 𝑂 = ( 𝑖 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑖 ↑m 𝒫 𝑖 ) ↦ ( 𝑗 ∈ 𝒫 𝑖 ↦ ( 𝑖 ∖ ( 𝑘 ‘ ( 𝑖 ∖ 𝑗 ) ) ) ) ) )
2 ntrcls.d ⊢ 𝐷 = ( 𝑂 ‘ 𝐵 )
3 ntrcls.r ⊢ ( 𝜑 → 𝐼 𝐷 𝐾 )
4 2fveq3 ⊢ ( 𝑠 = 𝑡 → ( 𝐼 ‘ ( 𝐼 ‘ 𝑠 ) ) = ( 𝐼 ‘ ( 𝐼 ‘ 𝑡 ) ) )
5 fveq2 ⊢ ( 𝑠 = 𝑡 → ( 𝐼 ‘ 𝑠 ) = ( 𝐼 ‘ 𝑡 ) )
6 4 5 eqeq12d ⊢ ( 𝑠 = 𝑡 → ( ( 𝐼 ‘ ( 𝐼 ‘ 𝑠 ) ) = ( 𝐼 ‘ 𝑠 ) ↔ ( 𝐼 ‘ ( 𝐼 ‘ 𝑡 ) ) = ( 𝐼 ‘ 𝑡 ) ) )
7 6 cbvralvw ⊢ ( ∀ 𝑠 ∈ 𝒫 𝐵 ( 𝐼 ‘ ( 𝐼 ‘ 𝑠 ) ) = ( 𝐼 ‘ 𝑠 ) ↔ ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝐼 ‘ ( 𝐼 ‘ 𝑡 ) ) = ( 𝐼 ‘ 𝑡 ) )
8 2 3 ntrclsrcomplex ⊢ ( 𝜑 → ( 𝐵 ∖ 𝑠 ) ∈ 𝒫 𝐵 )
9 8 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( 𝐵 ∖ 𝑠 ) ∈ 𝒫 𝐵 )
10 2 3 ntrclsrcomplex ⊢ ( 𝜑 → ( 𝐵 ∖ 𝑡 ) ∈ 𝒫 𝐵 )
11 10 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝐵 ∖ 𝑡 ) ∈ 𝒫 𝐵 )
12 difeq2 ⊢ ( 𝑠 = ( 𝐵 ∖ 𝑡 ) → ( 𝐵 ∖ 𝑠 ) = ( 𝐵 ∖ ( 𝐵 ∖ 𝑡 ) ) )
13 12 eqeq2d ⊢ ( 𝑠 = ( 𝐵 ∖ 𝑡 ) → ( 𝑡 = ( 𝐵 ∖ 𝑠 ) ↔ 𝑡 = ( 𝐵 ∖ ( 𝐵 ∖ 𝑡 ) ) ) )
14 13 adantl ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑠 = ( 𝐵 ∖ 𝑡 ) ) → ( 𝑡 = ( 𝐵 ∖ 𝑠 ) ↔ 𝑡 = ( 𝐵 ∖ ( 𝐵 ∖ 𝑡 ) ) ) )
15 elpwi ⊢ ( 𝑡 ∈ 𝒫 𝐵 → 𝑡 ⊆ 𝐵 )
16 dfss4 ⊢ ( 𝑡 ⊆ 𝐵 ↔ ( 𝐵 ∖ ( 𝐵 ∖ 𝑡 ) ) = 𝑡 )
17 15 16 sylib ⊢ ( 𝑡 ∈ 𝒫 𝐵 → ( 𝐵 ∖ ( 𝐵 ∖ 𝑡 ) ) = 𝑡 )
18 17 eqcomd ⊢ ( 𝑡 ∈ 𝒫 𝐵 → 𝑡 = ( 𝐵 ∖ ( 𝐵 ∖ 𝑡 ) ) )
19 18 adantl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝒫 𝐵 ) → 𝑡 = ( 𝐵 ∖ ( 𝐵 ∖ 𝑡 ) ) )
20 11 14 19 rspcedvd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝒫 𝐵 ) → ∃ 𝑠 ∈ 𝒫 𝐵 𝑡 = ( 𝐵 ∖ 𝑠 ) )
21 2fveq3 ⊢ ( 𝑡 = ( 𝐵 ∖ 𝑠 ) → ( 𝐼 ‘ ( 𝐼 ‘ 𝑡 ) ) = ( 𝐼 ‘ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) )
22 fveq2 ⊢ ( 𝑡 = ( 𝐵 ∖ 𝑠 ) → ( 𝐼 ‘ 𝑡 ) = ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) )
23 21 22 eqeq12d ⊢ ( 𝑡 = ( 𝐵 ∖ 𝑠 ) → ( ( 𝐼 ‘ ( 𝐼 ‘ 𝑡 ) ) = ( 𝐼 ‘ 𝑡 ) ↔ ( 𝐼 ‘ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) = ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) )
24 23 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 = ( 𝐵 ∖ 𝑠 ) ) → ( ( 𝐼 ‘ ( 𝐼 ‘ 𝑡 ) ) = ( 𝐼 ‘ 𝑡 ) ↔ ( 𝐼 ‘ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) = ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) )
25 1 2 3 ntrclsiex ⊢ ( 𝜑 → 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
26 elmapi ⊢ ( 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) → 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
27 25 26 syl ⊢ ( 𝜑 → 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
28 27 8 ffvelrnd ⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∈ 𝒫 𝐵 )
29 27 28 ffvelrnd ⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ∈ 𝒫 𝐵 )
30 29 elpwid ⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ⊆ 𝐵 )
31 28 elpwid ⊢ ( 𝜑 → ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ⊆ 𝐵 )
32 rcompleq ⊢ ( ( ( 𝐼 ‘ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ⊆ 𝐵 ∧ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ⊆ 𝐵 ) → ( ( 𝐼 ‘ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) = ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ↔ ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) = ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) )
33 30 31 32 syl2anc ⊢ ( 𝜑 → ( ( 𝐼 ‘ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) = ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ↔ ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) = ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) )
34 33 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( ( 𝐼 ‘ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) = ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ↔ ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) = ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) )
35 1 2 3 ntrclsnvobr ⊢ ( 𝜑 → 𝐾 𝐷 𝐼 )
36 35 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → 𝐾 𝐷 𝐼 )
37 1 2 35 ntrclsiex ⊢ ( 𝜑 → 𝐾 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
38 elmapi ⊢ ( 𝐾 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) → 𝐾 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
39 37 38 syl ⊢ ( 𝜑 → 𝐾 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
40 39 ffvelrnda ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( 𝐾 ‘ 𝑠 ) ∈ 𝒫 𝐵 )
41 1 2 36 40 ntrclsfv ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( 𝐾 ‘ ( 𝐾 ‘ 𝑠 ) ) = ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ ( 𝐾 ‘ 𝑠 ) ) ) ) )
42 simpr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → 𝑠 ∈ 𝒫 𝐵 )
43 1 2 36 42 ntrclsfv ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( 𝐾 ‘ 𝑠 ) = ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) )
44 43 difeq2d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( 𝐵 ∖ ( 𝐾 ‘ 𝑠 ) ) = ( 𝐵 ∖ ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) )
45 dfss4 ⊢ ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ⊆ 𝐵 ↔ ( 𝐵 ∖ ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) = ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) )
46 31 45 sylib ⊢ ( 𝜑 → ( 𝐵 ∖ ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) = ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) )
47 46 adantr ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( 𝐵 ∖ ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) = ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) )
48 44 47 eqtrd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( 𝐵 ∖ ( 𝐾 ‘ 𝑠 ) ) = ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) )
49 48 fveq2d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( 𝐼 ‘ ( 𝐵 ∖ ( 𝐾 ‘ 𝑠 ) ) ) = ( 𝐼 ‘ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) )
50 49 difeq2d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ ( 𝐾 ‘ 𝑠 ) ) ) ) = ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) )
51 41 50 eqtrd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( 𝐾 ‘ ( 𝐾 ‘ 𝑠 ) ) = ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) )
52 51 43 eqeq12d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( ( 𝐾 ‘ ( 𝐾 ‘ 𝑠 ) ) = ( 𝐾 ‘ 𝑠 ) ↔ ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) = ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) )
53 34 52 bitr4d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( ( 𝐼 ‘ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) = ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ↔ ( 𝐾 ‘ ( 𝐾 ‘ 𝑠 ) ) = ( 𝐾 ‘ 𝑠 ) ) )
54 53 3adant3 ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 = ( 𝐵 ∖ 𝑠 ) ) → ( ( 𝐼 ‘ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) = ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ↔ ( 𝐾 ‘ ( 𝐾 ‘ 𝑠 ) ) = ( 𝐾 ‘ 𝑠 ) ) )
55 24 54 bitrd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 = ( 𝐵 ∖ 𝑠 ) ) → ( ( 𝐼 ‘ ( 𝐼 ‘ 𝑡 ) ) = ( 𝐼 ‘ 𝑡 ) ↔ ( 𝐾 ‘ ( 𝐾 ‘ 𝑠 ) ) = ( 𝐾 ‘ 𝑠 ) ) )
56 9 20 55 ralxfrd2 ⊢ ( 𝜑 → ( ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝐼 ‘ ( 𝐼 ‘ 𝑡 ) ) = ( 𝐼 ‘ 𝑡 ) ↔ ∀ 𝑠 ∈ 𝒫 𝐵 ( 𝐾 ‘ ( 𝐾 ‘ 𝑠 ) ) = ( 𝐾 ‘ 𝑠 ) ) )
57 7 56 syl5bb ⊢ ( 𝜑 → ( ∀ 𝑠 ∈ 𝒫 𝐵 ( 𝐼 ‘ ( 𝐼 ‘ 𝑠 ) ) = ( 𝐼 ‘ 𝑠 ) ↔ ∀ 𝑠 ∈ 𝒫 𝐵 ( 𝐾 ‘ ( 𝐾 ‘ 𝑠 ) ) = ( 𝐾 ‘ 𝑠 ) ) )