Theorem ssdomfi2

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

	Ref	Expression
Assertion	ssdomfi2	|- ( ( A e. Fin /\ B e. V /\ 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		f1domfi2	|- ( ( A e. Fin /\ B e. V /\ ( _I |` A ) : A -1-1-> B ) -> A ~<_ B )
7	5 6	syl3an3	|- ( ( A e. Fin /\ B e. V /\ A C_ B ) -> A ~<_ B )