Metamath Proof Explorer

Theorem bnj1173

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 bnj1173.3 
|- C = ( _trCl ( X , A , R ) i^i B )
bnj1173.5 
|- ( th <-> ( ( R _FrSe A /\ X e. A /\ z e. _trCl ( X , A , R ) ) /\ ( R _FrSe A /\ z e. A ) /\ w e. A ) )
bnj1173.9 
|- ( ( ph /\ ps ) -> R _FrSe A )
bnj1173.17 
|- ( ( ph /\ ps ) -> X e. A )
Assertion bnj1173 
|- ( ( ph /\ ps /\ z e. C ) -> ( th <-> w e. A ) )

Proof

Step Hyp Ref Expression
1 bnj1173.3 
 |-  C = ( _trCl ( X , A , R ) i^i B )
2 bnj1173.5 
 |-  ( th <-> ( ( R _FrSe A /\ X e. A /\ z e. _trCl ( X , A , R ) ) /\ ( R _FrSe A /\ z e. A ) /\ w e. A ) )
3 bnj1173.9 
 |-  ( ( ph /\ ps ) -> R _FrSe A )
4 bnj1173.17 
 |-  ( ( ph /\ ps ) -> X e. A )
5 3simpc 
 |-  ( ( ( R _FrSe A /\ X e. A /\ z e. _trCl ( X , A , R ) ) /\ ( R _FrSe A /\ z e. A ) /\ w e. A ) -> ( ( R _FrSe A /\ z e. A ) /\ w e. A ) )
6 3 3adant3 
 |-  ( ( ph /\ ps /\ z e. C ) -> R _FrSe A )
7 4 3adant3 
 |-  ( ( ph /\ ps /\ z e. C ) -> X e. A )
8 elin 
 |-  ( z e. ( _trCl ( X , A , R ) i^i B ) <-> ( z e. _trCl ( X , A , R ) /\ z e. B ) )
9 8 simplbi 
 |-  ( z e. ( _trCl ( X , A , R ) i^i B ) -> z e. _trCl ( X , A , R ) )
10 9 1 eleq2s 
 |-  ( z e. C -> z e. _trCl ( X , A , R ) )
11 10 3ad2ant3 
 |-  ( ( ph /\ ps /\ z e. C ) -> z e. _trCl ( X , A , R ) )
12 pm3.21 
 |-  ( ( R _FrSe A /\ X e. A /\ z e. _trCl ( X , A , R ) ) -> ( ( ( R _FrSe A /\ z e. A ) /\ w e. A ) -> ( ( ( R _FrSe A /\ z e. A ) /\ w e. A ) /\ ( R _FrSe A /\ X e. A /\ z e. _trCl ( X , A , R ) ) ) ) )
13 6 7 11 12 syl3anc 
 |-  ( ( ph /\ ps /\ z e. C ) -> ( ( ( R _FrSe A /\ z e. A ) /\ w e. A ) -> ( ( ( R _FrSe A /\ z e. A ) /\ w e. A ) /\ ( R _FrSe A /\ X e. A /\ z e. _trCl ( X , A , R ) ) ) ) )
14 bnj170 
 |-  ( ( ( R _FrSe A /\ X e. A /\ z e. _trCl ( X , A , R ) ) /\ ( R _FrSe A /\ z e. A ) /\ w e. A ) <-> ( ( ( R _FrSe A /\ z e. A ) /\ w e. A ) /\ ( R _FrSe A /\ X e. A /\ z e. _trCl ( X , A , R ) ) ) )
15 13 14 syl6ibr 
 |-  ( ( ph /\ ps /\ z e. C ) -> ( ( ( R _FrSe A /\ z e. A ) /\ w e. A ) -> ( ( R _FrSe A /\ X e. A /\ z e. _trCl ( X , A , R ) ) /\ ( R _FrSe A /\ z e. A ) /\ w e. A ) ) )
16 5 15 impbid2 
 |-  ( ( ph /\ ps /\ z e. C ) -> ( ( ( R _FrSe A /\ X e. A /\ z e. _trCl ( X , A , R ) ) /\ ( R _FrSe A /\ z e. A ) /\ w e. A ) <-> ( ( R _FrSe A /\ z e. A ) /\ w e. A ) ) )
17 2 16 syl5bb 
 |-  ( ( ph /\ ps /\ z e. C ) -> ( th <-> ( ( R _FrSe A /\ z e. A ) /\ w e. A ) ) )
18 bnj1147 
 |-  _trCl ( X , A , R ) C_ A
19 18 11 bnj1213 
 |-  ( ( ph /\ ps /\ z e. C ) -> z e. A )
20 6 19 jca 
 |-  ( ( ph /\ ps /\ z e. C ) -> ( R _FrSe A /\ z e. A ) )
21 20 biantrurd 
 |-  ( ( ph /\ ps /\ z e. C ) -> ( w e. A <-> ( ( R _FrSe A /\ z e. A ) /\ w e. A ) ) )
22 17 21 bitr4d 
 |-  ( ( ph /\ ps /\ z e. C ) -> ( th <-> w e. A ) )