Metamath Proof Explorer

Theorem 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 ffvelrnd ⊢ ( 𝜑 → ( 𝐼 ‘ 𝑆 ) ∈ 𝒫 𝐵 )
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 ffvelrnd ⊢ ( 𝜑 → ( 𝑁 ‘ 𝑋 ) ∈ 𝒫 𝒫 𝐵 )
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 syl5bi ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 ‘ 𝑋 ) ) → ( 𝑦 ∈ ( V ∖ 𝐵 ) → ( 𝑦 ∈ 𝑢 ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑆 ∈ ( 𝑁 ‘ 𝑦 ) ) ) ) )
41 40 ralrimiv ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 ‘ 𝑋 ) ) → ∀ 𝑦 ∈ ( V ∖ 𝐵 ) ( 𝑦 ∈ 𝑢 ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑆 ∈ ( 𝑁 ‘ 𝑦 ) ) ) )
42 22 41 raldifeq ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 ‘ 𝑋 ) ) → ( ∀ 𝑦 ∈ 𝐵 ( 𝑦 ∈ 𝑢 ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑆 ∈ ( 𝑁 ‘ 𝑦 ) ) ) ↔ ∀ 𝑦 ∈ V ( 𝑦 ∈ 𝑢 ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑆 ∈ ( 𝑁 ‘ 𝑦 ) ) ) ) )
43 20 42 syl5bb ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 ‘ 𝑋 ) ) → ( ∀ 𝑦 ∈ 𝐵 ( 𝑦 ∈ 𝑢 ↔ 𝑆 ∈ ( 𝑁 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ V ( 𝑦 ∈ 𝑢 ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑆 ∈ ( 𝑁 ‘ 𝑦 ) ) ) ) )
44 ralv ⊢ ( ∀ 𝑦 ∈ V ( 𝑦 ∈ 𝑢 ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑆 ∈ ( 𝑁 ‘ 𝑦 ) ) ) ↔ ∀ 𝑦 ( 𝑦 ∈ 𝑢 ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑆 ∈ ( 𝑁 ‘ 𝑦 ) ) ) )
45 43 44 bitr2di ⊢ ( ( 𝜑 ∧ 𝑢 ∈ ( 𝑁 ‘ 𝑋 ) ) → ( ∀ 𝑦 ( 𝑦 ∈ 𝑢 ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑆 ∈ ( 𝑁 ‘ 𝑦 ) ) ) ↔ ∀ 𝑦 ∈ 𝐵 ( 𝑦 ∈ 𝑢 ↔ 𝑆 ∈ ( 𝑁 ‘ 𝑦 ) ) ) )
46 45 rexbidva ⊢ ( 𝜑 → ( ∃ 𝑢 ∈ ( 𝑁 ‘ 𝑋 ) ∀ 𝑦 ( 𝑦 ∈ 𝑢 ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑆 ∈ ( 𝑁 ‘ 𝑦 ) ) ) ↔ ∃ 𝑢 ∈ ( 𝑁 ‘ 𝑋 ) ∀ 𝑦 ∈ 𝐵 ( 𝑦 ∈ 𝑢 ↔ 𝑆 ∈ ( 𝑁 ‘ 𝑦 ) ) ) )
47 17 46 syl5bb ⊢ ( 𝜑 → ( { 𝑦 ∣ ( 𝑦 ∈ 𝐵 ∧ 𝑆 ∈ ( 𝑁 ‘ 𝑦 ) ) } ∈ ( 𝑁 ‘ 𝑋 ) ↔ ∃ 𝑢 ∈ ( 𝑁 ‘ 𝑋 ) ∀ 𝑦 ∈ 𝐵 ( 𝑦 ∈ 𝑢 ↔ 𝑆 ∈ ( 𝑁 ‘ 𝑦 ) ) ) )
48 10 14 47 3bitrd ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝐼 ‘ ( 𝐼 ‘ 𝑆 ) ) ↔ ∃ 𝑢 ∈ ( 𝑁 ‘ 𝑋 ) ∀ 𝑦 ∈ 𝐵 ( 𝑦 ∈ 𝑢 ↔ 𝑆 ∈ ( 𝑁 ‘ 𝑦 ) ) ) )