Metamath Proof Explorer

Theorem bnj1172

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 bnj1172.3 ⊢ C = trCl X A R ∩ B
bnj1172.96 ⊢ ∃ z ∀ w φ ∧ ψ → φ ∧ ψ ∧ z ∈ C ∧ θ → w R z → ¬ w ∈ B
bnj1172.113 ⊢ φ ∧ ψ ∧ z ∈ C → θ ↔ w ∈ A
Assertion bnj1172 ⊢ ∃ z ∀ w φ ∧ ψ → z ∈ B ∧ w ∈ A → w R z → ¬ w ∈ B

Proof

Step Hyp Ref Expression
1 bnj1172.3 ⊢ C = trCl X A R ∩ B
2 bnj1172.96 ⊢ ∃ z ∀ w φ ∧ ψ → φ ∧ ψ ∧ z ∈ C ∧ θ → w R z → ¬ w ∈ B
3 bnj1172.113 ⊢ φ ∧ ψ ∧ z ∈ C → θ ↔ w ∈ A
4 3 imbi1d ⊢ φ ∧ ψ ∧ z ∈ C → θ → w R z → ¬ w ∈ B ↔ w ∈ A → w R z → ¬ w ∈ B
5 4 pm5.32i ⊢ φ ∧ ψ ∧ z ∈ C ∧ θ → w R z → ¬ w ∈ B ↔ φ ∧ ψ ∧ z ∈ C ∧ w ∈ A → w R z → ¬ w ∈ B
6 5 imbi2i ⊢ φ ∧ ψ → φ ∧ ψ ∧ z ∈ C ∧ θ → w R z → ¬ w ∈ B ↔ φ ∧ ψ → φ ∧ ψ ∧ z ∈ C ∧ w ∈ A → w R z → ¬ w ∈ B
7 6 albii ⊢ ∀ w φ ∧ ψ → φ ∧ ψ ∧ z ∈ C ∧ θ → w R z → ¬ w ∈ B ↔ ∀ w φ ∧ ψ → φ ∧ ψ ∧ z ∈ C ∧ w ∈ A → w R z → ¬ w ∈ B
8 7 exbii ⊢ ∃ z ∀ w φ ∧ ψ → φ ∧ ψ ∧ z ∈ C ∧ θ → w R z → ¬ w ∈ B ↔ ∃ z ∀ w φ ∧ ψ → φ ∧ ψ ∧ z ∈ C ∧ w ∈ A → w R z → ¬ w ∈ B
9 2 8 mpbi ⊢ ∃ z ∀ w φ ∧ ψ → φ ∧ ψ ∧ z ∈ C ∧ w ∈ A → w R z → ¬ w ∈ B
10 simp3 ⊢ φ ∧ ψ ∧ z ∈ C → z ∈ C
11 10 1 eleqtrdi ⊢ φ ∧ ψ ∧ z ∈ C → z ∈ trCl X A R ∩ B
12 11 elin2d ⊢ φ ∧ ψ ∧ z ∈ C → z ∈ B
13 12 anim1i ⊢ φ ∧ ψ ∧ z ∈ C ∧ w ∈ A → w R z → ¬ w ∈ B → z ∈ B ∧ w ∈ A → w R z → ¬ w ∈ B
14 13 imim2i ⊢ φ ∧ ψ → φ ∧ ψ ∧ z ∈ C ∧ w ∈ A → w R z → ¬ w ∈ B → φ ∧ ψ → z ∈ B ∧ w ∈ A → w R z → ¬ w ∈ B
15 14 alimi ⊢ ∀ w φ ∧ ψ → φ ∧ ψ ∧ z ∈ C ∧ w ∈ A → w R z → ¬ w ∈ B → ∀ w φ ∧ ψ → z ∈ B ∧ w ∈ A → w R z → ¬ w ∈ B
16 9 15 bnj101 ⊢ ∃ z ∀ w φ ∧ ψ → z ∈ B ∧ w ∈ A → w R z → ¬ w ∈ B