This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 ↔ 𝐴 ∈ ( ◡ 𝐹 “ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 funfvop ⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ ∈ 𝐹 )
2 fvex ⊢ ( 𝐹 ‘ 𝐴 ) ∈ V
3 opelcnvg ⊢ ( ( ( 𝐹 ‘ 𝐴 ) ∈ V ∧ 𝐴 ∈ dom 𝐹 ) → ( ⟨ ( 𝐹 ‘ 𝐴 ) , 𝐴 ⟩ ∈ ◡ 𝐹 ↔ ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ ∈ 𝐹 ) )
4 2 3 mpan ⊢ ( 𝐴 ∈ dom 𝐹 → ( ⟨ ( 𝐹 ‘ 𝐴 ) , 𝐴 ⟩ ∈ ◡ 𝐹 ↔ ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ ∈ 𝐹 ) )
5 4 adantl ⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ( ⟨ ( 𝐹 ‘ 𝐴 ) , 𝐴 ⟩ ∈ ◡ 𝐹 ↔ ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ ∈ 𝐹 ) )
6 1 5 mpbird ⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ⟨ ( 𝐹 ‘ 𝐴 ) , 𝐴 ⟩ ∈ ◡ 𝐹 )
7 elimasng ⊢ ( ( ( 𝐹 ‘ 𝐴 ) ∈ V ∧ 𝐴 ∈ dom 𝐹 ) → ( 𝐴 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝐴 ) } ) ↔ ⟨ ( 𝐹 ‘ 𝐴 ) , 𝐴 ⟩ ∈ ◡ 𝐹 ) )
8 2 7 mpan ⊢ ( 𝐴 ∈ dom 𝐹 → ( 𝐴 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝐴 ) } ) ↔ ⟨ ( 𝐹 ‘ 𝐴 ) , 𝐴 ⟩ ∈ ◡ 𝐹 ) )
9 8 adantl ⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ( 𝐴 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝐴 ) } ) ↔ ⟨ ( 𝐹 ‘ 𝐴 ) , 𝐴 ⟩ ∈ ◡ 𝐹 ) )
10 6 9 mpbird ⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → 𝐴 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝐴 ) } ) )
11 2 snss ⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 ↔ { ( 𝐹 ‘ 𝐴 ) } ⊆ 𝐵 )
12 imass2 ⊢ ( { ( 𝐹 ‘ 𝐴 ) } ⊆ 𝐵 → ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝐴 ) } ) ⊆ ( ◡ 𝐹 “ 𝐵 ) )
13 11 12 sylbi ⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 → ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝐴 ) } ) ⊆ ( ◡ 𝐹 “ 𝐵 ) )
14 13 sseld ⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 → ( 𝐴 ∈ ( ◡ 𝐹 “ { ( 𝐹 ‘ 𝐴 ) } ) → 𝐴 ∈ ( ◡ 𝐹 “ 𝐵 ) ) )
15 10 14 syl5com ⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 → 𝐴 ∈ ( ◡ 𝐹 “ 𝐵 ) ) )
16 fvimacnvi ⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ ( ◡ 𝐹 “ 𝐵 ) ) → ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 )
17 16 ex ⊢ ( Fun 𝐹 → ( 𝐴 ∈ ( ◡ 𝐹 “ 𝐵 ) → ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 ) )
18 17 adantr ⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ( 𝐴 ∈ ( ◡ 𝐹 “ 𝐵 ) → ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 ) )
19 15 18 impbid ⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 ↔ 𝐴 ∈ ( ◡ 𝐹 “ 𝐵 ) ) )