Metamath Proof Explorer

Theorem funpartfv

Description: The function value of the functional part is identical to the original functional value. (Contributed by Scott Fenton, 17-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion funpartfv ( Funpart 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐴 )

Proof

Step Hyp Ref Expression
1 df-funpart ⊢ Funpart 𝐹 = ( 𝐹 ↾ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) )
2 1 fveq1i ⊢ ( Funpart 𝐹 ‘ 𝐴 ) = ( ( 𝐹 ↾ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) ) ‘ 𝐴 )
3 fvres ⊢ ( 𝐴 ∈ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) → ( ( 𝐹 ↾ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) ) ‘ 𝐴 ) = ( 𝐹 ‘ 𝐴 ) )
4 nfvres ⊢ ( ¬ 𝐴 ∈ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) → ( ( 𝐹 ↾ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) ) ‘ 𝐴 ) = ∅ )
5 funpartlem ⊢ ( 𝐴 ∈ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) ↔ ∃ 𝑥 ( 𝐹 “ { 𝐴 } ) = { 𝑥 } )
6 eusn ⊢ ( ∃! 𝑥 𝑥 ∈ ( 𝐹 “ { 𝐴 } ) ↔ ∃ 𝑥 ( 𝐹 “ { 𝐴 } ) = { 𝑥 } )
7 5 6 bitr4i ⊢ ( 𝐴 ∈ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) ↔ ∃! 𝑥 𝑥 ∈ ( 𝐹 “ { 𝐴 } ) )
8 elimasng ⊢ ( ( 𝐴 ∈ V ∧ 𝑥 ∈ V ) → ( 𝑥 ∈ ( 𝐹 “ { 𝐴 } ) ↔ ⟨ 𝐴 , 𝑥 ⟩ ∈ 𝐹 ) )
9 8 elvd ⊢ ( 𝐴 ∈ V → ( 𝑥 ∈ ( 𝐹 “ { 𝐴 } ) ↔ ⟨ 𝐴 , 𝑥 ⟩ ∈ 𝐹 ) )
10 df-br ⊢ ( 𝐴 𝐹 𝑥 ↔ ⟨ 𝐴 , 𝑥 ⟩ ∈ 𝐹 )
11 9 10 bitr4di ⊢ ( 𝐴 ∈ V → ( 𝑥 ∈ ( 𝐹 “ { 𝐴 } ) ↔ 𝐴 𝐹 𝑥 ) )
12 11 eubidv ⊢ ( 𝐴 ∈ V → ( ∃! 𝑥 𝑥 ∈ ( 𝐹 “ { 𝐴 } ) ↔ ∃! 𝑥 𝐴 𝐹 𝑥 ) )
13 7 12 bitrid ⊢ ( 𝐴 ∈ V → ( 𝐴 ∈ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) ↔ ∃! 𝑥 𝐴 𝐹 𝑥 ) )
14 13 notbid ⊢ ( 𝐴 ∈ V → ( ¬ 𝐴 ∈ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) ↔ ¬ ∃! 𝑥 𝐴 𝐹 𝑥 ) )
15 tz6.12-2 ⊢ ( ¬ ∃! 𝑥 𝐴 𝐹 𝑥 → ( 𝐹 ‘ 𝐴 ) = ∅ )
16 14 15 biimtrdi ⊢ ( 𝐴 ∈ V → ( ¬ 𝐴 ∈ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) → ( 𝐹 ‘ 𝐴 ) = ∅ ) )
17 fvprc ⊢ ( ¬ 𝐴 ∈ V → ( 𝐹 ‘ 𝐴 ) = ∅ )
18 17 a1d ⊢ ( ¬ 𝐴 ∈ V → ( ¬ 𝐴 ∈ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) → ( 𝐹 ‘ 𝐴 ) = ∅ ) )
19 16 18 pm2.61i ⊢ ( ¬ 𝐴 ∈ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) → ( 𝐹 ‘ 𝐴 ) = ∅ )
20 4 19 eqtr4d ⊢ ( ¬ 𝐴 ∈ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) → ( ( 𝐹 ↾ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) ) ‘ 𝐴 ) = ( 𝐹 ‘ 𝐴 ) )
21 3 20 pm2.61i ⊢ ( ( 𝐹 ↾ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) ) ‘ 𝐴 ) = ( 𝐹 ‘ 𝐴 )
22 2 21 eqtri ⊢ ( Funpart 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐴 )