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

Metamath Proof Explorer

Theorem fvimacnvi

Description: A member of a preimage is a function value argument. (Contributed by NM, 4-May-2007)

Ref Expression
Assertion fvimacnvi ( ( Fun 𝐹 ∧ 𝐴 ∈ ( ◡ 𝐹 “ 𝐵 ) ) → ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 snssi ⊢ ( 𝐴 ∈ ( ◡ 𝐹 “ 𝐵 ) → { 𝐴 } ⊆ ( ◡ 𝐹 “ 𝐵 ) )
2 funimass2 ⊢ ( ( Fun 𝐹 ∧ { 𝐴 } ⊆ ( ◡ 𝐹 “ 𝐵 ) ) → ( 𝐹 “ { 𝐴 } ) ⊆ 𝐵 )
3 1 2 sylan2 ⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ ( ◡ 𝐹 “ 𝐵 ) ) → ( 𝐹 “ { 𝐴 } ) ⊆ 𝐵 )
4 fvex ⊢ ( 𝐹 ‘ 𝐴 ) ∈ V
5 4 snss ⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 ↔ { ( 𝐹 ‘ 𝐴 ) } ⊆ 𝐵 )
6 cnvimass ⊢ ( ◡ 𝐹 “ 𝐵 ) ⊆ dom 𝐹
7 6 sseli ⊢ ( 𝐴 ∈ ( ◡ 𝐹 “ 𝐵 ) → 𝐴 ∈ dom 𝐹 )
8 funfn ⊢ ( Fun 𝐹 ↔ 𝐹 Fn dom 𝐹 )
9 fnsnfv ⊢ ( ( 𝐹 Fn dom 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → { ( 𝐹 ‘ 𝐴 ) } = ( 𝐹 “ { 𝐴 } ) )
10 8 9 sylanb ⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → { ( 𝐹 ‘ 𝐴 ) } = ( 𝐹 “ { 𝐴 } ) )
11 7 10 sylan2 ⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ ( ◡ 𝐹 “ 𝐵 ) ) → { ( 𝐹 ‘ 𝐴 ) } = ( 𝐹 “ { 𝐴 } ) )
12 11 sseq1d ⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ ( ◡ 𝐹 “ 𝐵 ) ) → ( { ( 𝐹 ‘ 𝐴 ) } ⊆ 𝐵 ↔ ( 𝐹 “ { 𝐴 } ) ⊆ 𝐵 ) )
13 5 12 bitrid ⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ ( ◡ 𝐹 “ 𝐵 ) ) → ( ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 ↔ ( 𝐹 “ { 𝐴 } ) ⊆ 𝐵 ) )
14 3 13 mpbird ⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ ( ◡ 𝐹 “ 𝐵 ) ) → ( 𝐹 ‘ 𝐴 ) ∈ 𝐵 )