Metamath Proof Explorer

Theorem bnj1174

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

Proof

Step Hyp Ref Expression
1 bnj1174.3 ⊢ C = trCl X A R ∩ B
2 bnj1174.59 ⊢ ∃ z ∀ w φ ∧ ψ → z ∈ C ∧ θ → w R z → ¬ w ∈ C
3 bnj1174.74 ⊢ θ → w R z → w ∈ trCl X A R
4 1 eleq2i ⊢ w ∈ C ↔ w ∈ trCl X A R ∩ B
5 4 notbii ⊢ ¬ w ∈ C ↔ ¬ w ∈ trCl X A R ∩ B
6 ianor ⊢ ¬ w ∈ trCl X A R ∧ w ∈ B ↔ ¬ w ∈ trCl X A R ∨ ¬ w ∈ B
7 elin ⊢ w ∈ trCl X A R ∩ B ↔ w ∈ trCl X A R ∧ w ∈ B
8 7 notbii ⊢ ¬ w ∈ trCl X A R ∩ B ↔ ¬ w ∈ trCl X A R ∧ w ∈ B
9 pm4.62 ⊢ w ∈ trCl X A R → ¬ w ∈ B ↔ ¬ w ∈ trCl X A R ∨ ¬ w ∈ B
10 6 8 9 3bitr4i ⊢ ¬ w ∈ trCl X A R ∩ B ↔ w ∈ trCl X A R → ¬ w ∈ B
11 10 biimpi ⊢ ¬ w ∈ trCl X A R ∩ B → w ∈ trCl X A R → ¬ w ∈ B
12 11 impcom ⊢ w ∈ trCl X A R ∧ ¬ w ∈ trCl X A R ∩ B → ¬ w ∈ B
13 5 12 sylan2b ⊢ w ∈ trCl X A R ∧ ¬ w ∈ C → ¬ w ∈ B
14 13 ex ⊢ w ∈ trCl X A R → ¬ w ∈ C → ¬ w ∈ B
15 3 14 syl6 ⊢ θ → w R z → ¬ w ∈ C → ¬ w ∈ B
16 15 a2d ⊢ θ → w R z → ¬ w ∈ C → w R z → ¬ w ∈ B
17 16 biantru ⊢ z ∈ C ∧ θ → w R z → ¬ w ∈ C ↔ z ∈ C ∧ θ → w R z → ¬ w ∈ C ∧ θ → w R z → ¬ w ∈ C → w R z → ¬ w ∈ B
18 df-3an ⊢ z ∈ C ∧ θ → w R z → ¬ w ∈ C ∧ θ → w R z → ¬ w ∈ C → w R z → ¬ w ∈ B ↔ z ∈ C ∧ θ → w R z → ¬ w ∈ C ∧ θ → w R z → ¬ w ∈ C → w R z → ¬ w ∈ B
19 3anass ⊢ z ∈ C ∧ θ → w R z → ¬ w ∈ C ∧ θ → w R z → ¬ w ∈ C → w R z → ¬ w ∈ B ↔ z ∈ C ∧ θ → w R z → ¬ w ∈ C ∧ θ → w R z → ¬ w ∈ C → w R z → ¬ w ∈ B
20 17 18 19 3bitr2i ⊢ z ∈ C ∧ θ → w R z → ¬ w ∈ C ↔ z ∈ C ∧ θ → w R z → ¬ w ∈ C ∧ θ → w R z → ¬ w ∈ C → w R z → ¬ w ∈ B
21 20 imbi2i ⊢ φ ∧ ψ → z ∈ C ∧ θ → w R z → ¬ w ∈ C ↔ φ ∧ ψ → z ∈ C ∧ θ → w R z → ¬ w ∈ C ∧ θ → w R z → ¬ w ∈ C → w R z → ¬ w ∈ B
22 21 albii ⊢ ∀ w φ ∧ ψ → z ∈ C ∧ θ → w R z → ¬ w ∈ C ↔ ∀ w φ ∧ ψ → z ∈ C ∧ θ → w R z → ¬ w ∈ C ∧ θ → w R z → ¬ w ∈ C → w R z → ¬ w ∈ B
23 22 exbii ⊢ ∃ z ∀ w φ ∧ ψ → z ∈ C ∧ θ → w R z → ¬ w ∈ C ↔ ∃ z ∀ w φ ∧ ψ → z ∈ C ∧ θ → w R z → ¬ w ∈ C ∧ θ → w R z → ¬ w ∈ C → w R z → ¬ w ∈ B
24 2 23 mpbi ⊢ ∃ z ∀ w φ ∧ ψ → z ∈ C ∧ θ → w R z → ¬ w ∈ C ∧ θ → w R z → ¬ w ∈ C → w R z → ¬ w ∈ B
25 imdi ⊢ θ → w R z → ¬ w ∈ C → w R z → ¬ w ∈ B ↔ θ → w R z → ¬ w ∈ C → θ → w R z → ¬ w ∈ B
26 pm3.35 ⊢ θ → w R z → ¬ w ∈ C ∧ θ → w R z → ¬ w ∈ C → θ → w R z → ¬ w ∈ B → θ → w R z → ¬ w ∈ B
27 25 26 sylan2b ⊢ θ → w R z → ¬ w ∈ C ∧ θ → w R z → ¬ w ∈ C → w R z → ¬ w ∈ B → θ → w R z → ¬ w ∈ B
28 27 anim2i ⊢ z ∈ C ∧ θ → w R z → ¬ w ∈ C ∧ θ → w R z → ¬ w ∈ C → w R z → ¬ w ∈ B → z ∈ C ∧ θ → w R z → ¬ w ∈ B
29 28 imim2i ⊢ φ ∧ ψ → z ∈ C ∧ θ → w R z → ¬ w ∈ C ∧ θ → w R z → ¬ w ∈ C → w R z → ¬ w ∈ B → φ ∧ ψ → z ∈ C ∧ θ → w R z → ¬ w ∈ B
30 29 alimi ⊢ ∀ w φ ∧ ψ → z ∈ C ∧ θ → w R z → ¬ w ∈ C ∧ θ → w R z → ¬ w ∈ C → w R z → ¬ w ∈ B → ∀ w φ ∧ ψ → z ∈ C ∧ θ → w R z → ¬ w ∈ B
31 24 30 bnj101 ⊢ ∃ z ∀ w φ ∧ ψ → z ∈ C ∧ θ → w R z → ¬ w ∈ B
32 ancl ⊢ φ ∧ ψ → z ∈ C ∧ θ → w R z → ¬ w ∈ B → φ ∧ ψ → φ ∧ ψ ∧ z ∈ C ∧ θ → w R z → ¬ w ∈ B
33 bnj256 ⊢ φ ∧ ψ ∧ z ∈ C ∧ θ → w R z → ¬ w ∈ B ↔ φ ∧ ψ ∧ z ∈ C ∧ θ → w R z → ¬ w ∈ B
34 32 33 imbitrrdi ⊢ φ ∧ ψ → z ∈ C ∧ θ → w R z → ¬ w ∈ B → φ ∧ ψ → φ ∧ ψ ∧ z ∈ C ∧ θ → w R z → ¬ w ∈ B
35 34 alimi ⊢ ∀ w φ ∧ ψ → z ∈ C ∧ θ → w R z → ¬ w ∈ B → ∀ w φ ∧ ψ → φ ∧ ψ ∧ z ∈ C ∧ θ → w R z → ¬ w ∈ B
36 31 35 bnj101 ⊢ ∃ z ∀ w φ ∧ ψ → φ ∧ ψ ∧ z ∈ C ∧ θ → w R z → ¬ w ∈ B
37 df-bnj17 ⊢ φ ∧ ψ ∧ z ∈ C ∧ θ → w R z → ¬ w ∈ B ↔ φ ∧ ψ ∧ z ∈ C ∧ θ → w R z → ¬ w ∈ B
38 37 imbi2i ⊢ φ ∧ ψ → φ ∧ ψ ∧ z ∈ C ∧ θ → w R z → ¬ w ∈ B ↔ φ ∧ ψ → φ ∧ ψ ∧ z ∈ C ∧ θ → w R z → ¬ w ∈ B
39 38 albii ⊢ ∀ w φ ∧ ψ → φ ∧ ψ ∧ z ∈ C ∧ θ → w R z → ¬ w ∈ B ↔ ∀ w φ ∧ ψ → φ ∧ ψ ∧ z ∈ C ∧ θ → w R z → ¬ w ∈ B
40 39 exbii ⊢ ∃ z ∀ w φ ∧ ψ → φ ∧ ψ ∧ z ∈ C ∧ θ → w R z → ¬ w ∈ B ↔ ∃ z ∀ w φ ∧ ψ → φ ∧ ψ ∧ z ∈ C ∧ θ → w R z → ¬ w ∈ B
41 36 40 mpbi ⊢ ∃ z ∀ w φ ∧ ψ → φ ∧ ψ ∧ z ∈ C ∧ θ → w R z → ¬ w ∈ B