Theorem ntrneik13

Description: The interior of the intersection of any pair equals intersection of interiors if and only if the intersection of any pair belonging to the neighborhood of a point is equivalent to both of the pair belonging to the neighborhood of that point. (Contributed by RP, 19-Jun-2021)

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

Proof

Step	Hyp	Ref	Expression
1		ntrnei.o	⊢ 𝑂 = ( 𝑖 ∈ V , 𝑗 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑗 ↑m 𝑖 ) ↦ ( 𝑙 ∈ 𝑗 ↦ { 𝑚 ∈ 𝑖 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) ) )
2		ntrnei.f	⊢ 𝐹 = ( 𝒫 𝐵 𝑂 𝐵 )
3		ntrnei.r	⊢ ( 𝜑 → 𝐼 𝐹 𝑁 )
4		dfss3	⊢ ( ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) ⊆ ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ↔ ∀ 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) )
5	1 2 3	ntrneiiex	⊢ ( 𝜑 → 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) )
6		elmapi	⊢ ( 𝐼 ∈ ( 𝒫 𝐵 ↑m 𝒫 𝐵 ) → 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
7	5 6	syl	⊢ ( 𝜑 → 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
8	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
9	1 2 3	ntrneibex	⊢ ( 𝜑 → 𝐵 ∈ V )
10	9	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → 𝐵 ∈ V )
11		simplr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → 𝑠 ∈ 𝒫 𝐵 )
12		elpwi	⊢ ( 𝑠 ∈ 𝒫 𝐵 → 𝑠 ⊆ 𝐵 )
13		ssinss1	⊢ ( 𝑠 ⊆ 𝐵 → ( 𝑠 ∩ 𝑡 ) ⊆ 𝐵 )
14	11 12 13	3syl	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝑠 ∩ 𝑡 ) ⊆ 𝐵 )
15	10 14	sselpwd	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝑠 ∩ 𝑡 ) ∈ 𝒫 𝐵 )
16	8 15	ffvelrnd	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) ∈ 𝒫 𝐵 )
17	16	elpwid	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) ⊆ 𝐵 )
18		ralss	⊢ ( ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) ⊆ 𝐵 → ( ∀ 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) → 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ) ) )
19	17 18	syl	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ∀ 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) → 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ) ) )
20	4 19	syl5bb	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) ⊆ ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) → 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ) ) )
21		dfss3	⊢ ( ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ⊆ ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) ↔ ∀ 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) )
22	7	ffvelrnda	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( 𝐼 ‘ 𝑠 ) ∈ 𝒫 𝐵 )
23	22	elpwid	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( 𝐼 ‘ 𝑠 ) ⊆ 𝐵 )
24		ssinss1	⊢ ( ( 𝐼 ‘ 𝑠 ) ⊆ 𝐵 → ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ⊆ 𝐵 )
25	23 24	syl	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ⊆ 𝐵 )
26	25	adantr	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ⊆ 𝐵 )
27		ralss	⊢ ( ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ⊆ 𝐵 → ( ∀ 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) → 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) ) ) )
28	26 27	syl	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ∀ 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) → 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) ) ) )
29	21 28	syl5bb	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ⊆ ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) → 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) ) ) )
30	20 29	anbi12d	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ( ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) ⊆ ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ∧ ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ⊆ ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) ) ↔ ( ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) → 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) → 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) ) ) ) )
31		eqss	⊢ ( ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) = ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ↔ ( ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) ⊆ ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ∧ ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ⊆ ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) ) )
32		ralbiim	⊢ ( ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) ↔ 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ) ↔ ( ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) → 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ) ∧ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) → 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) ) ) )
33	30 31 32	3bitr4g	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) = ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) ↔ 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ) ) )
34	3	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝐼 𝐹 𝑁 )
35		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑥 ∈ 𝐵 )
36	9	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → 𝐵 ∈ V )
37		simpr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → 𝑠 ∈ 𝒫 𝐵 )
38	37	elpwid	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → 𝑠 ⊆ 𝐵 )
39	38 13	syl	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( 𝑠 ∩ 𝑡 ) ⊆ 𝐵 )
40	36 39	sselpwd	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( 𝑠 ∩ 𝑡 ) ∈ 𝒫 𝐵 )
41	40	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑠 ∩ 𝑡 ) ∈ 𝒫 𝐵 )
42	1 2 34 35 41	ntrneiel	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) ↔ ( 𝑠 ∩ 𝑡 ) ∈ ( 𝑁 ‘ 𝑥 ) ) )
43		elin	⊢ ( 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ↔ ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) )
44		simpllr	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑠 ∈ 𝒫 𝐵 )
45	1 2 34 35 44	ntrneiel	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ↔ 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ) )
46		simplr	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → 𝑡 ∈ 𝒫 𝐵 )
47	1 2 34 35 46	ntrneiel	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ↔ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) )
48	45 47	anbi12d	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑥 ∈ ( 𝐼 ‘ 𝑠 ) ∧ 𝑥 ∈ ( 𝐼 ‘ 𝑡 ) ) ↔ ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) )
49	43 48	syl5bb	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ↔ ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) )
50	42 49	bibi12d	⊢ ( ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) ∧ 𝑥 ∈ 𝐵 ) → ( ( 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) ↔ 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ) ↔ ( ( 𝑠 ∩ 𝑡 ) ∈ ( 𝑁 ‘ 𝑥 ) ↔ ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) ) )
51	50	ralbidva	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ∀ 𝑥 ∈ 𝐵 ( 𝑥 ∈ ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) ↔ 𝑥 ∈ ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( ( 𝑠 ∩ 𝑡 ) ∈ ( 𝑁 ‘ 𝑥 ) ↔ ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) ) )
52	33 51	bitrd	⊢ ( ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) ∧ 𝑡 ∈ 𝒫 𝐵 ) → ( ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) = ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ( ( 𝑠 ∩ 𝑡 ) ∈ ( 𝑁 ‘ 𝑥 ) ↔ ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) ) )
53	52	ralbidva	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) = ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ↔ ∀ 𝑡 ∈ 𝒫 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑠 ∩ 𝑡 ) ∈ ( 𝑁 ‘ 𝑥 ) ↔ ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) ) )
54		ralcom	⊢ ( ∀ 𝑡 ∈ 𝒫 𝐵 ∀ 𝑥 ∈ 𝐵 ( ( 𝑠 ∩ 𝑡 ) ∈ ( 𝑁 ‘ 𝑥 ) ↔ ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∩ 𝑡 ) ∈ ( 𝑁 ‘ 𝑥 ) ↔ ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) )
55	53 54	bitrdi	⊢ ( ( 𝜑 ∧ 𝑠 ∈ 𝒫 𝐵 ) → ( ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) = ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∩ 𝑡 ) ∈ ( 𝑁 ‘ 𝑥 ) ↔ ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) ) )
56	55	ralbidva	⊢ ( 𝜑 → ( ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) = ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ↔ ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑥 ∈ 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∩ 𝑡 ) ∈ ( 𝑁 ‘ 𝑥 ) ↔ ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) ) )
57		ralcom	⊢ ( ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑥 ∈ 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∩ 𝑡 ) ∈ ( 𝑁 ‘ 𝑥 ) ↔ ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∩ 𝑡 ) ∈ ( 𝑁 ‘ 𝑥 ) ↔ ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) )
58	56 57	bitrdi	⊢ ( 𝜑 → ( ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( 𝐼 ‘ ( 𝑠 ∩ 𝑡 ) ) = ( ( 𝐼 ‘ 𝑠 ) ∩ ( 𝐼 ‘ 𝑡 ) ) ↔ ∀ 𝑥 ∈ 𝐵 ∀ 𝑠 ∈ 𝒫 𝐵 ∀ 𝑡 ∈ 𝒫 𝐵 ( ( 𝑠 ∩ 𝑡 ) ∈ ( 𝑁 ‘ 𝑥 ) ↔ ( 𝑠 ∈ ( 𝑁 ‘ 𝑥 ) ∧ 𝑡 ∈ ( 𝑁 ‘ 𝑥 ) ) ) ) )