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	biimpi	$⊢ a \subseteq B \to B ∖ (B ∖ a) = a$
31	30	adantl	$⊢ (B \in V \land a \subseteq B) \to B ∖ (B ∖ a) = a$
32	23 28 31	rspcedvd	$⊢ (B \in V \land a \subseteq B) \to \exists s \in 𝒫 B a = B ∖ s$
33	16 20 32	syl2an	$⊢ (φ \land a \in 𝒫 B) \to \exists s \in 𝒫 B a = B ∖ s$
34		simpl1	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B) \to φ$
35	34 16	syl	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B) \to B \in V$
36		difssd	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B) \to B ∖ t \subseteq B$
37	35 36	sselpwd	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B) \to B ∖ t \in 𝒫 B$
38		elpwi	$⊢ b \in 𝒫 B \to b \subseteq B$
39		simpl	$⊢ (B \in V \land b \subseteq B) \to B \in V$
40		difssd	$⊢ (B \in V \land b \subseteq B) \to B ∖ b \subseteq B$
41	39 40	sselpwd	$⊢ (B \in V \land b \subseteq B) \to B ∖ b \in 𝒫 B$
42		simpr	$⊢ ((B \in V \land b \subseteq B) \land t = B ∖ b) \to t = B ∖ b$
43	42	difeq2d	$⊢ ((B \in V \land b \subseteq B) \land t = B ∖ b) \to B ∖ t = B ∖ (B ∖ b)$
44	43	eqeq2d	$⊢ ((B \in V \land b \subseteq B) \land t = B ∖ b) \to (b = B ∖ t \leftrightarrow b = B ∖ (B ∖ b))$
45		eqcom	$⊢ b = B ∖ (B ∖ b) \leftrightarrow B ∖ (B ∖ b) = b$
46	44 45	bitrdi	$⊢ ((B \in V \land b \subseteq B) \land t = B ∖ b) \to (b = B ∖ t \leftrightarrow B ∖ (B ∖ b) = b)$
47		dfss4	$⊢ b \subseteq B \leftrightarrow B ∖ (B ∖ b) = b$
48	47	biimpi	$⊢ b \subseteq B \to B ∖ (B ∖ b) = b$
49	48	adantl	$⊢ (B \in V \land b \subseteq B) \to B ∖ (B ∖ b) = b$
50	41 46 49	rspcedvd	$⊢ (B \in V \land b \subseteq B) \to \exists t \in 𝒫 B b = B ∖ t$
51	16 38 50	syl2an	$⊢ (φ \land b \in 𝒫 B) \to \exists t \in 𝒫 B b = B ∖ t$
52	51	3ad2antl1	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land b \in 𝒫 B) \to \exists t \in 𝒫 B b = B ∖ t$
53		simp12	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to s \in 𝒫 B$
54	53	elpwid	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to s \subseteq B$
55		simp2	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to t \in 𝒫 B$
56	55	elpwid	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to t \subseteq B$
57		sscon34b	$⊢ (s \subseteq B \land t \subseteq B) \to (s \subseteq t \leftrightarrow B ∖ t \subseteq B ∖ s)$
58	54 56 57	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)$
59	58	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)$
60		simp11	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to φ$
61	1 2 3	ntrclsiex	$⊢ φ \to I \in ({𝒫 B}^{𝒫 B})$
62	60 61	syl	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to I \in ({𝒫 B}^{𝒫 B})$
63		elmapi	$⊢ I \in ({𝒫 B}^{𝒫 B}) \to I : 𝒫 B ⟶ 𝒫 B$
64	62 63	syl	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to I : 𝒫 B ⟶ 𝒫 B$
65	60 16	syl	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to B \in V$
66		difssd	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to B ∖ t \subseteq B$
67	65 66	sselpwd	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to B ∖ t \in 𝒫 B$
68	64 67	ffvelcdmd	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to I (B ∖ t) \in 𝒫 B$
69	68	elpwid	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to I (B ∖ t) \subseteq B$
70		difssd	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to B ∖ s \subseteq B$
71	65 70	sselpwd	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to B ∖ s \in 𝒫 B$
72	64 71	ffvelcdmd	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to I (B ∖ s) \in 𝒫 B$
73	72	elpwid	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to I (B ∖ s) \subseteq B$
74		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))$
75	69 73 74	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))$
76	59 75	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)))$
77		simp3	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to b = B ∖ t$
78		simp13	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to a = B ∖ s$
79	77 78	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)$
80	77	fveq2d	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to I (b) = I (B ∖ t)$
81	78	fveq2d	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to I (a) = I (B ∖ s)$
82	80 81	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))$
83	79 82	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)))$
84	1 2 3	ntrclsfv1	$⊢ φ \to D (I) = K$
85	60 84	syl	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to D (I) = K$
86	85	fveq1d	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to D (I) (s) = K (s)$
87		eqid	$⊢ D (I) = D (I)$
88		eqid	$⊢ D (I) (s) = D (I) (s)$
89	1 2 65 62 87 53 88	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)$
90	86 89	eqtr3d	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to K (s) = B ∖ I (B ∖ s)$
91	60 3	syl	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to I D K$
92	1 2 91	ntrclsfv1	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to D (I) = K$
93	92	fveq1d	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to D (I) (t) = K (t)$
94		eqid	$⊢ D (I) (t) = D (I) (t)$
95	1 2 65 62 87 55 94	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)$
96	93 95	eqtr3d	$⊢ ((φ \land s \in 𝒫 B \land a = B ∖ s) \land t \in 𝒫 B \land b = B ∖ t) \to K (t) = B ∖ I (B ∖ t)$
97	90 96	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))$
98	97	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)))$
99	76 83 98	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)))$
100	37 52 99	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)))$
101	19 33 100	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)))$
102	14 101	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