Theorem ssdomfi

Description: A finite set dominates its subsets, proved without using the Axiom of Power Sets (unlike ssdomg ). (Contributed by BTernaryTau, 12-Nov-2024)

	Ref	Expression
Assertion	ssdomfi	|- ( B e. Fin -> ( A C_ B -> A ~<_ B ) )

Proof

Step	Hyp	Ref	Expression
1		f1oi	|- ( _I |` A ) : A -1-1-onto-> A
2		f1of1	|- ( ( _I |` A ) : A -1-1-onto-> A -> ( _I |` A ) : A -1-1-> A )
3	1 2	ax-mp	|- ( _I |` A ) : A -1-1-> A
4		f1ss	|- ( ( ( _I |` A ) : A -1-1-> A /\ A C_ B ) -> ( _I |` A ) : A -1-1-> B )
5	3 4	mpan	|- ( A C_ B -> ( _I |` A ) : A -1-1-> B )
6		f1domfi	|- ( ( B e. Fin /\ ( _I |` A ) : A -1-1-> B ) -> A ~<_ B )
7	5 6	sylan2	|- ( ( B e. Fin /\ A C_ B ) -> A ~<_ B )
8	7	ex	|- ( B e. Fin -> ( A C_ B -> A ~<_ B ) )