neitr

Description: The neighborhood of a trace is the trace of the neighborhood. (Contributed by Thierry Arnoux, 17-Jan-2018)

		Ref	Expression
	Hypothesis	neitr.1	$⊢ X = ⋃ J$
	Assertion	neitr	$⊢ (J \in Top \land A \subseteq X \land B \subseteq A) \to nei (J ↾_{𝑡} A) (B) = nei (J) (B) ↾_{𝑡} A$

Proof

Step	Hyp	Ref	Expression
1		neitr.1	$⊢ X = ⋃ J$
2		nfv	$⊢ Ⅎ d (J \in Top \land A \subseteq X \land B \subseteq A)$
3		nfv	$⊢ Ⅎ d c \subseteq ⋃ (J ↾_{𝑡} A)$
4		nfre1	$⊢ Ⅎ d \exists d \in (J ↾_{𝑡} A) (B \subseteq d \land d \subseteq c)$
5	3 4	nfan	$⊢ Ⅎ d (c \subseteq ⋃ (J ↾_{𝑡} A) \land \exists d \in (J ↾_{𝑡} A) (B \subseteq d \land d \subseteq c))$
6	2 5	nfan	$⊢ Ⅎ d ((J \in Top \land A \subseteq X \land B \subseteq A) \land (c \subseteq ⋃ (J ↾_{𝑡} A) \land \exists d \in (J ↾_{𝑡} A) (B \subseteq d \land d \subseteq c)))$
7		simpl	$⊢ (c \subseteq ⋃ (J ↾_{𝑡} A) \land \exists d \in (J ↾_{𝑡} A) (B \subseteq d \land d \subseteq c)) \to c \subseteq ⋃ (J ↾_{𝑡} A)$
8	7	anim2i	$⊢ ((J \in Top \land A \subseteq X \land B \subseteq A) \land (c \subseteq ⋃ (J ↾_{𝑡} A) \land \exists d \in (J ↾_{𝑡} A) (B \subseteq d \land d \subseteq c))) \to ((J \in Top \land A \subseteq X \land B \subseteq A) \land c \subseteq ⋃ (J ↾_{𝑡} A))$
9		simp-5r	$⊢ ((((((J \in Top \land A \subseteq X \land B \subseteq A) \land c \subseteq ⋃ (J ↾_{𝑡} A)) \land d \in (J ↾_{𝑡} A)) \land (B \subseteq d \land d \subseteq c)) \land e \in J) \land d = e \cap A) \to c \subseteq ⋃ (J ↾_{𝑡} A)$
10		simp1	$⊢ (J \in Top \land A \subseteq X \land B \subseteq A) \to J \in Top$
11		simp2	$⊢ (J \in Top \land A \subseteq X \land B \subseteq A) \to A \subseteq X$
12	1	restuni	$⊢ (J \in Top \land A \subseteq X) \to A = ⋃ (J ↾_{𝑡} A)$
13	10 11 12	syl2anc	$⊢ (J \in Top \land A \subseteq X \land B \subseteq A) \to A = ⋃ (J ↾_{𝑡} A)$
14	13	ad5antr	$⊢ ((((((J \in Top \land A \subseteq X \land B \subseteq A) \land c \subseteq ⋃ (J ↾_{𝑡} A)) \land d \in (J ↾_{𝑡} A)) \land (B \subseteq d \land d \subseteq c)) \land e \in J) \land d = e \cap A) \to A = ⋃ (J ↾_{𝑡} A)$
15	9 14	sseqtrrd	$⊢ ((((((J \in Top \land A \subseteq X \land B \subseteq A) \land c \subseteq ⋃ (J ↾_{𝑡} A)) \land d \in (J ↾_{𝑡} A)) \land (B \subseteq d \land d \subseteq c)) \land e \in J) \land d = e \cap A) \to c \subseteq A$
16	11	ad5antr	$⊢ ((((((J \in Top \land A \subseteq X \land B \subseteq A) \land c \subseteq ⋃ (J ↾_{𝑡} A)) \land d \in (J ↾_{𝑡} A)) \land (B \subseteq d \land d \subseteq c)) \land e \in J) \land d = e \cap A) \to A \subseteq X$
17	15 16	sstrd	$⊢ ((((((J \in Top \land A \subseteq X \land B \subseteq A) \land c \subseteq ⋃ (J ↾_{𝑡} A)) \land d \in (J ↾_{𝑡} A)) \land (B \subseteq d \land d \subseteq c)) \land e \in J) \land d = e \cap A) \to c \subseteq X$
18	10	ad5antr	$⊢ ((((((J \in Top \land A \subseteq X \land B \subseteq A) \land c \subseteq ⋃ (J ↾_{𝑡} A)) \land d \in (J ↾_{𝑡} A)) \land (B \subseteq d \land d \subseteq c)) \land e \in J) \land d = e \cap A) \to J \in Top$
19		simplr	$⊢ ((((((J \in Top \land A \subseteq X \land B \subseteq A) \land c \subseteq ⋃ (J ↾_{𝑡} A)) \land d \in (J ↾_{𝑡} A)) \land (B \subseteq d \land d \subseteq c)) \land e \in J) \land d = e \cap A) \to e \in J$
20	1	eltopss	$⊢ (J \in Top \land e \in J) \to e \subseteq X$
21	18 19 20	syl2anc	$⊢ ((((((J \in Top \land A \subseteq X \land B \subseteq A) \land c \subseteq ⋃ (J ↾_{𝑡} A)) \land d \in (J ↾_{𝑡} A)) \land (B \subseteq d \land d \subseteq c)) \land e \in J) \land d = e \cap A) \to e \subseteq X$
22	21	ssdifssd	$⊢ ((((((J \in Top \land A \subseteq X \land B \subseteq A) \land c \subseteq ⋃ (J ↾_{𝑡} A)) \land d \in (J ↾_{𝑡} A)) \land (B \subseteq d \land d \subseteq c)) \land e \in J) \land d = e \cap A) \to e ∖ A \subseteq X$
23	17 22	unssd	$⊢ ((((((J \in Top \land A \subseteq X \land B \subseteq A) \land c \subseteq ⋃ (J ↾_{𝑡} A)) \land d \in (J ↾_{𝑡} A)) \land (B \subseteq d \land d \subseteq c)) \land e \in J) \land d = e \cap A) \to c \cup (e ∖ A) \subseteq X$
24		simpr1l	$⊢ ((((J \in Top \land A \subseteq X \land B \subseteq A) \land c \subseteq ⋃ (J ↾_{𝑡} A)) \land d \in (J ↾_{𝑡} A)) \land ((B \subseteq d \land d \subseteq c) \land e \in J \land d = e \cap A)) \to B \subseteq d$
25	24	3anassrs	$⊢ ((((((J \in Top \land A \subseteq X \land B \subseteq A) \land c \subseteq ⋃ (J ↾_{𝑡} A)) \land d \in (J ↾_{𝑡} A)) \land (B \subseteq d \land d \subseteq c)) \land e \in J) \land d = e \cap A) \to B \subseteq d$
26		simpr	$⊢ ((((((J \in Top \land A \subseteq X \land B \subseteq A) \land c \subseteq ⋃ (J ↾_{𝑡} A)) \land d \in (J ↾_{𝑡} A)) \land (B \subseteq d \land d \subseteq c)) \land e \in J) \land d = e \cap A) \to d = e \cap A$
27	25 26	sseqtrd	$⊢ ((((((J \in Top \land A \subseteq X \land B \subseteq A) \land c \subseteq ⋃ (J ↾_{𝑡} A)) \land d \in (J ↾_{𝑡} A)) \land (B \subseteq d \land d \subseteq c)) \land e \in J) \land d = e \cap A) \to B \subseteq e \cap A$
28		inss1	$⊢ e \cap A \subseteq e$
29	27 28	sstrdi	$⊢ ((((((J \in Top \land A \subseteq X \land B \subseteq A) \land c \subseteq ⋃ (J ↾_{𝑡} A)) \land d \in (J ↾_{𝑡} A)) \land (B \subseteq d \land d \subseteq c)) \land e \in J) \land d = e \cap A) \to B \subseteq e$
30		inundif	$⊢ (e \cap A) \cup (e ∖ A) = e$
31		simpr1r	$⊢ ((((J \in Top \land A \subseteq X \land B \subseteq A) \land c \subseteq ⋃ (J ↾_{𝑡} A)) \land d \in (J ↾_{𝑡} A)) \land ((B \subseteq d \land d \subseteq c) \land e \in J \land d = e \cap A)) \to d \subseteq c$
32	31	3anassrs	$⊢ ((((((J \in Top \land A \subseteq X \land B \subseteq A) \land c \subseteq ⋃ (J ↾_{𝑡} A)) \land d \in (J ↾_{𝑡} A)) \land (B \subseteq d \land d \subseteq c)) \land e \in J) \land d = e \cap A) \to d \subseteq c$
33	26 32	eqsstrrd	$⊢ ((((((J \in Top \land A \subseteq X \land B \subseteq A) \land c \subseteq ⋃ (J ↾_{𝑡} A)) \land d \in (J ↾_{𝑡} A)) \land (B \subseteq d \land d \subseteq c)) \land e \in J) \land d = e \cap A) \to e \cap A \subseteq c$
34		unss1	$⊢ e \cap A \subseteq c \to (e \cap A) \cup (e ∖ A) \subseteq c \cup (e ∖ A)$
35	33 34	syl	$⊢ ((((((J \in Top \land A \subseteq X \land B \subseteq A) \land c \subseteq ⋃ (J ↾_{𝑡} A)) \land d \in (J ↾_{𝑡} A)) \land (B \subseteq d \land d \subseteq c)) \land e \in J) \land d = e \cap A) \to (e \cap A) \cup (e ∖ A) \subseteq c \cup (e ∖ A)$
36	30 35	eqsstrrid	$⊢ ((((((J \in Top \land A \subseteq X \land B \subseteq A) \land c \subseteq ⋃ (J ↾_{𝑡} A)) \land d \in (J ↾_{𝑡} A)) \land (B \subseteq d \land d \subseteq c)) \land e \in J) \land d = e \cap A) \to e \subseteq c \cup (e ∖ A)$
37		sseq2	$⊢ b = e \to (B \subseteq b \leftrightarrow B \subseteq e)$
38		sseq1	$⊢ b = e \to (b \subseteq c \cup (e ∖ A) \leftrightarrow e \subseteq c \cup (e ∖ A))$
39	37 38	anbi12d	$⊢ b = e \to ((B \subseteq b \land b \subseteq c \cup (e ∖ A)) \leftrightarrow (B \subseteq e \land e \subseteq c \cup (e ∖ A)))$
40	39	rspcev	$⊢ (e \in J \land (B \subseteq e \land e \subseteq c \cup (e ∖ A))) \to \exists b \in J (B \subseteq b \land b \subseteq c \cup (e ∖ A))$
41	19 29 36 40	syl12anc	$⊢ ((((((J \in Top \land A \subseteq X \land B \subseteq A) \land c \subseteq ⋃ (J ↾_{𝑡} A)) \land d \in (J ↾_{𝑡} A)) \land (B \subseteq d \land d \subseteq c)) \land e \in J) \land d = e \cap A) \to \exists b \in J (B \subseteq b \land b \subseteq c \cup (e ∖ A))$
42		indir	$⊢ (c \cup (e ∖ A)) \cap A = (c \cap A) \cup ((e ∖ A) \cap A)$
43		disjdifr	$⊢ (e ∖ A) \cap A = \emptyset$
44	43	uneq2i	$⊢ (c \cap A) \cup ((e ∖ A) \cap A) = (c \cap A) \cup \emptyset$
45		un0	$⊢ (c \cap A) \cup \emptyset = c \cap A$
46	42 44 45	3eqtri	$⊢ (c \cup (e ∖ A)) \cap A = c \cap A$
47		df-ss	$⊢ c \subseteq A \leftrightarrow c \cap A = c$
48	47	biimpi	$⊢ c \subseteq A \to c \cap A = c$
49	46 48	eqtr2id	$⊢ c \subseteq A \to c = (c \cup (e ∖ A)) \cap A$
50	15 49	syl	$⊢ ((((((J \in Top \land A \subseteq X \land B \subseteq A) \land c \subseteq ⋃ (J ↾_{𝑡} A)) \land d \in (J ↾_{𝑡} A)) \land (B \subseteq d \land d \subseteq c)) \land e \in J) \land d = e \cap A) \to c = (c \cup (e ∖ A)) \cap A$
51		vex	$⊢ c \in V$
52		vex	$⊢ e \in V$
53	52	difexi	$⊢ e ∖ A \in V$
54	51 53	unex	$⊢ c \cup (e ∖ A) \in V$
55		sseq1	$⊢ a = c \cup (e ∖ A) \to (a \subseteq X \leftrightarrow c \cup (e ∖ A) \subseteq X)$
56		sseq2	$⊢ a = c \cup (e ∖ A) \to (b \subseteq a \leftrightarrow b \subseteq c \cup (e ∖ A))$
57	56	anbi2d	$⊢ a = c \cup (e ∖ A) \to ((B \subseteq b \land b \subseteq a) \leftrightarrow (B \subseteq b \land b \subseteq c \cup (e ∖ A)))$
58	57	rexbidv	$⊢ a = c \cup (e ∖ A) \to (\exists b \in J (B \subseteq b \land b \subseteq a) \leftrightarrow \exists b \in J (B \subseteq b \land b \subseteq c \cup (e ∖ A)))$
59	55 58	anbi12d	$⊢ a = c \cup (e ∖ A) \to ((a \subseteq X \land \exists b \in J (B \subseteq b \land b \subseteq a)) \leftrightarrow (c \cup (e ∖ A) \subseteq X \land \exists b \in J (B \subseteq b \land b \subseteq c \cup (e ∖ A))))$
60		ineq1	$⊢ a = c \cup (e ∖ A) \to a \cap A = (c \cup (e ∖ A)) \cap A$
61	60	eqeq2d	$⊢ a = c \cup (e ∖ A) \to (c = a \cap A \leftrightarrow c = (c \cup (e ∖ A)) \cap A)$
62	59 61	anbi12d	$⊢ a = c \cup (e ∖ A) \to (((a \subseteq X \land \exists b \in J (B \subseteq b \land b \subseteq a)) \land c = a \cap A) \leftrightarrow ((c \cup (e ∖ A) \subseteq X \land \exists b \in J (B \subseteq b \land b \subseteq c \cup (e ∖ A))) \land c = (c \cup (e ∖ A)) \cap A))$
63	54 62	spcev	$⊢ ((c \cup (e ∖ A) \subseteq X \land \exists b \in J (B \subseteq b \land b \subseteq c \cup (e ∖ A))) \land c = (c \cup (e ∖ A)) \cap A) \to \exists a ((a \subseteq X \land \exists b \in J (B \subseteq b \land b \subseteq a)) \land c = a \cap A)$
64	23 41 50 63	syl21anc	$⊢ ((((((J \in Top \land A \subseteq X \land B \subseteq A) \land c \subseteq ⋃ (J ↾_{𝑡} A)) \land d \in (J ↾_{𝑡} A)) \land (B \subseteq d \land d \subseteq c)) \land e \in J) \land d = e \cap A) \to \exists a ((a \subseteq X \land \exists b \in J (B \subseteq b \land b \subseteq a)) \land c = a \cap A)$
65	10	ad3antrrr	$⊢ ((((J \in Top \land A \subseteq X \land B \subseteq A) \land c \subseteq ⋃ (J ↾_{𝑡} A)) \land d \in (J ↾_{𝑡} A)) \land (B \subseteq d \land d \subseteq c)) \to J \in Top$
66	10	uniexd	$⊢ (J \in Top \land A \subseteq X \land B \subseteq A) \to ⋃ J \in V$
67	1 66	eqeltrid	$⊢ (J \in Top \land A \subseteq X \land B \subseteq A) \to X \in V$
68	67 11	ssexd	$⊢ (J \in Top \land A \subseteq X \land B \subseteq A) \to A \in V$
69	68	ad3antrrr	$⊢ ((((J \in Top \land A \subseteq X \land B \subseteq A) \land c \subseteq ⋃ (J ↾_{𝑡} A)) \land d \in (J ↾_{𝑡} A)) \land (B \subseteq d \land d \subseteq c)) \to A \in V$
70		simplr	$⊢ ((((J \in Top \land A \subseteq X \land B \subseteq A) \land c \subseteq ⋃ (J ↾_{𝑡} A)) \land d \in (J ↾_{𝑡} A)) \land (B \subseteq d \land d \subseteq c)) \to d \in (J ↾_{𝑡} A)$
71		elrest	$⊢ (J \in Top \land A \in V) \to (d \in (J ↾_{𝑡} A) \leftrightarrow \exists e \in J d = e \cap A)$
72	71	biimpa	$⊢ ((J \in Top \land A \in V) \land d \in (J ↾_{𝑡} A)) \to \exists e \in J d = e \cap A$
73	65 69 70 72	syl21anc	$⊢ ((((J \in Top \land A \subseteq X \land B \subseteq A) \land c \subseteq ⋃ (J ↾_{𝑡} A)) \land d \in (J ↾_{𝑡} A)) \land (B \subseteq d \land d \subseteq c)) \to \exists e \in J d = e \cap A$
74	64 73	r19.29a	$⊢ ((((J \in Top \land A \subseteq X \land B \subseteq A) \land c \subseteq ⋃ (J ↾_{𝑡} A)) \land d \in (J ↾_{𝑡} A)) \land (B \subseteq d \land d \subseteq c)) \to \exists a ((a \subseteq X \land \exists b \in J (B \subseteq b \land b \subseteq a)) \land c = a \cap A)$
75	8 74	sylanl1	$⊢ ((((J \in Top \land A \subseteq X \land B \subseteq A) \land (c \subseteq ⋃ (J ↾_{𝑡} A) \land \exists d \in (J ↾_{𝑡} A) (B \subseteq d \land d \subseteq c))) \land d \in (J ↾_{𝑡} A)) \land (B \subseteq d \land d \subseteq c)) \to \exists a ((a \subseteq X \land \exists b \in J (B \subseteq b \land b \subseteq a)) \land c = a \cap A)$
76		simprr	$⊢ ((J \in Top \land A \subseteq X \land B \subseteq A) \land (c \subseteq ⋃ (J ↾_{𝑡} A) \land \exists d \in (J ↾_{𝑡} A) (B \subseteq d \land d \subseteq c))) \to \exists d \in (J ↾_{𝑡} A) (B \subseteq d \land d \subseteq c)$
77	6 75 76	r19.29af	$⊢ ((J \in Top \land A \subseteq X \land B \subseteq A) \land (c \subseteq ⋃ (J ↾_{𝑡} A) \land \exists d \in (J ↾_{𝑡} A) (B \subseteq d \land d \subseteq c))) \to \exists a ((a \subseteq X \land \exists b \in J (B \subseteq b \land b \subseteq a)) \land c = a \cap A)$
78		inss2	$⊢ a \cap A \subseteq A$
79		sseq1	$⊢ c = a \cap A \to (c \subseteq A \leftrightarrow a \cap A \subseteq A)$
80	78 79	mpbiri	$⊢ c = a \cap A \to c \subseteq A$
81	80	adantl	$⊢ ((a \subseteq X \land \exists b \in J (B \subseteq b \land b \subseteq a)) \land c = a \cap A) \to c \subseteq A$
82	81	exlimiv	$⊢ \exists a ((a \subseteq X \land \exists b \in J (B \subseteq b \land b \subseteq a)) \land c = a \cap A) \to c \subseteq A$
83	82	adantl	$⊢ ((J \in Top \land A \subseteq X \land B \subseteq A) \land \exists a ((a \subseteq X \land \exists b \in J (B \subseteq b \land b \subseteq a)) \land c = a \cap A)) \to c \subseteq A$
84	13	adantr	$⊢ ((J \in Top \land A \subseteq X \land B \subseteq A) \land \exists a ((a \subseteq X \land \exists b \in J (B \subseteq b \land b \subseteq a)) \land c = a \cap A)) \to A = ⋃ (J ↾_{𝑡} A)$
85	83 84	sseqtrd	$⊢ ((J \in Top \land A \subseteq X \land B \subseteq A) \land \exists a ((a \subseteq X \land \exists b \in J (B \subseteq b \land b \subseteq a)) \land c = a \cap A)) \to c \subseteq ⋃ (J ↾_{𝑡} A)$
86	10	ad4antr	$⊢ (((((J \in Top \land A \subseteq X \land B \subseteq A) \land c = a \cap A) \land a \subseteq X) \land b \in J) \land (B \subseteq b \land b \subseteq a)) \to J \in Top$
87	68	ad4antr	$⊢ (((((J \in Top \land A \subseteq X \land B \subseteq A) \land c = a \cap A) \land a \subseteq X) \land b \in J) \land (B \subseteq b \land b \subseteq a)) \to A \in V$
88		simplr	$⊢ (((((J \in Top \land A \subseteq X \land B \subseteq A) \land c = a \cap A) \land a \subseteq X) \land b \in J) \land (B \subseteq b \land b \subseteq a)) \to b \in J$
89		elrestr	$⊢ (J \in Top \land A \in V \land b \in J) \to b \cap A \in (J ↾_{𝑡} A)$
90	86 87 88 89	syl3anc	$⊢ (((((J \in Top \land A \subseteq X \land B \subseteq A) \land c = a \cap A) \land a \subseteq X) \land b \in J) \land (B \subseteq b \land b \subseteq a)) \to b \cap A \in (J ↾_{𝑡} A)$
91		simprl	$⊢ (((((J \in Top \land A \subseteq X \land B \subseteq A) \land c = a \cap A) \land a \subseteq X) \land b \in J) \land (B \subseteq b \land b \subseteq a)) \to B \subseteq b$
92		simp3	$⊢ (J \in Top \land A \subseteq X \land B \subseteq A) \to B \subseteq A$
93	92	ad4antr	$⊢ (((((J \in Top \land A \subseteq X \land B \subseteq A) \land c = a \cap A) \land a \subseteq X) \land b \in J) \land (B \subseteq b \land b \subseteq a)) \to B \subseteq A$
94	91 93	ssind	$⊢ (((((J \in Top \land A \subseteq X \land B \subseteq A) \land c = a \cap A) \land a \subseteq X) \land b \in J) \land (B \subseteq b \land b \subseteq a)) \to B \subseteq b \cap A$
95		simprr	$⊢ (((((J \in Top \land A \subseteq X \land B \subseteq A) \land c = a \cap A) \land a \subseteq X) \land b \in J) \land (B \subseteq b \land b \subseteq a)) \to b \subseteq a$
96	95	ssrind	$⊢ (((((J \in Top \land A \subseteq X \land B \subseteq A) \land c = a \cap A) \land a \subseteq X) \land b \in J) \land (B \subseteq b \land b \subseteq a)) \to b \cap A \subseteq a \cap A$
97		simp-4r	$⊢ (((((J \in Top \land A \subseteq X \land B \subseteq A) \land c = a \cap A) \land a \subseteq X) \land b \in J) \land (B \subseteq b \land b \subseteq a)) \to c = a \cap A$
98	96 97	sseqtrrd	$⊢ (((((J \in Top \land A \subseteq X \land B \subseteq A) \land c = a \cap A) \land a \subseteq X) \land b \in J) \land (B \subseteq b \land b \subseteq a)) \to b \cap A \subseteq c$
99	90 94 98	jca32	$⊢ (((((J \in Top \land A \subseteq X \land B \subseteq A) \land c = a \cap A) \land a \subseteq X) \land b \in J) \land (B \subseteq b \land b \subseteq a)) \to (b \cap A \in (J ↾_{𝑡} A) \land (B \subseteq b \cap A \land b \cap A \subseteq c))$
100	99	ex	$⊢ ((((J \in Top \land A \subseteq X \land B \subseteq A) \land c = a \cap A) \land a \subseteq X) \land b \in J) \to ((B \subseteq b \land b \subseteq a) \to (b \cap A \in (J ↾_{𝑡} A) \land (B \subseteq b \cap A \land b \cap A \subseteq c)))$
101	100	reximdva	$⊢ (((J \in Top \land A \subseteq X \land B \subseteq A) \land c = a \cap A) \land a \subseteq X) \to (\exists b \in J (B \subseteq b \land b \subseteq a) \to \exists b \in J (b \cap A \in (J ↾_{𝑡} A) \land (B \subseteq b \cap A \land b \cap A \subseteq c)))$
102	101	impr	$⊢ (((J \in Top \land A \subseteq X \land B \subseteq A) \land c = a \cap A) \land (a \subseteq X \land \exists b \in J (B \subseteq b \land b \subseteq a))) \to \exists b \in J (b \cap A \in (J ↾_{𝑡} A) \land (B \subseteq b \cap A \land b \cap A \subseteq c))$
103	102	an32s	$⊢ (((J \in Top \land A \subseteq X \land B \subseteq A) \land (a \subseteq X \land \exists b \in J (B \subseteq b \land b \subseteq a))) \land c = a \cap A) \to \exists b \in J (b \cap A \in (J ↾_{𝑡} A) \land (B \subseteq b \cap A \land b \cap A \subseteq c))$
104	103	expl	$⊢ (J \in Top \land A \subseteq X \land B \subseteq A) \to (((a \subseteq X \land \exists b \in J (B \subseteq b \land b \subseteq a)) \land c = a \cap A) \to \exists b \in J (b \cap A \in (J ↾_{𝑡} A) \land (B \subseteq b \cap A \land b \cap A \subseteq c)))$
105	104	exlimdv	$⊢ (J \in Top \land A \subseteq X \land B \subseteq A) \to (\exists a ((a \subseteq X \land \exists b \in J (B \subseteq b \land b \subseteq a)) \land c = a \cap A) \to \exists b \in J (b \cap A \in (J ↾_{𝑡} A) \land (B \subseteq b \cap A \land b \cap A \subseteq c)))$
106	105	imp	$⊢ ((J \in Top \land A \subseteq X \land B \subseteq A) \land \exists a ((a \subseteq X \land \exists b \in J (B \subseteq b \land b \subseteq a)) \land c = a \cap A)) \to \exists b \in J (b \cap A \in (J ↾_{𝑡} A) \land (B \subseteq b \cap A \land b \cap A \subseteq c))$
107		sseq2	$⊢ d = b \cap A \to (B \subseteq d \leftrightarrow B \subseteq b \cap A)$
108		sseq1	$⊢ d = b \cap A \to (d \subseteq c \leftrightarrow b \cap A \subseteq c)$
109	107 108	anbi12d	$⊢ d = b \cap A \to ((B \subseteq d \land d \subseteq c) \leftrightarrow (B \subseteq b \cap A \land b \cap A \subseteq c))$
110	109	rspcev	$⊢ (b \cap A \in (J ↾_{𝑡} A) \land (B \subseteq b \cap A \land b \cap A \subseteq c)) \to \exists d \in (J ↾_{𝑡} A) (B \subseteq d \land d \subseteq c)$
111	110	rexlimivw	$⊢ \exists b \in J (b \cap A \in (J ↾_{𝑡} A) \land (B \subseteq b \cap A \land b \cap A \subseteq c)) \to \exists d \in (J ↾_{𝑡} A) (B \subseteq d \land d \subseteq c)$
112	106 111	syl	$⊢ ((J \in Top \land A \subseteq X \land B \subseteq A) \land \exists a ((a \subseteq X \land \exists b \in J (B \subseteq b \land b \subseteq a)) \land c = a \cap A)) \to \exists d \in (J ↾_{𝑡} A) (B \subseteq d \land d \subseteq c)$
113	85 112	jca	$⊢ ((J \in Top \land A \subseteq X \land B \subseteq A) \land \exists a ((a \subseteq X \land \exists b \in J (B \subseteq b \land b \subseteq a)) \land c = a \cap A)) \to (c \subseteq ⋃ (J ↾_{𝑡} A) \land \exists d \in (J ↾_{𝑡} A) (B \subseteq d \land d \subseteq c))$
114	77 113	impbida	$⊢ (J \in Top \land A \subseteq X \land B \subseteq A) \to ((c \subseteq ⋃ (J ↾_{𝑡} A) \land \exists d \in (J ↾_{𝑡} A) (B \subseteq d \land d \subseteq c)) \leftrightarrow \exists a ((a \subseteq X \land \exists b \in J (B \subseteq b \land b \subseteq a)) \land c = a \cap A))$
115		resttop	$⊢ (J \in Top \land A \in V) \to J ↾_{𝑡} A \in Top$
116	10 68 115	syl2anc	$⊢ (J \in Top \land A \subseteq X \land B \subseteq A) \to J ↾_{𝑡} A \in Top$
117	92 13	sseqtrd	$⊢ (J \in Top \land A \subseteq X \land B \subseteq A) \to B \subseteq ⋃ (J ↾_{𝑡} A)$
118		eqid	$⊢ ⋃ (J ↾_{𝑡} A) = ⋃ (J ↾_{𝑡} A)$
119	118	isnei	$⊢ (J ↾_{𝑡} A \in Top \land B \subseteq ⋃ (J ↾_{𝑡} A)) \to (c \in nei (J ↾_{𝑡} A) (B) \leftrightarrow (c \subseteq ⋃ (J ↾_{𝑡} A) \land \exists d \in (J ↾_{𝑡} A) (B \subseteq d \land d \subseteq c)))$
120	116 117 119	syl2anc	$⊢ (J \in Top \land A \subseteq X \land B \subseteq A) \to (c \in nei (J ↾_{𝑡} A) (B) \leftrightarrow (c \subseteq ⋃ (J ↾_{𝑡} A) \land \exists d \in (J ↾_{𝑡} A) (B \subseteq d \land d \subseteq c)))$
121		fvex	$⊢ nei (J) (B) \in V$
122		restval	$⊢ (nei (J) (B) \in V \land A \in V) \to nei (J) (B) ↾_{𝑡} A = ran (a \in nei (J) (B) ⟼ a \cap A)$
123	121 68 122	sylancr	$⊢ (J \in Top \land A \subseteq X \land B \subseteq A) \to nei (J) (B) ↾_{𝑡} A = ran (a \in nei (J) (B) ⟼ a \cap A)$
124	123	eleq2d	$⊢ (J \in Top \land A \subseteq X \land B \subseteq A) \to (c \in (nei (J) (B) ↾_{𝑡} A) \leftrightarrow c \in ran (a \in nei (J) (B) ⟼ a \cap A))$
125	92 11	sstrd	$⊢ (J \in Top \land A \subseteq X \land B \subseteq A) \to B \subseteq X$
126		eqid	$⊢ (a \in nei (J) (B) ⟼ a \cap A) = (a \in nei (J) (B) ⟼ a \cap A)$
127	126	elrnmpt	$⊢ c \in V \to (c \in ran (a \in nei (J) (B) ⟼ a \cap A) \leftrightarrow \exists a \in nei (J) (B) c = a \cap A)$
128	127	elv	$⊢ c \in ran (a \in nei (J) (B) ⟼ a \cap A) \leftrightarrow \exists a \in nei (J) (B) c = a \cap A$
129		df-rex	$⊢ \exists a \in nei (J) (B) c = a \cap A \leftrightarrow \exists a (a \in nei (J) (B) \land c = a \cap A)$
130	128 129	bitri	$⊢ c \in ran (a \in nei (J) (B) ⟼ a \cap A) \leftrightarrow \exists a (a \in nei (J) (B) \land c = a \cap A)$
131	1	isnei	$⊢ (J \in Top \land B \subseteq X) \to (a \in nei (J) (B) \leftrightarrow (a \subseteq X \land \exists b \in J (B \subseteq b \land b \subseteq a)))$
132	131	anbi1d	$⊢ (J \in Top \land B \subseteq X) \to ((a \in nei (J) (B) \land c = a \cap A) \leftrightarrow ((a \subseteq X \land \exists b \in J (B \subseteq b \land b \subseteq a)) \land c = a \cap A))$
133	132	exbidv	$⊢ (J \in Top \land B \subseteq X) \to (\exists a (a \in nei (J) (B) \land c = a \cap A) \leftrightarrow \exists a ((a \subseteq X \land \exists b \in J (B \subseteq b \land b \subseteq a)) \land c = a \cap A))$
134	130 133	bitrid	$⊢ (J \in Top \land B \subseteq X) \to (c \in ran (a \in nei (J) (B) ⟼ a \cap A) \leftrightarrow \exists a ((a \subseteq X \land \exists b \in J (B \subseteq b \land b \subseteq a)) \land c = a \cap A))$
135	10 125 134	syl2anc	$⊢ (J \in Top \land A \subseteq X \land B \subseteq A) \to (c \in ran (a \in nei (J) (B) ⟼ a \cap A) \leftrightarrow \exists a ((a \subseteq X \land \exists b \in J (B \subseteq b \land b \subseteq a)) \land c = a \cap A))$
136	124 135	bitrd	$⊢ (J \in Top \land A \subseteq X \land B \subseteq A) \to (c \in (nei (J) (B) ↾_{𝑡} A) \leftrightarrow \exists a ((a \subseteq X \land \exists b \in J (B \subseteq b \land b \subseteq a)) \land c = a \cap A))$
137	114 120 136	3bitr4d	$⊢ (J \in Top \land A \subseteq X \land B \subseteq A) \to (c \in nei (J ↾_{𝑡} A) (B) \leftrightarrow c \in (nei (J) (B) ↾_{𝑡} A))$
138	137	eqrdv	$⊢ (J \in Top \land A \subseteq X \land B \subseteq A) \to nei (J ↾_{𝑡} A) (B) = nei (J) (B) ↾_{𝑡} A$

Metamath Proof Explorer

Theorem neitr

Proof