ntrclsiso

Description: If (pseudo-)interior and (pseudo-)closure functions are related by the duality operator then conditions equal to claiming that either is isotonic hold equally. (Contributed by RP, 3-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	ntrclsiso	$⊢ φ \to (\forall s \in 𝒫 B \forall t \in 𝒫 B (s \subseteq t \to I (s) \subseteq I (t)) \leftrightarrow \forall s \in 𝒫 B \forall t \in 𝒫 B (s \subseteq t \to K (s) \subseteq K (t)))$

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		sseq1	$⊢ s = b \to (s \subseteq t \leftrightarrow b \subseteq t)$
5		fveq2	$⊢ s = b \to I (s) = I (b)$
6	5	sseq1d	$⊢ s = b \to (I (s) \subseteq I (t) \leftrightarrow I (b) \subseteq I (t))$
7	4 6	imbi12d	$⊢ s = b \to ((s \subseteq t \to I (s) \subseteq I (t)) \leftrightarrow (b \subseteq t \to I (b) \subseteq I (t)))$
8		sseq2	$⊢ t = a \to (b \subseteq t \leftrightarrow b \subseteq a)$
9		fveq2	$⊢ t = a \to I (t) = I (a)$
10	9	sseq2d	$⊢ t = a \to (I (b) \subseteq I (t) \leftrightarrow I (b) \subseteq I (a))$
11	8 10	imbi12d	$⊢ t = a \to ((b \subseteq t \to I (b) \subseteq I (t)) \leftrightarrow (b \subseteq a \to I (b) \subseteq I (a)))$
12	7 11	cbvral2vw	$⊢ \forall s \in 𝒫 B \forall t \in 𝒫 B (s \subseteq t \to I (s) \subseteq I (t)) \leftrightarrow \forall b \in 𝒫 B \forall a \in 𝒫 B (b \subseteq a \to I (b) \subseteq I (a))$
13		ralcom	$⊢ \forall b \in 𝒫 B \forall a \in 𝒫 B (b \subseteq a \to I (b) \subseteq I (a)) \leftrightarrow \forall a \in 𝒫 B \forall b \in 𝒫 B (b \subseteq a \to I (b) \subseteq I (a))$
14	12 13	bitri	$⊢ \forall s \in 𝒫 B \forall t \in 𝒫 B (s \subseteq t \to I (s) \subseteq I (t)) \leftrightarrow \forall a \in 𝒫 B \forall b \in 𝒫 B (b \subseteq a \to I (b) \subseteq I (a))$
15		simpl	$⊢ (φ \land s \in 𝒫 B) \to φ$
16	2 3	ntrclsbex	$⊢ φ \to B \in V$
17	15 16	syl	$⊢ (φ \land s \in 𝒫 B) \to B \in V$
18		difssd	$⊢ (φ \land s \in 𝒫 B) \to B ∖ s \subseteq B$
19	17 18	sselpwd	$⊢ (φ \land s \in 𝒫 B) \to B ∖ s \in 𝒫 B$
20		elpwi	$⊢ a \in 𝒫 B \to a \subseteq B$
21		simpl	$⊢ (B \in V \land a \subseteq B) \to B \in V$
22		difssd	$⊢ (B \in V \land a \subseteq B) \to B ∖ a \subseteq B$
23	21 22	sselpwd	$⊢ (B \in V \land a \subseteq B) \to B ∖ a \in 𝒫 B$
24		simpr	$⊢ ((B \in V \land a \subseteq B) \land s = B ∖ a) \to s = B ∖ a$
25	24	difeq2d	$⊢ ((B \in V \land a \subseteq B) \land s = B ∖ a) \to B ∖ s = B ∖ (B ∖ a)$
26	25	eqeq2d	$⊢ ((B \in V \land a \subseteq B) \land s = B ∖ a) \to (a = B ∖ s \leftrightarrow a = B ∖ (B ∖ a))$
27		eqcom	$⊢ a = B ∖ (B ∖ a) \leftrightarrow B ∖ (B ∖ a) = a$
28	26 27	bitrdi	$⊢ ((B \in V \land a \subseteq B) \land s = B ∖ a) \to (a = B ∖ s \leftrightarrow B ∖ (B ∖ a) = a)$
29		dfss4	$⊢ a \subseteq B \leftrightarrow B ∖ (B ∖ a) = a$
30	29	bilani	$⊢ (B \in V \land a \subseteq B) \to B ∖ (B ∖ a) = a$
31	23 28 30	rspcedvd	$⊢ (B \in V \land a \subseteq B) \to \exists s \in 𝒫 B a = B ∖ s$
32	16 20 31	syl2an	$⊢ (φ \land a \in 𝒫 B) \to \exists s \in 𝒫 B a = B ∖ s$
33		simpl1	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B) \to φ$
34	33 16	syl	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B) \to B \in V$
35		difssd	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B) \to B ∖ t \subseteq B$
36	34 35	sselpwd	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B) \to B ∖ t \in 𝒫 B$
37		elpwi	$⊢ b \in 𝒫 B \to b \subseteq B$
38		simpl	$⊢ (B \in V \land b \subseteq B) \to B \in V$
39		difssd	$⊢ (B \in V \land b \subseteq B) \to B ∖ b \subseteq B$
40	38 39	sselpwd	$⊢ (B \in V \land b \subseteq B) \to B ∖ b \in 𝒫 B$
41		simpr	$⊢ ((B \in V \land b \subseteq B) \land t = B ∖ b) \to t = B ∖ b$
42	41	difeq2d	$⊢ ((B \in V \land b \subseteq B) \land t = B ∖ b) \to B ∖ t = B ∖ (B ∖ b)$
43	42	eqeq2d	$⊢ ((B \in V \land b \subseteq B) \land t = B ∖ b) \to (b = B ∖ t \leftrightarrow b = B ∖ (B ∖ b))$
44		eqcom	$⊢ b = B ∖ (B ∖ b) \leftrightarrow B ∖ (B ∖ b) = b$
45	43 44	bitrdi	$⊢ ((B \in V \land b \subseteq B) \land t = B ∖ b) \to (b = B ∖ t \leftrightarrow B ∖ (B ∖ b) = b)$
46		dfss4	$⊢ b \subseteq B \leftrightarrow B ∖ (B ∖ b) = b$
47	46	bilani	$⊢ (B \in V \land b \subseteq B) \to B ∖ (B ∖ b) = b$
48	40 45 47	rspcedvd	$⊢ (B \in V \land b \subseteq B) \to \exists t \in 𝒫 B b = B ∖ t$
49	16 37 48	syl2an	$⊢ (φ \land b \in 𝒫 B) \to \exists t \in 𝒫 B b = B ∖ t$
50	49	3ad2antl1	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land b \in 𝒫 B) \to \exists t \in 𝒫 B b = B ∖ t$
51		simp12	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to s \in 𝒫 B$
52	51	elpwid	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to s \subseteq B$
53		simp2	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to t \in 𝒫 B$
54	53	elpwid	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to t \subseteq B$
55		sscon34b	$⊢ (s \subseteq B \land t \subseteq B) \to (s \subseteq t \leftrightarrow B ∖ t \subseteq B ∖ s)$
56	52 54 55	syl2anc	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to (s \subseteq t \leftrightarrow B ∖ t \subseteq B ∖ s)$
57	56	bicomd	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to (B ∖ t \subseteq B ∖ s \leftrightarrow s \subseteq t)$
58		simp11	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to φ$
59	1 2 3	ntrclsiex	$⊢ φ \to I \in ({𝒫 B}^{𝒫 B})$
60	58 59	syl	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to I \in ({𝒫 B}^{𝒫 B})$
61		elmapi	$⊢ I \in ({𝒫 B}^{𝒫 B}) \to I : 𝒫 B ⟶ 𝒫 B$
62	60 61	syl	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to I : 𝒫 B ⟶ 𝒫 B$
63	58 16	syl	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to B \in V$
64		difssd	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to B ∖ t \subseteq B$
65	63 64	sselpwd	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to B ∖ t \in 𝒫 B$
66	62 65	ffvelcdmd	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to I (B ∖ t) \in 𝒫 B$
67	66	elpwid	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to I (B ∖ t) \subseteq B$
68		difssd	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to B ∖ s \subseteq B$
69	63 68	sselpwd	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to B ∖ s \in 𝒫 B$
70	62 69	ffvelcdmd	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to I (B ∖ s) \in 𝒫 B$
71	70	elpwid	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to I (B ∖ s) \subseteq B$
72		sscon34b	$⊢ (I (B ∖ t) \subseteq B \land I (B ∖ s) \subseteq B) \to (I (B ∖ t) \subseteq I (B ∖ s) \leftrightarrow B ∖ I (B ∖ s) \subseteq B ∖ I (B ∖ t))$
73	67 71 72	syl2anc	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to (I (B ∖ t) \subseteq I (B ∖ s) \leftrightarrow B ∖ I (B ∖ s) \subseteq B ∖ I (B ∖ t))$
74	57 73	imbi12d	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to ((B ∖ t \subseteq B ∖ s \to I (B ∖ t) \subseteq I (B ∖ s)) \leftrightarrow (s \subseteq t \to B ∖ I (B ∖ s) \subseteq B ∖ I (B ∖ t)))$
75		simp3	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to b = B ∖ t$
76		simp13	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to a = B ∖ s$
77	75 76	sseq12d	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to (b \subseteq a \leftrightarrow B ∖ t \subseteq B ∖ s)$
78	75	fveq2d	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to I (b) = I (B ∖ t)$
79	76	fveq2d	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to I (a) = I (B ∖ s)$
80	78 79	sseq12d	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to (I (b) \subseteq I (a) \leftrightarrow I (B ∖ t) \subseteq I (B ∖ s))$
81	77 80	imbi12d	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to ((b \subseteq a \to I (b) \subseteq I (a)) \leftrightarrow (B ∖ t \subseteq B ∖ s \to I (B ∖ t) \subseteq I (B ∖ s)))$
82	1 2 3	ntrclsfv1	$⊢ φ \to D (I) = K$
83	58 82	syl	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to D (I) = K$
84	83	fveq1d	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to D (I) (s) = K (s)$
85		eqid	$⊢ D (I) = D (I)$
86		eqid	$⊢ D (I) (s) = D (I) (s)$
87	1 2 63 60 85 51 86	dssmapfv3d	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to D (I) (s) = B ∖ I (B ∖ s)$
88	84 87	eqtr3d	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to K (s) = B ∖ I (B ∖ s)$
89	58 3	syl	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to I D K$
90	1 2 89	ntrclsfv1	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to D (I) = K$
91	90	fveq1d	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to D (I) (t) = K (t)$
92		eqid	$⊢ D (I) (t) = D (I) (t)$
93	1 2 63 60 85 53 92	dssmapfv3d	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to D (I) (t) = B ∖ I (B ∖ t)$
94	91 93	eqtr3d	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to K (t) = B ∖ I (B ∖ t)$
95	88 94	sseq12d	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to (K (s) \subseteq K (t) \leftrightarrow B ∖ I (B ∖ s) \subseteq B ∖ I (B ∖ t))$
96	95	imbi2d	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to ((s \subseteq t \to K (s) \subseteq K (t)) \leftrightarrow (s \subseteq t \to B ∖ I (B ∖ s) \subseteq B ∖ I (B ∖ t)))$
97	74 81 96	3bitr4d	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to ((b \subseteq a \to I (b) \subseteq I (a)) \leftrightarrow (s \subseteq t \to K (s) \subseteq K (t)))$
98	36 50 97	ralxfrd2	$⊢ (φ \land s \in 𝒫 B \land a = B ∖ s) \to (\forall b \in 𝒫 B (b \subseteq a \to I (b) \subseteq I (a)) \leftrightarrow \forall t \in 𝒫 B (s \subseteq t \to K (s) \subseteq K (t)))$
99	19 32 98	ralxfrd2	$⊢ φ \to (\forall a \in 𝒫 B \forall b \in 𝒫 B (b \subseteq a \to I (b) \subseteq I (a)) \leftrightarrow \forall s \in 𝒫 B \forall t \in 𝒫 B (s \subseteq t \to K (s) \subseteq K (t)))$
100	14 99	bitrid	$⊢ φ \to (\forall s \in 𝒫 B \forall t \in 𝒫 B (s \subseteq t \to I (s) \subseteq I (t)) \leftrightarrow \forall s \in 𝒫 B \forall t \in 𝒫 B (s \subseteq t \to K (s) \subseteq K (t)))$

Metamath Proof Explorer

Theorem ntrclsiso

Proof