ntrneiel2

Description: Membership in iterated interior of a set is equivalent to there existing a particular neighborhood of that member such that points are members of that neighborhood if and only if the set is a neighborhood of each of those points. (Contributed by RP, 11-Jul-2021)

	Ref	Expression
Hypotheses	ntrnei.o	⊢ 𝑂 = ( 𝑖 ∈ V , 𝑗 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑗 ↑_m 𝑖 ) ↦ ( 𝑙 ∈ 𝑗 ↦ { 𝑚 ∈ 𝑖 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) ) )
	ntrnei.f	⊢ 𝐹 = ( 𝒫 𝐵 𝑂 𝐵 )
	ntrnei.r	⊢ ( 𝜑 → 𝐼 𝐹 𝑁 )
	ntrneiel2.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
	ntrneiel2.s	⊢ ( 𝜑 → 𝑆 ∈ 𝒫 𝐵 )
Assertion	ntrneiel2	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐼 ‘ ( 𝐼 ‘ 𝑆 ) ) ↔ ∃ 𝑢 ∈ ( 𝑁 ‘ 𝑋 ) ∀ 𝑦 ∈ 𝐵 ( 𝑦 ∈ 𝑢 ↔ 𝑆 ∈ ( 𝑁 ‘ 𝑦 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ntrnei.o	⊢ 𝑂 = ( 𝑖 ∈ V , 𝑗 ∈ V ↦ ( 𝑘 ∈ ( 𝒫 𝑗 ↑_m 𝑖 ) ↦ ( 𝑙 ∈ 𝑗 ↦ { 𝑚 ∈ 𝑖 ∣ 𝑙 ∈ ( 𝑘 ‘ 𝑚 ) } ) ) )
2		ntrnei.f	⊢ 𝐹 = ( 𝒫 𝐵 𝑂 𝐵 )
3		ntrnei.r	⊢ ( 𝜑 → 𝐼 𝐹 𝑁 )
4		ntrneiel2.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
5		ntrneiel2.s	⊢ ( 𝜑 → 𝑆 ∈ 𝒫 𝐵 )
6	1 2 3	ntrneiiex	⊢ ( 𝜑 → 𝐼 ∈ ( 𝒫 𝐵 ↑_m 𝒫 𝐵 ) )
7		elmapi	⊢ ( 𝐼 ∈ ( 𝒫 𝐵 ↑_m 𝒫 𝐵 ) → 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
8	6 7	syl	⊢ ( 𝜑 → 𝐼 : 𝒫 𝐵 ⟶ 𝒫 𝐵 )
9	8 5	ffvelcdmd	⊢ ( 𝜑 → ( 𝐼 ‘ 𝑆 ) ∈ 𝒫 𝐵 )
10	1 2 3 4 9	ntrneiel	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐼 ‘ ( 𝐼 ‘ 𝑆 ) ) ↔ ( 𝐼 ‘ 𝑆 ) ∈ ( 𝑁 ‘ 𝑋 ) ) )
11	1 2 3 5	ntrneifv4	⊢ ( 𝜑 → ( 𝐼 ‘ 𝑆 ) = { 𝑦 ∈ 𝐵 ∣ 𝑆 ∈ ( 𝑁 ‘ 𝑦 ) } )
12		df-rab	⊢ { 𝑦 ∈ 𝐵 ∣ 𝑆 ∈ ( 𝑁 ‘ 𝑦 ) } = { 𝑦 ∣ ( 𝑦 ∈ 𝐵 ∧ 𝑆 ∈ ( 𝑁 ‘ 𝑦 ) ) }
13	11 12	eqtrdi	⊢ ( 𝜑 → ( 𝐼 ‘ 𝑆 ) = { 𝑦 ∣ ( 𝑦 ∈ 𝐵 ∧ 𝑆 ∈ ( 𝑁 ‘ 𝑦 ) ) } )
14	13	eleq1d	⊢ ( 𝜑 → ( ( 𝐼 ‘ 𝑆 ) ∈ ( 𝑁 ‘ 𝑋 ) ↔ { 𝑦 ∣ ( 𝑦 ∈ 𝐵 ∧ 𝑆 ∈ ( 𝑁 ‘ 𝑦 ) ) } ∈ ( 𝑁 ‘ 𝑋 ) ) )
15		clabel	⊢ ( { 𝑦 ∣ ( 𝑦 ∈ 𝐵 ∧ 𝑆 ∈ ( 𝑁 ‘ 𝑦 ) ) } ∈ ( 𝑁 ‘ 𝑋 ) ↔ ∃ 𝑢 ( 𝑢 ∈ ( 𝑁 ‘ 𝑋 ) ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑢 ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑆 ∈ ( 𝑁 ‘ 𝑦 ) ) ) ) )
16		df-rex	⊢ ( ∃ 𝑢 ∈ ( 𝑁 ‘ 𝑋 ) ∀ 𝑦 ( 𝑦 ∈ 𝑢 ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑆 ∈ ( 𝑁 ‘ 𝑦 ) ) ) ↔ ∃ 𝑢 ( 𝑢 ∈ ( 𝑁 ‘ 𝑋 ) ∧ ∀ 𝑦 ( 𝑦 ∈ 𝑢 ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑆 ∈ ( 𝑁 ‘ 𝑦 ) ) ) ) )
17	15 16	bitr4i	⊢ ( { 𝑦 ∣ ( 𝑦 ∈ 𝐵 ∧ 𝑆 ∈ ( 𝑁 ‘ 𝑦 ) ) } ∈ ( 𝑁 ‘ 𝑋 ) ↔ ∃ 𝑢 ∈ ( 𝑁 ‘ 𝑋 ) ∀ 𝑦 ( 𝑦 ∈ 𝑢 ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑆 ∈ ( 𝑁 ‘ 𝑦 ) ) ) )
18		ibar	⊢ ( 𝑦 ∈ 𝐵 → ( 𝑆 ∈ ( 𝑁 ‘ 𝑦 ) ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑆 ∈ ( 𝑁 ‘ 𝑦 ) ) ) )
19	18	bibi2d	⊢ ( 𝑦 ∈ 𝐵 → ( ( 𝑦 ∈ 𝑢 ↔ 𝑆 ∈ ( 𝑁 ‘ 𝑦 ) ) ↔ ( 𝑦 ∈ 𝑢 ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑆 ∈ ( 𝑁 ‘ 𝑦 ) ) ) ) )
20	19	ralbiia	⊢ ( ∀ 𝑦 ∈ 𝐵 ( 𝑦 ∈ 𝑢 ↔ 𝑆 ∈ ( 𝑁 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ 𝐵 ( 𝑦 ∈ 𝑢 ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑆 ∈ ( 𝑁 ‘ 𝑦 ) ) ) )
21		ssv	⊢ 𝐵 ⊆ V
22	21	a1i	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 ‘ 𝑋 ) ) → 𝐵 ⊆ V )
23		vex	⊢ 𝑦 ∈ V
24		eldif	⊢ ( 𝑦 ∈ ( V ∖ 𝐵 ) ↔ ( 𝑦 ∈ V ∧ ¬ 𝑦 ∈ 𝐵 ) )
25	23 24	mpbiran	⊢ ( 𝑦 ∈ ( V ∖ 𝐵 ) ↔ ¬ 𝑦 ∈ 𝐵 )
26	1 2 3	ntrneinex	⊢ ( 𝜑 → 𝑁 ∈ ( 𝒫 𝒫 𝐵 ↑_m 𝐵 ) )
27		elmapi	⊢ ( 𝑁 ∈ ( 𝒫 𝒫 𝐵 ↑_m 𝐵 ) → 𝑁 : 𝐵 ⟶ 𝒫 𝒫 𝐵 )
28	26 27	syl	⊢ ( 𝜑 → 𝑁 : 𝐵 ⟶ 𝒫 𝒫 𝐵 )
29	28 4	ffvelcdmd	⊢ ( 𝜑 → ( 𝑁 ‘ 𝑋 ) ∈ 𝒫 𝒫 𝐵 )
30	29	elpwid	⊢ ( 𝜑 → ( 𝑁 ‘ 𝑋 ) ⊆ 𝒫 𝐵 )
31	30	sselda	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 ‘ 𝑋 ) ) → 𝑢 ∈ 𝒫 𝐵 )
32	31	elpwid	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 ‘ 𝑋 ) ) → 𝑢 ⊆ 𝐵 )
33	32	sseld	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 ‘ 𝑋 ) ) → ( 𝑦 ∈ 𝑢 → 𝑦 ∈ 𝐵 ) )
34	33	con3dimp	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 ‘ 𝑋 ) ) ∧ ¬ 𝑦 ∈ 𝐵 ) → ¬ 𝑦 ∈ 𝑢 )
35		pm3.14	⊢ ( ( ¬ 𝑦 ∈ 𝐵 ∨ ¬ 𝑆 ∈ ( 𝑁 ‘ 𝑦 ) ) → ¬ ( 𝑦 ∈ 𝐵 ∧ 𝑆 ∈ ( 𝑁 ‘ 𝑦 ) ) )
36	35	orcs	⊢ ( ¬ 𝑦 ∈ 𝐵 → ¬ ( 𝑦 ∈ 𝐵 ∧ 𝑆 ∈ ( 𝑁 ‘ 𝑦 ) ) )
37	36	adantl	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 ‘ 𝑋 ) ) ∧ ¬ 𝑦 ∈ 𝐵 ) → ¬ ( 𝑦 ∈ 𝐵 ∧ 𝑆 ∈ ( 𝑁 ‘ 𝑦 ) ) )
38	34 37	2falsed	⊢ ( ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 ‘ 𝑋 ) ) ∧ ¬ 𝑦 ∈ 𝐵 ) → ( 𝑦 ∈ 𝑢 ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑆 ∈ ( 𝑁 ‘ 𝑦 ) ) ) )
39	38	ex	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 ‘ 𝑋 ) ) → ( ¬ 𝑦 ∈ 𝐵 → ( 𝑦 ∈ 𝑢 ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑆 ∈ ( 𝑁 ‘ 𝑦 ) ) ) ) )
40	25 39	biimtrid	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 ‘ 𝑋 ) ) → ( 𝑦 ∈ ( V ∖ 𝐵 ) → ( 𝑦 ∈ 𝑢 ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑆 ∈ ( 𝑁 ‘ 𝑦 ) ) ) ) )
41	40	ralrimiv	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 ‘ 𝑋 ) ) → ∀ 𝑦 ∈ ( V ∖ 𝐵 ) ( 𝑦 ∈ 𝑢 ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑆 ∈ ( 𝑁 ‘ 𝑦 ) ) ) )
42	22 41	raldifeq	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 ‘ 𝑋 ) ) → ( ∀ 𝑦 ∈ 𝐵 ( 𝑦 ∈ 𝑢 ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑆 ∈ ( 𝑁 ‘ 𝑦 ) ) ) ↔ ∀ 𝑦 ∈ V ( 𝑦 ∈ 𝑢 ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑆 ∈ ( 𝑁 ‘ 𝑦 ) ) ) ) )
43	20 42	bitrid	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 ‘ 𝑋 ) ) → ( ∀ 𝑦 ∈ 𝐵 ( 𝑦 ∈ 𝑢 ↔ 𝑆 ∈ ( 𝑁 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ V ( 𝑦 ∈ 𝑢 ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑆 ∈ ( 𝑁 ‘ 𝑦 ) ) ) ) )
44		ralv	⊢ ( ∀ 𝑦 ∈ V ( 𝑦 ∈ 𝑢 ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑆 ∈ ( 𝑁 ‘ 𝑦 ) ) ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑢 ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑆 ∈ ( 𝑁 ‘ 𝑦 ) ) ) )
45	43 44	bitr2di	⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 ‘ 𝑋 ) ) → ( ∀ 𝑦 ( 𝑦 ∈ 𝑢 ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑆 ∈ ( 𝑁 ‘ 𝑦 ) ) ) ↔ ∀ 𝑦 ∈ 𝐵 ( 𝑦 ∈ 𝑢 ↔ 𝑆 ∈ ( 𝑁 ‘ 𝑦 ) ) ) )
46	45	rexbidva	⊢ ( 𝜑 → ( ∃ 𝑢 ∈ ( 𝑁 ‘ 𝑋 ) ∀ 𝑦 ( 𝑦 ∈ 𝑢 ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑆 ∈ ( 𝑁 ‘ 𝑦 ) ) ) ↔ ∃ 𝑢 ∈ ( 𝑁 ‘ 𝑋 ) ∀ 𝑦 ∈ 𝐵 ( 𝑦 ∈ 𝑢 ↔ 𝑆 ∈ ( 𝑁 ‘ 𝑦 ) ) ) )
47	17 46	bitrid	⊢ ( 𝜑 → ( { 𝑦 ∣ ( 𝑦 ∈ 𝐵 ∧ 𝑆 ∈ ( 𝑁 ‘ 𝑦 ) ) } ∈ ( 𝑁 ‘ 𝑋 ) ↔ ∃ 𝑢 ∈ ( 𝑁 ‘ 𝑋 ) ∀ 𝑦 ∈ 𝐵 ( 𝑦 ∈ 𝑢 ↔ 𝑆 ∈ ( 𝑁 ‘ 𝑦 ) ) ) )
48	10 14 47	3bitrd	⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐼 ‘ ( 𝐼 ‘ 𝑆 ) ) ↔ ∃ 𝑢 ∈ ( 𝑁 ‘ 𝑋 ) ∀ 𝑦 ∈ 𝐵 ( 𝑦 ∈ 𝑢 ↔ 𝑆 ∈ ( 𝑁 ‘ 𝑦 ) ) ) )

Metamath Proof Explorer

Theorem ntrneiel2

Proof