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 ‘ 𝐽 ) ‘ 𝑆 ) )