neicvgbex

Description: If (pseudo-)neighborhood and (pseudo-)convergent functions are related by the composite operator, H , then the base set exists. (Contributed by RP, 4-Jun-2021)

	Ref	Expression
Hypotheses	neicvgbex.d	$⊢ D = P (B)$
	neicvgbex.h	$⊢ H = F \circ (D \circ G)$
	neicvgbex.r	$⊢ φ \to N H M$
Assertion	neicvgbex	$⊢ φ \to B \in V$

Proof

Step	Hyp	Ref	Expression
1		neicvgbex.d	$⊢ D = P (B)$
2		neicvgbex.h	$⊢ H = F \circ (D \circ G)$
3		neicvgbex.r	$⊢ φ \to N H M$
4	1	coeq1i	$⊢ D \circ G = P (B) \circ G$
5	4	coeq2i	$⊢ F \circ (D \circ G) = F \circ (P (B) \circ G)$
6	2 5	eqtri	$⊢ H = F \circ (P (B) \circ G)$
7	6	a1i	$⊢ φ \to H = F \circ (P (B) \circ G)$
8	7 3	breqdi	$⊢ φ \to N (F \circ (P (B) \circ G)) M$
9		brne0	$⊢ N (F \circ (P (B) \circ G)) M \to F \circ (P (B) \circ G) \neq \emptyset$
10		fvprc	$⊢ \neg B \in V \to P (B) = \emptyset$
11	10	dmeqd	$⊢ \neg B \in V \to dom P (B) = dom \emptyset$
12		dm0	$⊢ dom \emptyset = \emptyset$
13	11 12	eqtrdi	$⊢ \neg B \in V \to dom P (B) = \emptyset$
14	13	ineq1d	$⊢ \neg B \in V \to dom P (B) \cap ran G = \emptyset \cap ran G$
15		0in	$⊢ \emptyset \cap ran G = \emptyset$
16	14 15	eqtrdi	$⊢ \neg B \in V \to dom P (B) \cap ran G = \emptyset$
17	16	coemptyd	$⊢ \neg B \in V \to P (B) \circ G = \emptyset$
18	17	rneqd	$⊢ \neg B \in V \to ran (P (B) \circ G) = ran \emptyset$
19		rn0	$⊢ ran \emptyset = \emptyset$
20	18 19	eqtrdi	$⊢ \neg B \in V \to ran (P (B) \circ G) = \emptyset$
21	20	ineq2d	$⊢ \neg B \in V \to dom F \cap ran (P (B) \circ G) = dom F \cap \emptyset$
22		in0	$⊢ dom F \cap \emptyset = \emptyset$
23	21 22	eqtrdi	$⊢ \neg B \in V \to dom F \cap ran (P (B) \circ G) = \emptyset$
24	23	coemptyd	$⊢ \neg B \in V \to F \circ (P (B) \circ G) = \emptyset$
25	24	necon1ai	$⊢ F \circ (P (B) \circ G) \neq \emptyset \to B \in V$
26	8 9 25	3syl	$⊢ φ \to B \in V$

Metamath Proof Explorer

Theorem neicvgbex

Proof