Metamath Proof Explorer


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 )