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		incom	$⊢ A \cap (e ∖ A) = (e ∖ A) \cap A$
44		disjdif	$⊢ A \cap (e ∖ A) = \emptyset$
45	43 44	eqtr3i	$⊢ (e ∖ A) \cap A = \emptyset$
46	45	uneq2i	$⊢ (c \cap A) \cup ((e ∖ A) \cap A) = (c \cap A) \cup \emptyset$
47		un0	$⊢ (c \cap A) \cup \emptyset = c \cap A$
48	42 46 47	3eqtri	$⊢ (c \cup (e ∖ A)) \cap A = c \cap A$
49		df-ss	$⊢ c \subseteq A \leftrightarrow c \cap A = c$
50	49	biimpi	$⊢ c \subseteq A \to c \cap A = c$
51	48 50	syl5req	$⊢ c \subseteq A \to c = (c \cup (e ∖ A)) \cap A$
52	15 51	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$
53		vex	$⊢ c \in V$
54		vex	$⊢ e \in V$
55	54	difexi	$⊢ e ∖ A \in V$
56	53 55	unex	$⊢ c \cup (e ∖ A) \in V$
57		sseq1	$⊢ a = c \cup (e ∖ A) \to (a \subseteq X \leftrightarrow c \cup (e ∖ A) \subseteq X)$
58		sseq2	$⊢ a = c \cup (e ∖ A) \to (b \subseteq a \leftrightarrow b \subseteq c \cup (e ∖ A))$
59	58	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)))$
60	59	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)))$
61	57 60	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))))$
62		ineq1	$⊢ a = c \cup (e ∖ A) \to a \cap A = (c \cup (e ∖ A)) \cap A$
63	62	eqeq2d	$⊢ a = c \cup (e ∖ A) \to (c = a \cap A \leftrightarrow c = (c \cup (e ∖ A)) \cap A)$
64	61 63	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))$
65	56 64	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)$
66	23 41 52 65	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)$
67	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$
68	10	uniexd	$⊢ (J \in Top \land A \subseteq X \land B \subseteq A) \to ⋃ J \in V$
69	1 68	eqeltrid	$⊢ (J \in Top \land A \subseteq X \land B \subseteq A) \to X \in V$
70	69 11	ssexd	$⊢ (J \in Top \land A \subseteq X \land B \subseteq A) \to A \in V$
71	70	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$
72		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)$
73		elrest	$⊢ (J \in Top \land A \in V) \to (d \in (J ↾_{𝑡} A) \leftrightarrow \exists e \in J d = e \cap A)$
74	73	biimpa	$⊢ ((J \in Top \land A \in V) \land d \in (J ↾_{𝑡} A)) \to \exists e \in J d = e \cap A$
75	67 71 72 74	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$
76	66 75	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)$
77	8 76	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)$
78		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)$
79	6 77 78	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)$
80		inss2	$⊢ a \cap A \subseteq A$
81		sseq1	$⊢ c = a \cap A \to (c \subseteq A \leftrightarrow a \cap A \subseteq A)$
82	80 81	mpbiri	$⊢ c = a \cap A \to c \subseteq A$
83	82	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$
84	83	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$
85	84	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$
86	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)$
87	85 86	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)$
88	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$
89	70	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$
90		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$
91		elrestr	$⊢ (J \in Top \land A \in V \land b \in J) \to b \cap A \in (J ↾_{𝑡} A)$
92	88 89 90 91	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)$
93		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$
94		simp3	$⊢ (J \in Top \land A \subseteq X \land B \subseteq A) \to B \subseteq A$
95	94	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$
96	93 95	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$
97		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$
98	97	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$
99		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$
100	98 99	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$
101	92 96 100	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))$
102	101	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)))$
103	102	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)))$
104	103	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))$
105	104	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))$
106	105	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)))$
107	106	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)))$
108	107	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))$
109		sseq2	$⊢ d = b \cap A \to (B \subseteq d \leftrightarrow B \subseteq b \cap A)$
110		sseq1	$⊢ d = b \cap A \to (d \subseteq c \leftrightarrow b \cap A \subseteq c)$
111	109 110	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))$
112	111	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)$
113	112	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)$
114	108 113	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)$
115	87 114	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))$
116	79 115	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))$
117		resttop	$⊢ (J \in Top \land A \in V) \to J ↾_{𝑡} A \in Top$
118	10 70 117	syl2anc	$⊢ (J \in Top \land A \subseteq X \land B \subseteq A) \to J ↾_{𝑡} A \in Top$
119	94 13	sseqtrd	$⊢ (J \in Top \land A \subseteq X \land B \subseteq A) \to B \subseteq ⋃ (J ↾_{𝑡} A)$
120		eqid	$⊢ ⋃ (J ↾_{𝑡} A) = ⋃ (J ↾_{𝑡} A)$
121	120	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)))$
122	118 119 121	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)))$
123		fvex	$⊢ nei (J) (B) \in V$
124		restval	$⊢ (nei (J) (B) \in V \land A \in V) \to nei (J) (B) ↾_{𝑡} A = ran (a \in nei (J) (B) ⟼ a \cap A)$
125	123 70 124	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)$
126	125	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))$
127	94 11	sstrd	$⊢ (J \in Top \land A \subseteq X \land B \subseteq A) \to B \subseteq X$
128		eqid	$⊢ (a \in nei (J) (B) ⟼ a \cap A) = (a \in nei (J) (B) ⟼ a \cap A)$
129	128	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)$
130	129	elv	$⊢ c \in ran (a \in nei (J) (B) ⟼ a \cap A) \leftrightarrow \exists a \in nei (J) (B) c = a \cap A$
131		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)$
132	130 131	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)$
133	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)))$
134	133	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))$
135	134	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))$
136	132 135	syl5bb	$⊢ (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))$
137	10 127 136	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))$
138	126 137	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))$
139	116 122 138	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))$
140	139	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