# 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 𝐹 = recs ( ( 𝑧 ∈ V ↦ ( 𝐺 ‘ ( 𝐴 ∖ ran 𝑧 ) ) ) )
dnnumch.a ( 𝜑𝐴𝑉 )
dnnumch.g ( 𝜑 → ∀ 𝑦 ∈ 𝒫 𝐴 ( 𝑦 ≠ ∅ → ( 𝐺𝑦 ) ∈ 𝑦 ) )
Assertion dnnumch2 ( 𝜑𝐴 ⊆ ran 𝐹 )

### Proof

Step Hyp Ref Expression
1 dnnumch.f 𝐹 = recs ( ( 𝑧 ∈ V ↦ ( 𝐺 ‘ ( 𝐴 ∖ ran 𝑧 ) ) ) )
2 dnnumch.a ( 𝜑𝐴𝑉 )
3 dnnumch.g ( 𝜑 → ∀ 𝑦 ∈ 𝒫 𝐴 ( 𝑦 ≠ ∅ → ( 𝐺𝑦 ) ∈ 𝑦 ) )
4 1 2 3 dnnumch1 ( 𝜑 → ∃ 𝑥 ∈ On ( 𝐹𝑥 ) : 𝑥1-1-onto𝐴 )
5 f1ofo ( ( 𝐹𝑥 ) : 𝑥1-1-onto𝐴 → ( 𝐹𝑥 ) : 𝑥onto𝐴 )
6 forn ( ( 𝐹𝑥 ) : 𝑥onto𝐴 → ran ( 𝐹𝑥 ) = 𝐴 )
7 5 6 syl ( ( 𝐹𝑥 ) : 𝑥1-1-onto𝐴 → ran ( 𝐹𝑥 ) = 𝐴 )
8 resss ( 𝐹𝑥 ) ⊆ 𝐹
9 rnss ( ( 𝐹𝑥 ) ⊆ 𝐹 → ran ( 𝐹𝑥 ) ⊆ ran 𝐹 )
10 8 9 mp1i ( ( 𝐹𝑥 ) : 𝑥1-1-onto𝐴 → ran ( 𝐹𝑥 ) ⊆ ran 𝐹 )
11 7 10 eqsstrrd ( ( 𝐹𝑥 ) : 𝑥1-1-onto𝐴𝐴 ⊆ ran 𝐹 )
12 11 a1i ( 𝜑 → ( ( 𝐹𝑥 ) : 𝑥1-1-onto𝐴𝐴 ⊆ ran 𝐹 ) )
13 12 rexlimdvw ( 𝜑 → ( ∃ 𝑥 ∈ On ( 𝐹𝑥 ) : 𝑥1-1-onto𝐴𝐴 ⊆ ran 𝐹 ) )
14 4 13 mpd ( 𝜑𝐴 ⊆ ran 𝐹 )