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