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

Metamath Proof Explorer

Theorem funfvima3

Description: A class including a function contains the function's value in the image of the singleton of the argument. (Contributed by NM, 23-Mar-2004)

Ref Expression
Assertion funfvima3 ( ( Fun 𝐹 ∧ 𝐹 ⊆ 𝐺 ) → ( 𝐴 ∈ dom 𝐹 → ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐺 “ { 𝐴 } ) ) )

Proof

Step Hyp Ref Expression
1 ssel ⊢ ( 𝐹 ⊆ 𝐺 → ( ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ ∈ 𝐹 → ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ ∈ 𝐺 ) )
2 funfvop ⊢ ( ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) → ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ ∈ 𝐹 )
3 1 2 impel ⊢ ( ( 𝐹 ⊆ 𝐺 ∧ ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) ) → ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ ∈ 𝐺 )
4 sneq ⊢ ( 𝑥 = 𝐴 → { 𝑥 } = { 𝐴 } )
5 4 imaeq2d ⊢ ( 𝑥 = 𝐴 → ( 𝐺 “ { 𝑥 } ) = ( 𝐺 “ { 𝐴 } ) )
6 5 eleq2d ⊢ ( 𝑥 = 𝐴 → ( ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐺 “ { 𝑥 } ) ↔ ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐺 “ { 𝐴 } ) ) )
7 opeq1 ⊢ ( 𝑥 = 𝐴 → ⟨ 𝑥 , ( 𝐹 ‘ 𝐴 ) ⟩ = ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ )
8 7 eleq1d ⊢ ( 𝑥 = 𝐴 → ( ⟨ 𝑥 , ( 𝐹 ‘ 𝐴 ) ⟩ ∈ 𝐺 ↔ ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ ∈ 𝐺 ) )
9 vex ⊢ 𝑥 ∈ V
10 fvex ⊢ ( 𝐹 ‘ 𝐴 ) ∈ V
11 9 10 elimasn ⊢ ( ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐺 “ { 𝑥 } ) ↔ ⟨ 𝑥 , ( 𝐹 ‘ 𝐴 ) ⟩ ∈ 𝐺 )
12 6 8 11 vtoclbg ⊢ ( 𝐴 ∈ dom 𝐹 → ( ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐺 “ { 𝐴 } ) ↔ ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ ∈ 𝐺 ) )
13 12 ad2antll ⊢ ( ( 𝐹 ⊆ 𝐺 ∧ ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) ) → ( ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐺 “ { 𝐴 } ) ↔ ⟨ 𝐴 , ( 𝐹 ‘ 𝐴 ) ⟩ ∈ 𝐺 ) )
14 3 13 mpbird ⊢ ( ( 𝐹 ⊆ 𝐺 ∧ ( Fun 𝐹 ∧ 𝐴 ∈ dom 𝐹 ) ) → ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐺 “ { 𝐴 } ) )
15 14 exp32 ⊢ ( 𝐹 ⊆ 𝐺 → ( Fun 𝐹 → ( 𝐴 ∈ dom 𝐹 → ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐺 “ { 𝐴 } ) ) ) )
16 15 impcom ⊢ ( ( Fun 𝐹 ∧ 𝐹 ⊆ 𝐺 ) → ( 𝐴 ∈ dom 𝐹 → ( 𝐹 ‘ 𝐴 ) ∈ ( 𝐺 “ { 𝐴 } ) ) )