ntrclsss

Description: If interior and closure functions are related then a subset relation of a pair of function values is equivalent to subset relation of a pair of the other function's values. (Contributed by RP, 27-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$
	ntrclsfv.s	$⊢ φ \to S \in 𝒫 B$
	ntrclsfv.t	$⊢ φ \to T \in 𝒫 B$
Assertion	ntrclsss	$⊢ φ \to (I (S) \subseteq I (T) \leftrightarrow K (B ∖ T) \subseteq K (B ∖ 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		ntrclsfv.s	$⊢ φ \to S \in 𝒫 B$
5		ntrclsfv.t	$⊢ φ \to T \in 𝒫 B$
6	1 2 3 4	ntrclsfv	$⊢ φ \to I (S) = B ∖ K (B ∖ S)$
7	1 2 3 5	ntrclsfv	$⊢ φ \to I (T) = B ∖ K (B ∖ T)$
8	6 7	sseq12d	$⊢ φ \to (I (S) \subseteq I (T) \leftrightarrow B ∖ K (B ∖ S) \subseteq B ∖ K (B ∖ T))$
9	1 2 3	ntrclskex	$⊢ φ \to K \in ({𝒫 B}^{𝒫 B})$
10	9	ancli	$⊢ φ \to (φ \land K \in ({𝒫 B}^{𝒫 B}))$
11		elmapi	$⊢ K \in ({𝒫 B}^{𝒫 B}) \to K : 𝒫 B ⟶ 𝒫 B$
12	11	adantl	$⊢ (φ \land K \in ({𝒫 B}^{𝒫 B})) \to K : 𝒫 B ⟶ 𝒫 B$
13	2 3	ntrclsrcomplex	$⊢ φ \to B ∖ T \in 𝒫 B$
14	13	adantr	$⊢ (φ \land K \in ({𝒫 B}^{𝒫 B})) \to B ∖ T \in 𝒫 B$
15	12 14	ffvelrnd	$⊢ (φ \land K \in ({𝒫 B}^{𝒫 B})) \to K (B ∖ T) \in 𝒫 B$
16	15	elpwid	$⊢ (φ \land K \in ({𝒫 B}^{𝒫 B})) \to K (B ∖ T) \subseteq B$
17	2 3	ntrclsrcomplex	$⊢ φ \to B ∖ S \in 𝒫 B$
18	17	adantr	$⊢ (φ \land K \in ({𝒫 B}^{𝒫 B})) \to B ∖ S \in 𝒫 B$
19	12 18	ffvelrnd	$⊢ (φ \land K \in ({𝒫 B}^{𝒫 B})) \to K (B ∖ S) \in 𝒫 B$
20	19	elpwid	$⊢ (φ \land K \in ({𝒫 B}^{𝒫 B})) \to K (B ∖ S) \subseteq B$
21	16 20	jca	$⊢ (φ \land K \in ({𝒫 B}^{𝒫 B})) \to (K (B ∖ T) \subseteq B \land K (B ∖ S) \subseteq B)$
22		sscon34b	$⊢ (K (B ∖ T) \subseteq B \land K (B ∖ S) \subseteq B) \to (K (B ∖ T) \subseteq K (B ∖ S) \leftrightarrow B ∖ K (B ∖ S) \subseteq B ∖ K (B ∖ T))$
23	10 21 22	3syl	$⊢ φ \to (K (B ∖ T) \subseteq K (B ∖ S) \leftrightarrow B ∖ K (B ∖ S) \subseteq B ∖ K (B ∖ T))$
24	8 23	bitr4d	$⊢ φ \to (I (S) \subseteq I (T) \leftrightarrow K (B ∖ T) \subseteq K (B ∖ S))$

Metamath Proof Explorer

Theorem ntrclsss

Proof