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 ( 𝐴𝐵 → ( ∃ 𝑦 ∈ 𝒫 𝐴 ( 𝑦 ≠ ∅ → ( 𝑦 ) ∈ 𝑦 ) → 𝐴 ∈ dom card ) )

Proof

Step Hyp Ref Expression
1 eqid recs ( ( 𝑣 ∈ V ↦ ( ‘ ( 𝐴 ∖ ran 𝑣 ) ) ) ) = recs ( ( 𝑣 ∈ V ↦ ( ‘ ( 𝐴 ∖ ran 𝑣 ) ) ) )
2 rneq ( 𝑣 = 𝑓 → ran 𝑣 = ran 𝑓 )
3 2 difeq2d ( 𝑣 = 𝑓 → ( 𝐴 ∖ ran 𝑣 ) = ( 𝐴 ∖ ran 𝑓 ) )
4 3 fveq2d ( 𝑣 = 𝑓 → ( ‘ ( 𝐴 ∖ ran 𝑣 ) ) = ( ‘ ( 𝐴 ∖ ran 𝑓 ) ) )
5 4 cbvmptv ( 𝑣 ∈ V ↦ ( ‘ ( 𝐴 ∖ ran 𝑣 ) ) ) = ( 𝑓 ∈ V ↦ ( ‘ ( 𝐴 ∖ ran 𝑓 ) ) )
6 1 5 dfac8alem ( 𝐴𝐵 → ( ∃ 𝑦 ∈ 𝒫 𝐴 ( 𝑦 ≠ ∅ → ( 𝑦 ) ∈ 𝑦 ) → 𝐴 ∈ dom card ) )