Theorem opnneilv

Description: The converse of opnneir with different dummy variables. Note that the second hypothesis could be generalized by adding y e. J to the antecedent. See the proof for details. Although J e. Top might be redundant here (see neircl ), it is listed for explicitness. (Contributed by Zhi Wang, 31-Aug-2024)

	Ref	Expression
Hypotheses	opnneir.1	|- ( ph -> J e. Top )
	opnneilv.2	|- ( ( ph /\ y C_ x ) -> ( ps -> ch ) )
Assertion	opnneilv	|- ( ph -> ( E. x e. ( ( nei ` J ) ` S ) ps -> E. y e. J ( S C_ y /\ ch ) ) )

Proof

Step	Hyp	Ref	Expression
1		opnneir.1	|- ( ph -> J e. Top )
2		opnneilv.2	|- ( ( ph /\ y C_ x ) -> ( ps -> ch ) )
3		df-rex	|- ( E. x e. ( ( nei ` J ) ` S ) ps <-> E. x ( x e. ( ( nei ` J ) ` S ) /\ ps ) )
4		neii2	|- ( ( J e. Top /\ x e. ( ( nei ` J ) ` S ) ) -> E. y e. J ( S C_ y /\ y C_ x ) )
5	1 4	sylan	|- ( ( ph /\ x e. ( ( nei ` J ) ` S ) ) -> E. y e. J ( S C_ y /\ y C_ x ) )
6	5	r19.41dv	|- ( ( ( ph /\ x e. ( ( nei ` J ) ` S ) ) /\ ps ) -> E. y e. J ( ( S C_ y /\ y C_ x ) /\ ps ) )
7	6	expl	|- ( ph -> ( ( x e. ( ( nei ` J ) ` S ) /\ ps ) -> E. y e. J ( ( S C_ y /\ y C_ x ) /\ ps ) ) )
8		anass	|- ( ( ( S C_ y /\ y C_ x ) /\ ps ) <-> ( S C_ y /\ ( y C_ x /\ ps ) ) )
9	2	expimpd	|- ( ph -> ( ( y C_ x /\ ps ) -> ch ) )
10	9	anim2d	|- ( ph -> ( ( S C_ y /\ ( y C_ x /\ ps ) ) -> ( S C_ y /\ ch ) ) )
11	8 10	syl5bi	|- ( ph -> ( ( ( S C_ y /\ y C_ x ) /\ ps ) -> ( S C_ y /\ ch ) ) )
12	11	reximdv	|- ( ph -> ( E. y e. J ( ( S C_ y /\ y C_ x ) /\ ps ) -> E. y e. J ( S C_ y /\ ch ) ) )
13	7 12	syld	|- ( ph -> ( ( x e. ( ( nei ` J ) ` S ) /\ ps ) -> E. y e. J ( S C_ y /\ ch ) ) )
14	13	exlimdv	|- ( ph -> ( E. x ( x e. ( ( nei ` J ) ` S ) /\ ps ) -> E. y e. J ( S C_ y /\ ch ) ) )
15	3 14	syl5bi	|- ( ph -> ( E. x e. ( ( nei ` J ) ` S ) ps -> E. y e. J ( S C_ y /\ ch ) ) )