bnj1020

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	bnj1020.1	\|- ( ph <-> ( f ` (/) ) = _pred ( X , A , R ) )
	bnj1020.2	\|- ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
	bnj1020.3	\|- ( ch <-> ( n e. D /\ f Fn n /\ ph /\ ps ) )
	bnj1020.4	\|- ( th <-> ( R _FrSe A /\ X e. A /\ y e. _trCl ( X , A , R ) /\ z e. _pred ( y , A , R ) ) )
	bnj1020.5	\|- ( ta <-> ( m e. _om /\ n = suc m /\ p = suc n ) )
	bnj1020.6	\|- ( et <-> ( i e. n /\ y e. ( f ` i ) ) )
	bnj1020.7	\|- ( ph' <-> [. p / n ]. ph )
	bnj1020.8	\|- ( ps' <-> [. p / n ]. ps )
	bnj1020.9	\|- ( ch' <-> [. p / n ]. ch )
	bnj1020.10	\|- ( ph" <-> [. G / f ]. ph' )
	bnj1020.11	\|- ( ps" <-> [. G / f ]. ps' )
	bnj1020.12	\|- ( ch" <-> [. G / f ]. ch' )
	bnj1020.13	\|- D = ( _om \ { (/) } )
	bnj1020.14	\|- B = { f \| E. n e. D ( f Fn n /\ ph /\ ps ) }
	bnj1020.15	\|- C = U_ y e. ( f ` m ) _pred ( y , A , R )
	bnj1020.16	\|- G = ( f u. { <. n , C >. } )
	bnj1020.26	\|- ( ch" <-> ( p e. D /\ G Fn p /\ ph" /\ ps" ) )
Assertion	bnj1020	\|- ( ( th /\ ch /\ et /\ E. p ta ) -> _pred ( y , A , R ) C_ _trCl ( X , A , R ) )

Proof

Step	Hyp	Ref	Expression
1		bnj1020.1	\|- ( ph <-> ( f ` (/) ) = _pred ( X , A , R ) )
2		bnj1020.2	\|- ( ps <-> A. i e. _om ( suc i e. n -> ( f ` suc i ) = U_ y e. ( f ` i ) _pred ( y , A , R ) ) )
3		bnj1020.3	\|- ( ch <-> ( n e. D /\ f Fn n /\ ph /\ ps ) )
4		bnj1020.4	\|- ( th <-> ( R _FrSe A /\ X e. A /\ y e. _trCl ( X , A , R ) /\ z e. _pred ( y , A , R ) ) )
5		bnj1020.5	\|- ( ta <-> ( m e. _om /\ n = suc m /\ p = suc n ) )
6		bnj1020.6	\|- ( et <-> ( i e. n /\ y e. ( f ` i ) ) )
7		bnj1020.7	\|- ( ph' <-> [. p / n ]. ph )
8		bnj1020.8	\|- ( ps' <-> [. p / n ]. ps )
9		bnj1020.9	\|- ( ch' <-> [. p / n ]. ch )
10		bnj1020.10	\|- ( ph" <-> [. G / f ]. ph' )
11		bnj1020.11	\|- ( ps" <-> [. G / f ]. ps' )
12		bnj1020.12	\|- ( ch" <-> [. G / f ]. ch' )
13		bnj1020.13	\|- D = ( _om \ { (/) } )
14		bnj1020.14	\|- B = { f \| E. n e. D ( f Fn n /\ ph /\ ps ) }
15		bnj1020.15	\|- C = U_ y e. ( f ` m ) _pred ( y , A , R )
16		bnj1020.16	\|- G = ( f u. { <. n , C >. } )
17		bnj1020.26	\|- ( ch" <-> ( p e. D /\ G Fn p /\ ph" /\ ps" ) )
18		bnj1019	\|- ( E. p ( th /\ ch /\ ta /\ et ) <-> ( th /\ ch /\ et /\ E. p ta ) )
19	1 2 3 4 5 7 8 9 10 11 12 13 14 15 16	bnj998	\|- ( ( th /\ ch /\ ta /\ et ) -> ch" )
20	3 5 6 13 19	bnj1001	\|- ( ( th /\ ch /\ ta /\ et ) -> ( ch" /\ i e. _om /\ suc i e. p ) )
21	1 2 3 4 5 6 7 8 9 10 11 12 13 15 16 20	bnj1006	\|- ( ( th /\ ch /\ ta /\ et ) -> _pred ( y , A , R ) C_ ( G ` suc i ) )
22	21	exlimiv	\|- ( E. p ( th /\ ch /\ ta /\ et ) -> _pred ( y , A , R ) C_ ( G ` suc i ) )
23	18 22	sylbir	\|- ( ( th /\ ch /\ et /\ E. p ta ) -> _pred ( y , A , R ) C_ ( G ` suc i ) )
24	1 2 3 4 5 7 8 9 10 11 12 13 14 15 16 17 19 20	bnj1018	\|- ( ( th /\ ch /\ et /\ E. p ta ) -> ( G ` suc i ) C_ _trCl ( X , A , R ) )
25	23 24	sstrd	\|- ( ( th /\ ch /\ et /\ E. p ta ) -> _pred ( y , A , R ) C_ _trCl ( X , A , R ) )

Metamath Proof Explorer

Theorem bnj1020

Proof