Theorem tz9.12lem1

Description: Lemma for tz9.12 . (Contributed by NM, 22-Sep-2003) (Revised by Mario Carneiro, 11-Sep-2015)

	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.12lem1	|- ( F " A ) C_ 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		imassrn	|- ( F " A ) C_ ran F
4	2	rnmpt	|- ran F = { x | E. z e. _V x = |^| { v e. On | z e. ( R1 ` v ) } }
5		id	|- ( x = |^| { v e. On | z e. ( R1 ` v ) } -> x = |^| { v e. On | z e. ( R1 ` v ) } )
6		ssrab2	|- { v e. On | z e. ( R1 ` v ) } C_ On
7		eqvisset	|- ( x = |^| { v e. On | z e. ( R1 ` v ) } -> |^| { v e. On | z e. ( R1 ` v ) } e. _V )
8		intex	|- ( { v e. On | z e. ( R1 ` v ) } =/= (/) <-> |^| { v e. On | z e. ( R1 ` v ) } e. _V )
9	7 8	sylibr	|- ( x = |^| { v e. On | z e. ( R1 ` v ) } -> { v e. On | z e. ( R1 ` v ) } =/= (/) )
10		oninton	|- ( ( { v e. On | z e. ( R1 ` v ) } C_ On /\ { v e. On | z e. ( R1 ` v ) } =/= (/) ) -> |^| { v e. On | z e. ( R1 ` v ) } e. On )
11	6 9 10	sylancr	|- ( x = |^| { v e. On | z e. ( R1 ` v ) } -> |^| { v e. On | z e. ( R1 ` v ) } e. On )
12	5 11	eqeltrd	|- ( x = |^| { v e. On | z e. ( R1 ` v ) } -> x e. On )
13	12	rexlimivw	|- ( E. z e. _V x = |^| { v e. On | z e. ( R1 ` v ) } -> x e. On )
14	13	abssi	|- { x | E. z e. _V x = |^| { v e. On | z e. ( R1 ` v ) } } C_ On
15	4 14	eqsstri	|- ran F C_ On
16	3 15	sstri	|- ( F " A ) C_ On