Description: A subset of a numerable set is numerable. (Contributed by Mario Carneiro, 28-Apr-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | ssnum | ⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ∈ dom card ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssdomg | ⊢ ( 𝐴 ∈ dom card → ( 𝐵 ⊆ 𝐴 → 𝐵 ≼ 𝐴 ) ) | |
2 | 1 | imp | ⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ≼ 𝐴 ) |
3 | numdom | ⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ≼ 𝐴 ) → 𝐵 ∈ dom card ) | |
4 | 2 3 | syldan | ⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ∈ dom card ) |