neicvgel1

Description: A subset being an element of a neighborhood of a point is equivalent to the complement of that subset not being a element of the convergent of that point. (Contributed by RP, 12-Jun-2021)

	Ref	Expression
Hypotheses	neicvg.o	$⊢ O = (i \in V, j \in V ⟼ (k \in ({𝒫 j}^{i}) ⟼ (l \in j ⟼ \{m \in i \| l \in k (m)\})))$
	neicvg.p	$⊢ P = (n \in V ⟼ (p \in ({𝒫 n}^{𝒫 n}) ⟼ (o \in 𝒫 n ⟼ n ∖ p (n ∖ o))))$
	neicvg.d	$⊢ D = P (B)$
	neicvg.f	$⊢ F = 𝒫 B O B$
	neicvg.g	$⊢ G = B O 𝒫 B$
	neicvg.h	$⊢ H = F \circ (D \circ G)$
	neicvg.r	$⊢ φ \to N H M$
	neicvgel.x	$⊢ φ \to X \in B$
	neicvgel.s	$⊢ φ \to S \in 𝒫 B$
Assertion	neicvgel1	$⊢ φ \to (S \in N (X) \leftrightarrow \neg B ∖ S \in M (X))$

Proof

Step	Hyp	Ref	Expression
1		neicvg.o	$⊢ O = (i \in V, j \in V ⟼ (k \in ({𝒫 j}^{i}) ⟼ (l \in j ⟼ \{m \in i \| l \in k (m)\})))$
2		neicvg.p	$⊢ P = (n \in V ⟼ (p \in ({𝒫 n}^{𝒫 n}) ⟼ (o \in 𝒫 n ⟼ n ∖ p (n ∖ o))))$
3		neicvg.d	$⊢ D = P (B)$
4		neicvg.f	$⊢ F = 𝒫 B O B$
5		neicvg.g	$⊢ G = B O 𝒫 B$
6		neicvg.h	$⊢ H = F \circ (D \circ G)$
7		neicvg.r	$⊢ φ \to N H M$
8		neicvgel.x	$⊢ φ \to X \in B$
9		neicvgel.s	$⊢ φ \to S \in 𝒫 B$
10	3 6 7	neicvgbex	$⊢ φ \to B \in V$
11		simpr	$⊢ (φ \land B \in V) \to B \in V$
12	11	pwexd	$⊢ (φ \land B \in V) \to 𝒫 B \in V$
13	1 12 11 4	fsovf1od	$⊢ (φ \land B \in V) \to F : {𝒫 B}^{𝒫 B} \underset{1-1 onto}{⟶} {𝒫 𝒫 B}^{B}$
14		f1ofn	$⊢ F : {𝒫 B}^{𝒫 B} \underset{1-1 onto}{⟶} {𝒫 𝒫 B}^{B} \to F Fn ({𝒫 B}^{𝒫 B})$
15	13 14	syl	$⊢ (φ \land B \in V) \to F Fn ({𝒫 B}^{𝒫 B})$
16	2 3 11	dssmapf1od	$⊢ (φ \land B \in V) \to D : {𝒫 B}^{𝒫 B} \underset{1-1 onto}{⟶} {𝒫 B}^{𝒫 B}$
17		f1of	$⊢ D : {𝒫 B}^{𝒫 B} \underset{1-1 onto}{⟶} {𝒫 B}^{𝒫 B} \to D : {𝒫 B}^{𝒫 B} ⟶ {𝒫 B}^{𝒫 B}$
18	16 17	syl	$⊢ (φ \land B \in V) \to D : {𝒫 B}^{𝒫 B} ⟶ {𝒫 B}^{𝒫 B}$
19	1 11 12 5	fsovfd	$⊢ (φ \land B \in V) \to G : {𝒫 𝒫 B}^{B} ⟶ {𝒫 B}^{𝒫 B}$
20	6	breqi	$⊢ N H M \leftrightarrow N (F \circ (D \circ G)) M$
21	7 20	sylib	$⊢ φ \to N (F \circ (D \circ G)) M$
22	21	adantr	$⊢ (φ \land B \in V) \to N (F \circ (D \circ G)) M$
23	15 18 19 22	brcofffn	$⊢ (φ \land B \in V) \to (N G G (N) \land G (N) D D (G (N)) \land D (G (N)) F M)$
24	10 23	mpdan	$⊢ φ \to (N G G (N) \land G (N) D D (G (N)) \land D (G (N)) F M)$
25		simpr2	$⊢ (φ \land (N G G (N) \land G (N) D D (G (N)) \land D (G (N)) F M)) \to G (N) D D (G (N))$
26	8	adantr	$⊢ (φ \land (N G G (N) \land G (N) D D (G (N)) \land D (G (N)) F M)) \to X \in B$
27	9	adantr	$⊢ (φ \land (N G G (N) \land G (N) D D (G (N)) \land D (G (N)) F M)) \to S \in 𝒫 B$
28	2 3 25 26 27	ntrclselnel1	$⊢ (φ \land (N G G (N) \land G (N) D D (G (N)) \land D (G (N)) F M)) \to (X \in G (N) (S) \leftrightarrow \neg X \in D (G (N)) (B ∖ S))$
29		eqid	$⊢ 𝒫 B O B = 𝒫 B O B$
30		simpr1	$⊢ (φ \land (N G G (N) \land G (N) D D (G (N)) \land D (G (N)) F M)) \to N G G (N)$
31	5	breqi	$⊢ N G G (N) \leftrightarrow N (B O 𝒫 B) G (N)$
32	31	a1i	$⊢ (φ \land (N G G (N) \land G (N) D D (G (N)) \land D (G (N)) F M)) \to (N G G (N) \leftrightarrow N (B O 𝒫 B) G (N))$
33	10	adantr	$⊢ (φ \land (N G G (N) \land G (N) D D (G (N)) \land D (G (N)) F M)) \to B \in V$
34		id	$⊢ B \in V \to B \in V$
35		pwexg	$⊢ B \in V \to 𝒫 B \in V$
36		eqid	$⊢ B O 𝒫 B = B O 𝒫 B$
37	1 34 35 36	fsovf1od	$⊢ B \in V \to (B O 𝒫 B) : {𝒫 𝒫 B}^{B} \underset{1-1 onto}{⟶} {𝒫 B}^{𝒫 B}$
38	33 37	syl	$⊢ (φ \land (N G G (N) \land G (N) D D (G (N)) \land D (G (N)) F M)) \to (B O 𝒫 B) : {𝒫 𝒫 B}^{B} \underset{1-1 onto}{⟶} {𝒫 B}^{𝒫 B}$
39		f1orel	$⊢ (B O 𝒫 B) : {𝒫 𝒫 B}^{B} \underset{1-1 onto}{⟶} {𝒫 B}^{𝒫 B} \to Rel (B O 𝒫 B)$
40		relbrcnvg	$⊢ Rel (B O 𝒫 B) \to (G (N) {(B O 𝒫 B)}^{-1} N \leftrightarrow N (B O 𝒫 B) G (N))$
41	38 39 40	3syl	$⊢ (φ \land (N G G (N) \land G (N) D D (G (N)) \land D (G (N)) F M)) \to (G (N) {(B O 𝒫 B)}^{-1} N \leftrightarrow N (B O 𝒫 B) G (N))$
42	1 34 35 36 29	fsovcnvd	$⊢ B \in V \to {(B O 𝒫 B)}^{-1} = 𝒫 B O B$
43	42	breqd	$⊢ B \in V \to (G (N) {(B O 𝒫 B)}^{-1} N \leftrightarrow G (N) (𝒫 B O B) N)$
44	33 43	syl	$⊢ (φ \land (N G G (N) \land G (N) D D (G (N)) \land D (G (N)) F M)) \to (G (N) {(B O 𝒫 B)}^{-1} N \leftrightarrow G (N) (𝒫 B O B) N)$
45	32 41 44	3bitr2d	$⊢ (φ \land (N G G (N) \land G (N) D D (G (N)) \land D (G (N)) F M)) \to (N G G (N) \leftrightarrow G (N) (𝒫 B O B) N)$
46	30 45	mpbid	$⊢ (φ \land (N G G (N) \land G (N) D D (G (N)) \land D (G (N)) F M)) \to G (N) (𝒫 B O B) N$
47	1 29 46 26 27	ntrneiel	$⊢ (φ \land (N G G (N) \land G (N) D D (G (N)) \land D (G (N)) F M)) \to (X \in G (N) (S) \leftrightarrow S \in N (X))$
48		simpr3	$⊢ (φ \land (N G G (N) \land G (N) D D (G (N)) \land D (G (N)) F M)) \to D (G (N)) F M$
49		difssd	$⊢ φ \to B ∖ S \subseteq B$
50	10 49	sselpwd	$⊢ φ \to B ∖ S \in 𝒫 B$
51	50	adantr	$⊢ (φ \land (N G G (N) \land G (N) D D (G (N)) \land D (G (N)) F M)) \to B ∖ S \in 𝒫 B$
52	1 4 48 26 51	ntrneiel	$⊢ (φ \land (N G G (N) \land G (N) D D (G (N)) \land D (G (N)) F M)) \to (X \in D (G (N)) (B ∖ S) \leftrightarrow B ∖ S \in M (X))$
53	52	notbid	$⊢ (φ \land (N G G (N) \land G (N) D D (G (N)) \land D (G (N)) F M)) \to (\neg X \in D (G (N)) (B ∖ S) \leftrightarrow \neg B ∖ S \in M (X))$
54	28 47 53	3bitr3d	$⊢ (φ \land (N G G (N) \land G (N) D D (G (N)) \land D (G (N)) F M)) \to (S \in N (X) \leftrightarrow \neg B ∖ S \in M (X))$
55	24 54	mpdan	$⊢ φ \to (S \in N (X) \leftrightarrow \neg B ∖ S \in M (X))$

Metamath Proof Explorer

Theorem neicvgel1

Proof