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