Metamath Proof Explorer

Theorem neiint

Description: An intuitive definition of a neighborhood in terms of interior. (Contributed by Szymon Jaroszewicz, 18-Dec-2007) (Revised by Mario Carneiro, 11-Nov-2013)

Ref Expression
Hypothesis neifval.1 ⊢ 𝑋 = ∪ 𝐽
Assertion neiint ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑁 ⊆ 𝑋 ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ↔ 𝑆 ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 neifval.1 ⊢ 𝑋 = ∪ 𝐽
2 1 isnei ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ↔ ( 𝑁 ⊆ 𝑋 ∧ ∃ 𝑣 ∈ 𝐽 ( 𝑆 ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑁 ) ) ) )
3 2 3adant3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑁 ⊆ 𝑋 ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ↔ ( 𝑁 ⊆ 𝑋 ∧ ∃ 𝑣 ∈ 𝐽 ( 𝑆 ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑁 ) ) ) )
4 3 3anibar ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑁 ⊆ 𝑋 ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ↔ ∃ 𝑣 ∈ 𝐽 ( 𝑆 ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑁 ) ) )
5 simprrl ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑁 ⊆ 𝑋 ) ∧ ( 𝑣 ∈ 𝐽 ∧ ( 𝑆 ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑁 ) ) ) → 𝑆 ⊆ 𝑣 )
6 1 ssntr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑁 ⊆ 𝑋 ) ∧ ( 𝑣 ∈ 𝐽 ∧ 𝑣 ⊆ 𝑁 ) ) → 𝑣 ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑁 ) )
7 6 3adantl2 ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑁 ⊆ 𝑋 ) ∧ ( 𝑣 ∈ 𝐽 ∧ 𝑣 ⊆ 𝑁 ) ) → 𝑣 ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑁 ) )
8 7 adantrrl ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑁 ⊆ 𝑋 ) ∧ ( 𝑣 ∈ 𝐽 ∧ ( 𝑆 ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑁 ) ) ) → 𝑣 ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑁 ) )
9 5 8 sstrd ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑁 ⊆ 𝑋 ) ∧ ( 𝑣 ∈ 𝐽 ∧ ( 𝑆 ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑁 ) ) ) → 𝑆 ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑁 ) )
10 9 rexlimdvaa ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑁 ⊆ 𝑋 ) → ( ∃ 𝑣 ∈ 𝐽 ( 𝑆 ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑁 ) → 𝑆 ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ) )
11 simpl1 ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑁 ⊆ 𝑋 ) ∧ 𝑆 ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ) → 𝐽 ∈ Top )
12 simpl3 ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑁 ⊆ 𝑋 ) ∧ 𝑆 ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ) → 𝑁 ⊆ 𝑋 )
13 1 ntropn ⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ∈ 𝐽 )
14 11 12 13 syl2anc ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑁 ⊆ 𝑋 ) ∧ 𝑆 ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ) → ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ∈ 𝐽 )
15 simpr ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑁 ⊆ 𝑋 ) ∧ 𝑆 ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ) → 𝑆 ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑁 ) )
16 1 ntrss2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ⊆ 𝑋 ) → ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ⊆ 𝑁 )
17 11 12 16 syl2anc ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑁 ⊆ 𝑋 ) ∧ 𝑆 ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ) → ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ⊆ 𝑁 )
18 sseq2 ⊢ ( 𝑣 = ( ( int ‘ 𝐽 ) ‘ 𝑁 ) → ( 𝑆 ⊆ 𝑣 ↔ 𝑆 ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ) )
19 sseq1 ⊢ ( 𝑣 = ( ( int ‘ 𝐽 ) ‘ 𝑁 ) → ( 𝑣 ⊆ 𝑁 ↔ ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ⊆ 𝑁 ) )
20 18 19 anbi12d ⊢ ( 𝑣 = ( ( int ‘ 𝐽 ) ‘ 𝑁 ) → ( ( 𝑆 ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑁 ) ↔ ( 𝑆 ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ∧ ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ⊆ 𝑁 ) ) )
21 20 rspcev ⊢ ( ( ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ∈ 𝐽 ∧ ( 𝑆 ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ∧ ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ⊆ 𝑁 ) ) → ∃ 𝑣 ∈ 𝐽 ( 𝑆 ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑁 ) )
22 14 15 17 21 syl12anc ⊢ ( ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑁 ⊆ 𝑋 ) ∧ 𝑆 ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ) → ∃ 𝑣 ∈ 𝐽 ( 𝑆 ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑁 ) )
23 22 ex ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑁 ⊆ 𝑋 ) → ( 𝑆 ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑁 ) → ∃ 𝑣 ∈ 𝐽 ( 𝑆 ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑁 ) ) )
24 10 23 impbid ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑁 ⊆ 𝑋 ) → ( ∃ 𝑣 ∈ 𝐽 ( 𝑆 ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑁 ) ↔ 𝑆 ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ) )
25 4 24 bitrd ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ 𝑁 ⊆ 𝑋 ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ↔ 𝑆 ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ) )