Theorem clsneibex

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

	Ref	Expression
Hypotheses	clsneibex.d	⊢ 𝐷 = ( 𝑃 ‘ 𝐵 )
	clsneibex.h	⊢ 𝐻 = ( 𝐹 ∘ 𝐷 )
	clsneibex.r	⊢ ( 𝜑 → 𝐾 𝐻 𝑁 )
Assertion	clsneibex	⊢ ( 𝜑 → 𝐵 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		clsneibex.d	⊢ 𝐷 = ( 𝑃 ‘ 𝐵 )
2		clsneibex.h	⊢ 𝐻 = ( 𝐹 ∘ 𝐷 )
3		clsneibex.r	⊢ ( 𝜑 → 𝐾 𝐻 𝑁 )
4	1	coeq2i	⊢ ( 𝐹 ∘ 𝐷 ) = ( 𝐹 ∘ ( 𝑃 ‘ 𝐵 ) )
5	2 4	eqtri	⊢ 𝐻 = ( 𝐹 ∘ ( 𝑃 ‘ 𝐵 ) )
6	5	a1i	⊢ ( 𝜑 → 𝐻 = ( 𝐹 ∘ ( 𝑃 ‘ 𝐵 ) ) )
7	6 3	breqdi	⊢ ( 𝜑 → 𝐾 ( 𝐹 ∘ ( 𝑃 ‘ 𝐵 ) ) 𝑁 )
8		brne0	⊢ ( 𝐾 ( 𝐹 ∘ ( 𝑃 ‘ 𝐵 ) ) 𝑁 → ( 𝐹 ∘ ( 𝑃 ‘ 𝐵 ) ) ≠ ∅ )
9		fvprc	⊢ ( ¬ 𝐵 ∈ V → ( 𝑃 ‘ 𝐵 ) = ∅ )
10	9	rneqd	⊢ ( ¬ 𝐵 ∈ V → ran ( 𝑃 ‘ 𝐵 ) = ran ∅ )
11		rn0	⊢ ran ∅ = ∅
12	10 11	eqtrdi	⊢ ( ¬ 𝐵 ∈ V → ran ( 𝑃 ‘ 𝐵 ) = ∅ )
13	12	ineq2d	⊢ ( ¬ 𝐵 ∈ V → ( dom 𝐹 ∩ ran ( 𝑃 ‘ 𝐵 ) ) = ( dom 𝐹 ∩ ∅ ) )
14		in0	⊢ ( dom 𝐹 ∩ ∅ ) = ∅
15	13 14	eqtrdi	⊢ ( ¬ 𝐵 ∈ V → ( dom 𝐹 ∩ ran ( 𝑃 ‘ 𝐵 ) ) = ∅ )
16	15	coemptyd	⊢ ( ¬ 𝐵 ∈ V → ( 𝐹 ∘ ( 𝑃 ‘ 𝐵 ) ) = ∅ )
17	16	necon1ai	⊢ ( ( 𝐹 ∘ ( 𝑃 ‘ 𝐵 ) ) ≠ ∅ → 𝐵 ∈ V )
18	7 8 17	3syl	⊢ ( 𝜑 → 𝐵 ∈ V )