Theorem ntrkbimka

Description: If the interiors of disjoint sets are disjoint, then the interior of the empty set is the empty set. (Contributed by RP, 14-Jun-2021)

	Ref	Expression
Assertion	ntrkbimka	⊢ ( ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∩ 𝑡 ) = ∅ → ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ) → ( 𝐼 ‘ ∅ ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		inidm	⊢ ( ( 𝐼 ‘ ∅ ) ∩ ( 𝐼 ‘ ∅ ) ) = ( 𝐼 ‘ ∅ )
2		0elpw	⊢ ∅ ∈ 𝒫 𝐵
3		ineq1	⊢ ( 𝑠 = ∅ → ( 𝑠 ∩ 𝑡 ) = ( ∅ ∩ 𝑡 ) )
4	3	eqeq1d	⊢ ( 𝑠 = ∅ → ( ( 𝑠 ∩ 𝑡 ) = ∅ ↔ ( ∅ ∩ 𝑡 ) = ∅ ) )
5		fveq2	⊢ ( 𝑠 = ∅ → ( 𝐼 ‘ 𝑠 ) = ( 𝐼 ‘ ∅ ) )
6	5	ineq1d	⊢ ( 𝑠 = ∅ → ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ( ( 𝐼 ‘ ∅ ) ∩ ( 𝐼 ‘ 𝑡 ) ) )
7	6	eqeq1d	⊢ ( 𝑠 = ∅ → ( ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ↔ ( ( 𝐼 ‘ ∅ ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ) )
8	4 7	imbi12d	⊢ ( 𝑠 = ∅ → ( ( ( 𝑠 ∩ 𝑡 ) = ∅ → ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ) ↔ ( ( ∅ ∩ 𝑡 ) = ∅ → ( ( 𝐼 ‘ ∅ ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ) ) )
9		0in	⊢ ( ∅ ∩ 𝑡 ) = ∅
10		pm5.5	⊢ ( ( ∅ ∩ 𝑡 ) = ∅ → ( ( ( ∅ ∩ 𝑡 ) = ∅ → ( ( 𝐼 ‘ ∅ ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ) ↔ ( ( 𝐼 ‘ ∅ ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ) )
11	9 10	ax-mp	⊢ ( ( ( ∅ ∩ 𝑡 ) = ∅ → ( ( 𝐼 ‘ ∅ ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ) ↔ ( ( 𝐼 ‘ ∅ ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ )
12	8 11	bitrdi	⊢ ( 𝑠 = ∅ → ( ( ( 𝑠 ∩ 𝑡 ) = ∅ → ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ) ↔ ( ( 𝐼 ‘ ∅ ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ) )
13		fveq2	⊢ ( 𝑡 = ∅ → ( 𝐼 ‘ 𝑡 ) = ( 𝐼 ‘ ∅ ) )
14	13	ineq2d	⊢ ( 𝑡 = ∅ → ( ( 𝐼 ‘ ∅ ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ( ( 𝐼 ‘ ∅ ) ∩ ( 𝐼 ‘ ∅ ) ) )
15	14	eqeq1d	⊢ ( 𝑡 = ∅ → ( ( ( 𝐼 ‘ ∅ ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ↔ ( ( 𝐼 ‘ ∅ ) ∩ ( 𝐼 ‘ ∅ ) ) = ∅ ) )
16	12 15	rspc2v	⊢ ( ( ∅ ∈ 𝒫 𝐵 ∧ ∅ ∈ 𝒫 𝐵 ) → ( ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∩ 𝑡 ) = ∅ → ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ) → ( ( 𝐼 ‘ ∅ ) ∩ ( 𝐼 ‘ ∅ ) ) = ∅ ) )
17	2 2 16	mp2an	⊢ ( ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∩ 𝑡 ) = ∅ → ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ) → ( ( 𝐼 ‘ ∅ ) ∩ ( 𝐼 ‘ ∅ ) ) = ∅ )
18	1 17	eqtr3id	⊢ ( ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∩ 𝑡 ) = ∅ → ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ) → ( 𝐼 ‘ ∅ ) = ∅ )