Metamath Proof Explorer

Theorem elpreima

Description: Membership in the preimage of a set under a function. (Contributed by Jeff Madsen, 2-Sep-2009)

Ref Expression
Assertion elpreima ⊢ F Fn A → B ∈ F -1 C ↔ B ∈ A ∧ F ⁡ B ∈ C

Proof

Step Hyp Ref Expression
1 cnvimass ⊢ F -1 C ⊆ dom ⁡ F
2 1 sseli ⊢ B ∈ F -1 C → B ∈ dom ⁡ F
3 fndm ⊢ F Fn A → dom ⁡ F = A
4 3 eleq2d ⊢ F Fn A → B ∈ dom ⁡ F ↔ B ∈ A
5 2 4 imbitrid ⊢ F Fn A → B ∈ F -1 C → B ∈ A
6 fnfun ⊢ F Fn A → Fun ⁡ F
7 fvimacnvi ⊢ Fun ⁡ F ∧ B ∈ F -1 C → F ⁡ B ∈ C
8 6 7 sylan ⊢ F Fn A ∧ B ∈ F -1 C → F ⁡ B ∈ C
9 8 ex ⊢ F Fn A → B ∈ F -1 C → F ⁡ B ∈ C
10 5 9 jcad ⊢ F Fn A → B ∈ F -1 C → B ∈ A ∧ F ⁡ B ∈ C
11 fvimacnv ⊢ Fun ⁡ F ∧ B ∈ dom ⁡ F → F ⁡ B ∈ C ↔ B ∈ F -1 C
12 11 funfni ⊢ F Fn A ∧ B ∈ A → F ⁡ B ∈ C ↔ B ∈ F -1 C
13 12 biimpd ⊢ F Fn A ∧ B ∈ A → F ⁡ B ∈ C → B ∈ F -1 C
14 13 expimpd ⊢ F Fn A → B ∈ A ∧ F ⁡ B ∈ C → B ∈ F -1 C
15 10 14 impbid ⊢ F Fn A → B ∈ F -1 C ↔ B ∈ A ∧ F ⁡ B ∈ C