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 ) ) )