Theorem unnum

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

	Ref	Expression
Assertion	unnum	|- ( ( A e. dom card /\ B e. dom card ) -> ( A u. B ) e. dom card )

Proof

Step	Hyp	Ref	Expression
1		djunum	|- ( ( A e. dom card /\ B e. dom card ) -> ( A |_| B ) e. dom card )
2		undjudom	|- ( ( A e. dom card /\ B e. dom card ) -> ( A u. B ) ~<_ ( A |_| B ) )
3		numdom	|- ( ( ( A |_| B ) e. dom card /\ ( A u. B ) ~<_ ( A |_| B ) ) -> ( A u. B ) e. dom card )
4	1 2 3	syl2anc	|- ( ( A e. dom card /\ B e. dom card ) -> ( A u. B ) e. dom card )