Metamath Proof Explorer

Theorem funpartfun

Description: The functional part of F is a function. (Contributed by Scott Fenton, 16-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014) (Proof shortened by Peter Mazsa, 2-Oct-2022)

Ref Expression
Assertion funpartfun Fun Funpart 𝐹

Proof

Step Hyp Ref Expression
1 relres ⊢ Rel ( 𝐹 ↾ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) )
2 vex ⊢ 𝑧 ∈ V
3 2 brresi ⊢ ( 𝑥 ( 𝐹 ↾ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) ) 𝑧 ↔ ( 𝑥 ∈ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) ∧ 𝑥 𝐹 𝑧 ) )
4 3 simprbi ⊢ ( 𝑥 ( 𝐹 ↾ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) ) 𝑧 → 𝑥 𝐹 𝑧 )
5 vex ⊢ 𝑦 ∈ V
6 5 brresi ⊢ ( 𝑥 ( 𝐹 ↾ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) ) 𝑦 ↔ ( 𝑥 ∈ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) ∧ 𝑥 𝐹 𝑦 ) )
7 funpartlem ⊢ ( 𝑥 ∈ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) ↔ ∃ 𝑤 ( 𝐹 “ { 𝑥 } ) = { 𝑤 } )
8 7 anbi1i ⊢ ( ( 𝑥 ∈ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) ∧ 𝑥 𝐹 𝑦 ) ↔ ( ∃ 𝑤 ( 𝐹 “ { 𝑥 } ) = { 𝑤 } ∧ 𝑥 𝐹 𝑦 ) )
9 6 8 bitri ⊢ ( 𝑥 ( 𝐹 ↾ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) ) 𝑦 ↔ ( ∃ 𝑤 ( 𝐹 “ { 𝑥 } ) = { 𝑤 } ∧ 𝑥 𝐹 𝑦 ) )
10 df-br ⊢ ( 𝑥 𝐹 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 )
11 df-br ⊢ ( 𝑥 𝐹 𝑧 ↔ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 )
12 10 11 anbi12i ⊢ ( ( 𝑥 𝐹 𝑦 ∧ 𝑥 𝐹 𝑧 ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) )
13 vex ⊢ 𝑥 ∈ V
14 13 5 elimasn ⊢ ( 𝑦 ∈ ( 𝐹 “ { 𝑥 } ) ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 )
15 13 2 elimasn ⊢ ( 𝑧 ∈ ( 𝐹 “ { 𝑥 } ) ↔ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 )
16 14 15 anbi12i ⊢ ( ( 𝑦 ∈ ( 𝐹 “ { 𝑥 } ) ∧ 𝑧 ∈ ( 𝐹 “ { 𝑥 } ) ) ↔ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ 𝐹 ∧ ⟨ 𝑥 , 𝑧 ⟩ ∈ 𝐹 ) )
17 12 16 bitr4i ⊢ ( ( 𝑥 𝐹 𝑦 ∧ 𝑥 𝐹 𝑧 ) ↔ ( 𝑦 ∈ ( 𝐹 “ { 𝑥 } ) ∧ 𝑧 ∈ ( 𝐹 “ { 𝑥 } ) ) )
18 eleq2 ⊢ ( ( 𝐹 “ { 𝑥 } ) = { 𝑤 } → ( 𝑦 ∈ ( 𝐹 “ { 𝑥 } ) ↔ 𝑦 ∈ { 𝑤 } ) )
19 eleq2 ⊢ ( ( 𝐹 “ { 𝑥 } ) = { 𝑤 } → ( 𝑧 ∈ ( 𝐹 “ { 𝑥 } ) ↔ 𝑧 ∈ { 𝑤 } ) )
20 18 19 anbi12d ⊢ ( ( 𝐹 “ { 𝑥 } ) = { 𝑤 } → ( ( 𝑦 ∈ ( 𝐹 “ { 𝑥 } ) ∧ 𝑧 ∈ ( 𝐹 “ { 𝑥 } ) ) ↔ ( 𝑦 ∈ { 𝑤 } ∧ 𝑧 ∈ { 𝑤 } ) ) )
21 velsn ⊢ ( 𝑦 ∈ { 𝑤 } ↔ 𝑦 = 𝑤 )
22 velsn ⊢ ( 𝑧 ∈ { 𝑤 } ↔ 𝑧 = 𝑤 )
23 equtr2 ⊢ ( ( 𝑦 = 𝑤 ∧ 𝑧 = 𝑤 ) → 𝑦 = 𝑧 )
24 21 22 23 syl2anb ⊢ ( ( 𝑦 ∈ { 𝑤 } ∧ 𝑧 ∈ { 𝑤 } ) → 𝑦 = 𝑧 )
25 20 24 syl6bi ⊢ ( ( 𝐹 “ { 𝑥 } ) = { 𝑤 } → ( ( 𝑦 ∈ ( 𝐹 “ { 𝑥 } ) ∧ 𝑧 ∈ ( 𝐹 “ { 𝑥 } ) ) → 𝑦 = 𝑧 ) )
26 17 25 syl5bi ⊢ ( ( 𝐹 “ { 𝑥 } ) = { 𝑤 } → ( ( 𝑥 𝐹 𝑦 ∧ 𝑥 𝐹 𝑧 ) → 𝑦 = 𝑧 ) )
27 26 exlimiv ⊢ ( ∃ 𝑤 ( 𝐹 “ { 𝑥 } ) = { 𝑤 } → ( ( 𝑥 𝐹 𝑦 ∧ 𝑥 𝐹 𝑧 ) → 𝑦 = 𝑧 ) )
28 27 impl ⊢ ( ( ( ∃ 𝑤 ( 𝐹 “ { 𝑥 } ) = { 𝑤 } ∧ 𝑥 𝐹 𝑦 ) ∧ 𝑥 𝐹 𝑧 ) → 𝑦 = 𝑧 )
29 9 28 sylanb ⊢ ( ( 𝑥 ( 𝐹 ↾ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) ) 𝑦 ∧ 𝑥 𝐹 𝑧 ) → 𝑦 = 𝑧 )
30 4 29 sylan2 ⊢ ( ( 𝑥 ( 𝐹 ↾ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) ) 𝑦 ∧ 𝑥 ( 𝐹 ↾ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) ) 𝑧 ) → 𝑦 = 𝑧 )
31 30 gen2 ⊢ ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ( 𝐹 ↾ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) ) 𝑦 ∧ 𝑥 ( 𝐹 ↾ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) ) 𝑧 ) → 𝑦 = 𝑧 )
32 31 ax-gen ⊢ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ( 𝐹 ↾ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) ) 𝑦 ∧ 𝑥 ( 𝐹 ↾ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) ) 𝑧 ) → 𝑦 = 𝑧 )
33 df-funpart ⊢ Funpart 𝐹 = ( 𝐹 ↾ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) )
34 33 funeqi ⊢ ( Fun Funpart 𝐹 ↔ Fun ( 𝐹 ↾ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) ) )
35 dffun2 ⊢ ( Fun ( 𝐹 ↾ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) ) ↔ ( Rel ( 𝐹 ↾ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) ) ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ( 𝐹 ↾ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) ) 𝑦 ∧ 𝑥 ( 𝐹 ↾ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) ) 𝑧 ) → 𝑦 = 𝑧 ) ) )
36 34 35 bitri ⊢ ( Fun Funpart 𝐹 ↔ ( Rel ( 𝐹 ↾ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) ) ∧ ∀ 𝑥 ∀ 𝑦 ∀ 𝑧 ( ( 𝑥 ( 𝐹 ↾ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) ) 𝑦 ∧ 𝑥 ( 𝐹 ↾ dom ( ( Image 𝐹 ∘ Singleton ) ∩ ( V × Singletons ) ) ) 𝑧 ) → 𝑦 = 𝑧 ) ) )
37 1 32 36 mpbir2an ⊢ Fun Funpart 𝐹