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 ‘ 𝐽 ) ‘ ( 𝐴𝐵 ) ) )