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	⊢ ( ( ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝑠 ⊆ 𝑡 → ( 𝐼 ‘ 𝑠 ) ⊆ ( 𝐼 ‘ 𝑡 ) ) ∧ ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ⊆ ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) ) ↔ ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) = ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) )

Proof

Step	Hyp	Ref	Expression
1		r19.26-2	⊢ ( ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) ⊆ ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ∧ ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ⊆ ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) ) ↔ ( ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) ⊆ ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ∧ ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ⊆ ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) ) )
2		eqss	⊢ ( ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) = ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ↔ ( ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) ⊆ ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ∧ ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ⊆ ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) ) )
3	2	2ralbii	⊢ ( ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) = ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ↔ ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) ⊆ ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ∧ ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ⊆ ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) ) )
4		isotone2	⊢ ( ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝑠 ⊆ 𝑡 → ( 𝐼 ‘ 𝑠 ) ⊆ ( 𝐼 ‘ 𝑡 ) ) ↔ ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) ⊆ ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) )
5	4	anbi1i	⊢ ( ( ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝑠 ⊆ 𝑡 → ( 𝐼 ‘ 𝑠 ) ⊆ ( 𝐼 ‘ 𝑡 ) ) ∧ ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ⊆ ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) ) ↔ ( ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) ⊆ ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ∧ ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ⊆ ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) ) )
6	1 3 5	3bitr4ri	⊢ ( ( ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝑠 ⊆ 𝑡 → ( 𝐼 ‘ 𝑠 ) ⊆ ( 𝐼 ‘ 𝑡 ) ) ∧ ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ⊆ ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) ) ↔ ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) = ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) )