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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | f1oi | |
|
2 | f1of1 | |
|
3 | 1 2 | ax-mp | |
4 | f1ss | |
|
5 | 3 4 | mpan | |
6 | f1domfi2 | |
|
7 | 5 6 | syl3an3 | |