Metamath Proof Explorer

Theorem bnj1186

Description: Technical lemma for bnj69 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypothesis bnj1186.1 ⊢ ∃ z ∀ w φ ∧ ψ → z ∈ B ∧ w ∈ B → ¬ w R z
Assertion bnj1186 ⊢ φ ∧ ψ → ∃ z ∈ B ∀ w ∈ B ¬ w R z

Proof

Step Hyp Ref Expression
1 bnj1186.1 ⊢ ∃ z ∀ w φ ∧ ψ → z ∈ B ∧ w ∈ B → ¬ w R z
2 19.21v ⊢ ∀ w φ ∧ ψ → z ∈ B ∧ w ∈ B → ¬ w R z ↔ φ ∧ ψ → ∀ w z ∈ B ∧ w ∈ B → ¬ w R z
3 2 exbii ⊢ ∃ z ∀ w φ ∧ ψ → z ∈ B ∧ w ∈ B → ¬ w R z ↔ ∃ z φ ∧ ψ → ∀ w z ∈ B ∧ w ∈ B → ¬ w R z
4 1 3 mpbi ⊢ ∃ z φ ∧ ψ → ∀ w z ∈ B ∧ w ∈ B → ¬ w R z
5 4 19.37iv ⊢ φ ∧ ψ → ∃ z ∀ w z ∈ B ∧ w ∈ B → ¬ w R z
6 19.28v ⊢ ∀ w z ∈ B ∧ w ∈ B → ¬ w R z ↔ z ∈ B ∧ ∀ w w ∈ B → ¬ w R z
7 6 exbii ⊢ ∃ z ∀ w z ∈ B ∧ w ∈ B → ¬ w R z ↔ ∃ z z ∈ B ∧ ∀ w w ∈ B → ¬ w R z
8 5 7 sylib ⊢ φ ∧ ψ → ∃ z z ∈ B ∧ ∀ w w ∈ B → ¬ w R z
9 df-ral ⊢ ∀ w ∈ B ¬ w R z ↔ ∀ w w ∈ B → ¬ w R z
10 9 anbi2i ⊢ z ∈ B ∧ ∀ w ∈ B ¬ w R z ↔ z ∈ B ∧ ∀ w w ∈ B → ¬ w R z
11 10 exbii ⊢ ∃ z z ∈ B ∧ ∀ w ∈ B ¬ w R z ↔ ∃ z z ∈ B ∧ ∀ w w ∈ B → ¬ w R z
12 8 11 sylibr ⊢ φ ∧ ψ → ∃ z z ∈ B ∧ ∀ w ∈ B ¬ w R z
13 df-rex ⊢ ∃ z ∈ B ∀ w ∈ B ¬ w R z ↔ ∃ z z ∈ B ∧ ∀ w ∈ B ¬ w R z
14 12 13 sylibr ⊢ φ ∧ ψ → ∃ z ∈ B ∀ w ∈ B ¬ w R z