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 syl5bb ( 𝐴 ∈ V → ( 𝐴 ∈ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) ↔ ∃! 𝑥 𝐴 𝐹 𝑥 ) )
14 13 notbid ( 𝐴 ∈ V → ( ¬ 𝐴 ∈ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) ↔ ¬ ∃! 𝑥 𝐴 𝐹 𝑥 ) )
15 tz6.12-2 ( ¬ ∃! 𝑥 𝐴 𝐹 𝑥 → ( 𝐹𝐴 ) = ∅ )
16 14 15 syl6bi ( 𝐴 ∈ 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 𝐹𝐴 ) = ( 𝐹𝐴 )