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 ) i^i B )
bnj1174.59 
|- E. z A. w ( ( ph /\ ps ) -> ( z e. C /\ ( th -> ( w R z -> -. w e. C ) ) ) )
bnj1174.74 
|- ( th -> ( w R z -> w e. _trCl ( X , A , R ) ) )
Assertion bnj1174 
|- E. z A. w ( ( ph /\ ps ) -> ( ( ph /\ ps /\ z e. C ) /\ ( th -> ( w R z -> -. w e. B ) ) ) )

Proof

Step Hyp Ref Expression
1 bnj1174.3 
 |-  C = ( _trCl ( X , A , R ) i^i B )
2 bnj1174.59 
 |-  E. z A. w ( ( ph /\ ps ) -> ( z e. C /\ ( th -> ( w R z -> -. w e. C ) ) ) )
3 bnj1174.74 
 |-  ( th -> ( w R z -> w e. _trCl ( X , A , R ) ) )
4 1 eleq2i 
 |-  ( w e. C <-> w e. ( _trCl ( X , A , R ) i^i B ) )
5 4 notbii 
 |-  ( -. w e. C <-> -. w e. ( _trCl ( X , A , R ) i^i B ) )
6 ianor 
 |-  ( -. ( w e. _trCl ( X , A , R ) /\ w e. B ) <-> ( -. w e. _trCl ( X , A , R ) \/ -. w e. B ) )
7 elin 
 |-  ( w e. ( _trCl ( X , A , R ) i^i B ) <-> ( w e. _trCl ( X , A , R ) /\ w e. B ) )
8 7 notbii 
 |-  ( -. w e. ( _trCl ( X , A , R ) i^i B ) <-> -. ( w e. _trCl ( X , A , R ) /\ w e. B ) )
9 pm4.62 
 |-  ( ( w e. _trCl ( X , A , R ) -> -. w e. B ) <-> ( -. w e. _trCl ( X , A , R ) \/ -. w e. B ) )
10 6 8 9 3bitr4i 
 |-  ( -. w e. ( _trCl ( X , A , R ) i^i B ) <-> ( w e. _trCl ( X , A , R ) -> -. w e. B ) )
11 10 biimpi 
 |-  ( -. w e. ( _trCl ( X , A , R ) i^i B ) -> ( w e. _trCl ( X , A , R ) -> -. w e. B ) )
12 11 impcom 
 |-  ( ( w e. _trCl ( X , A , R ) /\ -. w e. ( _trCl ( X , A , R ) i^i B ) ) -> -. w e. B )
13 5 12 sylan2b 
 |-  ( ( w e. _trCl ( X , A , R ) /\ -. w e. C ) -> -. w e. B )
14 13 ex 
 |-  ( w e. _trCl ( X , A , R ) -> ( -. w e. C -> -. w e. B ) )
15 3 14 syl6 
 |-  ( th -> ( w R z -> ( -. w e. C -> -. w e. B ) ) )
16 15 a2d 
 |-  ( th -> ( ( w R z -> -. w e. C ) -> ( w R z -> -. w e. B ) ) )
17 16 biantru 
 |-  ( ( z e. C /\ ( th -> ( w R z -> -. w e. C ) ) ) <-> ( ( z e. C /\ ( th -> ( w R z -> -. w e. C ) ) ) /\ ( th -> ( ( w R z -> -. w e. C ) -> ( w R z -> -. w e. B ) ) ) ) )
18 df-3an 
 |-  ( ( z e. C /\ ( th -> ( w R z -> -. w e. C ) ) /\ ( th -> ( ( w R z -> -. w e. C ) -> ( w R z -> -. w e. B ) ) ) ) <-> ( ( z e. C /\ ( th -> ( w R z -> -. w e. C ) ) ) /\ ( th -> ( ( w R z -> -. w e. C ) -> ( w R z -> -. w e. B ) ) ) ) )
19 3anass 
 |-  ( ( z e. C /\ ( th -> ( w R z -> -. w e. C ) ) /\ ( th -> ( ( w R z -> -. w e. C ) -> ( w R z -> -. w e. B ) ) ) ) <-> ( z e. C /\ ( ( th -> ( w R z -> -. w e. C ) ) /\ ( th -> ( ( w R z -> -. w e. C ) -> ( w R z -> -. w e. B ) ) ) ) ) )
20 17 18 19 3bitr2i 
 |-  ( ( z e. C /\ ( th -> ( w R z -> -. w e. C ) ) ) <-> ( z e. C /\ ( ( th -> ( w R z -> -. w e. C ) ) /\ ( th -> ( ( w R z -> -. w e. C ) -> ( w R z -> -. w e. B ) ) ) ) ) )
21 20 imbi2i 
 |-  ( ( ( ph /\ ps ) -> ( z e. C /\ ( th -> ( w R z -> -. w e. C ) ) ) ) <-> ( ( ph /\ ps ) -> ( z e. C /\ ( ( th -> ( w R z -> -. w e. C ) ) /\ ( th -> ( ( w R z -> -. w e. C ) -> ( w R z -> -. w e. B ) ) ) ) ) ) )
22 21 albii 
 |-  ( A. w ( ( ph /\ ps ) -> ( z e. C /\ ( th -> ( w R z -> -. w e. C ) ) ) ) <-> A. w ( ( ph /\ ps ) -> ( z e. C /\ ( ( th -> ( w R z -> -. w e. C ) ) /\ ( th -> ( ( w R z -> -. w e. C ) -> ( w R z -> -. w e. B ) ) ) ) ) ) )
23 22 exbii 
 |-  ( E. z A. w ( ( ph /\ ps ) -> ( z e. C /\ ( th -> ( w R z -> -. w e. C ) ) ) ) <-> E. z A. w ( ( ph /\ ps ) -> ( z e. C /\ ( ( th -> ( w R z -> -. w e. C ) ) /\ ( th -> ( ( w R z -> -. w e. C ) -> ( w R z -> -. w e. B ) ) ) ) ) ) )
24 2 23 mpbi 
 |-  E. z A. w ( ( ph /\ ps ) -> ( z e. C /\ ( ( th -> ( w R z -> -. w e. C ) ) /\ ( th -> ( ( w R z -> -. w e. C ) -> ( w R z -> -. w e. B ) ) ) ) ) )
25 imdi 
 |-  ( ( th -> ( ( w R z -> -. w e. C ) -> ( w R z -> -. w e. B ) ) ) <-> ( ( th -> ( w R z -> -. w e. C ) ) -> ( th -> ( w R z -> -. w e. B ) ) ) )
26 pm3.35 
 |-  ( ( ( th -> ( w R z -> -. w e. C ) ) /\ ( ( th -> ( w R z -> -. w e. C ) ) -> ( th -> ( w R z -> -. w e. B ) ) ) ) -> ( th -> ( w R z -> -. w e. B ) ) )
27 25 26 sylan2b 
 |-  ( ( ( th -> ( w R z -> -. w e. C ) ) /\ ( th -> ( ( w R z -> -. w e. C ) -> ( w R z -> -. w e. B ) ) ) ) -> ( th -> ( w R z -> -. w e. B ) ) )
28 27 anim2i 
 |-  ( ( z e. C /\ ( ( th -> ( w R z -> -. w e. C ) ) /\ ( th -> ( ( w R z -> -. w e. C ) -> ( w R z -> -. w e. B ) ) ) ) ) -> ( z e. C /\ ( th -> ( w R z -> -. w e. B ) ) ) )
29 28 imim2i 
 |-  ( ( ( ph /\ ps ) -> ( z e. C /\ ( ( th -> ( w R z -> -. w e. C ) ) /\ ( th -> ( ( w R z -> -. w e. C ) -> ( w R z -> -. w e. B ) ) ) ) ) ) -> ( ( ph /\ ps ) -> ( z e. C /\ ( th -> ( w R z -> -. w e. B ) ) ) ) )
30 29 alimi 
 |-  ( A. w ( ( ph /\ ps ) -> ( z e. C /\ ( ( th -> ( w R z -> -. w e. C ) ) /\ ( th -> ( ( w R z -> -. w e. C ) -> ( w R z -> -. w e. B ) ) ) ) ) ) -> A. w ( ( ph /\ ps ) -> ( z e. C /\ ( th -> ( w R z -> -. w e. B ) ) ) ) )
31 24 30 bnj101 
 |-  E. z A. w ( ( ph /\ ps ) -> ( z e. C /\ ( th -> ( w R z -> -. w e. B ) ) ) )
32 ancl 
 |-  ( ( ( ph /\ ps ) -> ( z e. C /\ ( th -> ( w R z -> -. w e. B ) ) ) ) -> ( ( ph /\ ps ) -> ( ( ph /\ ps ) /\ ( z e. C /\ ( th -> ( w R z -> -. w e. B ) ) ) ) ) )
33 bnj256 
 |-  ( ( ph /\ ps /\ z e. C /\ ( th -> ( w R z -> -. w e. B ) ) ) <-> ( ( ph /\ ps ) /\ ( z e. C /\ ( th -> ( w R z -> -. w e. B ) ) ) ) )
34 32 33 imbitrrdi 
 |-  ( ( ( ph /\ ps ) -> ( z e. C /\ ( th -> ( w R z -> -. w e. B ) ) ) ) -> ( ( ph /\ ps ) -> ( ph /\ ps /\ z e. C /\ ( th -> ( w R z -> -. w e. B ) ) ) ) )
35 34 alimi 
 |-  ( A. w ( ( ph /\ ps ) -> ( z e. C /\ ( th -> ( w R z -> -. w e. B ) ) ) ) -> A. w ( ( ph /\ ps ) -> ( ph /\ ps /\ z e. C /\ ( th -> ( w R z -> -. w e. B ) ) ) ) )
36 31 35 bnj101 
 |-  E. z A. w ( ( ph /\ ps ) -> ( ph /\ ps /\ z e. C /\ ( th -> ( w R z -> -. w e. B ) ) ) )
37 df-bnj17 
 |-  ( ( ph /\ ps /\ z e. C /\ ( th -> ( w R z -> -. w e. B ) ) ) <-> ( ( ph /\ ps /\ z e. C ) /\ ( th -> ( w R z -> -. w e. B ) ) ) )
38 37 imbi2i 
 |-  ( ( ( ph /\ ps ) -> ( ph /\ ps /\ z e. C /\ ( th -> ( w R z -> -. w e. B ) ) ) ) <-> ( ( ph /\ ps ) -> ( ( ph /\ ps /\ z e. C ) /\ ( th -> ( w R z -> -. w e. B ) ) ) ) )
39 38 albii 
 |-  ( A. w ( ( ph /\ ps ) -> ( ph /\ ps /\ z e. C /\ ( th -> ( w R z -> -. w e. B ) ) ) ) <-> A. w ( ( ph /\ ps ) -> ( ( ph /\ ps /\ z e. C ) /\ ( th -> ( w R z -> -. w e. B ) ) ) ) )
40 39 exbii 
 |-  ( E. z A. w ( ( ph /\ ps ) -> ( ph /\ ps /\ z e. C /\ ( th -> ( w R z -> -. w e. B ) ) ) ) <-> E. z A. w ( ( ph /\ ps ) -> ( ( ph /\ ps /\ z e. C ) /\ ( th -> ( w R z -> -. w e. B ) ) ) ) )
41 36 40 mpbi 
 |-  E. z A. w ( ( ph /\ ps ) -> ( ( ph /\ ps /\ z e. C ) /\ ( th -> ( w R z -> -. w e. B ) ) ) )