Theorem ntrk0kbimka

Description: If the interiors of disjoint sets are disjoint and the interior of the base set is the base set, then the interior of the empty set is the empty set. Obsolete version of ntrkbimka . (Contributed by RP, 12-Jun-2021)

	Ref	Expression
Assertion	ntrk0kbimka	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) → ( ( ( 𝐼 ‘ 𝐵 ) = 𝐵 ∧ ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∩ 𝑡 ) = ∅ → ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ) ) → ( 𝐼 ‘ ∅ ) = ∅ ) )

Proof

Step	Hyp	Ref	Expression
1		pwidg	⊢ ( 𝐵 ∈ 𝑉 → 𝐵 ∈ 𝒫 𝐵 )
2	1	ad2antrr	⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) ∧ ( ( 𝐼 ‘ 𝐵 ) = 𝐵 ∧ ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∩ 𝑡 ) = ∅ → ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ) ) ) → 𝐵 ∈ 𝒫 𝐵 )
3		0elpw	⊢ ∅ ∈ 𝒫 𝐵
4	3	a1i	⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) ∧ ( ( 𝐼 ‘ 𝐵 ) = 𝐵 ∧ ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∩ 𝑡 ) = ∅ → ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ) ) ) → ∅ ∈ 𝒫 𝐵 )
5		simprr	⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) ∧ ( ( 𝐼 ‘ 𝐵 ) = 𝐵 ∧ ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∩ 𝑡 ) = ∅ → ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ) ) ) → ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∩ 𝑡 ) = ∅ → ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ) )
6		ineq1	⊢ ( 𝑠 = 𝐵 → ( 𝑠 ∩ 𝑡 ) = ( 𝐵 ∩ 𝑡 ) )
7	6	eqeq1d	⊢ ( 𝑠 = 𝐵 → ( ( 𝑠 ∩ 𝑡 ) = ∅ ↔ ( 𝐵 ∩ 𝑡 ) = ∅ ) )
8		fveq2	⊢ ( 𝑠 = 𝐵 → ( 𝐼 ‘ 𝑠 ) = ( 𝐼 ‘ 𝐵 ) )
9	8	ineq1d	⊢ ( 𝑠 = 𝐵 → ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ( ( 𝐼 ‘ 𝐵 ) ∩ ( 𝐼 ‘ 𝑡 ) ) )
10	9	eqeq1d	⊢ ( 𝑠 = 𝐵 → ( ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ↔ ( ( 𝐼 ‘ 𝐵 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ) )
11	7 10	imbi12d	⊢ ( 𝑠 = 𝐵 → ( ( ( 𝑠 ∩ 𝑡 ) = ∅ → ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ) ↔ ( ( 𝐵 ∩ 𝑡 ) = ∅ → ( ( 𝐼 ‘ 𝐵 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ) ) )
12		ineq2	⊢ ( 𝑡 = ∅ → ( 𝐵 ∩ 𝑡 ) = ( 𝐵 ∩ ∅ ) )
13	12	eqeq1d	⊢ ( 𝑡 = ∅ → ( ( 𝐵 ∩ 𝑡 ) = ∅ ↔ ( 𝐵 ∩ ∅ ) = ∅ ) )
14		fveq2	⊢ ( 𝑡 = ∅ → ( 𝐼 ‘ 𝑡 ) = ( 𝐼 ‘ ∅ ) )
15	14	ineq2d	⊢ ( 𝑡 = ∅ → ( ( 𝐼 ‘ 𝐵 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ( ( 𝐼 ‘ 𝐵 ) ∩ ( 𝐼 ‘ ∅ ) ) )
16	15	eqeq1d	⊢ ( 𝑡 = ∅ → ( ( ( 𝐼 ‘ 𝐵 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ↔ ( ( 𝐼 ‘ 𝐵 ) ∩ ( 𝐼 ‘ ∅ ) ) = ∅ ) )
17	13 16	imbi12d	⊢ ( 𝑡 = ∅ → ( ( ( 𝐵 ∩ 𝑡 ) = ∅ → ( ( 𝐼 ‘ 𝐵 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ) ↔ ( ( 𝐵 ∩ ∅ ) = ∅ → ( ( 𝐼 ‘ 𝐵 ) ∩ ( 𝐼 ‘ ∅ ) ) = ∅ ) ) )
18		in0	⊢ ( 𝐵 ∩ ∅ ) = ∅
19		pm5.5	⊢ ( ( 𝐵 ∩ ∅ ) = ∅ → ( ( ( 𝐵 ∩ ∅ ) = ∅ → ( ( 𝐼 ‘ 𝐵 ) ∩ ( 𝐼 ‘ ∅ ) ) = ∅ ) ↔ ( ( 𝐼 ‘ 𝐵 ) ∩ ( 𝐼 ‘ ∅ ) ) = ∅ ) )
20	18 19	mp1i	⊢ ( 𝑡 = ∅ → ( ( ( 𝐵 ∩ ∅ ) = ∅ → ( ( 𝐼 ‘ 𝐵 ) ∩ ( 𝐼 ‘ ∅ ) ) = ∅ ) ↔ ( ( 𝐼 ‘ 𝐵 ) ∩ ( 𝐼 ‘ ∅ ) ) = ∅ ) )
21	17 20	bitrd	⊢ ( 𝑡 = ∅ → ( ( ( 𝐵 ∩ 𝑡 ) = ∅ → ( ( 𝐼 ‘ 𝐵 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ) ↔ ( ( 𝐼 ‘ 𝐵 ) ∩ ( 𝐼 ‘ ∅ ) ) = ∅ ) )
22	11 21	rspc2va	⊢ ( ( ( 𝐵 ∈ 𝒫 𝐵 ∧ ∅ ∈ 𝒫 𝐵 ) ∧ ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∩ 𝑡 ) = ∅ → ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ) ) → ( ( 𝐼 ‘ 𝐵 ) ∩ ( 𝐼 ‘ ∅ ) ) = ∅ )
23	2 4 5 22	syl21anc	⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) ∧ ( ( 𝐼 ‘ 𝐵 ) = 𝐵 ∧ ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∩ 𝑡 ) = ∅ → ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ) ) ) → ( ( 𝐼 ‘ 𝐵 ) ∩ ( 𝐼 ‘ ∅ ) ) = ∅ )
24	23	ex	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) → ( ( ( 𝐼 ‘ 𝐵 ) = 𝐵 ∧ ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∩ 𝑡 ) = ∅ → ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ) ) → ( ( 𝐼 ‘ 𝐵 ) ∩ ( 𝐼 ‘ ∅ ) ) = ∅ ) )
25		elmapi	⊢ ( 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) → 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
26	25	adantl	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) → 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
27	3	a1i	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) → ∅ ∈ 𝒫 𝐵 )
28	26 27	ffvelcdmd	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) → ( 𝐼 ‘ ∅ ) ∈ 𝒫 𝐵 )
29	28	elpwid	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) → ( 𝐼 ‘ ∅ ) ⊆ 𝐵 )
30		simpl	⊢ ( ( ( 𝐼 ‘ 𝐵 ) = 𝐵 ∧ ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∩ 𝑡 ) = ∅ → ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ) ) → ( 𝐼 ‘ 𝐵 ) = 𝐵 )
31		ineq1	⊢ ( ( 𝐼 ‘ 𝐵 ) = 𝐵 → ( ( 𝐼 ‘ 𝐵 ) ∩ ( 𝐼 ‘ ∅ ) ) = ( 𝐵 ∩ ( 𝐼 ‘ ∅ ) ) )
32		incom	⊢ ( 𝐵 ∩ ( 𝐼 ‘ ∅ ) ) = ( ( 𝐼 ‘ ∅ ) ∩ 𝐵 )
33	31 32	eqtrdi	⊢ ( ( 𝐼 ‘ 𝐵 ) = 𝐵 → ( ( 𝐼 ‘ 𝐵 ) ∩ ( 𝐼 ‘ ∅ ) ) = ( ( 𝐼 ‘ ∅ ) ∩ 𝐵 ) )
34	33	eqeq1d	⊢ ( ( 𝐼 ‘ 𝐵 ) = 𝐵 → ( ( ( 𝐼 ‘ 𝐵 ) ∩ ( 𝐼 ‘ ∅ ) ) = ∅ ↔ ( ( 𝐼 ‘ ∅ ) ∩ 𝐵 ) = ∅ ) )
35	34	biimpd	⊢ ( ( 𝐼 ‘ 𝐵 ) = 𝐵 → ( ( ( 𝐼 ‘ 𝐵 ) ∩ ( 𝐼 ‘ ∅ ) ) = ∅ → ( ( 𝐼 ‘ ∅ ) ∩ 𝐵 ) = ∅ ) )
36		reldisj	⊢ ( ( 𝐼 ‘ ∅ ) ⊆ 𝐵 → ( ( ( 𝐼 ‘ ∅ ) ∩ 𝐵 ) = ∅ ↔ ( 𝐼 ‘ ∅ ) ⊆ ( 𝐵 ∖ 𝐵 ) ) )
37	36	biimpd	⊢ ( ( 𝐼 ‘ ∅ ) ⊆ 𝐵 → ( ( ( 𝐼 ‘ ∅ ) ∩ 𝐵 ) = ∅ → ( 𝐼 ‘ ∅ ) ⊆ ( 𝐵 ∖ 𝐵 ) ) )
38		difid	⊢ ( 𝐵 ∖ 𝐵 ) = ∅
39	38	sseq2i	⊢ ( ( 𝐼 ‘ ∅ ) ⊆ ( 𝐵 ∖ 𝐵 ) ↔ ( 𝐼 ‘ ∅ ) ⊆ ∅ )
40		ss0	⊢ ( ( 𝐼 ‘ ∅ ) ⊆ ∅ → ( 𝐼 ‘ ∅ ) = ∅ )
41	39 40	sylbi	⊢ ( ( 𝐼 ‘ ∅ ) ⊆ ( 𝐵 ∖ 𝐵 ) → ( 𝐼 ‘ ∅ ) = ∅ )
42	37 41	syl6com	⊢ ( ( ( 𝐼 ‘ ∅ ) ∩ 𝐵 ) = ∅ → ( ( 𝐼 ‘ ∅ ) ⊆ 𝐵 → ( 𝐼 ‘ ∅ ) = ∅ ) )
43	35 42	syl6com	⊢ ( ( ( 𝐼 ‘ 𝐵 ) ∩ ( 𝐼 ‘ ∅ ) ) = ∅ → ( ( 𝐼 ‘ 𝐵 ) = 𝐵 → ( ( 𝐼 ‘ ∅ ) ⊆ 𝐵 → ( 𝐼 ‘ ∅ ) = ∅ ) ) )
44	43	com13	⊢ ( ( 𝐼 ‘ ∅ ) ⊆ 𝐵 → ( ( 𝐼 ‘ 𝐵 ) = 𝐵 → ( ( ( 𝐼 ‘ 𝐵 ) ∩ ( 𝐼 ‘ ∅ ) ) = ∅ → ( 𝐼 ‘ ∅ ) = ∅ ) ) )
45	29 30 44	syl2im	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) → ( ( ( 𝐼 ‘ 𝐵 ) = 𝐵 ∧ ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∩ 𝑡 ) = ∅ → ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ) ) → ( ( ( 𝐼 ‘ 𝐵 ) ∩ ( 𝐼 ‘ ∅ ) ) = ∅ → ( 𝐼 ‘ ∅ ) = ∅ ) ) )
46	24 45	mpdd	⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) ) → ( ( ( 𝐼 ‘ 𝐵 ) = 𝐵 ∧ ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∩ 𝑡 ) = ∅ → ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ) ) → ( 𝐼 ‘ ∅ ) = ∅ ) )