Metamath Proof Explorer

Theorem ntrclsk2

Description: An interior function is contracting if and only if the closure function is expansive. (Contributed by RP, 9-Jun-2021)

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

Proof

Step Hyp Ref Expression
1 ntrcls.o ⊢ 𝑂 = ( 𝑖 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑖 ↑m 𝒫 𝑖 ) ↦ ( 𝑗 ∈ 𝒫 𝑖 ↦ ( 𝑖 ∖ ( 𝑘 ‘ ( 𝑖 ∖ 𝑗 ) ) ) ) ) )
2 ntrcls.d ⊢ 𝐷 = ( 𝑂 ‘ 𝐵 )
3 ntrcls.r ⊢ ( 𝜑 → 𝐼 𝐷 𝐾 )
4 fveq2 ⊢ ( 𝑠 = 𝑡 → ( 𝐼 ‘ 𝑠 ) = ( 𝐼 ‘ 𝑡 ) )
5 id ⊢ ( 𝑠 = 𝑡 → 𝑠 = 𝑡 )
6 4 5 sseq12d ⊢ ( 𝑠 = 𝑡 → ( ( 𝐼 ‘ 𝑠 ) ⊆ 𝑠 ↔ ( 𝐼 ‘ 𝑡 ) ⊆ 𝑡 ) )
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 adantl ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝐵 ∖ ( 𝐵 ∖ 𝑡 ) ) = 𝑡 )
19 18 eqcomd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝒫 𝐵 ) → 𝑡 = ( 𝐵 ∖ ( 𝐵 ∖ 𝑡 ) ) )
20 11 14 19 rspcedvd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝒫 𝐵 ) → ∃ 𝑠 ∈ 𝒫 𝐵 𝑡 = ( 𝐵 ∖ 𝑠 ) )
21 fveq2 ⊢ ( 𝑡 = ( 𝐵 ∖ 𝑠 ) → ( 𝐼 ‘ 𝑡 ) = ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) )
22 id ⊢ ( 𝑡 = ( 𝐵 ∖ 𝑠 ) → 𝑡 = ( 𝐵 ∖ 𝑠 ) )
23 21 22 sseq12d ⊢ ( 𝑡 = ( 𝐵 ∖ 𝑠 ) → ( ( 𝐼 ‘ 𝑡 ) ⊆ 𝑡 ↔ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ⊆ ( 𝐵 ∖ 𝑠 ) ) )
24 23 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 = ( 𝐵 ∖ 𝑠 ) ) → ( ( 𝐼 ‘ 𝑡 ) ⊆ 𝑡 ↔ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ⊆ ( 𝐵 ∖ 𝑠 ) ) )
25 1 2 3 ntrclsiex ⊢ ( 𝜑 → 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
26 elmapi ⊢ ( 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) → 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
27 25 26 syl ⊢ ( 𝜑 → 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
28 27 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 = ( 𝐵 ∖ 𝑠 ) ) → 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
29 8 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 = ( 𝐵 ∖ 𝑠 ) ) → ( 𝐵 ∖ 𝑠 ) ∈ 𝒫 𝐵 )
30 28 29 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 = ( 𝐵 ∖ 𝑠 ) ) → ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ∈ 𝒫 𝐵 )
31 30 elpwid ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 = ( 𝐵 ∖ 𝑠 ) ) → ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ⊆ 𝐵 )
32 difssd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 = ( 𝐵 ∖ 𝑠 ) ) → ( 𝐵 ∖ 𝑠 ) ⊆ 𝐵 )
33 sscon34b ⊢ ( ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ⊆ 𝐵 ∧ ( 𝐵 ∖ 𝑠 ) ⊆ 𝐵 ) → ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ⊆ ( 𝐵 ∖ 𝑠 ) ↔ ( 𝐵 ∖ ( 𝐵 ∖ 𝑠 ) ) ⊆ ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) )
34 31 32 33 syl2anc ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 = ( 𝐵 ∖ 𝑠 ) ) → ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ⊆ ( 𝐵 ∖ 𝑠 ) ↔ ( 𝐵 ∖ ( 𝐵 ∖ 𝑠 ) ) ⊆ ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) )
35 simp2 ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 = ( 𝐵 ∖ 𝑠 ) ) → 𝑠 ∈ 𝒫 𝐵 )
36 elpwi ⊢ ( 𝑠 ∈ 𝒫 𝐵 → 𝑠 ⊆ 𝐵 )
37 dfss4 ⊢ ( 𝑠 ⊆ 𝐵 ↔ ( 𝐵 ∖ ( 𝐵 ∖ 𝑠 ) ) = 𝑠 )
38 36 37 sylib ⊢ ( 𝑠 ∈ 𝒫 𝐵 → ( 𝐵 ∖ ( 𝐵 ∖ 𝑠 ) ) = 𝑠 )
39 38 sseq1d ⊢ ( 𝑠 ∈ 𝒫 𝐵 → ( ( 𝐵 ∖ ( 𝐵 ∖ 𝑠 ) ) ⊆ ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ↔ 𝑠 ⊆ ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) )
40 35 39 syl ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 = ( 𝐵 ∖ 𝑠 ) ) → ( ( 𝐵 ∖ ( 𝐵 ∖ 𝑠 ) ) ⊆ ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ↔ 𝑠 ⊆ ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) )
41 34 40 bitrd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 = ( 𝐵 ∖ 𝑠 ) ) → ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ⊆ ( 𝐵 ∖ 𝑠 ) ↔ 𝑠 ⊆ ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) )
42 2 3 ntrclsbex ⊢ ( 𝜑 → 𝐵 ∈ V )
43 42 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 = ( 𝐵 ∖ 𝑠 ) ) → 𝐵 ∈ V )
44 25 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 = ( 𝐵 ∖ 𝑠 ) ) → 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
45 eqid ⊢ ( 𝐷 ‘ 𝐼 ) = ( 𝐷 ‘ 𝐼 )
46 eqid ⊢ ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑠 ) = ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑠 )
47 1 2 43 44 45 35 46 dssmapfv3d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 = ( 𝐵 ∖ 𝑠 ) ) → ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑠 ) = ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) )
48 47 sseq2d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 = ( 𝐵 ∖ 𝑠 ) ) → ( 𝑠 ⊆ ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑠 ) ↔ 𝑠 ⊆ ( 𝐵 ∖ ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ) ) )
49 1 2 3 ntrclsfv1 ⊢ ( 𝜑 → ( 𝐷 ‘ 𝐼 ) = 𝐾 )
50 49 fveq1d ⊢ ( 𝜑 → ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑠 ) = ( 𝐾 ‘ 𝑠 ) )
51 50 sseq2d ⊢ ( 𝜑 → ( 𝑠 ⊆ ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑠 ) ↔ 𝑠 ⊆ ( 𝐾 ‘ 𝑠 ) ) )
52 51 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 = ( 𝐵 ∖ 𝑠 ) ) → ( 𝑠 ⊆ ( ( 𝐷 ‘ 𝐼 ) ‘ 𝑠 ) ↔ 𝑠 ⊆ ( 𝐾 ‘ 𝑠 ) ) )
53 41 48 52 3bitr2d ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 = ( 𝐵 ∖ 𝑠 ) ) → ( ( 𝐼 ‘ ( 𝐵 ∖ 𝑠 ) ) ⊆ ( 𝐵 ∖ 𝑠 ) ↔ 𝑠 ⊆ ( 𝐾 ‘ 𝑠 ) ) )
54 24 53 bitrd ⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ∧ 𝑡 = ( 𝐵 ∖ 𝑠 ) ) → ( ( 𝐼 ‘ 𝑡 ) ⊆ 𝑡 ↔ 𝑠 ⊆ ( 𝐾 ‘ 𝑠 ) ) )
55 9 20 54 ralxfrd2 ⊢ ( 𝜑 → ( ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝐼 ‘ 𝑡 ) ⊆ 𝑡 ↔ ∀ 𝑠 ∈ 𝒫 𝐵 𝑠 ⊆ ( 𝐾 ‘ 𝑠 ) ) )
56 7 55 syl5bb ⊢ ( 𝜑 → ( ∀ 𝑠 ∈ 𝒫 𝐵 ( 𝐼 ‘ 𝑠 ) ⊆ 𝑠 ↔ ∀ 𝑠 ∈ 𝒫 𝐵 𝑠 ⊆ ( 𝐾 ‘ 𝑠 ) ) )