Theorem tz9.12lem2

Description: Lemma for tz9.12 . (Contributed by NM, 22-Sep-2003)

	Ref	Expression
Hypotheses	tz9.12lem.1	|- A e. _V
	tz9.12lem.2	|- F = ( z e. _V |-> |^| { v e. On | z e. ( R1 ` v ) } )
Assertion	tz9.12lem2	|- suc U. ( F " A ) e. On

Proof

Step	Hyp	Ref	Expression
1		tz9.12lem.1	|- A e. _V
2		tz9.12lem.2	|- F = ( z e. _V |-> |^| { v e. On | z e. ( R1 ` v ) } )
3	1 2	tz9.12lem1	|- ( F " A ) C_ On
4	2	funmpt2	|- Fun F
5	1	funimaex	|- ( Fun F -> ( F " A ) e. _V )
6	4 5	ax-mp	|- ( F " A ) e. _V
7	6	ssonunii	|- ( ( F " A ) C_ On -> U. ( F " A ) e. On )
8	3 7	ax-mp	|- U. ( F " A ) e. On
9	8	onsuci	|- suc U. ( F " A ) e. On