Metamath Proof Explorer

Theorem preimafvelsetpreimafv

Description: The preimage of a function value is an element of the class P of all preimages of function values. (Contributed by AV, 10-Mar-2024)

Ref Expression
Hypothesis setpreimafvex.p ⊢ P = z | ∃ x ∈ A z = F -1 F ⁡ x
Assertion preimafvelsetpreimafv ⊢ F Fn A ∧ A ∈ V ∧ X ∈ A → F -1 F ⁡ X ∈ P

Proof

Step Hyp Ref Expression
1 setpreimafvex.p ⊢ P = z | ∃ x ∈ A z = F -1 F ⁡ x
2 id ⊢ X ∈ A → X ∈ A
3 fveq2 ⊢ x = X → F ⁡ x = F ⁡ X
4 3 sneqd ⊢ x = X → F ⁡ x = F ⁡ X
5 4 imaeq2d ⊢ x = X → F -1 F ⁡ x = F -1 F ⁡ X
6 5 eqeq2d ⊢ x = X → F -1 F ⁡ X = F -1 F ⁡ x ↔ F -1 F ⁡ X = F -1 F ⁡ X
7 6 adantl ⊢ X ∈ A ∧ x = X → F -1 F ⁡ X = F -1 F ⁡ x ↔ F -1 F ⁡ X = F -1 F ⁡ X
8 eqidd ⊢ X ∈ A → F -1 F ⁡ X = F -1 F ⁡ X
9 2 7 8 rspcedvd ⊢ X ∈ A → ∃ x ∈ A F -1 F ⁡ X = F -1 F ⁡ x
10 9 3ad2ant3 ⊢ F Fn A ∧ A ∈ V ∧ X ∈ A → ∃ x ∈ A F -1 F ⁡ X = F -1 F ⁡ x
11 fnex ⊢ F Fn A ∧ A ∈ V → F ∈ V
12 cnvexg ⊢ F ∈ V → F -1 ∈ V
13 imaexg ⊢ F -1 ∈ V → F -1 F ⁡ X ∈ V
14 11 12 13 3syl ⊢ F Fn A ∧ A ∈ V → F -1 F ⁡ X ∈ V
15 14 3adant3 ⊢ F Fn A ∧ A ∈ V ∧ X ∈ A → F -1 F ⁡ X ∈ V
16 1 elsetpreimafvb ⊢ F -1 F ⁡ X ∈ V → F -1 F ⁡ X ∈ P ↔ ∃ x ∈ A F -1 F ⁡ X = F -1 F ⁡ x
17 15 16 syl ⊢ F Fn A ∧ A ∈ V ∧ X ∈ A → F -1 F ⁡ X ∈ P ↔ ∃ x ∈ A F -1 F ⁡ X = F -1 F ⁡ x
18 10 17 mpbird ⊢ F Fn A ∧ A ∈ V ∧ X ∈ A → F -1 F ⁡ X ∈ P