Theorem unnum

Description: The union of two numerable sets is numerable. (Contributed by Mario Carneiro, 29-Apr-2015)

	Ref	Expression
Assertion	unnum	⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( 𝐴 ∪ 𝐵 ) ∈ dom card )

Proof

Step	Hyp	Ref	Expression
1		djunum	⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( 𝐴 ⊔ 𝐵 ) ∈ dom card )
2		undjudom	⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( 𝐴 ∪ 𝐵 ) ≼ ( 𝐴 ⊔ 𝐵 ) )
3		numdom	⊢ ( ( ( 𝐴 ⊔ 𝐵 ) ∈ dom card ∧ ( 𝐴 ∪ 𝐵 ) ≼ ( 𝐴 ⊔ 𝐵 ) ) → ( 𝐴 ∪ 𝐵 ) ∈ dom card )
4	1 2 3	syl2anc	⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( 𝐴 ∪ 𝐵 ) ∈ dom card )