This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bnj1185

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypothesis bnj1185.1 ⊢ φ → ∃ z ∈ B ∀ w ∈ B ¬ w R z
Assertion bnj1185 ⊢ φ → ∃ x ∈ B ∀ y ∈ B ¬ y R x

Proof

Step Hyp Ref Expression
1 bnj1185.1 ⊢ φ → ∃ z ∈ B ∀ w ∈ B ¬ w R z
2 breq1 ⊢ w = y → w R z ↔ y R z
3 2 notbid ⊢ w = y → ¬ w R z ↔ ¬ y R z
4 3 cbvralvw ⊢ ∀ w ∈ B ¬ w R z ↔ ∀ y ∈ B ¬ y R z
5 4 rexbii ⊢ ∃ z ∈ B ∀ w ∈ B ¬ w R z ↔ ∃ z ∈ B ∀ y ∈ B ¬ y R z
6 1 5 sylib ⊢ φ → ∃ z ∈ B ∀ y ∈ B ¬ y R z
7 eleq1w ⊢ z = x → z ∈ B ↔ x ∈ B
8 breq2 ⊢ z = x → y R z ↔ y R x
9 8 notbid ⊢ z = x → ¬ y R z ↔ ¬ y R x
10 9 ralbidv ⊢ z = x → ∀ y ∈ B ¬ y R z ↔ ∀ y ∈ B ¬ y R x
11 7 10 anbi12d ⊢ z = x → z ∈ B ∧ ∀ y ∈ B ¬ y R z ↔ x ∈ B ∧ ∀ y ∈ B ¬ y R x
12 11 cbvexvw ⊢ ∃ z z ∈ B ∧ ∀ y ∈ B ¬ y R z ↔ ∃ x x ∈ B ∧ ∀ y ∈ B ¬ y R x
13 df-rex ⊢ ∃ z ∈ B ∀ y ∈ B ¬ y R z ↔ ∃ z z ∈ B ∧ ∀ y ∈ B ¬ y R z
14 df-rex ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y R x ↔ ∃ x x ∈ B ∧ ∀ y ∈ B ¬ y R x
15 12 13 14 3bitr4ri ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y R x ↔ ∃ z ∈ B ∀ y ∈ B ¬ y R z
16 6 15 sylibr ⊢ φ → ∃ x ∈ B ∀ y ∈ B ¬ y R x