Metamath Proof Explorer

Theorem fvimacnv

Description: The argument of a function value belongs to the preimage of any class containing the function value. Raph Levien remarks: "This proof is unsatisfying, because it seems to me that funimass2 could probably be strengthened to a biconditional." (Contributed by Raph Levien, 20-Nov-2006)

Ref Expression
Assertion fvimacnv ⊢ Fun ⁡ F ∧ A ∈ dom ⁡ F → F ⁡ A ∈ B ↔ A ∈ F -1 B

Proof

Step Hyp Ref Expression
1 funfvop ⊢ Fun ⁡ F ∧ A ∈ dom ⁡ F → A F ⁡ A ∈ F
2 fvex ⊢ F ⁡ A ∈ V
3 opelcnvg ⊢ F ⁡ A ∈ V ∧ A ∈ dom ⁡ F → F ⁡ A A ∈ F -1 ↔ A F ⁡ A ∈ F
4 2 3 mpan ⊢ A ∈ dom ⁡ F → F ⁡ A A ∈ F -1 ↔ A F ⁡ A ∈ F
5 4 adantl ⊢ Fun ⁡ F ∧ A ∈ dom ⁡ F → F ⁡ A A ∈ F -1 ↔ A F ⁡ A ∈ F
6 1 5 mpbird ⊢ Fun ⁡ F ∧ A ∈ dom ⁡ F → F ⁡ A A ∈ F -1
7 elimasng ⊢ F ⁡ A ∈ V ∧ A ∈ dom ⁡ F → A ∈ F -1 F ⁡ A ↔ F ⁡ A A ∈ F -1
8 2 7 mpan ⊢ A ∈ dom ⁡ F → A ∈ F -1 F ⁡ A ↔ F ⁡ A A ∈ F -1
9 8 adantl ⊢ Fun ⁡ F ∧ A ∈ dom ⁡ F → A ∈ F -1 F ⁡ A ↔ F ⁡ A A ∈ F -1
10 6 9 mpbird ⊢ Fun ⁡ F ∧ A ∈ dom ⁡ F → A ∈ F -1 F ⁡ A
11 2 snss ⊢ F ⁡ A ∈ B ↔ F ⁡ A ⊆ B
12 imass2 ⊢ F ⁡ A ⊆ B → F -1 F ⁡ A ⊆ F -1 B
13 11 12 sylbi ⊢ F ⁡ A ∈ B → F -1 F ⁡ A ⊆ F -1 B
14 13 sseld ⊢ F ⁡ A ∈ B → A ∈ F -1 F ⁡ A → A ∈ F -1 B
15 10 14 syl5com ⊢ Fun ⁡ F ∧ A ∈ dom ⁡ F → F ⁡ A ∈ B → A ∈ F -1 B
16 fvimacnvi ⊢ Fun ⁡ F ∧ A ∈ F -1 B → F ⁡ A ∈ B
17 16 ex ⊢ Fun ⁡ F → A ∈ F -1 B → F ⁡ A ∈ B
18 17 adantr ⊢ Fun ⁡ F ∧ A ∈ dom ⁡ F → A ∈ F -1 B → F ⁡ A ∈ B
19 15 18 impbid ⊢ Fun ⁡ F ∧ A ∈ dom ⁡ F → F ⁡ A ∈ B ↔ A ∈ F -1 B