Theorem bnj98

Description: Technical lemma for bnj150 . 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
Assertion	bnj98	|- A. i e. _om ( suc i e. 1o -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) )

Proof

Step	Hyp	Ref	Expression
1		vex	|- i e. _V
2	1	sucid	|- i e. suc i
3	2	n0ii	|- -. suc i = (/)
4		df-suc	|- suc i = ( i u. { i } )
5		df-un	|- ( i u. { i } ) = { x | ( x e. i \/ x e. { i } ) }
6	4 5	eqtri	|- suc i = { x | ( x e. i \/ x e. { i } ) }
7		df1o2	|- 1o = { (/) }
8	6 7	eleq12i	|- ( suc i e. 1o <-> { x | ( x e. i \/ x e. { i } ) } e. { (/) } )
9		elsni	|- ( { x | ( x e. i \/ x e. { i } ) } e. { (/) } -> { x | ( x e. i \/ x e. { i } ) } = (/) )
10	8 9	sylbi	|- ( suc i e. 1o -> { x | ( x e. i \/ x e. { i } ) } = (/) )
11	6 10	syl5eq	|- ( suc i e. 1o -> suc i = (/) )
12	3 11	mto	|- -. suc i e. 1o
13	12	pm2.21i	|- ( suc i e. 1o -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) )
14	13	rgenw	|- A. i e. _om ( suc i e. 1o -> ( F ` suc i ) = U_ y e. ( F ` i ) _pred ( y , A , R ) )