Metamath Proof Explorer

Theorem bnj1176

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 bnj1176.51 
|- ( ( ph /\ ps ) -> ( R Fr A /\ C C_ A /\ C =/= (/) /\ C e. _V ) )
bnj1176.52 
|- ( ( R Fr A /\ C C_ A /\ C =/= (/) /\ C e. _V ) -> E. z e. C A. w e. C -. w R z )
Assertion bnj1176 
|- E. z A. w ( ( ph /\ ps ) -> ( z e. C /\ ( th -> ( w R z -> -. w e. C ) ) ) )

Proof

Step Hyp Ref Expression
1 bnj1176.51 
 |-  ( ( ph /\ ps ) -> ( R Fr A /\ C C_ A /\ C =/= (/) /\ C e. _V ) )
2 bnj1176.52 
 |-  ( ( R Fr A /\ C C_ A /\ C =/= (/) /\ C e. _V ) -> E. z e. C A. w e. C -. w R z )
3 1 2 syl 
 |-  ( ( ph /\ ps ) -> E. z e. C A. w e. C -. w R z )
4 df-ral 
 |-  ( A. w e. C -. w R z <-> A. w ( w e. C -> -. w R z ) )
5 4 rexbii 
 |-  ( E. z e. C A. w e. C -. w R z <-> E. z e. C A. w ( w e. C -> -. w R z ) )
6 3 5 sylib 
 |-  ( ( ph /\ ps ) -> E. z e. C A. w ( w e. C -> -. w R z ) )
7 df-rex 
 |-  ( E. z e. C A. w ( w e. C -> -. w R z ) <-> E. z ( z e. C /\ A. w ( w e. C -> -. w R z ) ) )
8 6 7 sylib 
 |-  ( ( ph /\ ps ) -> E. z ( z e. C /\ A. w ( w e. C -> -. w R z ) ) )
9 19.28v 
 |-  ( A. w ( z e. C /\ ( w e. C -> -. w R z ) ) <-> ( z e. C /\ A. w ( w e. C -> -. w R z ) ) )
10 9 exbii 
 |-  ( E. z A. w ( z e. C /\ ( w e. C -> -. w R z ) ) <-> E. z ( z e. C /\ A. w ( w e. C -> -. w R z ) ) )
11 8 10 sylibr 
 |-  ( ( ph /\ ps ) -> E. z A. w ( z e. C /\ ( w e. C -> -. w R z ) ) )
12 19.37v 
 |-  ( E. z ( ( ph /\ ps ) -> A. w ( z e. C /\ ( w e. C -> -. w R z ) ) ) <-> ( ( ph /\ ps ) -> E. z A. w ( z e. C /\ ( w e. C -> -. w R z ) ) ) )
13 11 12 mpbir 
 |-  E. z ( ( ph /\ ps ) -> A. w ( z e. C /\ ( w e. C -> -. w R z ) ) )
14 19.21v 
 |-  ( A. w ( ( ph /\ ps ) -> ( z e. C /\ ( w e. C -> -. w R z ) ) ) <-> ( ( ph /\ ps ) -> A. w ( z e. C /\ ( w e. C -> -. w R z ) ) ) )
15 14 exbii 
 |-  ( E. z A. w ( ( ph /\ ps ) -> ( z e. C /\ ( w e. C -> -. w R z ) ) ) <-> E. z ( ( ph /\ ps ) -> A. w ( z e. C /\ ( w e. C -> -. w R z ) ) ) )
16 13 15 mpbir 
 |-  E. z A. w ( ( ph /\ ps ) -> ( z e. C /\ ( w e. C -> -. w R z ) ) )
17 con2b 
 |-  ( ( w e. C -> -. w R z ) <-> ( w R z -> -. w e. C ) )
18 17 anbi2i 
 |-  ( ( z e. C /\ ( w e. C -> -. w R z ) ) <-> ( z e. C /\ ( w R z -> -. w e. C ) ) )
19 18 imbi2i 
 |-  ( ( ( ph /\ ps ) -> ( z e. C /\ ( w e. C -> -. w R z ) ) ) <-> ( ( ph /\ ps ) -> ( z e. C /\ ( w R z -> -. w e. C ) ) ) )
20 19 albii 
 |-  ( A. w ( ( ph /\ ps ) -> ( z e. C /\ ( w e. C -> -. w R z ) ) ) <-> A. w ( ( ph /\ ps ) -> ( z e. C /\ ( w R z -> -. w e. C ) ) ) )
21 20 exbii 
 |-  ( E. z A. w ( ( ph /\ ps ) -> ( z e. C /\ ( w e. C -> -. w R z ) ) ) <-> E. z A. w ( ( ph /\ ps ) -> ( z e. C /\ ( w R z -> -. w e. C ) ) ) )
22 16 21 mpbi 
 |-  E. z A. w ( ( ph /\ ps ) -> ( z e. C /\ ( w R z -> -. w e. C ) ) )
23 ax-1 
 |-  ( ( w R z -> -. w e. C ) -> ( th -> ( w R z -> -. w e. C ) ) )
24 23 anim2i 
 |-  ( ( z e. C /\ ( w R z -> -. w e. C ) ) -> ( z e. C /\ ( th -> ( w R z -> -. w e. C ) ) ) )
25 24 imim2i 
 |-  ( ( ( ph /\ ps ) -> ( z e. C /\ ( w R z -> -. w e. C ) ) ) -> ( ( ph /\ ps ) -> ( z e. C /\ ( th -> ( w R z -> -. w e. C ) ) ) ) )
26 25 alimi 
 |-  ( A. w ( ( ph /\ ps ) -> ( z e. C /\ ( w R z -> -. w e. C ) ) ) -> A. w ( ( ph /\ ps ) -> ( z e. C /\ ( th -> ( w R z -> -. w e. C ) ) ) ) )
27 22 26 bnj101 
 |-  E. z A. w ( ( ph /\ ps ) -> ( z e. C /\ ( th -> ( w R z -> -. w e. C ) ) ) )