# Metamath Proof Explorer

## Theorem unfilem2

Description: Lemma for proving that the union of two finite sets is finite. (Contributed by NM, 10-Nov-2002) (Revised by Mario Carneiro, 31-Aug-2015)

Ref Expression
Hypotheses unfilem1.1 ${⊢}{A}\in \mathrm{\omega }$
unfilem1.2 ${⊢}{B}\in \mathrm{\omega }$
unfilem1.3 ${⊢}{F}=\left({x}\in {B}⟼{A}{+}_{𝑜}{x}\right)$
Assertion unfilem2 ${⊢}{F}:{B}\underset{1-1 onto}{⟶}\left({A}{+}_{𝑜}{B}\right)\setminus {A}$

### Proof

Step Hyp Ref Expression
1 unfilem1.1 ${⊢}{A}\in \mathrm{\omega }$
2 unfilem1.2 ${⊢}{B}\in \mathrm{\omega }$
3 unfilem1.3 ${⊢}{F}=\left({x}\in {B}⟼{A}{+}_{𝑜}{x}\right)$
4 ovex ${⊢}{A}{+}_{𝑜}{x}\in \mathrm{V}$
5 4 3 fnmpti ${⊢}{F}Fn{B}$
6 1 2 3 unfilem1 ${⊢}\mathrm{ran}{F}=\left({A}{+}_{𝑜}{B}\right)\setminus {A}$
7 df-fo ${⊢}{F}:{B}\underset{onto}{⟶}\left({A}{+}_{𝑜}{B}\right)\setminus {A}↔\left({F}Fn{B}\wedge \mathrm{ran}{F}=\left({A}{+}_{𝑜}{B}\right)\setminus {A}\right)$
8 5 6 7 mpbir2an ${⊢}{F}:{B}\underset{onto}{⟶}\left({A}{+}_{𝑜}{B}\right)\setminus {A}$
9 fof ${⊢}{F}:{B}\underset{onto}{⟶}\left({A}{+}_{𝑜}{B}\right)\setminus {A}\to {F}:{B}⟶\left({A}{+}_{𝑜}{B}\right)\setminus {A}$
10 8 9 ax-mp ${⊢}{F}:{B}⟶\left({A}{+}_{𝑜}{B}\right)\setminus {A}$
11 oveq2 ${⊢}{x}={z}\to {A}{+}_{𝑜}{x}={A}{+}_{𝑜}{z}$
12 ovex ${⊢}{A}{+}_{𝑜}{z}\in \mathrm{V}$
13 11 3 12 fvmpt ${⊢}{z}\in {B}\to {F}\left({z}\right)={A}{+}_{𝑜}{z}$
14 oveq2 ${⊢}{x}={w}\to {A}{+}_{𝑜}{x}={A}{+}_{𝑜}{w}$
15 ovex ${⊢}{A}{+}_{𝑜}{w}\in \mathrm{V}$
16 14 3 15 fvmpt ${⊢}{w}\in {B}\to {F}\left({w}\right)={A}{+}_{𝑜}{w}$
17 13 16 eqeqan12d ${⊢}\left({z}\in {B}\wedge {w}\in {B}\right)\to \left({F}\left({z}\right)={F}\left({w}\right)↔{A}{+}_{𝑜}{z}={A}{+}_{𝑜}{w}\right)$
18 elnn ${⊢}\left({z}\in {B}\wedge {B}\in \mathrm{\omega }\right)\to {z}\in \mathrm{\omega }$
19 2 18 mpan2 ${⊢}{z}\in {B}\to {z}\in \mathrm{\omega }$
20 elnn ${⊢}\left({w}\in {B}\wedge {B}\in \mathrm{\omega }\right)\to {w}\in \mathrm{\omega }$
21 2 20 mpan2 ${⊢}{w}\in {B}\to {w}\in \mathrm{\omega }$
22 nnacan ${⊢}\left({A}\in \mathrm{\omega }\wedge {z}\in \mathrm{\omega }\wedge {w}\in \mathrm{\omega }\right)\to \left({A}{+}_{𝑜}{z}={A}{+}_{𝑜}{w}↔{z}={w}\right)$
23 1 19 21 22 mp3an3an ${⊢}\left({z}\in {B}\wedge {w}\in {B}\right)\to \left({A}{+}_{𝑜}{z}={A}{+}_{𝑜}{w}↔{z}={w}\right)$
24 17 23 bitrd ${⊢}\left({z}\in {B}\wedge {w}\in {B}\right)\to \left({F}\left({z}\right)={F}\left({w}\right)↔{z}={w}\right)$
25 24 biimpd ${⊢}\left({z}\in {B}\wedge {w}\in {B}\right)\to \left({F}\left({z}\right)={F}\left({w}\right)\to {z}={w}\right)$
26 25 rgen2 ${⊢}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\forall {w}\in {B}\phantom{\rule{.4em}{0ex}}\left({F}\left({z}\right)={F}\left({w}\right)\to {z}={w}\right)$
27 dff13 ${⊢}{F}:{B}\underset{1-1}{⟶}\left({A}{+}_{𝑜}{B}\right)\setminus {A}↔\left({F}:{B}⟶\left({A}{+}_{𝑜}{B}\right)\setminus {A}\wedge \forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\forall {w}\in {B}\phantom{\rule{.4em}{0ex}}\left({F}\left({z}\right)={F}\left({w}\right)\to {z}={w}\right)\right)$
28 10 26 27 mpbir2an ${⊢}{F}:{B}\underset{1-1}{⟶}\left({A}{+}_{𝑜}{B}\right)\setminus {A}$
29 df-f1o ${⊢}{F}:{B}\underset{1-1 onto}{⟶}\left({A}{+}_{𝑜}{B}\right)\setminus {A}↔\left({F}:{B}\underset{1-1}{⟶}\left({A}{+}_{𝑜}{B}\right)\setminus {A}\wedge {F}:{B}\underset{onto}{⟶}\left({A}{+}_{𝑜}{B}\right)\setminus {A}\right)$
30 28 8 29 mpbir2an ${⊢}{F}:{B}\underset{1-1 onto}{⟶}\left({A}{+}_{𝑜}{B}\right)\setminus {A}$