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	⊢ ( 𝜑 → 𝐽 ∈ Top )
	opnneilv.2	⊢ ( ( 𝜑 ∧ 𝑦 ⊆ 𝑥 ) → ( 𝜓 → 𝜒 ) )
Assertion	opnneilv	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) 𝜓 → ∃ 𝑦 ∈ 𝐽 ( 𝑆 ⊆ 𝑦 ∧ 𝜒 ) ) )

Proof

Step	Hyp	Ref	Expression
1		opnneir.1	⊢ ( 𝜑 → 𝐽 ∈ Top )
2		opnneilv.2	⊢ ( ( 𝜑 ∧ 𝑦 ⊆ 𝑥 ) → ( 𝜓 → 𝜒 ) )
3		df-rex	⊢ ( ∃ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) 𝜓 ↔ ∃ 𝑥 ( 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝜓 ) )
4		neii2	⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → ∃ 𝑦 ∈ 𝐽 ( 𝑆 ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑥 ) )
5	1 4	sylan	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) → ∃ 𝑦 ∈ 𝐽 ( 𝑆 ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑥 ) )
6	5	r19.41dv	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ) ∧ 𝜓 ) → ∃ 𝑦 ∈ 𝐽 ( ( 𝑆 ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑥 ) ∧ 𝜓 ) )
7	6	expl	⊢ ( 𝜑 → ( ( 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝜓 ) → ∃ 𝑦 ∈ 𝐽 ( ( 𝑆 ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑥 ) ∧ 𝜓 ) ) )
8		anass	⊢ ( ( ( 𝑆 ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑥 ) ∧ 𝜓 ) ↔ ( 𝑆 ⊆ 𝑦 ∧ ( 𝑦 ⊆ 𝑥 ∧ 𝜓 ) ) )
9	2	expimpd	⊢ ( 𝜑 → ( ( 𝑦 ⊆ 𝑥 ∧ 𝜓 ) → 𝜒 ) )
10	9	anim2d	⊢ ( 𝜑 → ( ( 𝑆 ⊆ 𝑦 ∧ ( 𝑦 ⊆ 𝑥 ∧ 𝜓 ) ) → ( 𝑆 ⊆ 𝑦 ∧ 𝜒 ) ) )
11	8 10	syl5bi	⊢ ( 𝜑 → ( ( ( 𝑆 ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑥 ) ∧ 𝜓 ) → ( 𝑆 ⊆ 𝑦 ∧ 𝜒 ) ) )
12	11	reximdv	⊢ ( 𝜑 → ( ∃ 𝑦 ∈ 𝐽 ( ( 𝑆 ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑥 ) ∧ 𝜓 ) → ∃ 𝑦 ∈ 𝐽 ( 𝑆 ⊆ 𝑦 ∧ 𝜒 ) ) )
13	7 12	syld	⊢ ( 𝜑 → ( ( 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝜓 ) → ∃ 𝑦 ∈ 𝐽 ( 𝑆 ⊆ 𝑦 ∧ 𝜒 ) ) )
14	13	exlimdv	⊢ ( 𝜑 → ( ∃ 𝑥 ( 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝜓 ) → ∃ 𝑦 ∈ 𝐽 ( 𝑆 ⊆ 𝑦 ∧ 𝜒 ) ) )
15	3 14	syl5bi	⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ 𝑆 ) 𝜓 → ∃ 𝑦 ∈ 𝐽 ( 𝑆 ⊆ 𝑦 ∧ 𝜒 ) ) )