# 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 )