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

Proof

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