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 C_ A
	hashsslei.a	\|- ( A e. Fin /\ ( # ` A ) <_ N )
	hashsslei.n	\|- N e. NN0
Assertion	hashsslei	\|- ( B e. Fin /\ ( # ` B ) <_ N )

Proof

Step	Hyp	Ref	Expression
1		hashsslei.b	\|- B C_ A
2		hashsslei.a	\|- ( A e. Fin /\ ( # ` A ) <_ N )
3		hashsslei.n	\|- N e. NN0
4	2	simpli	\|- A e. Fin
5		ssfi	\|- ( ( A e. Fin /\ B C_ A ) -> B e. Fin )
6	4 1 5	mp2an	\|- B e. Fin
7		ssdomg	\|- ( A e. Fin -> ( B C_ A -> B ~<_ A ) )
8	4 1 7	mp2	\|- B ~<_ A
9		hashdom	\|- ( ( B e. Fin /\ A e. 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 e. Fin -> ( # ` B ) e. NN0 )
14	6 13	ax-mp	\|- ( # ` B ) e. NN0
15	14	nn0rei	\|- ( # ` B ) e. RR
16		hashcl	\|- ( A e. Fin -> ( # ` A ) e. NN0 )
17	4 16	ax-mp	\|- ( # ` A ) e. NN0
18	17	nn0rei	\|- ( # ` A ) e. RR
19	3	nn0rei	\|- N e. RR
20	15 18 19	letri	\|- ( ( ( # ` B ) <_ ( # ` A ) /\ ( # ` A ) <_ N ) -> ( # ` B ) <_ N )
21	11 12 20	mp2an	\|- ( # ` B ) <_ N
22	6 21	pm3.2i	\|- ( B e. Fin /\ ( # ` B ) <_ N )

Metamath Proof Explorer

Theorem hashsslei

Proof