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

Metamath Proof Explorer

Theorem hashimaf1

Description: Taking the image of a set by a one-to-one function does not affect size. (Contributed by Thierry Arnoux, 18-Jan-2026)

Ref Expression
Hypotheses hashimaf1.1 ⊢ φ → F : A ⟶ 1-1 B
hashimaf1.2 ⊢ φ → C ⊆ A
hashimaf1.3 ⊢ φ → A ∈ V
Assertion hashimaf1 ⊢ φ → F C = C

Proof

Step Hyp Ref Expression
1 hashimaf1.1 ⊢ φ → F : A ⟶ 1-1 B
2 hashimaf1.2 ⊢ φ → C ⊆ A
3 hashimaf1.3 ⊢ φ → A ∈ V
4 3 2 sselpwd ⊢ φ → C ∈ 𝒫 A
5 f1ores ⊢ F : A ⟶ 1-1 B ∧ C ⊆ A → F ↾ C : C ⟶ 1-1 onto F C
6 1 2 5 syl2anc ⊢ φ → F ↾ C : C ⟶ 1-1 onto F C
7 f1oeng ⊢ C ∈ 𝒫 A ∧ F ↾ C : C ⟶ 1-1 onto F C → C ≈ F C
8 4 6 7 syl2anc ⊢ φ → C ≈ F C
9 8 ensymd ⊢ φ → F C ≈ C
10 hasheni ⊢ F C ≈ C → F C = C
11 9 10 syl ⊢ φ → F C = C