Metamath Proof Explorer

Theorem bnj1189

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 bnj1189.1 ⊢ φ ↔ R FrSe A ∧ B ⊆ A ∧ B ≠ ∅
bnj1189.2 ⊢ ψ ↔ x ∈ B ∧ y ∈ B ∧ y R x
bnj1189.3 ⊢ χ ↔ ∀ y ∈ B ¬ y R x
Assertion bnj1189 ⊢ φ → ∃ x ∈ B ∀ y ∈ B ¬ y R x

Proof

Step Hyp Ref Expression
1 bnj1189.1 ⊢ φ ↔ R FrSe A ∧ B ⊆ A ∧ B ≠ ∅
2 bnj1189.2 ⊢ ψ ↔ x ∈ B ∧ y ∈ B ∧ y R x
3 bnj1189.3 ⊢ χ ↔ ∀ y ∈ B ¬ y R x
4 n0 ⊢ B ≠ ∅ ↔ ∃ x x ∈ B
5 4 biimpi ⊢ B ≠ ∅ → ∃ x x ∈ B
6 1 5 bnj837 ⊢ φ → ∃ x x ∈ B
7 6 ancli ⊢ φ → φ ∧ ∃ x x ∈ B
8 19.42v ⊢ ∃ x φ ∧ x ∈ B ↔ φ ∧ ∃ x x ∈ B
9 7 8 sylibr ⊢ φ → ∃ x φ ∧ x ∈ B
10 3simpc ⊢ φ ∧ x ∈ B ∧ χ → x ∈ B ∧ χ
11 3 anbi2i ⊢ x ∈ B ∧ χ ↔ x ∈ B ∧ ∀ y ∈ B ¬ y R x
12 10 11 sylib ⊢ φ ∧ x ∈ B ∧ χ → x ∈ B ∧ ∀ y ∈ B ¬ y R x
13 12 19.8ad ⊢ φ ∧ x ∈ B ∧ χ → ∃ x x ∈ B ∧ ∀ y ∈ B ¬ y R x
14 df-rex ⊢ ∃ x ∈ B ∀ y ∈ B ¬ y R x ↔ ∃ x x ∈ B ∧ ∀ y ∈ B ¬ y R x
15 13 14 sylibr ⊢ φ ∧ x ∈ B ∧ χ → ∃ x ∈ B ∀ y ∈ B ¬ y R x
16 15 3comr ⊢ χ ∧ φ ∧ x ∈ B → ∃ x ∈ B ∀ y ∈ B ¬ y R x
17 16 3expib ⊢ χ → φ ∧ x ∈ B → ∃ x ∈ B ∀ y ∈ B ¬ y R x
18 simp1 ⊢ φ ∧ x ∈ B ∧ ¬ χ → φ
19 simp2 ⊢ φ ∧ x ∈ B ∧ ¬ χ → x ∈ B
20 rexnal ⊢ ∃ y ∈ B ¬ ¬ y R x ↔ ¬ ∀ y ∈ B ¬ y R x
21 20 bicomi ⊢ ¬ ∀ y ∈ B ¬ y R x ↔ ∃ y ∈ B ¬ ¬ y R x
22 21 3 xchnxbir ⊢ ¬ χ ↔ ∃ y ∈ B ¬ ¬ y R x
23 notnotb ⊢ y R x ↔ ¬ ¬ y R x
24 23 rexbii ⊢ ∃ y ∈ B y R x ↔ ∃ y ∈ B ¬ ¬ y R x
25 22 24 bitr4i ⊢ ¬ χ ↔ ∃ y ∈ B y R x
26 25 biimpi ⊢ ¬ χ → ∃ y ∈ B y R x
27 26 bnj1196 ⊢ ¬ χ → ∃ y y ∈ B ∧ y R x
28 27 3ad2ant3 ⊢ φ ∧ x ∈ B ∧ ¬ χ → ∃ y y ∈ B ∧ y R x
29 3anass ⊢ x ∈ B ∧ y ∈ B ∧ y R x ↔ x ∈ B ∧ y ∈ B ∧ y R x
30 29 exbii ⊢ ∃ y x ∈ B ∧ y ∈ B ∧ y R x ↔ ∃ y x ∈ B ∧ y ∈ B ∧ y R x
31 19.42v ⊢ ∃ y x ∈ B ∧ y ∈ B ∧ y R x ↔ x ∈ B ∧ ∃ y y ∈ B ∧ y R x
32 30 31 bitri ⊢ ∃ y x ∈ B ∧ y ∈ B ∧ y R x ↔ x ∈ B ∧ ∃ y y ∈ B ∧ y R x
33 19 28 32 sylanbrc ⊢ φ ∧ x ∈ B ∧ ¬ χ → ∃ y x ∈ B ∧ y ∈ B ∧ y R x
34 33 2 bnj1198 ⊢ φ ∧ x ∈ B ∧ ¬ χ → ∃ y ψ
35 19.42v ⊢ ∃ y φ ∧ ψ ↔ φ ∧ ∃ y ψ
36 18 34 35 sylanbrc ⊢ φ ∧ x ∈ B ∧ ¬ χ → ∃ y φ ∧ ψ
37 1 2 bnj1190 ⊢ φ ∧ ψ → ∃ w ∈ B ∀ z ∈ B ¬ z R w
38 36 37 bnj593 ⊢ φ ∧ x ∈ B ∧ ¬ χ → ∃ y ∃ w ∈ B ∀ z ∈ B ¬ z R w
39 38 bnj937 ⊢ φ ∧ x ∈ B ∧ ¬ χ → ∃ w ∈ B ∀ z ∈ B ¬ z R w
40 39 bnj1185 ⊢ φ ∧ x ∈ B ∧ ¬ χ → ∃ x ∈ B ∀ y ∈ B ¬ y R x
41 40 3comr ⊢ ¬ χ ∧ φ ∧ x ∈ B → ∃ x ∈ B ∀ y ∈ B ¬ y R x
42 41 3expib ⊢ ¬ χ → φ ∧ x ∈ B → ∃ x ∈ B ∀ y ∈ B ¬ y R x
43 17 42 pm2.61i ⊢ φ ∧ x ∈ B → ∃ x ∈ B ∀ y ∈ B ¬ y R x
44 9 43 bnj593 ⊢ φ → ∃ x ∃ x ∈ B ∀ y ∈ B ¬ y R x
45 nfre1 ⊢ Ⅎ x ∃ x ∈ B ∀ y ∈ B ¬ y R x
46 45 19.9 ⊢ ∃ x ∃ x ∈ B ∀ y ∈ B ¬ y R x ↔ ∃ x ∈ B ∀ y ∈ B ¬ y R x
47 44 46 sylib ⊢ φ → ∃ x ∈ B ∀ y ∈ B ¬ y R x