Metamath Proof Explorer

Theorem bnj1176

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
Hypotheses bnj1176.51 ⊢ φ ∧ ψ → R Fr A ∧ C ⊆ A ∧ C ≠ ∅ ∧ C ∈ V
bnj1176.52 ⊢ R Fr A ∧ C ⊆ A ∧ C ≠ ∅ ∧ C ∈ V → ∃ z ∈ C ∀ w ∈ C ¬ w R z
Assertion bnj1176 ⊢ ∃ z ∀ w φ ∧ ψ → z ∈ C ∧ θ → w R z → ¬ w ∈ C

Proof

Step Hyp Ref Expression
1 bnj1176.51 ⊢ φ ∧ ψ → R Fr A ∧ C ⊆ A ∧ C ≠ ∅ ∧ C ∈ V
2 bnj1176.52 ⊢ R Fr A ∧ C ⊆ A ∧ C ≠ ∅ ∧ C ∈ V → ∃ z ∈ C ∀ w ∈ C ¬ w R z
3 1 2 syl ⊢ φ ∧ ψ → ∃ z ∈ C ∀ w ∈ C ¬ w R z
4 df-ral ⊢ ∀ w ∈ C ¬ w R z ↔ ∀ w w ∈ C → ¬ w R z
5 4 rexbii ⊢ ∃ z ∈ C ∀ w ∈ C ¬ w R z ↔ ∃ z ∈ C ∀ w w ∈ C → ¬ w R z
6 3 5 sylib ⊢ φ ∧ ψ → ∃ z ∈ C ∀ w w ∈ C → ¬ w R z
7 df-rex ⊢ ∃ z ∈ C ∀ w w ∈ C → ¬ w R z ↔ ∃ z z ∈ C ∧ ∀ w w ∈ C → ¬ w R z
8 6 7 sylib ⊢ φ ∧ ψ → ∃ z z ∈ C ∧ ∀ w w ∈ C → ¬ w R z
9 19.28v ⊢ ∀ w z ∈ C ∧ w ∈ C → ¬ w R z ↔ z ∈ C ∧ ∀ w w ∈ C → ¬ w R z
10 9 exbii ⊢ ∃ z ∀ w z ∈ C ∧ w ∈ C → ¬ w R z ↔ ∃ z z ∈ C ∧ ∀ w w ∈ C → ¬ w R z
11 8 10 sylibr ⊢ φ ∧ ψ → ∃ z ∀ w z ∈ C ∧ w ∈ C → ¬ w R z
12 19.37v ⊢ ∃ z φ ∧ ψ → ∀ w z ∈ C ∧ w ∈ C → ¬ w R z ↔ φ ∧ ψ → ∃ z ∀ w z ∈ C ∧ w ∈ C → ¬ w R z
13 11 12 mpbir ⊢ ∃ z φ ∧ ψ → ∀ w z ∈ C ∧ w ∈ C → ¬ w R z
14 19.21v ⊢ ∀ w φ ∧ ψ → z ∈ C ∧ w ∈ C → ¬ w R z ↔ φ ∧ ψ → ∀ w z ∈ C ∧ w ∈ C → ¬ w R z
15 14 exbii ⊢ ∃ z ∀ w φ ∧ ψ → z ∈ C ∧ w ∈ C → ¬ w R z ↔ ∃ z φ ∧ ψ → ∀ w z ∈ C ∧ w ∈ C → ¬ w R z
16 13 15 mpbir ⊢ ∃ z ∀ w φ ∧ ψ → z ∈ C ∧ w ∈ C → ¬ w R z
17 con2b ⊢ w ∈ C → ¬ w R z ↔ w R z → ¬ w ∈ C
18 17 anbi2i ⊢ z ∈ C ∧ w ∈ C → ¬ w R z ↔ z ∈ C ∧ w R z → ¬ w ∈ C
19 18 imbi2i ⊢ φ ∧ ψ → z ∈ C ∧ w ∈ C → ¬ w R z ↔ φ ∧ ψ → z ∈ C ∧ w R z → ¬ w ∈ C
20 19 albii ⊢ ∀ w φ ∧ ψ → z ∈ C ∧ w ∈ C → ¬ w R z ↔ ∀ w φ ∧ ψ → z ∈ C ∧ w R z → ¬ w ∈ C
21 20 exbii ⊢ ∃ z ∀ w φ ∧ ψ → z ∈ C ∧ w ∈ C → ¬ w R z ↔ ∃ z ∀ w φ ∧ ψ → z ∈ C ∧ w R z → ¬ w ∈ C
22 16 21 mpbi ⊢ ∃ z ∀ w φ ∧ ψ → z ∈ C ∧ w R z → ¬ w ∈ C
23 ax-1 ⊢ w R z → ¬ w ∈ C → θ → w R z → ¬ w ∈ C
24 23 anim2i ⊢ z ∈ C ∧ w R z → ¬ w ∈ C → z ∈ C ∧ θ → w R z → ¬ w ∈ C
25 24 imim2i ⊢ φ ∧ ψ → z ∈ C ∧ w R z → ¬ w ∈ C → φ ∧ ψ → z ∈ C ∧ θ → w R z → ¬ w ∈ C
26 25 alimi ⊢ ∀ w φ ∧ ψ → z ∈ C ∧ w R z → ¬ w ∈ C → ∀ w φ ∧ ψ → z ∈ C ∧ θ → w R z → ¬ w ∈ C
27 22 26 bnj101 ⊢ ∃ z ∀ w φ ∧ ψ → z ∈ C ∧ θ → w R z → ¬ w ∈ C