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

Metamath Proof Explorer

Theorem dfac8a

Description: Numeration theorem: every set with a choice function on its power set is numerable. With AC, this reduces to the statement that every set is numerable. Similar to Theorem 10.3 of TakeutiZaring p. 84. (Contributed by NM, 10-Feb-1997) (Revised by Mario Carneiro, 5-Jan-2013)

Ref Expression
Assertion dfac8a ⊢ A ∈ B → ∃ h ∀ y ∈ 𝒫 A y ≠ ∅ → h ⁡ y ∈ y → A ∈ dom ⁡ card

Proof

Step Hyp Ref Expression
1 eqid ⊢ recs ⁡ v ∈ V ⟼ h ⁡ A ∖ ran ⁡ v = recs ⁡ v ∈ V ⟼ h ⁡ A ∖ ran ⁡ v
2 rneq ⊢ v = f → ran ⁡ v = ran ⁡ f
3 2 difeq2d ⊢ v = f → A ∖ ran ⁡ v = A ∖ ran ⁡ f
4 3 fveq2d ⊢ v = f → h ⁡ A ∖ ran ⁡ v = h ⁡ A ∖ ran ⁡ f
5 4 cbvmptv ⊢ v ∈ V ⟼ h ⁡ A ∖ ran ⁡ v = f ∈ V ⟼ h ⁡ A ∖ ran ⁡ f
6 1 5 dfac8alem ⊢ A ∈ B → ∃ h ∀ y ∈ 𝒫 A y ≠ ∅ → h ⁡ y ∈ y → A ∈ dom ⁡ card