Theorem coe1mul2lem2

Description: An equivalence for coe1mul2 . (Contributed by Stefan O'Rear, 25-Mar-2015)

	Ref	Expression
Hypothesis	coe1mul2lem2.h	$$⊢H=\left\{d\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|d{\le }_f\left(1_{𝑜}\times \left\{k\right\}\right)\right\}$$
Assertion	coe1mul2lem2	$$⊢k\in {\mathbb{N}}_0\to \left(c\in H⟼c\left(\varnothing \right)\right):H\underset{1-1\; onto}{⟶}\left(0\dots k\right)$$

Proof

Step	Hyp	Ref	Expression
1		coe1mul2lem2.h	$$⊢H=\left\{d\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|d{\le }_f\left(1_{𝑜}\times \left\{k\right\}\right)\right\}$$
2		df1o2	$$⊢1_{𝑜}=\left\{\varnothing \right\}$$
3		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
4		0ex	$$⊢\varnothing \in \mathrm{V}$$
5		eqid	$$⊢\left(c\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼c\left(\varnothing \right)\right)=\left(c\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼c\left(\varnothing \right)\right)$$
6	2 3 4 5	mapsnf1o2	$$⊢\left(c\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼c\left(\varnothing \right)\right):{{\mathbb{N}}_0}^{1_{𝑜}}\underset{1-1\; onto}{⟶}{\mathbb{N}}_0$$
7		f1of1	$$⊢\left(c\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼c\left(\varnothing \right)\right):{{\mathbb{N}}_0}^{1_{𝑜}}\underset{1-1\; onto}{⟶}{\mathbb{N}}_0\to \left(c\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼c\left(\varnothing \right)\right):{{\mathbb{N}}_0}^{1_{𝑜}}\underset{1-1}{⟶}{\mathbb{N}}_0$$
8	6 7	ax-mp	$$⊢\left(c\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼c\left(\varnothing \right)\right):{{\mathbb{N}}_0}^{1_{𝑜}}\underset{1-1}{⟶}{\mathbb{N}}_0$$
9	1	ssrab3	$$⊢H\subseteq {{\mathbb{N}}_0}^{1_{𝑜}}$$
10	9	a1i	$$⊢k\in {\mathbb{N}}_0\to H\subseteq {{\mathbb{N}}_0}^{1_{𝑜}}$$
11		f1ores	$$⊢\left(\left(c\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼c\left(\varnothing \right)\right):{{\mathbb{N}}_0}^{1_{𝑜}}\underset{1-1}{⟶}{\mathbb{N}}_0\wedge H\subseteq {{\mathbb{N}}_0}^{1_{𝑜}}\right)\to \left({\left(c\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼c\left(\varnothing \right)\right)\upharpoonright }_H\right):H\underset{1-1\; onto}{⟶}\left(c\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼c\left(\varnothing \right)\right)\left[H\right]$$
12	8 10 11	sylancr	$$⊢k\in {\mathbb{N}}_0\to \left({\left(c\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼c\left(\varnothing \right)\right)\upharpoonright }_H\right):H\underset{1-1\; onto}{⟶}\left(c\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼c\left(\varnothing \right)\right)\left[H\right]$$
13		coe1mul2lem1	$$⊢\left(k\in {\mathbb{N}}_0\wedge d\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)\right)\to \left(d{\le }_f\left(1_{𝑜}\times \left\{k\right\}\right)\leftrightarrow d\left(\varnothing \right)\in \left(0\dots k\right)\right)$$
14	13	rabbidva	$$⊢k\in {\mathbb{N}}_0\to \left\{d\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|d{\le }_f\left(1_{𝑜}\times \left\{k\right\}\right)\right\}=\left\{d\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|d\left(\varnothing \right)\in \left(0\dots k\right)\right\}$$
15		fveq1	$$⊢c=d\to c\left(\varnothing \right)=d\left(\varnothing \right)$$
16	15	eleq1d	$$⊢c=d\to \left(c\left(\varnothing \right)\in \left(0\dots k\right)\leftrightarrow d\left(\varnothing \right)\in \left(0\dots k\right)\right)$$
17	16	cbvrabv	$$⊢\left\{c\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|c\left(\varnothing \right)\in \left(0\dots k\right)\right\}=\left\{d\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|d\left(\varnothing \right)\in \left(0\dots k\right)\right\}$$
18	14 17	eqtr4di	$$⊢k\in {\mathbb{N}}_0\to \left\{d\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|d{\le }_f\left(1_{𝑜}\times \left\{k\right\}\right)\right\}=\left\{c\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|c\left(\varnothing \right)\in \left(0\dots k\right)\right\}$$
19	5	mptpreima	$$⊢{\left(c\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼c\left(\varnothing \right)\right)}^{-1}\left[\left(0\dots k\right)\right]=\left\{c\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)|c\left(\varnothing \right)\in \left(0\dots k\right)\right\}$$
20	18 1 19	3eqtr4g	$$⊢k\in {\mathbb{N}}_0\to H={\left(c\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼c\left(\varnothing \right)\right)}^{-1}\left[\left(0\dots k\right)\right]$$
21	20	imaeq2d	$$⊢k\in {\mathbb{N}}_0\to \left(c\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼c\left(\varnothing \right)\right)\left[H\right]=\left(c\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼c\left(\varnothing \right)\right)\left[{\left(c\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼c\left(\varnothing \right)\right)}^{-1}\left[\left(0\dots k\right)\right]\right]$$
22		f1ofo	$$⊢\left(c\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼c\left(\varnothing \right)\right):{{\mathbb{N}}_0}^{1_{𝑜}}\underset{1-1\; onto}{⟶}{\mathbb{N}}_0\to \left(c\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼c\left(\varnothing \right)\right):{{\mathbb{N}}_0}^{1_{𝑜}}\underset{onto}{⟶}{\mathbb{N}}_0$$
23	6 22	ax-mp	$$⊢\left(c\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼c\left(\varnothing \right)\right):{{\mathbb{N}}_0}^{1_{𝑜}}\underset{onto}{⟶}{\mathbb{N}}_0$$
24		fz0ssnn0	$$⊢\left(0\dots k\right)\subseteq {\mathbb{N}}_0$$
25		foimacnv	$$⊢\left(\left(c\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼c\left(\varnothing \right)\right):{{\mathbb{N}}_0}^{1_{𝑜}}\underset{onto}{⟶}{\mathbb{N}}_0\wedge \left(0\dots k\right)\subseteq {\mathbb{N}}_0\right)\to \left(c\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼c\left(\varnothing \right)\right)\left[{\left(c\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼c\left(\varnothing \right)\right)}^{-1}\left[\left(0\dots k\right)\right]\right]=\left(0\dots k\right)$$
26	23 24 25	mp2an	$$⊢\left(c\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼c\left(\varnothing \right)\right)\left[{\left(c\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼c\left(\varnothing \right)\right)}^{-1}\left[\left(0\dots k\right)\right]\right]=\left(0\dots k\right)$$
27	21 26	eqtrdi	$$⊢k\in {\mathbb{N}}_0\to \left(c\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼c\left(\varnothing \right)\right)\left[H\right]=\left(0\dots k\right)$$
28	27	f1oeq3d	$$⊢k\in {\mathbb{N}}_0\to \left(\left({\left(c\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼c\left(\varnothing \right)\right)\upharpoonright }_H\right):H\underset{1-1\; onto}{⟶}\left(c\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼c\left(\varnothing \right)\right)\left[H\right]\leftrightarrow \left({\left(c\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼c\left(\varnothing \right)\right)\upharpoonright }_H\right):H\underset{1-1\; onto}{⟶}\left(0\dots k\right)\right)$$
29		resmpt	$$⊢H\subseteq {{\mathbb{N}}_0}^{1_{𝑜}}\to {\left(c\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼c\left(\varnothing \right)\right)\upharpoonright }_H=\left(c\in H⟼c\left(\varnothing \right)\right)$$
30		f1oeq1	$$⊢{\left(c\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼c\left(\varnothing \right)\right)\upharpoonright }_H=\left(c\in H⟼c\left(\varnothing \right)\right)\to \left(\left({\left(c\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼c\left(\varnothing \right)\right)\upharpoonright }_H\right):H\underset{1-1\; onto}{⟶}\left(0\dots k\right)\leftrightarrow \left(c\in H⟼c\left(\varnothing \right)\right):H\underset{1-1\; onto}{⟶}\left(0\dots k\right)\right)$$
31	10 29 30	3syl	$$⊢k\in {\mathbb{N}}_0\to \left(\left({\left(c\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼c\left(\varnothing \right)\right)\upharpoonright }_H\right):H\underset{1-1\; onto}{⟶}\left(0\dots k\right)\leftrightarrow \left(c\in H⟼c\left(\varnothing \right)\right):H\underset{1-1\; onto}{⟶}\left(0\dots k\right)\right)$$
32	28 31	bitrd	$$⊢k\in {\mathbb{N}}_0\to \left(\left({\left(c\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼c\left(\varnothing \right)\right)\upharpoonright }_H\right):H\underset{1-1\; onto}{⟶}\left(c\in \left({{\mathbb{N}}_0}^{1_{𝑜}}\right)⟼c\left(\varnothing \right)\right)\left[H\right]\leftrightarrow \left(c\in H⟼c\left(\varnothing \right)\right):H\underset{1-1\; onto}{⟶}\left(0\dots k\right)\right)$$
33	12 32	mpbid	$$⊢k\in {\mathbb{N}}_0\to \left(c\in H⟼c\left(\varnothing \right)\right):H\underset{1-1\; onto}{⟶}\left(0\dots k\right)$$