Metamath Proof Explorer

Theorem f1preimaex

Description: If the image under a one-to-one function exists, then the corresponding preimage also exists. (Contributed by BTernaryTau, 21-Jun-2026)

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

Proof

Step Hyp Ref Expression
1 df-f1 ⊢ F : A ⟶ 1-1 B ↔ F : A ⟶ B ∧ Fun ⁡ F -1
2 1 simprbi ⊢ F : A ⟶ 1-1 B → Fun ⁡ F -1
3 funimaexg ⊢ Fun ⁡ F -1 ∧ F C ∈ V → F -1 F C ∈ V
4 2 3 sylan ⊢ F : A ⟶ 1-1 B ∧ F C ∈ V → F -1 F C ∈ V
5 4 3adant2 ⊢ F : A ⟶ 1-1 B ∧ C ⊆ A ∧ F C ∈ V → F -1 F C ∈ V
6 f1imacnv ⊢ F : A ⟶ 1-1 B ∧ C ⊆ A → F -1 F C = C
7 6 eleq1d ⊢ F : A ⟶ 1-1 B ∧ C ⊆ A → F -1 F C ∈ V ↔ C ∈ V
8 7 3adant3 ⊢ F : A ⟶ 1-1 B ∧ C ⊆ A ∧ F C ∈ V → F -1 F C ∈ V ↔ C ∈ V
9 5 8 mpbid ⊢ F : A ⟶ 1-1 B ∧ C ⊆ A ∧ F C ∈ V → C ∈ V