Theorem 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 o. ( D o. G ) )
	neicvgbex.r	|- ( ph -> N H M )
Assertion	neicvgbex	|- ( ph -> B e. _V )

Proof

Step	Hyp	Ref	Expression
1		neicvgbex.d	|- D = ( P ` B )
2		neicvgbex.h	|- H = ( F o. ( D o. G ) )
3		neicvgbex.r	|- ( ph -> N H M )
4	1	coeq1i	|- ( D o. G ) = ( ( P ` B ) o. G )
5	4	coeq2i	|- ( F o. ( D o. G ) ) = ( F o. ( ( P ` B ) o. G ) )
6	2 5	eqtri	|- H = ( F o. ( ( P ` B ) o. G ) )
7	6	a1i	|- ( ph -> H = ( F o. ( ( P ` B ) o. G ) ) )
8	7 3	breqdi	|- ( ph -> N ( F o. ( ( P ` B ) o. G ) ) M )
9		brne0	|- ( N ( F o. ( ( P ` B ) o. G ) ) M -> ( F o. ( ( P ` B ) o. G ) ) =/= (/) )
10		fvprc	|- ( -. B e. _V -> ( P ` B ) = (/) )
11	10	dmeqd	|- ( -. B e. _V -> dom ( P ` B ) = dom (/) )
12		dm0	|- dom (/) = (/)
13	11 12	eqtrdi	|- ( -. B e. _V -> dom ( P ` B ) = (/) )
14	13	ineq1d	|- ( -. B e. _V -> ( dom ( P ` B ) i^i ran G ) = ( (/) i^i ran G ) )
15		0in	|- ( (/) i^i ran G ) = (/)
16	14 15	eqtrdi	|- ( -. B e. _V -> ( dom ( P ` B ) i^i ran G ) = (/) )
17	16	coemptyd	|- ( -. B e. _V -> ( ( P ` B ) o. G ) = (/) )
18	17	rneqd	|- ( -. B e. _V -> ran ( ( P ` B ) o. G ) = ran (/) )
19		rn0	|- ran (/) = (/)
20	18 19	eqtrdi	|- ( -. B e. _V -> ran ( ( P ` B ) o. G ) = (/) )
21	20	ineq2d	|- ( -. B e. _V -> ( dom F i^i ran ( ( P ` B ) o. G ) ) = ( dom F i^i (/) ) )
22		in0	|- ( dom F i^i (/) ) = (/)
23	21 22	eqtrdi	|- ( -. B e. _V -> ( dom F i^i ran ( ( P ` B ) o. G ) ) = (/) )
24	23	coemptyd	|- ( -. B e. _V -> ( F o. ( ( P ` B ) o. G ) ) = (/) )
25	24	necon1ai	|- ( ( F o. ( ( P ` B ) o. G ) ) =/= (/) -> B e. _V )
26	8 9 25	3syl	|- ( ph -> B e. _V )