Metamath Proof Explorer

Theorem neiin

Description: Two neighborhoods intersect to form a neighborhood of the intersection. (Contributed by Jeff Hankins, 31-Aug-2009)

Ref Expression
Assertion neiin ( ( 𝐽 ∈ Top ∧ 𝑀 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐵 ) ) → ( 𝑀 ∩ 𝑁 ) ∈ ( ( nei ‘ 𝐽 ) ‘ ( 𝐴 ∩ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( 𝐽 ∈ Top ∧ 𝑀 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐴 ) ) → 𝑀 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐴 ) )
2 simpl ⊢ ( ( 𝐽 ∈ Top ∧ 𝑀 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐴 ) ) → 𝐽 ∈ Top )
3 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
4 3 neiss2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑀 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐴 ) ) → 𝐴 ⊆ ∪ 𝐽 )
5 3 neii1 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑀 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐴 ) ) → 𝑀 ⊆ ∪ 𝐽 )
6 3 neiint ⊢ ( ( 𝐽 ∈ Top ∧ 𝐴 ⊆ ∪ 𝐽 ∧ 𝑀 ⊆ ∪ 𝐽 ) → ( 𝑀 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐴 ) ↔ 𝐴 ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑀 ) ) )
7 2 4 5 6 syl3anc ⊢ ( ( 𝐽 ∈ Top ∧ 𝑀 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐴 ) ) → ( 𝑀 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐴 ) ↔ 𝐴 ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑀 ) ) )
8 1 7 mpbid ⊢ ( ( 𝐽 ∈ Top ∧ 𝑀 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐴 ) ) → 𝐴 ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑀 ) )
9 ssinss1 ⊢ ( 𝐴 ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑀 ) → ( 𝐴 ∩ 𝐵 ) ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑀 ) )
10 8 9 syl ⊢ ( ( 𝐽 ∈ Top ∧ 𝑀 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐴 ) ) → ( 𝐴 ∩ 𝐵 ) ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑀 ) )
11 10 3adant3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑀 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐵 ) ) → ( 𝐴 ∩ 𝐵 ) ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑀 ) )
12 inss2 ⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵
13 simpr ⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐵 ) ) → 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐵 ) )
14 simpl ⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐵 ) ) → 𝐽 ∈ Top )
15 3 neiss2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐵 ) ) → 𝐵 ⊆ ∪ 𝐽 )
16 3 neii1 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐵 ) ) → 𝑁 ⊆ ∪ 𝐽 )
17 3 neiint ⊢ ( ( 𝐽 ∈ Top ∧ 𝐵 ⊆ ∪ 𝐽 ∧ 𝑁 ⊆ ∪ 𝐽 ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐵 ) ↔ 𝐵 ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ) )
18 14 15 16 17 syl3anc ⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐵 ) ) → ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐵 ) ↔ 𝐵 ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ) )
19 13 18 mpbid ⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐵 ) ) → 𝐵 ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑁 ) )
20 19 3adant2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑀 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐵 ) ) → 𝐵 ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑁 ) )
21 12 20 sstrid ⊢ ( ( 𝐽 ∈ Top ∧ 𝑀 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐵 ) ) → ( 𝐴 ∩ 𝐵 ) ⊆ ( ( int ‘ 𝐽 ) ‘ 𝑁 ) )
22 11 21 ssind ⊢ ( ( 𝐽 ∈ Top ∧ 𝑀 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐵 ) ) → ( 𝐴 ∩ 𝐵 ) ⊆ ( ( ( int ‘ 𝐽 ) ‘ 𝑀 ) ∩ ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ) )
23 simp1 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑀 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐵 ) ) → 𝐽 ∈ Top )
24 5 3adant3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑀 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐵 ) ) → 𝑀 ⊆ ∪ 𝐽 )
25 16 3adant2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑀 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐵 ) ) → 𝑁 ⊆ ∪ 𝐽 )
26 3 ntrin ⊢ ( ( 𝐽 ∈ Top ∧ 𝑀 ⊆ ∪ 𝐽 ∧ 𝑁 ⊆ ∪ 𝐽 ) → ( ( int ‘ 𝐽 ) ‘ ( 𝑀 ∩ 𝑁 ) ) = ( ( ( int ‘ 𝐽 ) ‘ 𝑀 ) ∩ ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ) )
27 23 24 25 26 syl3anc ⊢ ( ( 𝐽 ∈ Top ∧ 𝑀 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐵 ) ) → ( ( int ‘ 𝐽 ) ‘ ( 𝑀 ∩ 𝑁 ) ) = ( ( ( int ‘ 𝐽 ) ‘ 𝑀 ) ∩ ( ( int ‘ 𝐽 ) ‘ 𝑁 ) ) )
28 22 27 sseqtrrd ⊢ ( ( 𝐽 ∈ Top ∧ 𝑀 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐵 ) ) → ( 𝐴 ∩ 𝐵 ) ⊆ ( ( int ‘ 𝐽 ) ‘ ( 𝑀 ∩ 𝑁 ) ) )
29 ssinss1 ⊢ ( 𝐴 ⊆ ∪ 𝐽 → ( 𝐴 ∩ 𝐵 ) ⊆ ∪ 𝐽 )
30 4 29 syl ⊢ ( ( 𝐽 ∈ Top ∧ 𝑀 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐴 ) ) → ( 𝐴 ∩ 𝐵 ) ⊆ ∪ 𝐽 )
31 ssinss1 ⊢ ( 𝑀 ⊆ ∪ 𝐽 → ( 𝑀 ∩ 𝑁 ) ⊆ ∪ 𝐽 )
32 5 31 syl ⊢ ( ( 𝐽 ∈ Top ∧ 𝑀 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐴 ) ) → ( 𝑀 ∩ 𝑁 ) ⊆ ∪ 𝐽 )
33 3 neiint ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝐴 ∩ 𝐵 ) ⊆ ∪ 𝐽 ∧ ( 𝑀 ∩ 𝑁 ) ⊆ ∪ 𝐽 ) → ( ( 𝑀 ∩ 𝑁 ) ∈ ( ( nei ‘ 𝐽 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ↔ ( 𝐴 ∩ 𝐵 ) ⊆ ( ( int ‘ 𝐽 ) ‘ ( 𝑀 ∩ 𝑁 ) ) ) )
34 2 30 32 33 syl3anc ⊢ ( ( 𝐽 ∈ Top ∧ 𝑀 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐴 ) ) → ( ( 𝑀 ∩ 𝑁 ) ∈ ( ( nei ‘ 𝐽 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ↔ ( 𝐴 ∩ 𝐵 ) ⊆ ( ( int ‘ 𝐽 ) ‘ ( 𝑀 ∩ 𝑁 ) ) ) )
35 34 3adant3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑀 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐵 ) ) → ( ( 𝑀 ∩ 𝑁 ) ∈ ( ( nei ‘ 𝐽 ) ‘ ( 𝐴 ∩ 𝐵 ) ) ↔ ( 𝐴 ∩ 𝐵 ) ⊆ ( ( int ‘ 𝐽 ) ‘ ( 𝑀 ∩ 𝑁 ) ) ) )
36 28 35 mpbird ⊢ ( ( 𝐽 ∈ Top ∧ 𝑀 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐴 ) ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝐵 ) ) → ( 𝑀 ∩ 𝑁 ) ∈ ( ( nei ‘ 𝐽 ) ‘ ( 𝐴 ∩ 𝐵 ) ) )