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 )