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

Metamath Proof Explorer

Theorem f1setex

Description: The set of injections between two classes exists if the codomain exists. (Contributed by AV, 14-Aug-2024)

Ref Expression
Assertion f1setex ⊢ B ∈ V → f | f : A ⟶ 1-1 B ∈ V

Proof

Step Hyp Ref Expression
1 fsetex ⊢ B ∈ V → f | f : A ⟶ B ∈ V
2 df-f1 ⊢ f : A ⟶ 1-1 B ↔ f : A ⟶ B ∧ Fun ⁡ f -1
3 2 abbii ⊢ f | f : A ⟶ 1-1 B = f | f : A ⟶ B ∧ Fun ⁡ f -1
4 abanssl ⊢ f | f : A ⟶ B ∧ Fun ⁡ f -1 ⊆ f | f : A ⟶ B
5 3 4 eqsstri ⊢ f | f : A ⟶ 1-1 B ⊆ f | f : A ⟶ B
6 5 a1i ⊢ B ∈ V → f | f : A ⟶ 1-1 B ⊆ f | f : A ⟶ B
7 1 6 ssexd ⊢ B ∈ V → f | f : A ⟶ 1-1 B ∈ V