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	⊢ 𝐷 = ( 𝑃 ‘ 𝐵 )
	neicvgbex.h	⊢ 𝐻 = ( 𝐹 ∘ ( 𝐷 ∘ 𝐺 ) )
	neicvgbex.r	⊢ ( 𝜑 → 𝑁 𝐻 𝑀 )
Assertion	neicvgbex	⊢ ( 𝜑 → 𝐵 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		neicvgbex.d	⊢ 𝐷 = ( 𝑃 ‘ 𝐵 )
2		neicvgbex.h	⊢ 𝐻 = ( 𝐹 ∘ ( 𝐷 ∘ 𝐺 ) )
3		neicvgbex.r	⊢ ( 𝜑 → 𝑁 𝐻 𝑀 )
4	1	coeq1i	⊢ ( 𝐷 ∘ 𝐺 ) = ( ( 𝑃 ‘ 𝐵 ) ∘ 𝐺 )
5	4	coeq2i	⊢ ( 𝐹 ∘ ( 𝐷 ∘ 𝐺 ) ) = ( 𝐹 ∘ ( ( 𝑃 ‘ 𝐵 ) ∘ 𝐺 ) )
6	2 5	eqtri	⊢ 𝐻 = ( 𝐹 ∘ ( ( 𝑃 ‘ 𝐵 ) ∘ 𝐺 ) )
7	6	a1i	⊢ ( 𝜑 → 𝐻 = ( 𝐹 ∘ ( ( 𝑃 ‘ 𝐵 ) ∘ 𝐺 ) ) )
8	7 3	breqdi	⊢ ( 𝜑 → 𝑁 ( 𝐹 ∘ ( ( 𝑃 ‘ 𝐵 ) ∘ 𝐺 ) ) 𝑀 )
9		brne0	⊢ ( 𝑁 ( 𝐹 ∘ ( ( 𝑃 ‘ 𝐵 ) ∘ 𝐺 ) ) 𝑀 → ( 𝐹 ∘ ( ( 𝑃 ‘ 𝐵 ) ∘ 𝐺 ) ) ≠ ∅ )
10		fvprc	⊢ ( ¬ 𝐵 ∈ V → ( 𝑃 ‘ 𝐵 ) = ∅ )
11	10	dmeqd	⊢ ( ¬ 𝐵 ∈ V → dom ( 𝑃 ‘ 𝐵 ) = dom ∅ )
12		dm0	⊢ dom ∅ = ∅
13	11 12	eqtrdi	⊢ ( ¬ 𝐵 ∈ V → dom ( 𝑃 ‘ 𝐵 ) = ∅ )
14	13	ineq1d	⊢ ( ¬ 𝐵 ∈ V → ( dom ( 𝑃 ‘ 𝐵 ) ∩ ran 𝐺 ) = ( ∅ ∩ ran 𝐺 ) )
15		0in	⊢ ( ∅ ∩ ran 𝐺 ) = ∅
16	14 15	eqtrdi	⊢ ( ¬ 𝐵 ∈ V → ( dom ( 𝑃 ‘ 𝐵 ) ∩ ran 𝐺 ) = ∅ )
17	16	coemptyd	⊢ ( ¬ 𝐵 ∈ V → ( ( 𝑃 ‘ 𝐵 ) ∘ 𝐺 ) = ∅ )
18	17	rneqd	⊢ ( ¬ 𝐵 ∈ V → ran ( ( 𝑃 ‘ 𝐵 ) ∘ 𝐺 ) = ran ∅ )
19		rn0	⊢ ran ∅ = ∅
20	18 19	eqtrdi	⊢ ( ¬ 𝐵 ∈ V → ran ( ( 𝑃 ‘ 𝐵 ) ∘ 𝐺 ) = ∅ )
21	20	ineq2d	⊢ ( ¬ 𝐵 ∈ V → ( dom 𝐹 ∩ ran ( ( 𝑃 ‘ 𝐵 ) ∘ 𝐺 ) ) = ( dom 𝐹 ∩ ∅ ) )
22		in0	⊢ ( dom 𝐹 ∩ ∅ ) = ∅
23	21 22	eqtrdi	⊢ ( ¬ 𝐵 ∈ V → ( dom 𝐹 ∩ ran ( ( 𝑃 ‘ 𝐵 ) ∘ 𝐺 ) ) = ∅ )
24	23	coemptyd	⊢ ( ¬ 𝐵 ∈ V → ( 𝐹 ∘ ( ( 𝑃 ‘ 𝐵 ) ∘ 𝐺 ) ) = ∅ )
25	24	necon1ai	⊢ ( ( 𝐹 ∘ ( ( 𝑃 ‘ 𝐵 ) ∘ 𝐺 ) ) ≠ ∅ → 𝐵 ∈ V )
26	8 9 25	3syl	⊢ ( 𝜑 → 𝐵 ∈ V )