Metamath Proof Explorer

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 ⊢ φ → J ∈ Top
opnneilv.2 ⊢ φ ∧ y ⊆ x → ψ → χ
Assertion opnneilv ⊢ φ → ∃ x ∈ nei ⁡ J ⁡ S ψ → ∃ y ∈ J S ⊆ y ∧ χ

Proof

Step Hyp Ref Expression
1 opnneir.1 ⊢ φ → J ∈ Top
2 opnneilv.2 ⊢ φ ∧ y ⊆ x → ψ → χ
3 df-rex ⊢ ∃ x ∈ nei ⁡ J ⁡ S ψ ↔ ∃ x x ∈ nei ⁡ J ⁡ S ∧ ψ
4 neii2 ⊢ J ∈ Top ∧ x ∈ nei ⁡ J ⁡ S → ∃ y ∈ J S ⊆ y ∧ y ⊆ x
5 1 4 sylan ⊢ φ ∧ x ∈ nei ⁡ J ⁡ S → ∃ y ∈ J S ⊆ y ∧ y ⊆ x
6 5 r19.41dv ⊢ φ ∧ x ∈ nei ⁡ J ⁡ S ∧ ψ → ∃ y ∈ J S ⊆ y ∧ y ⊆ x ∧ ψ
7 6 expl ⊢ φ → x ∈ nei ⁡ J ⁡ S ∧ ψ → ∃ y ∈ J S ⊆ y ∧ y ⊆ x ∧ ψ
8 anass ⊢ S ⊆ y ∧ y ⊆ x ∧ ψ ↔ S ⊆ y ∧ y ⊆ x ∧ ψ
9 2 expimpd ⊢ φ → y ⊆ x ∧ ψ → χ
10 9 anim2d ⊢ φ → S ⊆ y ∧ y ⊆ x ∧ ψ → S ⊆ y ∧ χ
11 8 10 syl5bi ⊢ φ → S ⊆ y ∧ y ⊆ x ∧ ψ → S ⊆ y ∧ χ
12 11 reximdv ⊢ φ → ∃ y ∈ J S ⊆ y ∧ y ⊆ x ∧ ψ → ∃ y ∈ J S ⊆ y ∧ χ
13 7 12 syld ⊢ φ → x ∈ nei ⁡ J ⁡ S ∧ ψ → ∃ y ∈ J S ⊆ y ∧ χ
14 13 exlimdv ⊢ φ → ∃ x x ∈ nei ⁡ J ⁡ S ∧ ψ → ∃ y ∈ J S ⊆ y ∧ χ
15 3 14 syl5bi ⊢ φ → ∃ x ∈ nei ⁡ J ⁡ S ψ → ∃ y ∈ J S ⊆ y ∧ χ