# Metamath Proof Explorer

## Theorem infunabs

Description: An infinite set is equinumerous to its union with a smaller one. (Contributed by NM, 28-Sep-2004) (Revised by Mario Carneiro, 29-Apr-2015)

Ref Expression
Assertion infunabs ${⊢}\left({A}\in \mathrm{dom}\mathrm{card}\wedge \mathrm{\omega }\preccurlyeq {A}\wedge {B}\preccurlyeq {A}\right)\to \left({A}\cup {B}\right)\approx {A}$

### Proof

Step Hyp Ref Expression
1 simp1 ${⊢}\left({A}\in \mathrm{dom}\mathrm{card}\wedge \mathrm{\omega }\preccurlyeq {A}\wedge {B}\preccurlyeq {A}\right)\to {A}\in \mathrm{dom}\mathrm{card}$
2 reldom ${⊢}\mathrm{Rel}\preccurlyeq$
3 2 brrelex1i ${⊢}{B}\preccurlyeq {A}\to {B}\in \mathrm{V}$
4 3 3ad2ant3 ${⊢}\left({A}\in \mathrm{dom}\mathrm{card}\wedge \mathrm{\omega }\preccurlyeq {A}\wedge {B}\preccurlyeq {A}\right)\to {B}\in \mathrm{V}$
5 undjudom ${⊢}\left({A}\in \mathrm{dom}\mathrm{card}\wedge {B}\in \mathrm{V}\right)\to \left({A}\cup {B}\right)\preccurlyeq \left({A}\mathrm{\bigsqcup ︀}{B}\right)$
6 1 4 5 syl2anc ${⊢}\left({A}\in \mathrm{dom}\mathrm{card}\wedge \mathrm{\omega }\preccurlyeq {A}\wedge {B}\preccurlyeq {A}\right)\to \left({A}\cup {B}\right)\preccurlyeq \left({A}\mathrm{\bigsqcup ︀}{B}\right)$
7 infdjuabs ${⊢}\left({A}\in \mathrm{dom}\mathrm{card}\wedge \mathrm{\omega }\preccurlyeq {A}\wedge {B}\preccurlyeq {A}\right)\to \left({A}\mathrm{\bigsqcup ︀}{B}\right)\approx {A}$
8 domentr ${⊢}\left(\left({A}\cup {B}\right)\preccurlyeq \left({A}\mathrm{\bigsqcup ︀}{B}\right)\wedge \left({A}\mathrm{\bigsqcup ︀}{B}\right)\approx {A}\right)\to \left({A}\cup {B}\right)\preccurlyeq {A}$
9 6 7 8 syl2anc ${⊢}\left({A}\in \mathrm{dom}\mathrm{card}\wedge \mathrm{\omega }\preccurlyeq {A}\wedge {B}\preccurlyeq {A}\right)\to \left({A}\cup {B}\right)\preccurlyeq {A}$
10 unexg ${⊢}\left({A}\in \mathrm{dom}\mathrm{card}\wedge {B}\in \mathrm{V}\right)\to {A}\cup {B}\in \mathrm{V}$
11 1 4 10 syl2anc ${⊢}\left({A}\in \mathrm{dom}\mathrm{card}\wedge \mathrm{\omega }\preccurlyeq {A}\wedge {B}\preccurlyeq {A}\right)\to {A}\cup {B}\in \mathrm{V}$
12 ssun1 ${⊢}{A}\subseteq {A}\cup {B}$
13 ssdomg ${⊢}{A}\cup {B}\in \mathrm{V}\to \left({A}\subseteq {A}\cup {B}\to {A}\preccurlyeq \left({A}\cup {B}\right)\right)$
14 11 12 13 mpisyl ${⊢}\left({A}\in \mathrm{dom}\mathrm{card}\wedge \mathrm{\omega }\preccurlyeq {A}\wedge {B}\preccurlyeq {A}\right)\to {A}\preccurlyeq \left({A}\cup {B}\right)$
15 sbth ${⊢}\left(\left({A}\cup {B}\right)\preccurlyeq {A}\wedge {A}\preccurlyeq \left({A}\cup {B}\right)\right)\to \left({A}\cup {B}\right)\approx {A}$
16 9 14 15 syl2anc ${⊢}\left({A}\in \mathrm{dom}\mathrm{card}\wedge \mathrm{\omega }\preccurlyeq {A}\wedge {B}\preccurlyeq {A}\right)\to \left({A}\cup {B}\right)\approx {A}$