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	$⊢ O = (i \in V ⟼ (k \in ({𝒫 i}^{𝒫 i}) ⟼ (j \in 𝒫 i ⟼ i ∖ k (i ∖ j))))$
	ntrcls.d	$⊢ D = O (B)$
	ntrcls.r	$⊢ φ \to I D K$
Assertion	ntrclsk2	$⊢ φ \to (\forall s \in 𝒫 B I (s) \subseteq s \leftrightarrow \forall s \in 𝒫 B s \subseteq K (s))$

Proof

Step	Hyp	Ref	Expression
1		ntrcls.o	$⊢ O = (i \in V ⟼ (k \in ({𝒫 i}^{𝒫 i}) ⟼ (j \in 𝒫 i ⟼ i ∖ k (i ∖ j))))$
2		ntrcls.d	$⊢ D = O (B)$
3		ntrcls.r	$⊢ φ \to I D K$
4		fveq2	$⊢ s = t \to I (s) = I (t)$
5		id	$⊢ s = t \to s = t$
6	4 5	sseq12d	$⊢ s = t \to (I (s) \subseteq s \leftrightarrow I (t) \subseteq t)$
7	6	cbvralvw	$⊢ \forall s \in 𝒫 B I (s) \subseteq s \leftrightarrow \forall t \in 𝒫 B I (t) \subseteq t$
8	2 3	ntrclsrcomplex	$⊢ φ \to B ∖ s \in 𝒫 B$
9	8	adantr	$⊢ (φ \land s \in 𝒫 B) \to B ∖ s \in 𝒫 B$
10	2 3	ntrclsrcomplex	$⊢ φ \to B ∖ t \in 𝒫 B$
11	10	adantr	$⊢ (φ \land t \in 𝒫 B) \to B ∖ t \in 𝒫 B$
12		difeq2	$⊢ s = B ∖ t \to B ∖ s = B ∖ (B ∖ t)$
13	12	eqeq2d	$⊢ s = B ∖ t \to (t = B ∖ s \leftrightarrow t = B ∖ (B ∖ t))$
14	13	adantl	$⊢ ((φ \land t \in 𝒫 B) \land s = B ∖ t) \to (t = B ∖ s \leftrightarrow t = B ∖ (B ∖ t))$
15		elpwi	$⊢ t \in 𝒫 B \to t \subseteq B$
16		dfss4	$⊢ t \subseteq B \leftrightarrow B ∖ (B ∖ t) = t$
17	15 16	sylib	$⊢ t \in 𝒫 B \to B ∖ (B ∖ t) = t$
18	17	adantl	$⊢ (φ \land t \in 𝒫 B) \to B ∖ (B ∖ t) = t$
19	18	eqcomd	$⊢ (φ \land t \in 𝒫 B) \to t = B ∖ (B ∖ t)$
20	11 14 19	rspcedvd	$⊢ (φ \land t \in 𝒫 B) \to \exists s \in 𝒫 B t = B ∖ s$
21		fveq2	$⊢ t = B ∖ s \to I (t) = I (B ∖ s)$
22		id	$⊢ t = B ∖ s \to t = B ∖ s$
23	21 22	sseq12d	$⊢ t = B ∖ s \to (I (t) \subseteq t \leftrightarrow I (B ∖ s) \subseteq B ∖ s)$
24	23	3ad2ant3	$⊢ (φ \land s \in 𝒫 B \land t = B ∖ s) \to (I (t) \subseteq t \leftrightarrow I (B ∖ s) \subseteq B ∖ s)$
25	1 2 3	ntrclsiex	$⊢ φ \to I \in ({𝒫 B}^{𝒫 B})$
26		elmapi	$⊢ I \in ({𝒫 B}^{𝒫 B}) \to I : 𝒫 B ⟶ 𝒫 B$
27	25 26	syl	$⊢ φ \to I : 𝒫 B ⟶ 𝒫 B$
28	27	3ad2ant1	$⊢ (φ \land s \in 𝒫 B \land t = B ∖ s) \to I : 𝒫 B ⟶ 𝒫 B$
29	8	3ad2ant1	$⊢ (φ \land s \in 𝒫 B \land t = B ∖ s) \to B ∖ s \in 𝒫 B$
30	28 29	ffvelcdmd	$⊢ (φ \land s \in 𝒫 B \land t = B ∖ s) \to I (B ∖ s) \in 𝒫 B$
31	30	elpwid	$⊢ (φ \land s \in 𝒫 B \land t = B ∖ s) \to I (B ∖ s) \subseteq B$
32		difssd	$⊢ (φ \land s \in 𝒫 B \land t = B ∖ s) \to B ∖ s \subseteq B$
33		sscon34b	$⊢ (I (B ∖ s) \subseteq B \land B ∖ s \subseteq B) \to (I (B ∖ s) \subseteq B ∖ s \leftrightarrow B ∖ (B ∖ s) \subseteq B ∖ I (B ∖ s))$
34	31 32 33	syl2anc	$⊢ (φ \land s \in 𝒫 B \land t = B ∖ s) \to (I (B ∖ s) \subseteq B ∖ s \leftrightarrow B ∖ (B ∖ s) \subseteq B ∖ I (B ∖ s))$
35		simp2	$⊢ (φ \land s \in 𝒫 B \land t = B ∖ s) \to s \in 𝒫 B$
36		elpwi	$⊢ s \in 𝒫 B \to s \subseteq B$
37		dfss4	$⊢ s \subseteq B \leftrightarrow B ∖ (B ∖ s) = s$
38	36 37	sylib	$⊢ s \in 𝒫 B \to B ∖ (B ∖ s) = s$
39	38	sseq1d	$⊢ s \in 𝒫 B \to (B ∖ (B ∖ s) \subseteq B ∖ I (B ∖ s) \leftrightarrow s \subseteq B ∖ I (B ∖ s))$
40	35 39	syl	$⊢ (φ \land s \in 𝒫 B \land t = B ∖ s) \to (B ∖ (B ∖ s) \subseteq B ∖ I (B ∖ s) \leftrightarrow s \subseteq B ∖ I (B ∖ s))$
41	34 40	bitrd	$⊢ (φ \land s \in 𝒫 B \land t = B ∖ s) \to (I (B ∖ s) \subseteq B ∖ s \leftrightarrow s \subseteq B ∖ I (B ∖ s))$
42	2 3	ntrclsbex	$⊢ φ \to B \in V$
43	42	3ad2ant1	$⊢ (φ \land s \in 𝒫 B \land t = B ∖ s) \to B \in V$
44	25	3ad2ant1	$⊢ (φ \land s \in 𝒫 B \land t = B ∖ s) \to I \in ({𝒫 B}^{𝒫 B})$
45		eqid	$⊢ D (I) = D (I)$
46		eqid	$⊢ D (I) (s) = D (I) (s)$
47	1 2 43 44 45 35 46	dssmapfv3d	$⊢ (φ \land s \in 𝒫 B \land t = B ∖ s) \to D (I) (s) = B ∖ I (B ∖ s)$
48	47	sseq2d	$⊢ (φ \land s \in 𝒫 B \land t = B ∖ s) \to (s \subseteq D (I) (s) \leftrightarrow s \subseteq B ∖ I (B ∖ s))$
49	1 2 3	ntrclsfv1	$⊢ φ \to D (I) = K$
50	49	fveq1d	$⊢ φ \to D (I) (s) = K (s)$
51	50	sseq2d	$⊢ φ \to (s \subseteq D (I) (s) \leftrightarrow s \subseteq K (s))$
52	51	3ad2ant1	$⊢ (φ \land s \in 𝒫 B \land t = B ∖ s) \to (s \subseteq D (I) (s) \leftrightarrow s \subseteq K (s))$
53	41 48 52	3bitr2d	$⊢ (φ \land s \in 𝒫 B \land t = B ∖ s) \to (I (B ∖ s) \subseteq B ∖ s \leftrightarrow s \subseteq K (s))$
54	24 53	bitrd	$⊢ (φ \land s \in 𝒫 B \land t = B ∖ s) \to (I (t) \subseteq t \leftrightarrow s \subseteq K (s))$
55	9 20 54	ralxfrd2	$⊢ φ \to (\forall t \in 𝒫 B I (t) \subseteq t \leftrightarrow \forall s \in 𝒫 B s \subseteq K (s))$
56	7 55	bitrid	$⊢ φ \to (\forall s \in 𝒫 B I (s) \subseteq s \leftrightarrow \forall s \in 𝒫 B s \subseteq K (s))$

Metamath Proof Explorer

Theorem ntrclsk2

Proof