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	$⊢ 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	ntrclsk4	$⊢ φ \to (\forall s \in 𝒫 B I (I (s)) = I (s) \leftrightarrow \forall s \in 𝒫 B K (K (s)) = 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		2fveq3	$⊢ s = t \to I (I (s)) = I (I (t))$
5		fveq2	$⊢ s = t \to I (s) = I (t)$
6	4 5	eqeq12d	$⊢ s = t \to (I (I (s)) = I (s) \leftrightarrow I (I (t)) = I (t))$
7	6	cbvralvw	$⊢ \forall s \in 𝒫 B I (I (s)) = I (s) \leftrightarrow \forall t \in 𝒫 B I (I (t)) = I (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	eqcomd	$⊢ t \in 𝒫 B \to t = B ∖ (B ∖ t)$
19	18	adantl	$⊢ (φ \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		2fveq3	$⊢ t = B ∖ s \to I (I (t)) = I (I (B ∖ s))$
22		fveq2	$⊢ t = B ∖ s \to I (t) = I (B ∖ s)$
23	21 22	eqeq12d	$⊢ t = B ∖ s \to (I (I (t)) = I (t) \leftrightarrow I (I (B ∖ s)) = I (B ∖ s))$
24	23	3ad2ant3	$⊢ (φ \land s \in 𝒫 B \land t = B ∖ s) \to (I (I (t)) = I (t) \leftrightarrow I (I (B ∖ s)) = I (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 8	ffvelcdmd	$⊢ φ \to I (B ∖ s) \in 𝒫 B$
29	27 28	ffvelcdmd	$⊢ φ \to I (I (B ∖ s)) \in 𝒫 B$
30	29	elpwid	$⊢ φ \to I (I (B ∖ s)) \subseteq B$
31	28	elpwid	$⊢ φ \to I (B ∖ s) \subseteq B$
32		rcompleq	$⊢ (I (I (B ∖ s)) \subseteq B \land I (B ∖ s) \subseteq B) \to (I (I (B ∖ s)) = I (B ∖ s) \leftrightarrow B ∖ I (I (B ∖ s)) = B ∖ I (B ∖ s))$
33	30 31 32	syl2anc	$⊢ φ \to (I (I (B ∖ s)) = I (B ∖ s) \leftrightarrow B ∖ I (I (B ∖ s)) = B ∖ I (B ∖ s))$
34	33	adantr	$⊢ (φ \land s \in 𝒫 B) \to (I (I (B ∖ s)) = I (B ∖ s) \leftrightarrow B ∖ I (I (B ∖ s)) = B ∖ I (B ∖ s))$
35	1 2 3	ntrclsnvobr	$⊢ φ \to K D I$
36	35	adantr	$⊢ (φ \land s \in 𝒫 B) \to K D I$
37	1 2 35	ntrclsiex	$⊢ φ \to K \in ({𝒫 B}^{𝒫 B})$
38		elmapi	$⊢ K \in ({𝒫 B}^{𝒫 B}) \to K : 𝒫 B ⟶ 𝒫 B$
39	37 38	syl	$⊢ φ \to K : 𝒫 B ⟶ 𝒫 B$
40	39	ffvelcdmda	$⊢ (φ \land s \in 𝒫 B) \to K (s) \in 𝒫 B$
41	1 2 36 40	ntrclsfv	$⊢ (φ \land s \in 𝒫 B) \to K (K (s)) = B ∖ I (B ∖ K (s))$
42		simpr	$⊢ (φ \land s \in 𝒫 B) \to s \in 𝒫 B$
43	1 2 36 42	ntrclsfv	$⊢ (φ \land s \in 𝒫 B) \to K (s) = B ∖ I (B ∖ s)$
44	43	difeq2d	$⊢ (φ \land s \in 𝒫 B) \to B ∖ K (s) = B ∖ (B ∖ I (B ∖ s))$
45		dfss4	$⊢ I (B ∖ s) \subseteq B \leftrightarrow B ∖ (B ∖ I (B ∖ s)) = I (B ∖ s)$
46	31 45	sylib	$⊢ φ \to B ∖ (B ∖ I (B ∖ s)) = I (B ∖ s)$
47	46	adantr	$⊢ (φ \land s \in 𝒫 B) \to B ∖ (B ∖ I (B ∖ s)) = I (B ∖ s)$
48	44 47	eqtrd	$⊢ (φ \land s \in 𝒫 B) \to B ∖ K (s) = I (B ∖ s)$
49	48	fveq2d	$⊢ (φ \land s \in 𝒫 B) \to I (B ∖ K (s)) = I (I (B ∖ s))$
50	49	difeq2d	$⊢ (φ \land s \in 𝒫 B) \to B ∖ I (B ∖ K (s)) = B ∖ I (I (B ∖ s))$
51	41 50	eqtrd	$⊢ (φ \land s \in 𝒫 B) \to K (K (s)) = B ∖ I (I (B ∖ s))$
52	51 43	eqeq12d	$⊢ (φ \land s \in 𝒫 B) \to (K (K (s)) = K (s) \leftrightarrow B ∖ I (I (B ∖ s)) = B ∖ I (B ∖ s))$
53	34 52	bitr4d	$⊢ (φ \land s \in 𝒫 B) \to (I (I (B ∖ s)) = I (B ∖ s) \leftrightarrow K (K (s)) = K (s))$
54	53	3adant3	$⊢ (φ \land s \in 𝒫 B \land t = B ∖ s) \to (I (I (B ∖ s)) = I (B ∖ s) \leftrightarrow K (K (s)) = K (s))$
55	24 54	bitrd	$⊢ (φ \land s \in 𝒫 B \land t = B ∖ s) \to (I (I (t)) = I (t) \leftrightarrow K (K (s)) = K (s))$
56	9 20 55	ralxfrd2	$⊢ φ \to (\forall t \in 𝒫 B I (I (t)) = I (t) \leftrightarrow \forall s \in 𝒫 B K (K (s)) = K (s))$
57	7 56	bitrid	$⊢ φ \to (\forall s \in 𝒫 B I (I (s)) = I (s) \leftrightarrow \forall s \in 𝒫 B K (K (s)) = K (s))$

Metamath Proof Explorer

Theorem ntrclsk4

Proof