This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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