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 
|- ( ph <-> ( R _FrSe A /\ B C_ A /\ B =/= (/) ) )
bnj1189.2 
|- ( ps <-> ( x e. B /\ y e. B /\ y R x ) )
bnj1189.3 
|- ( ch <-> A. y e. B -. y R x )
Assertion bnj1189 
|- ( ph -> E. x e. B A. y e. B -. y R x )

Proof

Step Hyp Ref Expression
1 bnj1189.1 
 |-  ( ph <-> ( R _FrSe A /\ B C_ A /\ B =/= (/) ) )
2 bnj1189.2 
 |-  ( ps <-> ( x e. B /\ y e. B /\ y R x ) )
3 bnj1189.3 
 |-  ( ch <-> A. y e. B -. y R x )
4 n0 
 |-  ( B =/= (/) <-> E. x x e. B )
5 4 biimpi 
 |-  ( B =/= (/) -> E. x x e. B )
6 1 5 bnj837 
 |-  ( ph -> E. x x e. B )
7 6 ancli 
 |-  ( ph -> ( ph /\ E. x x e. B ) )
8 19.42v 
 |-  ( E. x ( ph /\ x e. B ) <-> ( ph /\ E. x x e. B ) )
9 7 8 sylibr 
 |-  ( ph -> E. x ( ph /\ x e. B ) )
10 3simpc 
 |-  ( ( ph /\ x e. B /\ ch ) -> ( x e. B /\ ch ) )
11 3 anbi2i 
 |-  ( ( x e. B /\ ch ) <-> ( x e. B /\ A. y e. B -. y R x ) )
12 10 11 sylib 
 |-  ( ( ph /\ x e. B /\ ch ) -> ( x e. B /\ A. y e. B -. y R x ) )
13 12 19.8ad 
 |-  ( ( ph /\ x e. B /\ ch ) -> E. x ( x e. B /\ A. y e. B -. y R x ) )
14 df-rex 
 |-  ( E. x e. B A. y e. B -. y R x <-> E. x ( x e. B /\ A. y e. B -. y R x ) )
15 13 14 sylibr 
 |-  ( ( ph /\ x e. B /\ ch ) -> E. x e. B A. y e. B -. y R x )
16 15 3comr 
 |-  ( ( ch /\ ph /\ x e. B ) -> E. x e. B A. y e. B -. y R x )
17 16 3expib 
 |-  ( ch -> ( ( ph /\ x e. B ) -> E. x e. B A. y e. B -. y R x ) )
18 simp1 
 |-  ( ( ph /\ x e. B /\ -. ch ) -> ph )
19 simp2 
 |-  ( ( ph /\ x e. B /\ -. ch ) -> x e. B )
20 rexnal 
 |-  ( E. y e. B -. -. y R x <-> -. A. y e. B -. y R x )
21 20 bicomi 
 |-  ( -. A. y e. B -. y R x <-> E. y e. B -. -. y R x )
22 21 3 xchnxbir 
 |-  ( -. ch <-> E. y e. B -. -. y R x )
23 notnotb 
 |-  ( y R x <-> -. -. y R x )
24 23 rexbii 
 |-  ( E. y e. B y R x <-> E. y e. B -. -. y R x )
25 22 24 bitr4i 
 |-  ( -. ch <-> E. y e. B y R x )
26 25 biimpi 
 |-  ( -. ch -> E. y e. B y R x )
27 26 bnj1196 
 |-  ( -. ch -> E. y ( y e. B /\ y R x ) )
28 27 3ad2ant3 
 |-  ( ( ph /\ x e. B /\ -. ch ) -> E. y ( y e. B /\ y R x ) )
29 3anass 
 |-  ( ( x e. B /\ y e. B /\ y R x ) <-> ( x e. B /\ ( y e. B /\ y R x ) ) )
30 29 exbii 
 |-  ( E. y ( x e. B /\ y e. B /\ y R x ) <-> E. y ( x e. B /\ ( y e. B /\ y R x ) ) )
31 19.42v 
 |-  ( E. y ( x e. B /\ ( y e. B /\ y R x ) ) <-> ( x e. B /\ E. y ( y e. B /\ y R x ) ) )
32 30 31 bitri 
 |-  ( E. y ( x e. B /\ y e. B /\ y R x ) <-> ( x e. B /\ E. y ( y e. B /\ y R x ) ) )
33 19 28 32 sylanbrc 
 |-  ( ( ph /\ x e. B /\ -. ch ) -> E. y ( x e. B /\ y e. B /\ y R x ) )
34 33 2 bnj1198 
 |-  ( ( ph /\ x e. B /\ -. ch ) -> E. y ps )
35 19.42v 
 |-  ( E. y ( ph /\ ps ) <-> ( ph /\ E. y ps ) )
36 18 34 35 sylanbrc 
 |-  ( ( ph /\ x e. B /\ -. ch ) -> E. y ( ph /\ ps ) )
37 1 2 bnj1190 
 |-  ( ( ph /\ ps ) -> E. w e. B A. z e. B -. z R w )
38 36 37 bnj593 
 |-  ( ( ph /\ x e. B /\ -. ch ) -> E. y E. w e. B A. z e. B -. z R w )
39 38 bnj937 
 |-  ( ( ph /\ x e. B /\ -. ch ) -> E. w e. B A. z e. B -. z R w )
40 39 bnj1185 
 |-  ( ( ph /\ x e. B /\ -. ch ) -> E. x e. B A. y e. B -. y R x )
41 40 3comr 
 |-  ( ( -. ch /\ ph /\ x e. B ) -> E. x e. B A. y e. B -. y R x )
42 41 3expib 
 |-  ( -. ch -> ( ( ph /\ x e. B ) -> E. x e. B A. y e. B -. y R x ) )
43 17 42 pm2.61i 
 |-  ( ( ph /\ x e. B ) -> E. x e. B A. y e. B -. y R x )
44 9 43 bnj593 
 |-  ( ph -> E. x E. x e. B A. y e. B -. y R x )
45 nfre1 
 |-  F/ x E. x e. B A. y e. B -. y R x
46 45 19.9 
 |-  ( E. x E. x e. B A. y e. B -. y R x <-> E. x e. B A. y e. B -. y R x )
47 44 46 sylib 
 |-  ( ph -> E. x e. B A. y e. B -. y R x )