Metamath Proof Explorer

Theorem ntrk1k3eqk13

Description: An interior function is both monotone and sub-linear if and only if it is finitely linear. (Contributed by RP, 18-Jun-2021)

		Ref	Expression
	Assertion	ntrk1k3eqk13	$⊢ (\forall s \in 𝒫 B \forall t \in 𝒫 B (s \subseteq t \to I (s) \subseteq I (t)) \land \forall s \in 𝒫 B \forall t \in 𝒫 B I (s) \cap I (t) \subseteq I (s \cap t)) \leftrightarrow \forall s \in 𝒫 B \forall t \in 𝒫 B I (s \cap t) = I (s) \cap I (t)$

Proof

Step	Hyp	Ref	Expression
1		r19.26-2	$⊢ \forall s \in 𝒫 B \forall t \in 𝒫 B (I (s \cap t) \subseteq I (s) \cap I (t) \land I (s) \cap I (t) \subseteq I (s \cap t)) \leftrightarrow (\forall s \in 𝒫 B \forall t \in 𝒫 B I (s \cap t) \subseteq I (s) \cap I (t) \land \forall s \in 𝒫 B \forall t \in 𝒫 B I (s) \cap I (t) \subseteq I (s \cap t))$
2		eqss	$⊢ I (s \cap t) = I (s) \cap I (t) \leftrightarrow (I (s \cap t) \subseteq I (s) \cap I (t) \land I (s) \cap I (t) \subseteq I (s \cap t))$
3	2	2ralbii	$⊢ \forall s \in 𝒫 B \forall t \in 𝒫 B I (s \cap t) = I (s) \cap I (t) \leftrightarrow \forall s \in 𝒫 B \forall t \in 𝒫 B (I (s \cap t) \subseteq I (s) \cap I (t) \land I (s) \cap I (t) \subseteq I (s \cap t))$
4		isotone2	$⊢ \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 I (s \cap t) \subseteq I (s) \cap I (t)$
5	4	anbi1i	$⊢ (\forall s \in 𝒫 B \forall t \in 𝒫 B (s \subseteq t \to I (s) \subseteq I (t)) \land \forall s \in 𝒫 B \forall t \in 𝒫 B I (s) \cap I (t) \subseteq I (s \cap t)) \leftrightarrow (\forall s \in 𝒫 B \forall t \in 𝒫 B I (s \cap t) \subseteq I (s) \cap I (t) \land \forall s \in 𝒫 B \forall t \in 𝒫 B I (s) \cap I (t) \subseteq I (s \cap t))$
6	1 3 5	3bitr4ri	$⊢ (\forall s \in 𝒫 B \forall t \in 𝒫 B (s \subseteq t \to I (s) \subseteq I (t)) \land \forall s \in 𝒫 B \forall t \in 𝒫 B I (s) \cap I (t) \subseteq I (s \cap t)) \leftrightarrow \forall s \in 𝒫 B \forall t \in 𝒫 B I (s \cap t) = I (s) \cap I (t)$