Theorem neiint 7716

Description: An intuitive definition of a neighborhood in terms of interior. (Contributed by Szymon Jaroszewicz, 18-Dec-2007.)

Hypothesis

Ref	Expression
neifval.1	⊢ X = ∪J

Assertion

Ref	Expression
neiint	⊢ ((J ∈ Top ⋀ S ⊆ X ⋀ N ⊆ X) → (N ∈ ((nei ‘J) ‘S) ↔ S ⊆ ((int ‘J) ‘N)))

Proof of Theorem neiint

Step	Hyp	Ref	Expression
1		ssuni 2526	. . . . . . 7 ⊢ ((S ⊆ v ⋀ v ∈ {g ∈ J∣g ⊆ N}) → S ⊆ ∪{g ∈ J∣g ⊆ N})
2		sseq1 2085	. . . . . . . 8 ⊢ (g = v → (g ⊆ N ↔ v ⊆ N))
3	2	elrab 1908	. . . . . . 7 ⊢ (v ∈ {g ∈ J∣g ⊆ N} ↔ (v ∈ J ⋀ v ⊆ N))
4	1, 3	sylan2br 455	. . . . . 6 ⊢ ((S ⊆ v ⋀ (v ∈ J ⋀ v ⊆ N)) → S ⊆ ∪{g ∈ J∣g ⊆ N})
5	4	an1s 488	. . . . 5 ⊢ ((v ∈ J ⋀ (S ⊆ v ⋀ v ⊆ N)) → S ⊆ ∪{g ∈ J∣g ⊆ N})
6	5	r19.23aiva 1747	. . . 4 ⊢ (∃v ∈ J (S ⊆ v ⋀ v ⊆ N) → S ⊆ ∪{g ∈ J∣g ⊆ N})
7	6	adantl 390	. . 3 ⊢ ((N ⊆ X ⋀ ∃v ∈ J (S ⊆ v ⋀ v ⊆ N)) → S ⊆ ∪{g ∈ J∣g ⊆ N})
8		sseq2 2086	. . . . . . . 8 ⊢ (v = ∪{g ∈ J∣g ⊆ N} → (S ⊆ v ↔ S ⊆ ∪{g ∈ J∣g ⊆ N}))
9		sseq1 2085	. . . . . . . 8 ⊢ (v = ∪{g ∈ J∣g ⊆ N} → (v ⊆ N ↔ ∪{g ∈ J∣g ⊆ N} ⊆ N))
10	8, 9	anbi12d 630	. . . . . . 7 ⊢ (v = ∪{g ∈ J∣g ⊆ N} → ((S ⊆ v ⋀ v ⊆ N) ↔ (S ⊆ ∪{g ∈ J∣g ⊆ N} ⋀ ∪{g ∈ J∣g ⊆ N} ⊆ N)))
11	10	rcla4ev 1880	. . . . . 6 ⊢ ((∪{g ∈ J∣g ⊆ N} ∈ J ⋀ (S ⊆ ∪{g ∈ J∣g ⊆ N} ⋀ ∪{g ∈ J∣g ⊆ N} ⊆ N)) → ∃v ∈ J (S ⊆ v ⋀ v ⊆ N))
12		ssrab2 2134	. . . . . . . 8 ⊢ {g ∈ J∣g ⊆ N} ⊆ J
13		uniopnt 7599	. . . . . . . 8 ⊢ ((J ∈ Top ⋀ {g ∈ J∣g ⊆ N} ⊆ J) → ∪{g ∈ J∣g ⊆ N} ∈ J)
14	12, 13	mpan2 698	. . . . . . 7 ⊢ (J ∈ Top → ∪{g ∈ J∣g ⊆ N} ∈ J)
15	14	3ad2ant1 802	. . . . . 6 ⊢ ((J ∈ Top ⋀ S ⊆ X ⋀ N ⊆ X) → ∪{g ∈ J∣g ⊆ N} ∈ J)
16		unissb 2532	. . . . . . . 8 ⊢ (∪{g ∈ J∣g ⊆ N} ⊆ N ↔ ∀z ∈ {g ∈ J∣g ⊆ N}z ⊆ N)
17		sseq1 2085	. . . . . . . . . 10 ⊢ (g = z → (g ⊆ N ↔ z ⊆ N))
18	17	elrab 1908	. . . . . . . . 9 ⊢ (z ∈ {g ∈ J∣g ⊆ N} ↔ (z ∈ J ⋀ z ⊆ N))
19	18	pm3.27bi 326	. . . . . . . 8 ⊢ (z ∈ {g ∈ J∣g ⊆ N} → z ⊆ N)
20	16, 19	mprgbir 1704	. . . . . . 7 ⊢ ∪{g ∈ J∣g ⊆ N} ⊆ N
21	20	jctr 291	. . . . . 6 ⊢ (S ⊆ ∪{g ∈ J∣g ⊆ N} → (S ⊆ ∪{g ∈ J∣g ⊆ N} ⋀ ∪{g ∈ J∣g ⊆ N} ⊆ N))
22	11, 15, 21	syl2an 456	. . . . 5 ⊢ (((J ∈ Top ⋀ S ⊆ X ⋀ N ⊆ X) ⋀ S ⊆ ∪{g ∈ J∣g ⊆ N}) → ∃v ∈ J (S ⊆ v ⋀ v ⊆ N))
23	22	ex 373	. . . 4 ⊢ ((J ∈ Top ⋀ S ⊆ X ⋀ N ⊆ X) → (S ⊆ ∪{g ∈ J∣g ⊆ N} → ∃v ∈ J (S ⊆ v ⋀ v ⊆ N)))
24		3simp3 792	. . . 4 ⊢ ((J ∈ Top ⋀ S ⊆ X ⋀ N ⊆ X) → N ⊆ X)
25	23, 24	jctild 603	. . 3 ⊢ ((J ∈ Top ⋀ S ⊆ X ⋀ N ⊆ X) → (S ⊆ ∪{g ∈ J∣g ⊆ N} → (N ⊆ X ⋀ ∃v ∈ J (S ⊆ v ⋀ v ⊆ N))))
26	7, 25	impbid2 520	. 2 ⊢ ((J ∈ Top ⋀ S ⊆ X ⋀ N ⊆ X) → ((N ⊆ X ⋀ ∃v ∈ J (S ⊆ v ⋀ v ⊆ N)) ↔ S ⊆ ∪{g ∈ J∣g ⊆ N}))
27		neifval.1	. . . 4 ⊢ X = ∪J
28	27	isnei 7715	. . 3 ⊢ ((J ∈ Top ⋀ S ⊆ X) → (N ∈ ((nei ‘J) ‘S) ↔ (N ⊆ X ⋀ ∃v ∈ J (S ⊆ v ⋀ v ⊆ N))))
29	28	3adant3 801	. 2 ⊢ ((J ∈ Top ⋀ S ⊆ X ⋀ N ⊆ X) → (N ∈ ((nei ‘J) ‘S) ↔ (N ⊆ X ⋀ ∃v ∈ J (S ⊆ v ⋀ v ⊆ N))))
30	27	ntrval 7673	. . . 4 ⊢ ((J ∈ Top ⋀ N ⊆ X) → ((int ‘J) ‘N) = ∪{g ∈ J∣g ⊆ N})
31	30	3adant2 800	. . 3 ⊢ ((J ∈ Top ⋀ S ⊆ X ⋀ N ⊆ X) → ((int ‘J) ‘N) = ∪{g ∈ J∣g ⊆ N})
32	31	sseq2d 2092	. 2 ⊢ ((J ∈ Top ⋀ S ⊆ X ⋀ N ⊆ X) → (S ⊆ ((int ‘J) ‘N) ↔ S ⊆ ∪{g ∈ J∣g ⊆ N}))
33	26, 29, 32	3bitr4d 552	1 ⊢ ((J ∈ Top ⋀ S ⊆ X ⋀ N ⊆ X) → (N ∈ ((nei ‘J) ‘S) ↔ S ⊆ ((int ‘J) ‘N)))

Syntax hints:   → wi 3   ↔ wb 146   ⋀ wa 223   ⋀ w3a 777   = wceq 958   ∈ wcel 960  ∃wrex 1649  {crab 1651   ⊆ wss 2050  ∪cuni 2507   ‘cfv 3188  Topctop 7590  intcnt 7658  neicnei 7709

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 964  ax-gen 965  ax-8 966  ax-9 967  ax-10 968  ax-11 969  ax-12 970  ax-13 971  ax-14 972  ax-17 973  ax-4 975  ax-5o 977  ax-6o 980  ax-9o 1125  ax-10o 1142  ax-16 1212  ax-11o 1220  ax-ext 1462  ax-rep 2698  ax-sep 2708  ax-pow 2748  ax-pr 2785  ax-un 2872

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225  df-3an 779  df-ex 983  df-sb 1174  df-eu 1384  df-mo 1385  df-clab 1467  df-cleq 1472  df-clel 1475  df-ne 1590  df-ral 1652  df-rex 1653  df-rab 1655  df-v 1815  df-dif 2052  df-un 2053  df-in 2054  df-ss 2056  df-nul 2284  df-pw 2406  df-sn 2416  df-pr 2417  df-op 2420  df-uni 2508  df-br 2625  df-opab 2672  df-id 2841  df-xp 3190  df-rel 3191  df-cnv 3192  df-co 3193  df-dm 3194  df-rn 3195  df-res 3196  df-ima 3197  df-fun 3198  df-fn 3199  df-fv 3204  df-top 7594  df-ntr 7661  df-nei 7710

Copyright terms: Public domain