This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem innei

Description: The intersection of two neighborhoods of a set is also a neighborhood of the set. Generalization to subsets of Property V_ii of BourbakiTop1 p. I.3 for binary intersections. (Contributed by FL, 28-Sep-2006)

Ref Expression
Assertion innei ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑀 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → ( 𝑁 ∩ 𝑀 ) ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ∪ 𝐽 = ∪ 𝐽
2 1 neii1 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑁 ⊆ ∪ 𝐽 )
3 ssinss1 ⊢ ( 𝑁 ⊆ ∪ 𝐽 → ( 𝑁 ∩ 𝑀 ) ⊆ ∪ 𝐽 )
4 2 3 syl ⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → ( 𝑁 ∩ 𝑀 ) ⊆ ∪ 𝐽 )
5 4 3adant3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑀 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → ( 𝑁 ∩ 𝑀 ) ⊆ ∪ 𝐽 )
6 neii2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → ∃ ℎ ∈ 𝐽 ( 𝑆 ⊆ ℎ ∧ ℎ ⊆ 𝑁 ) )
7 neii2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑀 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → ∃ 𝑣 ∈ 𝐽 ( 𝑆 ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑀 ) )
8 6 7 anim12dan ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑀 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ) → ( ∃ ℎ ∈ 𝐽 ( 𝑆 ⊆ ℎ ∧ ℎ ⊆ 𝑁 ) ∧ ∃ 𝑣 ∈ 𝐽 ( 𝑆 ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑀 ) ) )
9 inopn ⊢ ( ( 𝐽 ∈ Top ∧ ℎ ∈ 𝐽 ∧ 𝑣 ∈ 𝐽 ) → ( ℎ ∩ 𝑣 ) ∈ 𝐽 )
10 9 3expa ⊢ ( ( ( 𝐽 ∈ Top ∧ ℎ ∈ 𝐽 ) ∧ 𝑣 ∈ 𝐽 ) → ( ℎ ∩ 𝑣 ) ∈ 𝐽 )
11 ssin ⊢ ( ( 𝑆 ⊆ ℎ ∧ 𝑆 ⊆ 𝑣 ) ↔ 𝑆 ⊆ ( ℎ ∩ 𝑣 ) )
12 11 biimpi ⊢ ( ( 𝑆 ⊆ ℎ ∧ 𝑆 ⊆ 𝑣 ) → 𝑆 ⊆ ( ℎ ∩ 𝑣 ) )
13 ss2in ⊢ ( ( ℎ ⊆ 𝑁 ∧ 𝑣 ⊆ 𝑀 ) → ( ℎ ∩ 𝑣 ) ⊆ ( 𝑁 ∩ 𝑀 ) )
14 12 13 anim12i ⊢ ( ( ( 𝑆 ⊆ ℎ ∧ 𝑆 ⊆ 𝑣 ) ∧ ( ℎ ⊆ 𝑁 ∧ 𝑣 ⊆ 𝑀 ) ) → ( 𝑆 ⊆ ( ℎ ∩ 𝑣 ) ∧ ( ℎ ∩ 𝑣 ) ⊆ ( 𝑁 ∩ 𝑀 ) ) )
15 14 an4s ⊢ ( ( ( 𝑆 ⊆ ℎ ∧ ℎ ⊆ 𝑁 ) ∧ ( 𝑆 ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑀 ) ) → ( 𝑆 ⊆ ( ℎ ∩ 𝑣 ) ∧ ( ℎ ∩ 𝑣 ) ⊆ ( 𝑁 ∩ 𝑀 ) ) )
16 sseq2 ⊢ ( 𝑔 = ( ℎ ∩ 𝑣 ) → ( 𝑆 ⊆ 𝑔 ↔ 𝑆 ⊆ ( ℎ ∩ 𝑣 ) ) )
17 sseq1 ⊢ ( 𝑔 = ( ℎ ∩ 𝑣 ) → ( 𝑔 ⊆ ( 𝑁 ∩ 𝑀 ) ↔ ( ℎ ∩ 𝑣 ) ⊆ ( 𝑁 ∩ 𝑀 ) ) )
18 16 17 anbi12d ⊢ ( 𝑔 = ( ℎ ∩ 𝑣 ) → ( ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ ( 𝑁 ∩ 𝑀 ) ) ↔ ( 𝑆 ⊆ ( ℎ ∩ 𝑣 ) ∧ ( ℎ ∩ 𝑣 ) ⊆ ( 𝑁 ∩ 𝑀 ) ) ) )
19 18 rspcev ⊢ ( ( ( ℎ ∩ 𝑣 ) ∈ 𝐽 ∧ ( 𝑆 ⊆ ( ℎ ∩ 𝑣 ) ∧ ( ℎ ∩ 𝑣 ) ⊆ ( 𝑁 ∩ 𝑀 ) ) ) → ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ ( 𝑁 ∩ 𝑀 ) ) )
20 10 15 19 syl2an ⊢ ( ( ( ( 𝐽 ∈ Top ∧ ℎ ∈ 𝐽 ) ∧ 𝑣 ∈ 𝐽 ) ∧ ( ( 𝑆 ⊆ ℎ ∧ ℎ ⊆ 𝑁 ) ∧ ( 𝑆 ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑀 ) ) ) → ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ ( 𝑁 ∩ 𝑀 ) ) )
21 20 expr ⊢ ( ( ( ( 𝐽 ∈ Top ∧ ℎ ∈ 𝐽 ) ∧ 𝑣 ∈ 𝐽 ) ∧ ( 𝑆 ⊆ ℎ ∧ ℎ ⊆ 𝑁 ) ) → ( ( 𝑆 ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑀 ) → ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ ( 𝑁 ∩ 𝑀 ) ) ) )
22 21 an32s ⊢ ( ( ( ( 𝐽 ∈ Top ∧ ℎ ∈ 𝐽 ) ∧ ( 𝑆 ⊆ ℎ ∧ ℎ ⊆ 𝑁 ) ) ∧ 𝑣 ∈ 𝐽 ) → ( ( 𝑆 ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑀 ) → ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ ( 𝑁 ∩ 𝑀 ) ) ) )
23 22 rexlimdva ⊢ ( ( ( 𝐽 ∈ Top ∧ ℎ ∈ 𝐽 ) ∧ ( 𝑆 ⊆ ℎ ∧ ℎ ⊆ 𝑁 ) ) → ( ∃ 𝑣 ∈ 𝐽 ( 𝑆 ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑀 ) → ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ ( 𝑁 ∩ 𝑀 ) ) ) )
24 23 rexlimdva2 ⊢ ( 𝐽 ∈ Top → ( ∃ ℎ ∈ 𝐽 ( 𝑆 ⊆ ℎ ∧ ℎ ⊆ 𝑁 ) → ( ∃ 𝑣 ∈ 𝐽 ( 𝑆 ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑀 ) → ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ ( 𝑁 ∩ 𝑀 ) ) ) ) )
25 24 imp32 ⊢ ( ( 𝐽 ∈ Top ∧ ( ∃ ℎ ∈ 𝐽 ( 𝑆 ⊆ ℎ ∧ ℎ ⊆ 𝑁 ) ∧ ∃ 𝑣 ∈ 𝐽 ( 𝑆 ⊆ 𝑣 ∧ 𝑣 ⊆ 𝑀 ) ) ) → ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ ( 𝑁 ∩ 𝑀 ) ) )
26 8 25 syldan ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑀 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ) → ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ ( 𝑁 ∩ 𝑀 ) ) )
27 26 3impb ⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑀 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ ( 𝑁 ∩ 𝑀 ) ) )
28 1 neiss2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → 𝑆 ⊆ ∪ 𝐽 )
29 1 isnei ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐽 ) → ( ( 𝑁 ∩ 𝑀 ) ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ↔ ( ( 𝑁 ∩ 𝑀 ) ⊆ ∪ 𝐽 ∧ ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ ( 𝑁 ∩ 𝑀 ) ) ) ) )
30 28 29 syldan ⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → ( ( 𝑁 ∩ 𝑀 ) ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ↔ ( ( 𝑁 ∩ 𝑀 ) ⊆ ∪ 𝐽 ∧ ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ ( 𝑁 ∩ 𝑀 ) ) ) ) )
31 30 3adant3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑀 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → ( ( 𝑁 ∩ 𝑀 ) ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ↔ ( ( 𝑁 ∩ 𝑀 ) ⊆ ∪ 𝐽 ∧ ∃ 𝑔 ∈ 𝐽 ( 𝑆 ⊆ 𝑔 ∧ 𝑔 ⊆ ( 𝑁 ∩ 𝑀 ) ) ) ) )
32 5 27 31 mpbir2and ⊢ ( ( 𝐽 ∈ Top ∧ 𝑁 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑀 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → ( 𝑁 ∩ 𝑀 ) ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) )