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

Metamath Proof Explorer

Theorem dnnumch2

Description: Define an enumeration (weak dominance version) of a set from a choice function. (Contributed by Stefan O'Rear, 18-Jan-2015)

Ref Expression
Hypotheses dnnumch.f 
|- F = recs ( ( z e. _V |-> ( G ` ( A \ ran z ) ) ) )
dnnumch.a 
|- ( ph -> A e. V )
dnnumch.g 
|- ( ph -> A. y e. ~P A ( y =/= (/) -> ( G ` y ) e. y ) )
Assertion dnnumch2 
|- ( ph -> A C_ ran F )

Proof

Step Hyp Ref Expression
1 dnnumch.f 
 |-  F = recs ( ( z e. _V |-> ( G ` ( A \ ran z ) ) ) )
2 dnnumch.a 
 |-  ( ph -> A e. V )
3 dnnumch.g 
 |-  ( ph -> A. y e. ~P A ( y =/= (/) -> ( G ` y ) e. y ) )
4 1 2 3 dnnumch1 
 |-  ( ph -> E. x e. On ( F |` x ) : x -1-1-onto-> A )
5 f1ofo 
 |-  ( ( F |` x ) : x -1-1-onto-> A -> ( F |` x ) : x -onto-> A )
6 forn 
 |-  ( ( F |` x ) : x -onto-> A -> ran ( F |` x ) = A )
7 5 6 syl 
 |-  ( ( F |` x ) : x -1-1-onto-> A -> ran ( F |` x ) = A )
8 resss 
 |-  ( F |` x ) C_ F
9 rnss 
 |-  ( ( F |` x ) C_ F -> ran ( F |` x ) C_ ran F )
10 8 9 mp1i 
 |-  ( ( F |` x ) : x -1-1-onto-> A -> ran ( F |` x ) C_ ran F )
11 7 10 eqsstrrd 
 |-  ( ( F |` x ) : x -1-1-onto-> A -> A C_ ran F )
12 11 a1i 
 |-  ( ph -> ( ( F |` x ) : x -1-1-onto-> A -> A C_ ran F ) )
13 12 rexlimdvw 
 |-  ( ph -> ( E. x e. On ( F |` x ) : x -1-1-onto-> A -> A C_ ran F ) )
14 4 13 mpd 
 |-  ( ph -> A C_ ran F )