Theorem neiin 34880

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

Assertion

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

Proof of Theorem neiin

Step	Hyp	Ref	Expression
1		simpr 485	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝑀 ∈ ((nei‘𝐽)‘𝐴)) → 𝑀 ∈ ((nei‘𝐽)‘𝐴))
2		simpl 483	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝑀 ∈ ((nei‘𝐽)‘𝐴)) → 𝐽 ∈ Top)
3		eqid 2731	. . . . . . . . 9 ⊢ ∪ 𝐽 = ∪ 𝐽
4	3	neiss2 22489	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝑀 ∈ ((nei‘𝐽)‘𝐴)) → 𝐴 ⊆ ∪ 𝐽)
5	3	neii1 22494	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝑀 ∈ ((nei‘𝐽)‘𝐴)) → 𝑀 ⊆ ∪ 𝐽)
6	3	neiint 22492	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ ∪ 𝐽 ∧ 𝑀 ⊆ ∪ 𝐽) → (𝑀 ∈ ((nei‘𝐽)‘𝐴) ↔ 𝐴 ⊆ ((int‘𝐽)‘𝑀)))
7	2, 4, 5, 6	syl3anc 1371	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝑀 ∈ ((nei‘𝐽)‘𝐴)) → (𝑀 ∈ ((nei‘𝐽)‘𝐴) ↔ 𝐴 ⊆ ((int‘𝐽)‘𝑀)))
8	1, 7	mpbid 231	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝑀 ∈ ((nei‘𝐽)‘𝐴)) → 𝐴 ⊆ ((int‘𝐽)‘𝑀))
9		ssinss1 4202	. . . . . 6 ⊢ (𝐴 ⊆ ((int‘𝐽)‘𝑀) → (𝐴 ∩ 𝐵) ⊆ ((int‘𝐽)‘𝑀))
10	8, 9	syl 17	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝑀 ∈ ((nei‘𝐽)‘𝐴)) → (𝐴 ∩ 𝐵) ⊆ ((int‘𝐽)‘𝑀))
11	10	3adant3 1132	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝑀 ∈ ((nei‘𝐽)‘𝐴) ∧ 𝑁 ∈ ((nei‘𝐽)‘𝐵)) → (𝐴 ∩ 𝐵) ⊆ ((int‘𝐽)‘𝑀))
12		inss2 4194	. . . . 5 ⊢ (𝐴 ∩ 𝐵) ⊆ 𝐵
13		simpr 485	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝐵)) → 𝑁 ∈ ((nei‘𝐽)‘𝐵))
14		simpl 483	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝐵)) → 𝐽 ∈ Top)
15	3	neiss2 22489	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝐵)) → 𝐵 ⊆ ∪ 𝐽)
16	3	neii1 22494	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝐵)) → 𝑁 ⊆ ∪ 𝐽)
17	3	neiint 22492	. . . . . . . 8 ⊢ ((𝐽 ∈ Top ∧ 𝐵 ⊆ ∪ 𝐽 ∧ 𝑁 ⊆ ∪ 𝐽) → (𝑁 ∈ ((nei‘𝐽)‘𝐵) ↔ 𝐵 ⊆ ((int‘𝐽)‘𝑁)))
18	14, 15, 16, 17	syl3anc 1371	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝐵)) → (𝑁 ∈ ((nei‘𝐽)‘𝐵) ↔ 𝐵 ⊆ ((int‘𝐽)‘𝑁)))
19	13, 18	mpbid 231	. . . . . 6 ⊢ ((𝐽 ∈ Top ∧ 𝑁 ∈ ((nei‘𝐽)‘𝐵)) → 𝐵 ⊆ ((int‘𝐽)‘𝑁))
20	19	3adant2 1131	. . . . 5 ⊢ ((𝐽 ∈ Top ∧ 𝑀 ∈ ((nei‘𝐽)‘𝐴) ∧ 𝑁 ∈ ((nei‘𝐽)‘𝐵)) → 𝐵 ⊆ ((int‘𝐽)‘𝑁))
21	12, 20	sstrid 3958	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝑀 ∈ ((nei‘𝐽)‘𝐴) ∧ 𝑁 ∈ ((nei‘𝐽)‘𝐵)) → (𝐴 ∩ 𝐵) ⊆ ((int‘𝐽)‘𝑁))
22	11, 21	ssind 4197	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝑀 ∈ ((nei‘𝐽)‘𝐴) ∧ 𝑁 ∈ ((nei‘𝐽)‘𝐵)) → (𝐴 ∩ 𝐵) ⊆ (((int‘𝐽)‘𝑀) ∩ ((int‘𝐽)‘𝑁)))
23		simp1 1136	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝑀 ∈ ((nei‘𝐽)‘𝐴) ∧ 𝑁 ∈ ((nei‘𝐽)‘𝐵)) → 𝐽 ∈ Top)
24	5	3adant3 1132	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝑀 ∈ ((nei‘𝐽)‘𝐴) ∧ 𝑁 ∈ ((nei‘𝐽)‘𝐵)) → 𝑀 ⊆ ∪ 𝐽)
25	16	3adant2 1131	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝑀 ∈ ((nei‘𝐽)‘𝐴) ∧ 𝑁 ∈ ((nei‘𝐽)‘𝐵)) → 𝑁 ⊆ ∪ 𝐽)
26	3	ntrin 22449	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝑀 ⊆ ∪ 𝐽 ∧ 𝑁 ⊆ ∪ 𝐽) → ((int‘𝐽)‘(𝑀 ∩ 𝑁)) = (((int‘𝐽)‘𝑀) ∩ ((int‘𝐽)‘𝑁)))
27	23, 24, 25, 26	syl3anc 1371	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝑀 ∈ ((nei‘𝐽)‘𝐴) ∧ 𝑁 ∈ ((nei‘𝐽)‘𝐵)) → ((int‘𝐽)‘(𝑀 ∩ 𝑁)) = (((int‘𝐽)‘𝑀) ∩ ((int‘𝐽)‘𝑁)))
28	22, 27	sseqtrrd 3988	. 2 ⊢ ((𝐽 ∈ Top ∧ 𝑀 ∈ ((nei‘𝐽)‘𝐴) ∧ 𝑁 ∈ ((nei‘𝐽)‘𝐵)) → (𝐴 ∩ 𝐵) ⊆ ((int‘𝐽)‘(𝑀 ∩ 𝑁)))
29		ssinss1 4202	. . . . 5 ⊢ (𝐴 ⊆ ∪ 𝐽 → (𝐴 ∩ 𝐵) ⊆ ∪ 𝐽)
30	4, 29	syl 17	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝑀 ∈ ((nei‘𝐽)‘𝐴)) → (𝐴 ∩ 𝐵) ⊆ ∪ 𝐽)
31		ssinss1 4202	. . . . 5 ⊢ (𝑀 ⊆ ∪ 𝐽 → (𝑀 ∩ 𝑁) ⊆ ∪ 𝐽)
32	5, 31	syl 17	. . . 4 ⊢ ((𝐽 ∈ Top ∧ 𝑀 ∈ ((nei‘𝐽)‘𝐴)) → (𝑀 ∩ 𝑁) ⊆ ∪ 𝐽)
33	3	neiint 22492	. . . 4 ⊢ ((𝐽 ∈ Top ∧ (𝐴 ∩ 𝐵) ⊆ ∪ 𝐽 ∧ (𝑀 ∩ 𝑁) ⊆ ∪ 𝐽) → ((𝑀 ∩ 𝑁) ∈ ((nei‘𝐽)‘(𝐴 ∩ 𝐵)) ↔ (𝐴 ∩ 𝐵) ⊆ ((int‘𝐽)‘(𝑀 ∩ 𝑁))))
34	2, 30, 32, 33	syl3anc 1371	. . 3 ⊢ ((𝐽 ∈ Top ∧ 𝑀 ∈ ((nei‘𝐽)‘𝐴)) → ((𝑀 ∩ 𝑁) ∈ ((nei‘𝐽)‘(𝐴 ∩ 𝐵)) ↔ (𝐴 ∩ 𝐵) ⊆ ((int‘𝐽)‘(𝑀 ∩ 𝑁))))
35	34	3adant3 1132	. 2 ⊢ ((𝐽 ∈ Top ∧ 𝑀 ∈ ((nei‘𝐽)‘𝐴) ∧ 𝑁 ∈ ((nei‘𝐽)‘𝐵)) → ((𝑀 ∩ 𝑁) ∈ ((nei‘𝐽)‘(𝐴 ∩ 𝐵)) ↔ (𝐴 ∩ 𝐵) ⊆ ((int‘𝐽)‘(𝑀 ∩ 𝑁))))
36	28, 35	mpbird 256	1 ⊢ ((𝐽 ∈ Top ∧ 𝑀 ∈ ((nei‘𝐽)‘𝐴) ∧ 𝑁 ∈ ((nei‘𝐽)‘𝐵)) → (𝑀 ∩ 𝑁) ∈ ((nei‘𝐽)‘(𝐴 ∩ 𝐵)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   ∧ w3a 1087   = wceq 1541   ∈ wcel 2106   ∩ cin 3912   ⊆ wss 3913  ∪ cuni 4870  ‘cfv 6501  Topctop 22279  intcnt 22405  neicnei 22485

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-rep 5247  ax-sep 5261  ax-nul 5268  ax-pow 5325  ax-pr 5389  ax-un 7677

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-reu 3352  df-rab 3406  df-v 3448  df-sbc 3743  df-csb 3859  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-pw 4567  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-int 4913  df-iun 4961  df-iin 4962  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-iota 6453  df-fun 6503  df-fn 6504  df-f 6505  df-f1 6506  df-fo 6507  df-f1o 6508  df-fv 6509  df-top 22280  df-cld 22407  df-ntr 22408  df-cls 22409  df-nei 22486

This theorem is referenced by: (None)