This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∧ ( ♯ ‘ 𝐵 ) ≤ 𝑁 )