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	$$⊢FFnB$$
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\leftrightarrow \left(FFnB\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)\leftrightarrow 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\leftrightarrow z=w\right)$$
23	1 19 21 22	mp3an3an	$$⊢\left(z\in B\wedge w\in B\right)\to \left(A{+}_{𝑜}z=A{+}_{𝑜}w\leftrightarrow 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)\leftrightarrow 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\forall w\in B\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\leftrightarrow \left(F:B⟶\left(A{+}_{𝑜}B\right)\setminus A\wedge \forall z\in B\forall w\in B\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\leftrightarrow \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$$