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	$⊢ φ \to J \in Top$
	opnneilv.2	$⊢ (φ \land y \subseteq x) \to (ψ \to χ)$
Assertion	opnneilv	$⊢ φ \to (\exists x \in nei (J) (S) ψ \to \exists y \in J (S \subseteq y \land χ))$

Proof

Step	Hyp	Ref	Expression
1		opnneir.1	$⊢ φ \to J \in Top$
2		opnneilv.2	$⊢ (φ \land y \subseteq x) \to (ψ \to χ)$
3		df-rex	$⊢ \exists x \in nei (J) (S) ψ \leftrightarrow \exists x (x \in nei (J) (S) \land ψ)$
4		neii2	$⊢ (J \in Top \land x \in nei (J) (S)) \to \exists y \in J (S \subseteq y \land y \subseteq x)$
5	1 4	sylan	$⊢ (φ \land x \in nei (J) (S)) \to \exists y \in J (S \subseteq y \land y \subseteq x)$
6	5	r19.41dv	$⊢ ((φ \land x \in nei (J) (S)) \land ψ) \to \exists y \in J ((S \subseteq y \land y \subseteq x) \land ψ)$
7	6	expl	$⊢ φ \to ((x \in nei (J) (S) \land ψ) \to \exists y \in J ((S \subseteq y \land y \subseteq x) \land ψ))$
8		anass	$⊢ ((S \subseteq y \land y \subseteq x) \land ψ) \leftrightarrow (S \subseteq y \land (y \subseteq x \land ψ))$
9	2	expimpd	$⊢ φ \to ((y \subseteq x \land ψ) \to χ)$
10	9	anim2d	$⊢ φ \to ((S \subseteq y \land (y \subseteq x \land ψ)) \to (S \subseteq y \land χ))$
11	8 10	biimtrid	$⊢ φ \to (((S \subseteq y \land y \subseteq x) \land ψ) \to (S \subseteq y \land χ))$
12	11	reximdv	$⊢ φ \to (\exists y \in J ((S \subseteq y \land y \subseteq x) \land ψ) \to \exists y \in J (S \subseteq y \land χ))$
13	7 12	syld	$⊢ φ \to ((x \in nei (J) (S) \land ψ) \to \exists y \in J (S \subseteq y \land χ))$
14	13	exlimdv	$⊢ φ \to (\exists x (x \in nei (J) (S) \land ψ) \to \exists y \in J (S \subseteq y \land χ))$
15	3 14	biimtrid	$⊢ φ \to (\exists x \in nei (J) (S) ψ \to \exists y \in J (S \subseteq y \land χ))$

Metamath Proof Explorer

Theorem opnneilv

Proof