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 ⊢ ∀ s ∈ 𝒫 B ∀ t ∈ 𝒫 B s ⊆ t → I ⁡ s ⊆ I ⁡ t ∧ ∀ s ∈ 𝒫 B ∀ t ∈ 𝒫 B I ⁡ s ∩ I ⁡ t ⊆ I ⁡ s ∩ t ↔ ∀ s ∈ 𝒫 B ∀ t ∈ 𝒫 B I ⁡ s ∩ t = I ⁡ s ∩ I ⁡ t

Proof

Step Hyp Ref Expression
1 r19.26-2 ⊢ ∀ s ∈ 𝒫 B ∀ t ∈ 𝒫 B I ⁡ s ∩ t ⊆ I ⁡ s ∩ I ⁡ t ∧ I ⁡ s ∩ I ⁡ t ⊆ I ⁡ s ∩ t ↔ ∀ s ∈ 𝒫 B ∀ t ∈ 𝒫 B I ⁡ s ∩ t ⊆ I ⁡ s ∩ I ⁡ t ∧ ∀ s ∈ 𝒫 B ∀ t ∈ 𝒫 B I ⁡ s ∩ I ⁡ t ⊆ I ⁡ s ∩ t
2 eqss ⊢ I ⁡ s ∩ t = I ⁡ s ∩ I ⁡ t ↔ I ⁡ s ∩ t ⊆ I ⁡ s ∩ I ⁡ t ∧ I ⁡ s ∩ I ⁡ t ⊆ I ⁡ s ∩ t
3 2 2ralbii ⊢ ∀ s ∈ 𝒫 B ∀ t ∈ 𝒫 B I ⁡ s ∩ t = I ⁡ s ∩ I ⁡ t ↔ ∀ s ∈ 𝒫 B ∀ t ∈ 𝒫 B I ⁡ s ∩ t ⊆ I ⁡ s ∩ I ⁡ t ∧ I ⁡ s ∩ I ⁡ t ⊆ I ⁡ s ∩ t
4 isotone2 ⊢ ∀ s ∈ 𝒫 B ∀ t ∈ 𝒫 B s ⊆ t → I ⁡ s ⊆ I ⁡ t ↔ ∀ s ∈ 𝒫 B ∀ t ∈ 𝒫 B I ⁡ s ∩ t ⊆ I ⁡ s ∩ I ⁡ t
5 4 anbi1i ⊢ ∀ s ∈ 𝒫 B ∀ t ∈ 𝒫 B s ⊆ t → I ⁡ s ⊆ I ⁡ t ∧ ∀ s ∈ 𝒫 B ∀ t ∈ 𝒫 B I ⁡ s ∩ I ⁡ t ⊆ I ⁡ s ∩ t ↔ ∀ s ∈ 𝒫 B ∀ t ∈ 𝒫 B I ⁡ s ∩ t ⊆ I ⁡ s ∩ I ⁡ t ∧ ∀ s ∈ 𝒫 B ∀ t ∈ 𝒫 B I ⁡ s ∩ I ⁡ t ⊆ I ⁡ s ∩ t
6 1 3 5 3bitr4ri ⊢ ∀ s ∈ 𝒫 B ∀ t ∈ 𝒫 B s ⊆ t → I ⁡ s ⊆ I ⁡ t ∧ ∀ s ∈ 𝒫 B ∀ t ∈ 𝒫 B I ⁡ s ∩ I ⁡ t ⊆ I ⁡ s ∩ t ↔ ∀ s ∈ 𝒫 B ∀ t ∈ 𝒫 B I ⁡ s ∩ t = I ⁡ s ∩ I ⁡ t