This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bnj1175

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 bnj1175.3 
|- C = ( _trCl ( X , A , R ) i^i B )
bnj1175.4 
|- ( ch <-> ( ( R _FrSe A /\ X e. A /\ z e. _trCl ( X , A , R ) ) /\ ( R _FrSe A /\ z e. A ) /\ ( w e. A /\ w R z ) ) )
bnj1175.5 
|- ( th <-> ( ( R _FrSe A /\ X e. A /\ z e. _trCl ( X , A , R ) ) /\ ( R _FrSe A /\ z e. A ) /\ w e. A ) )
Assertion bnj1175 
|- ( th -> ( w R z -> w e. _trCl ( X , A , R ) ) )

Proof

Step Hyp Ref Expression
1 bnj1175.3 
 |-  C = ( _trCl ( X , A , R ) i^i B )
2 bnj1175.4 
 |-  ( ch <-> ( ( R _FrSe A /\ X e. A /\ z e. _trCl ( X , A , R ) ) /\ ( R _FrSe A /\ z e. A ) /\ ( w e. A /\ w R z ) ) )
3 bnj1175.5 
 |-  ( th <-> ( ( R _FrSe A /\ X e. A /\ z e. _trCl ( X , A , R ) ) /\ ( R _FrSe A /\ z e. A ) /\ w e. A ) )
4 bnj255 
 |-  ( ( ( R _FrSe A /\ X e. A /\ z e. _trCl ( X , A , R ) ) /\ ( R _FrSe A /\ z e. A ) /\ w e. A /\ w R z ) <-> ( ( R _FrSe A /\ X e. A /\ z e. _trCl ( X , A , R ) ) /\ ( R _FrSe A /\ z e. A ) /\ ( w e. A /\ w R z ) ) )
5 df-bnj17 
 |-  ( ( ( R _FrSe A /\ X e. A /\ z e. _trCl ( X , A , R ) ) /\ ( R _FrSe A /\ z e. A ) /\ w e. A /\ w R z ) <-> ( ( ( R _FrSe A /\ X e. A /\ z e. _trCl ( X , A , R ) ) /\ ( R _FrSe A /\ z e. A ) /\ w e. A ) /\ w R z ) )
6 2 4 5 3bitr2i 
 |-  ( ch <-> ( ( ( R _FrSe A /\ X e. A /\ z e. _trCl ( X , A , R ) ) /\ ( R _FrSe A /\ z e. A ) /\ w e. A ) /\ w R z ) )
7 3 anbi1i 
 |-  ( ( th /\ w R z ) <-> ( ( ( R _FrSe A /\ X e. A /\ z e. _trCl ( X , A , R ) ) /\ ( R _FrSe A /\ z e. A ) /\ w e. A ) /\ w R z ) )
8 6 7 bitr4i 
 |-  ( ch <-> ( th /\ w R z ) )
9 bnj1125 
 |-  ( ( R _FrSe A /\ X e. A /\ z e. _trCl ( X , A , R ) ) -> _trCl ( z , A , R ) C_ _trCl ( X , A , R ) )
10 2 9 bnj835 
 |-  ( ch -> _trCl ( z , A , R ) C_ _trCl ( X , A , R ) )
11 bnj906 
 |-  ( ( R _FrSe A /\ z e. A ) -> _pred ( z , A , R ) C_ _trCl ( z , A , R ) )
12 2 11 bnj836 
 |-  ( ch -> _pred ( z , A , R ) C_ _trCl ( z , A , R ) )
13 bnj1152 
 |-  ( w e. _pred ( z , A , R ) <-> ( w e. A /\ w R z ) )
14 13 biimpri 
 |-  ( ( w e. A /\ w R z ) -> w e. _pred ( z , A , R ) )
15 2 14 bnj837 
 |-  ( ch -> w e. _pred ( z , A , R ) )
16 12 15 sseldd 
 |-  ( ch -> w e. _trCl ( z , A , R ) )
17 10 16 sseldd 
 |-  ( ch -> w e. _trCl ( X , A , R ) )
18 8 17 sylbir 
 |-  ( ( th /\ w R z ) -> w e. _trCl ( X , A , R ) )
19 18 ex 
 |-  ( th -> ( w R z -> w e. _trCl ( X , A , R ) ) )