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	⊢ 𝐵 ⊆ 𝐴
	hashsslei.a	⊢ ( 𝐴 ∈ Fin ∧ ( ♯ ‘ 𝐴 ) ≤ 𝑁 )
	hashsslei.n	⊢ 𝑁 ∈ ℕ0
Assertion	hashsslei	⊢ ( 𝐵 ∈ Fin ∧ ( ♯ ‘ 𝐵 ) ≤ 𝑁 )

Proof

Step	Hyp	Ref	Expression
1		hashsslei.b	⊢ 𝐵 ⊆ 𝐴
2		hashsslei.a	⊢ ( 𝐴 ∈ Fin ∧ ( ♯ ‘ 𝐴 ) ≤ 𝑁 )
3		hashsslei.n	⊢ 𝑁 ∈ ℕ0
4	2	simpli	⊢ 𝐴 ∈ Fin
5		ssfi	⊢ ( ( 𝐴 ∈ Fin ∧ 𝐵 ⊆ 𝐴 ) → 𝐵 ∈ Fin )
6	4 1 5	mp2an	⊢ 𝐵 ∈ Fin
7		ssdomg	⊢ ( 𝐴 ∈ Fin → ( 𝐵 ⊆ 𝐴 → 𝐵 ≼ 𝐴 ) )
8	4 1 7	mp2	⊢ 𝐵 ≼ 𝐴
9		hashdom	⊢ ( ( 𝐵 ∈ Fin ∧ 𝐴 ∈ Fin ) → ( ( ♯ ‘ 𝐵 ) ≤ ( ♯ ‘ 𝐴 ) ↔ 𝐵 ≼ 𝐴 ) )
10	6 4 9	mp2an	⊢ ( ( ♯ ‘ 𝐵 ) ≤ ( ♯ ‘ 𝐴 ) ↔ 𝐵 ≼ 𝐴 )
11	8 10	mpbir	⊢ ( ♯ ‘ 𝐵 ) ≤ ( ♯ ‘ 𝐴 )
12	2	simpri	⊢ ( ♯ ‘ 𝐴 ) ≤ 𝑁
13		hashcl	⊢ ( 𝐵 ∈ Fin → ( ♯ ‘ 𝐵 ) ∈ ℕ0 )
14	6 13	ax-mp	⊢ ( ♯ ‘ 𝐵 ) ∈ ℕ0
15	14	nn0rei	⊢ ( ♯ ‘ 𝐵 ) ∈ ℝ
16		hashcl	⊢ ( 𝐴 ∈ Fin → ( ♯ ‘ 𝐴 ) ∈ ℕ0 )
17	4 16	ax-mp	⊢ ( ♯ ‘ 𝐴 ) ∈ ℕ0
18	17	nn0rei	⊢ ( ♯ ‘ 𝐴 ) ∈ ℝ
19	3	nn0rei	⊢ 𝑁 ∈ ℝ
20	15 18 19	letri	⊢ ( ( ( ♯ ‘ 𝐵 ) ≤ ( ♯ ‘ 𝐴 ) ∧ ( ♯ ‘ 𝐴 ) ≤ 𝑁 ) → ( ♯ ‘ 𝐵 ) ≤ 𝑁 )
21	11 12 20	mp2an	⊢ ( ♯ ‘ 𝐵 ) ≤ 𝑁
22	6 21	pm3.2i	⊢ ( 𝐵 ∈ Fin ∧ ( ♯ ‘ 𝐵 ) ≤ 𝑁 )