Metamath Proof Explorer

Theorem ntrk2imkb

Description: If an interior function is contracting, the interiors of disjoint sets are disjoint. Kuratowski's K2 axiom implies KB. Interior version. (Contributed by RP, 9-Jun-2021)

Ref Expression
Assertion ntrk2imkb ⊢ ∀ s ∈ 𝒫 B I ⁡ s ⊆ s → ∀ s ∈ 𝒫 B ∀ t ∈ 𝒫 B s ∩ t = ∅ → I ⁡ s ∩ I ⁡ t = ∅

Proof

Step Hyp Ref Expression
1 id ⊢ ∀ s ∈ 𝒫 B I ⁡ s ⊆ s → ∀ s ∈ 𝒫 B I ⁡ s ⊆ s
2 fveq2 ⊢ s = t → I ⁡ s = I ⁡ t
3 id ⊢ s = t → s = t
4 2 3 sseq12d ⊢ s = t → I ⁡ s ⊆ s ↔ I ⁡ t ⊆ t
5 4 cbvralvw ⊢ ∀ s ∈ 𝒫 B I ⁡ s ⊆ s ↔ ∀ t ∈ 𝒫 B I ⁡ t ⊆ t
6 5 biimpi ⊢ ∀ s ∈ 𝒫 B I ⁡ s ⊆ s → ∀ t ∈ 𝒫 B I ⁡ t ⊆ t
7 raaanv ⊢ ∀ s ∈ 𝒫 B ∀ t ∈ 𝒫 B I ⁡ s ⊆ s ∧ I ⁡ t ⊆ t ↔ ∀ s ∈ 𝒫 B I ⁡ s ⊆ s ∧ ∀ t ∈ 𝒫 B I ⁡ t ⊆ t
8 1 6 7 sylanbrc ⊢ ∀ s ∈ 𝒫 B I ⁡ s ⊆ s → ∀ s ∈ 𝒫 B ∀ t ∈ 𝒫 B I ⁡ s ⊆ s ∧ I ⁡ t ⊆ t
9 ss2in ⊢ I ⁡ s ⊆ s ∧ I ⁡ t ⊆ t → I ⁡ s ∩ I ⁡ t ⊆ s ∩ t
10 9 adantr ⊢ I ⁡ s ⊆ s ∧ I ⁡ t ⊆ t ∧ s ∩ t = ∅ → I ⁡ s ∩ I ⁡ t ⊆ s ∩ t
11 simpr ⊢ I ⁡ s ⊆ s ∧ I ⁡ t ⊆ t ∧ s ∩ t = ∅ → s ∩ t = ∅
12 10 11 sseqtrd ⊢ I ⁡ s ⊆ s ∧ I ⁡ t ⊆ t ∧ s ∩ t = ∅ → I ⁡ s ∩ I ⁡ t ⊆ ∅
13 ss0 ⊢ I ⁡ s ∩ I ⁡ t ⊆ ∅ → I ⁡ s ∩ I ⁡ t = ∅
14 12 13 syl ⊢ I ⁡ s ⊆ s ∧ I ⁡ t ⊆ t ∧ s ∩ t = ∅ → I ⁡ s ∩ I ⁡ t = ∅
15 14 ex ⊢ I ⁡ s ⊆ s ∧ I ⁡ t ⊆ t → s ∩ t = ∅ → I ⁡ s ∩ I ⁡ t = ∅
16 15 2ralimi ⊢ ∀ s ∈ 𝒫 B ∀ t ∈ 𝒫 B I ⁡ s ⊆ s ∧ I ⁡ t ⊆ t → ∀ s ∈ 𝒫 B ∀ t ∈ 𝒫 B s ∩ t = ∅ → I ⁡ s ∩ I ⁡ t = ∅
17 8 16 syl ⊢ ∀ s ∈ 𝒫 B I ⁡ s ⊆ s → ∀ s ∈ 𝒫 B ∀ t ∈ 𝒫 B s ∩ t = ∅ → I ⁡ s ∩ I ⁡ t = ∅