Theorem numdom

Description: A set dominated by a numerable set is numerable. (Contributed by Mario Carneiro, 28-Apr-2015)

	Ref	Expression
Assertion	numdom	⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ≼ 𝐴 ) → 𝐵 ∈ dom card )

Proof

Step	Hyp	Ref	Expression
1		cardon	⊢ ( card ‘ 𝐴 ) ∈ On
2		cardid2	⊢ ( 𝐴 ∈ dom card → ( card ‘ 𝐴 ) ≈ 𝐴 )
3		domen2	⊢ ( ( card ‘ 𝐴 ) ≈ 𝐴 → ( 𝐵 ≼ ( card ‘ 𝐴 ) ↔ 𝐵 ≼ 𝐴 ) )
4	2 3	syl	⊢ ( 𝐴 ∈ dom card → ( 𝐵 ≼ ( card ‘ 𝐴 ) ↔ 𝐵 ≼ 𝐴 ) )
5	4	biimpar	⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ≼ 𝐴 ) → 𝐵 ≼ ( card ‘ 𝐴 ) )
6		ondomen	⊢ ( ( ( card ‘ 𝐴 ) ∈ On ∧ 𝐵 ≼ ( card ‘ 𝐴 ) ) → 𝐵 ∈ dom card )
7	1 5 6	sylancr	⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ≼ 𝐴 ) → 𝐵 ∈ dom card )