Metamath Proof Explorer

Theorem f1oexrnex

Description: If the range of a 1-1 onto function is a set, the function itself is a set. (Contributed by AV, 2-Jun-2019)

Ref Expression
Assertion f1oexrnex ⊢ F : A ⟶ 1-1 onto B ∧ B ∈ V → F ∈ V

Proof

Step Hyp Ref Expression
1 simpl ⊢ F : A ⟶ 1-1 onto B ∧ B ∈ V → F : A ⟶ 1-1 onto B
2 f1ocnv ⊢ F : A ⟶ 1-1 onto B → F -1 : B ⟶ 1-1 onto A
3 f1of ⊢ F -1 : B ⟶ 1-1 onto A → F -1 : B ⟶ A
4 1 2 3 3syl ⊢ F : A ⟶ 1-1 onto B ∧ B ∈ V → F -1 : B ⟶ A
5 fex ⊢ F -1 : B ⟶ A ∧ B ∈ V → F -1 ∈ V
6 4 5 sylancom ⊢ F : A ⟶ 1-1 onto B ∧ B ∈ V → F -1 ∈ V
7 f1orel ⊢ F : A ⟶ 1-1 onto B → Rel ⁡ F
8 7 adantr ⊢ F : A ⟶ 1-1 onto B ∧ B ∈ V → Rel ⁡ F
9 relcnvexb ⊢ Rel ⁡ F → F ∈ V ↔ F -1 ∈ V
10 8 9 syl ⊢ F : A ⟶ 1-1 onto B ∧ B ∈ V → F ∈ V ↔ F -1 ∈ V
11 6 10 mpbird ⊢ F : A ⟶ 1-1 onto B ∧ B ∈ V → F ∈ V