This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∈ Fin → A ⊆ 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 ⊆ B → I ↾ A : A ⟶ 1-1 B
5 3 4 mpan ⊢ A ⊆ B → I ↾ A : A ⟶ 1-1 B
6 f1domfi ⊢ B ∈ Fin ∧ I ↾ A : A ⟶ 1-1 B → A ≼ B
7 5 6 sylan2 ⊢ B ∈ Fin ∧ A ⊆ B → A ≼ B
8 7 ex ⊢ B ∈ Fin → A ⊆ B → A ≼ B