Theorem ntrneikb

Description: The interiors of disjoint sets are disjoint if and only if the neighborhoods of every point contain no disjoint sets. (Contributed by RP, 11-Jun-2021)

	Ref	Expression
Hypotheses	ntrnei.o	⊢ 𝑂 = ( 𝑖 ∈ V , 𝑗 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑗 ↑m 𝑖 ) ↦ ( 𝑙 ∈ 𝑗 ↦ { 𝑚 ∈ 𝑖 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) ) )
	ntrnei.f	⊢ 𝐹 = ( 𝒫 𝐵 𝑂 𝐵 )
	ntrnei.r	⊢ ( 𝜑 → 𝐼 𝐹 𝑁 )
Assertion	ntrneikb	⊢ ( 𝜑 → ( ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∩ 𝑡 ) = ∅ → ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) → ( 𝑠 ∩ 𝑡 ) ≠ ∅ ) ) )

Proof

Step	Hyp	Ref	Expression
1		ntrnei.o	⊢ 𝑂 = ( 𝑖 ∈ V , 𝑗 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑗 ↑m 𝑖 ) ↦ ( 𝑙 ∈ 𝑗 ↦ { 𝑚 ∈ 𝑖 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) ) )
2		ntrnei.f	⊢ 𝐹 = ( 𝒫 𝐵 𝑂 𝐵 )
3		ntrnei.r	⊢ ( 𝜑 → 𝐼 𝐹 𝑁 )
4		con34b	⊢ ( ( ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) → ( 𝑠 ∩ 𝑡 ) ≠ ∅ ) ↔ ( ¬ ( 𝑠 ∩ 𝑡 ) ≠ ∅ → ¬ ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) ) )
5	4	albii	⊢ ( ∀ 𝑥 ( ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) → ( 𝑠 ∩ 𝑡 ) ≠ ∅ ) ↔ ∀ 𝑥 ( ¬ ( 𝑠 ∩ 𝑡 ) ≠ ∅ → ¬ ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) ) )
6		19.21v	⊢ ( ∀ 𝑥 ( ¬ ( 𝑠 ∩ 𝑡 ) ≠ ∅ → ¬ ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) ) ↔ ( ¬ ( 𝑠 ∩ 𝑡 ) ≠ ∅ → ∀ 𝑥 ¬ ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) ) )
7		nne	⊢ ( ¬ ( 𝑠 ∩ 𝑡 ) ≠ ∅ ↔ ( 𝑠 ∩ 𝑡 ) = ∅ )
8		elin	⊢ ( 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ↔ ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) )
9	8	imbi1i	⊢ ( ( 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) → 𝑥 ∈ ∅ ) ↔ ( ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) → 𝑥 ∈ ∅ ) )
10		noel	⊢ ¬ 𝑥 ∈ ∅
11		imnot	⊢ ( ¬ 𝑥 ∈ ∅ → ( ( ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) → 𝑥 ∈ ∅ ) ↔ ¬ ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) ) )
12	10 11	ax-mp	⊢ ( ( ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) → 𝑥 ∈ ∅ ) ↔ ¬ ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) )
13	9 12	bitr2i	⊢ ( ¬ ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) ↔ ( 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) → 𝑥 ∈ ∅ ) )
14	13	albii	⊢ ( ∀ 𝑥 ¬ ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) ↔ ∀ 𝑥 ( 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) → 𝑥 ∈ ∅ ) )
15		df-ss	⊢ ( ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ⊆ ∅ ↔ ∀ 𝑥 ( 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) → 𝑥 ∈ ∅ ) )
16		ss0b	⊢ ( ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ⊆ ∅ ↔ ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ )
17	14 15 16	3bitr2i	⊢ ( ∀ 𝑥 ¬ ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) ↔ ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ )
18	7 17	imbi12i	⊢ ( ( ¬ ( 𝑠 ∩ 𝑡 ) ≠ ∅ → ∀ 𝑥 ¬ ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) ) ↔ ( ( 𝑠 ∩ 𝑡 ) = ∅ → ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ) )
19	5 6 18	3bitrri	⊢ ( ( ( 𝑠 ∩ 𝑡 ) = ∅ → ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ) ↔ ∀ 𝑥 ( ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) → ( 𝑠 ∩ 𝑡 ) ≠ ∅ ) )
20	1 2 3	ntrneiiex	⊢ ( 𝜑 → 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
21		elmapi	⊢ ( 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) → 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
22	20 21	syl	⊢ ( 𝜑 → 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
23	22	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( 𝐼 ‘ 𝑠 ) ∈ 𝒫 𝐵 )
24	23	adantr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝐼 ‘ 𝑠 ) ∈ 𝒫 𝐵 )
25	24	elpwid	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝐼 ‘ 𝑠 ) ⊆ 𝐵 )
26	25	sseld	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) → 𝑥 ∈ 𝐵 ) )
27	26	adantrd	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) → 𝑥 ∈ 𝐵 ) )
28	27	imp	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) ) → 𝑥 ∈ 𝐵 )
29		biimt	⊢ ( 𝑥 ∈ 𝐵 → ( ( 𝑠 ∩ 𝑡 ) ≠ ∅ ↔ ( 𝑥 ∈ 𝐵 → ( 𝑠 ∩ 𝑡 ) ≠ ∅ ) ) )
30	28 29	syl	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) ) → ( ( 𝑠 ∩ 𝑡 ) ≠ ∅ ↔ ( 𝑥 ∈ 𝐵 → ( 𝑠 ∩ 𝑡 ) ≠ ∅ ) ) )
31	30	pm5.74da	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ( ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) → ( 𝑠 ∩ 𝑡 ) ≠ ∅ ) ↔ ( ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) → ( 𝑥 ∈ 𝐵 → ( 𝑠 ∩ 𝑡 ) ≠ ∅ ) ) ) )
32		bi2.04	⊢ ( ( ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) → ( 𝑥 ∈ 𝐵 → ( 𝑠 ∩ 𝑡 ) ≠ ∅ ) ) ↔ ( 𝑥 ∈ 𝐵 → ( ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) → ( 𝑠 ∩ 𝑡 ) ≠ ∅ ) ) )
33	31 32	bitrdi	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ( ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) → ( 𝑠 ∩ 𝑡 ) ≠ ∅ ) ↔ ( 𝑥 ∈ 𝐵 → ( ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) → ( 𝑠 ∩ 𝑡 ) ≠ ∅ ) ) ) )
34	33	albidv	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ∀ 𝑥 ( ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) → ( 𝑠 ∩ 𝑡 ) ≠ ∅ ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → ( ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) → ( 𝑠 ∩ 𝑡 ) ≠ ∅ ) ) ) )
35		df-ral	⊢ ( ∀ 𝑥 ∈ 𝐵 ( ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) → ( 𝑠 ∩ 𝑡 ) ≠ ∅ ) ↔ ∀ 𝑥 ( 𝑥 ∈ 𝐵 → ( ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) → ( 𝑠 ∩ 𝑡 ) ≠ ∅ ) ) )
36	34 35	bitr4di	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ∀ 𝑥 ( ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) → ( 𝑠 ∩ 𝑡 ) ≠ ∅ ) ↔ ∀ 𝑥 ∈ 𝐵 ( ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) → ( 𝑠 ∩ 𝑡 ) ≠ ∅ ) ) )
37	3	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝐼 𝐹 𝑁 )
38		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
39		simpllr	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑠 ∈ 𝒫 𝐵 )
40	1 2 37 38 39	ntrneiel	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ↔ 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ) )
41		simplr	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑡 ∈ 𝒫 𝐵 )
42	1 2 37 38 41	ntrneiel	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ↔ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) )
43	40 42	anbi12d	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) ↔ ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) )
44	43	imbi1d	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) → ( 𝑠 ∩ 𝑡 ) ≠ ∅ ) ↔ ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) → ( 𝑠 ∩ 𝑡 ) ≠ ∅ ) ) )
45	44	ralbidva	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ( ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) → ( 𝑠 ∩ 𝑡 ) ≠ ∅ ) ↔ ∀ 𝑥 ∈ 𝐵 ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) → ( 𝑠 ∩ 𝑡 ) ≠ ∅ ) ) )
46	36 45	bitrd	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ∀ 𝑥 ( ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) → ( 𝑠 ∩ 𝑡 ) ≠ ∅ ) ↔ ∀ 𝑥 ∈ 𝐵 ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) → ( 𝑠 ∩ 𝑡 ) ≠ ∅ ) ) )
47	19 46	bitrid	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ( ( 𝑠 ∩ 𝑡 ) = ∅ → ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ) ↔ ∀ 𝑥 ∈ 𝐵 ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) → ( 𝑠 ∩ 𝑡 ) ≠ ∅ ) ) )
48	47	ralbidva	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∩ 𝑡 ) = ∅ → ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ) ↔ ∀ 𝑡 ∈ 𝒫 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) → ( 𝑠 ∩ 𝑡 ) ≠ ∅ ) ) )
49	48	ralbidva	⊢ ( 𝜑 → ( ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∩ 𝑡 ) = ∅ → ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ) ↔ ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) → ( 𝑠 ∩ 𝑡 ) ≠ ∅ ) ) )
50		ralrot3	⊢ ( ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) → ( 𝑠 ∩ 𝑡 ) ≠ ∅ ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) → ( 𝑠 ∩ 𝑡 ) ≠ ∅ ) )
51	49 50	bitrdi	⊢ ( 𝜑 → ( ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∩ 𝑡 ) = ∅ → ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) = ∅ ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) → ( 𝑠 ∩ 𝑡 ) ≠ ∅ ) ) )