Theorem ackbij1lem17

Description: Lemma for ackbij1 . (Contributed by Stefan O'Rear, 18-Nov-2014)

	Ref	Expression
Hypothesis	ackbij.f	$$⊢F=\left(x\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)⟼\mathrm{card}\left(\bigcup _{y\in x}\left(\left\{y\right\}\times 𝒫y\right)\right)\right)$$
Assertion	ackbij1lem17	$$⊢F:𝒫\mathrm{\omega }\cap \mathrm{Fin}\underset{1-1}{⟶}\mathrm{\omega }$$

Proof

Step	Hyp	Ref	Expression
1		ackbij.f	$$⊢F=\left(x\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)⟼\mathrm{card}\left(\bigcup _{y\in x}\left(\left\{y\right\}\times 𝒫y\right)\right)\right)$$
2	1	ackbij1lem10	$$⊢F:𝒫\mathrm{\omega }\cap \mathrm{Fin}⟶\mathrm{\omega }$$
3	1	ackbij1lem16	$$⊢\left(a\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\wedge b\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\right)\to \left(F\left(a\right)=F\left(b\right)\to a=b\right)$$
4	3	rgen2	$$⊢\forall a\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\forall b\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\left(F\left(a\right)=F\left(b\right)\to a=b\right)$$
5		dff13	$$⊢F:𝒫\mathrm{\omega }\cap \mathrm{Fin}\underset{1-1}{⟶}\mathrm{\omega }\leftrightarrow \left(F:𝒫\mathrm{\omega }\cap \mathrm{Fin}⟶\mathrm{\omega }\wedge \forall a\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\forall b\in \left(𝒫\mathrm{\omega }\cap \mathrm{Fin}\right)\left(F\left(a\right)=F\left(b\right)\to a=b\right)\right)$$
6	2 4 5	mpbir2an	$$⊢F:𝒫\mathrm{\omega }\cap \mathrm{Fin}\underset{1-1}{⟶}\mathrm{\omega }$$