# 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 ∈ V ⟼ G ⁡ A ∖ ran ⁡ z$
dnnumch.a $⊢ φ → A ∈ V$
dnnumch.g $⊢ φ → ∀ y ∈ 𝒫 A y ≠ ∅ → G ⁡ y ∈ y$
Assertion dnnumch2 $⊢ φ → A ⊆ ran ⁡ F$

### Proof

Step Hyp Ref Expression
1 dnnumch.f $⊢ F = recs ⁡ z ∈ V ⟼ G ⁡ A ∖ ran ⁡ z$
2 dnnumch.a $⊢ φ → A ∈ V$
3 dnnumch.g $⊢ φ → ∀ y ∈ 𝒫 A y ≠ ∅ → G ⁡ y ∈ y$
4 1 2 3 dnnumch1 $⊢ φ → ∃ x ∈ 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 ⊆ F$
9 rnss $⊢ F ↾ x ⊆ F → ran ⁡ F ↾ x ⊆ ran ⁡ F$
10 8 9 mp1i $⊢ F ↾ x : x ⟶ 1-1 onto A → ran ⁡ F ↾ x ⊆ ran ⁡ F$
11 7 10 eqsstrrd $⊢ F ↾ x : x ⟶ 1-1 onto A → A ⊆ ran ⁡ F$
12 11 a1i $⊢ φ → F ↾ x : x ⟶ 1-1 onto A → A ⊆ ran ⁡ F$
13 12 rexlimdvw $⊢ φ → ∃ x ∈ On F ↾ x : x ⟶ 1-1 onto A → A ⊆ ran ⁡ F$
14 4 13 mpd $⊢ φ → A ⊆ ran ⁡ F$