Theorem hashsslei

Description: Get an upper bound on a concretely specified finite set. Transfer boundedness to a subset. (Contributed by Mario Carneiro, 11-Feb-2015)

	Ref	Expression
Hypotheses	hashsslei.b	$$⊢B\subseteq A$$
	hashsslei.a	$$⊢\left(A\in \mathrm{Fin}\wedge \left|A\right|\le N\right)$$
	hashsslei.n	$$⊢N\in {\mathbb{N}}_0$$
Assertion	hashsslei	$$⊢\left(B\in \mathrm{Fin}\wedge \left|B\right|\le N\right)$$

Proof

Step	Hyp	Ref	Expression
1		hashsslei.b	$$⊢B\subseteq A$$
2		hashsslei.a	$$⊢\left(A\in \mathrm{Fin}\wedge \left|A\right|\le N\right)$$
3		hashsslei.n	$$⊢N\in {\mathbb{N}}_0$$
4	2	simpli	$$⊢A\in \mathrm{Fin}$$
5		ssfi	$$⊢\left(A\in \mathrm{Fin}\wedge B\subseteq A\right)\to B\in \mathrm{Fin}$$
6	4 1 5	mp2an	$$⊢B\in \mathrm{Fin}$$
7		ssdomg	$$⊢A\in \mathrm{Fin}\to \left(B\subseteq A\to B\preccurlyeq A\right)$$
8	4 1 7	mp2	$$⊢B\preccurlyeq A$$
9		hashdom	$$⊢\left(B\in \mathrm{Fin}\wedge A\in \mathrm{Fin}\right)\to \left(\left|B\right|\le \left|A\right|\leftrightarrow B\preccurlyeq A\right)$$
10	6 4 9	mp2an	$$⊢\left|B\right|\le \left|A\right|\leftrightarrow B\preccurlyeq A$$
11	8 10	mpbir	$$⊢\left|B\right|\le \left|A\right|$$
12	2	simpri	$$⊢\left|A\right|\le N$$
13		hashcl	$$⊢B\in \mathrm{Fin}\to \left|B\right|\in {\mathbb{N}}_0$$
14	6 13	ax-mp	$$⊢\left|B\right|\in {\mathbb{N}}_0$$
15	14	nn0rei	$$⊢\left|B\right|\in ℝ$$
16		hashcl	$$⊢A\in \mathrm{Fin}\to \left|A\right|\in {\mathbb{N}}_0$$
17	4 16	ax-mp	$$⊢\left|A\right|\in {\mathbb{N}}_0$$
18	17	nn0rei	$$⊢\left|A\right|\in ℝ$$
19	3	nn0rei	$$⊢N\in ℝ$$
20	15 18 19	letri	$$⊢\left(\left|B\right|\le \left|A\right|\wedge \left|A\right|\le N\right)\to \left|B\right|\le N$$
21	11 12 20	mp2an	$$⊢\left|B\right|\le N$$
22	6 21	pm3.2i	$$⊢\left(B\in \mathrm{Fin}\wedge \left|B\right|\le N\right)$$