# 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 ( ∀ 𝑠 ∈ 𝒫 𝐵 ( 𝐼𝑠 ) ⊆ 𝑠 → ∀ 𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵 ( ( 𝑠𝑡 ) = ∅ → ( ( 𝐼𝑠 ) ∩ ( 𝐼𝑡 ) ) = ∅ ) )

### Proof

Step Hyp Ref Expression
1 id ( ∀ 𝑠 ∈ 𝒫 𝐵 ( 𝐼𝑠 ) ⊆ 𝑠 → ∀ 𝑠 ∈ 𝒫 𝐵 ( 𝐼𝑠 ) ⊆ 𝑠 )
2 fveq2 ( 𝑠 = 𝑡 → ( 𝐼𝑠 ) = ( 𝐼𝑡 ) )
3 id ( 𝑠 = 𝑡𝑠 = 𝑡 )
4 2 3 sseq12d ( 𝑠 = 𝑡 → ( ( 𝐼𝑠 ) ⊆ 𝑠 ↔ ( 𝐼𝑡 ) ⊆ 𝑡 ) )
5 4 cbvralvw ( ∀ 𝑠 ∈ 𝒫 𝐵 ( 𝐼𝑠 ) ⊆ 𝑠 ↔ ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝐼𝑡 ) ⊆ 𝑡 )
6 5 biimpi ( ∀ 𝑠 ∈ 𝒫 𝐵 ( 𝐼𝑠 ) ⊆ 𝑠 → ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝐼𝑡 ) ⊆ 𝑡 )
7 raaanv ( ∀ 𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵 ( ( 𝐼𝑠 ) ⊆ 𝑠 ∧ ( 𝐼𝑡 ) ⊆ 𝑡 ) ↔ ( ∀ 𝑠 ∈ 𝒫 𝐵 ( 𝐼𝑠 ) ⊆ 𝑠 ∧ ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝐼𝑡 ) ⊆ 𝑡 ) )
8 1 6 7 sylanbrc ( ∀ 𝑠 ∈ 𝒫 𝐵 ( 𝐼𝑠 ) ⊆ 𝑠 → ∀ 𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵 ( ( 𝐼𝑠 ) ⊆ 𝑠 ∧ ( 𝐼𝑡 ) ⊆ 𝑡 ) )
9 ss2in ( ( ( 𝐼𝑠 ) ⊆ 𝑠 ∧ ( 𝐼𝑡 ) ⊆ 𝑡 ) → ( ( 𝐼𝑠 ) ∩ ( 𝐼𝑡 ) ) ⊆ ( 𝑠𝑡 ) )
10 9 adantr ( ( ( ( 𝐼𝑠 ) ⊆ 𝑠 ∧ ( 𝐼𝑡 ) ⊆ 𝑡 ) ∧ ( 𝑠𝑡 ) = ∅ ) → ( ( 𝐼𝑠 ) ∩ ( 𝐼𝑡 ) ) ⊆ ( 𝑠𝑡 ) )
11 simpr ( ( ( ( 𝐼𝑠 ) ⊆ 𝑠 ∧ ( 𝐼𝑡 ) ⊆ 𝑡 ) ∧ ( 𝑠𝑡 ) = ∅ ) → ( 𝑠𝑡 ) = ∅ )
12 10 11 sseqtrd ( ( ( ( 𝐼𝑠 ) ⊆ 𝑠 ∧ ( 𝐼𝑡 ) ⊆ 𝑡 ) ∧ ( 𝑠𝑡 ) = ∅ ) → ( ( 𝐼𝑠 ) ∩ ( 𝐼𝑡 ) ) ⊆ ∅ )
13 ss0 ( ( ( 𝐼𝑠 ) ∩ ( 𝐼𝑡 ) ) ⊆ ∅ → ( ( 𝐼𝑠 ) ∩ ( 𝐼𝑡 ) ) = ∅ )
14 12 13 syl ( ( ( ( 𝐼𝑠 ) ⊆ 𝑠 ∧ ( 𝐼𝑡 ) ⊆ 𝑡 ) ∧ ( 𝑠𝑡 ) = ∅ ) → ( ( 𝐼𝑠 ) ∩ ( 𝐼𝑡 ) ) = ∅ )
15 14 ex ( ( ( 𝐼𝑠 ) ⊆ 𝑠 ∧ ( 𝐼𝑡 ) ⊆ 𝑡 ) → ( ( 𝑠𝑡 ) = ∅ → ( ( 𝐼𝑠 ) ∩ ( 𝐼𝑡 ) ) = ∅ ) )
16 15 2ralimi ( ∀ 𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵 ( ( 𝐼𝑠 ) ⊆ 𝑠 ∧ ( 𝐼𝑡 ) ⊆ 𝑡 ) → ∀ 𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵 ( ( 𝑠𝑡 ) = ∅ → ( ( 𝐼𝑠 ) ∩ ( 𝐼𝑡 ) ) = ∅ ) )
17 8 16 syl ( ∀ 𝑠 ∈ 𝒫 𝐵 ( 𝐼𝑠 ) ⊆ 𝑠 → ∀ 𝑠 ∈ 𝒫 𝐵𝑡 ∈ 𝒫 𝐵 ( ( 𝑠𝑡 ) = ∅ → ( ( 𝐼𝑠 ) ∩ ( 𝐼𝑡 ) ) = ∅ ) )