Theorem djunum

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

	Ref	Expression
Assertion	djunum	⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( 𝐴 ⊔ 𝐵 ) ∈ dom card )

Proof

Step	Hyp	Ref	Expression
1		cardon	⊢ ( card ‘ 𝐴 ) ∈ On
2		cardon	⊢ ( card ‘ 𝐵 ) ∈ On
3		oacl	⊢ ( ( ( card ‘ 𝐴 ) ∈ On ∧ ( card ‘ 𝐵 ) ∈ On ) → ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ∈ On )
4	1 2 3	mp2an	⊢ ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ∈ On
5		cardadju	⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( 𝐴 ⊔ 𝐵 ) ≈ ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) )
6	5	ensymd	⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ≈ ( 𝐴 ⊔ 𝐵 ) )
7		isnumi	⊢ ( ( ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ∈ On ∧ ( ( card ‘ 𝐴 ) +o ( card ‘ 𝐵 ) ) ≈ ( 𝐴 ⊔ 𝐵 ) ) → ( 𝐴 ⊔ 𝐵 ) ∈ dom card )
8	4 6 7	sylancr	⊢ ( ( 𝐴 ∈ dom card ∧ 𝐵 ∈ dom card ) → ( 𝐴 ⊔ 𝐵 ) ∈ dom card )