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