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 ⊢ B ⊆ A
hashsslei.a ⊢ A ∈ Fin ∧ A ≤ N
hashsslei.n ⊢ N ∈ ℕ 0
Assertion hashsslei ⊢ B ∈ Fin ∧ B ≤ N

Proof

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