Metamath Proof Explorer

Theorem f1imaen2g

Description: A one-to-one function's image under a subset of its domain is equinumerous to the subset. (This version of f1imaen does not need ax-reg .) (Contributed by Mario Carneiro, 16-Nov-2014) (Revised by Mario Carneiro, 25-Jun-2015)

Ref Expression
Assertion f1imaen2g ⊢ F : A ⟶ 1-1 B ∧ B ∈ V ∧ C ⊆ A ∧ C ∈ V → F C ≈ C

Proof

Step Hyp Ref Expression
1 simprr ⊢ F : A ⟶ 1-1 B ∧ B ∈ V ∧ C ⊆ A ∧ C ∈ V → C ∈ V
2 simplr ⊢ F : A ⟶ 1-1 B ∧ B ∈ V ∧ C ⊆ A ∧ C ∈ V → B ∈ V
3 f1f ⊢ F : A ⟶ 1-1 B → F : A ⟶ B
4 fimass ⊢ F : A ⟶ B → F C ⊆ B
5 3 4 syl ⊢ F : A ⟶ 1-1 B → F C ⊆ B
6 5 ad2antrr ⊢ F : A ⟶ 1-1 B ∧ B ∈ V ∧ C ⊆ A ∧ C ∈ V → F C ⊆ B
7 2 6 ssexd ⊢ F : A ⟶ 1-1 B ∧ B ∈ V ∧ C ⊆ A ∧ C ∈ V → F C ∈ V
8 f1ores ⊢ F : A ⟶ 1-1 B ∧ C ⊆ A → F ↾ C : C ⟶ 1-1 onto F C
9 8 ad2ant2r ⊢ F : A ⟶ 1-1 B ∧ B ∈ V ∧ C ⊆ A ∧ C ∈ V → F ↾ C : C ⟶ 1-1 onto F C
10 f1oen2g ⊢ C ∈ V ∧ F C ∈ V ∧ F ↾ C : C ⟶ 1-1 onto F C → C ≈ F C
11 1 7 9 10 syl3anc ⊢ F : A ⟶ 1-1 B ∧ B ∈ V ∧ C ⊆ A ∧ C ∈ V → C ≈ F C
12 11 ensymd ⊢ F : A ⟶ 1-1 B ∧ B ∈ V ∧ C ⊆ A ∧ C ∈ V → F C ≈ C