This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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