This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )