Metamath Proof Explorer


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 AFinBVABAB

Proof

Step Hyp Ref Expression
1 f1oi IA:A1-1 ontoA
2 f1of1 IA:A1-1 ontoAIA:A1-1A
3 1 2 ax-mp IA:A1-1A
4 f1ss IA:A1-1AABIA:A1-1B
5 3 4 mpan ABIA:A1-1B
6 f1domfi2 AFinBVIA:A1-1BAB
7 5 6 syl3an3 AFinBVABAB