Metamath Proof Explorer


Theorem fnsingle

Description: The singleton relationship is a function over the universe. (Contributed by Scott Fenton, 4-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Assertion fnsingle βŠ’π–²π—‚π—‡π—€π—…π–Ύπ—π—ˆπ—‡FnV

Proof

Step Hyp Ref Expression
1 difss ⊒VΓ—Vβˆ–ran⁑VβŠ—Eβˆ†IβŠ—VβŠ†VΓ—V
2 df-rel ⊒Rel⁑VΓ—Vβˆ–ran⁑VβŠ—Eβˆ†IβŠ—V↔VΓ—Vβˆ–ran⁑VβŠ—Eβˆ†IβŠ—VβŠ†VΓ—V
3 1 2 mpbir ⊒Rel⁑VΓ—Vβˆ–ran⁑VβŠ—Eβˆ†IβŠ—V
4 df-singleton βŠ’π–²π—‚π—‡π—€π—…π–Ύπ—π—ˆπ—‡=VΓ—Vβˆ–ran⁑VβŠ—Eβˆ†IβŠ—V
5 4 releqi ⊒Relβ‘π–²π—‚π—‡π—€π—…π–Ύπ—π—ˆπ—‡β†”Rel⁑VΓ—Vβˆ–ran⁑VβŠ—Eβˆ†IβŠ—V
6 3 5 mpbir ⊒Relβ‘π–²π—‚π—‡π—€π—…π–Ύπ—π—ˆπ—‡
7 vex ⊒x∈V
8 vex ⊒y∈V
9 7 8 brsingle ⊒xπ–²π—‚π—‡π—€π—…π–Ύπ—π—ˆπ—‡y↔y=x
10 vex ⊒z∈V
11 7 10 brsingle ⊒xπ–²π—‚π—‡π—€π—…π–Ύπ—π—ˆπ—‡z↔z=x
12 eqtr3 ⊒y=x∧z=xβ†’y=z
13 9 11 12 syl2anb ⊒xπ–²π—‚π—‡π—€π—…π–Ύπ—π—ˆπ—‡y∧xπ–²π—‚π—‡π—€π—…π–Ύπ—π—ˆπ—‡zβ†’y=z
14 13 ax-gen βŠ’βˆ€zxπ–²π—‚π—‡π—€π—…π–Ύπ—π—ˆπ—‡y∧xπ–²π—‚π—‡π—€π—…π–Ύπ—π—ˆπ—‡zβ†’y=z
15 14 gen2 βŠ’βˆ€xβˆ€yβˆ€zxπ–²π—‚π—‡π—€π—…π–Ύπ—π—ˆπ—‡y∧xπ–²π—‚π—‡π—€π—…π–Ύπ—π—ˆπ—‡zβ†’y=z
16 dffun2 ⊒Funβ‘π–²π—‚π—‡π—€π—…π–Ύπ—π—ˆπ—‡β†”Relβ‘π–²π—‚π—‡π—€π—…π–Ύπ—π—ˆπ—‡βˆ§βˆ€xβˆ€yβˆ€zxπ–²π—‚π—‡π—€π—…π–Ύπ—π—ˆπ—‡y∧xπ–²π—‚π—‡π—€π—…π–Ύπ—π—ˆπ—‡zβ†’y=z
17 6 15 16 mpbir2an ⊒Funβ‘π–²π—‚π—‡π—€π—…π–Ύπ—π—ˆπ—‡
18 eqv ⊒domβ‘π–²π—‚π—‡π—€π—…π–Ύπ—π—ˆπ—‡=Vβ†”βˆ€xx∈domβ‘π–²π—‚π—‡π—€π—…π–Ύπ—π—ˆπ—‡
19 eqid ⊒x=x
20 snex ⊒x∈V
21 7 20 brsingle ⊒xπ–²π—‚π—‡π—€π—…π–Ύπ—π—ˆπ—‡x↔x=x
22 19 21 mpbir ⊒xπ–²π—‚π—‡π—€π—…π–Ύπ—π—ˆπ—‡x
23 breq2 ⊒y=xβ†’xπ–²π—‚π—‡π—€π—…π–Ύπ—π—ˆπ—‡y↔xπ–²π—‚π—‡π—€π—…π–Ύπ—π—ˆπ—‡x
24 20 23 spcev ⊒xπ–²π—‚π—‡π—€π—…π–Ύπ—π—ˆπ—‡xβ†’βˆƒyxπ–²π—‚π—‡π—€π—…π–Ύπ—π—ˆπ—‡y
25 22 24 ax-mp βŠ’βˆƒyxπ–²π—‚π—‡π—€π—…π–Ύπ—π—ˆπ—‡y
26 7 eldm ⊒x∈domβ‘π–²π—‚π—‡π—€π—…π–Ύπ—π—ˆπ—‡β†”βˆƒyxπ–²π—‚π—‡π—€π—…π–Ύπ—π—ˆπ—‡y
27 25 26 mpbir ⊒x∈domβ‘π–²π—‚π—‡π—€π—…π–Ύπ—π—ˆπ—‡
28 18 27 mpgbir ⊒domβ‘π–²π—‚π—‡π—€π—…π–Ύπ—π—ˆπ—‡=V
29 df-fn βŠ’π–²π—‚π—‡π—€π—…π–Ύπ—π—ˆπ—‡FnV↔Funβ‘π–²π—‚π—‡π—€π—…π–Ύπ—π—ˆπ—‡βˆ§domβ‘π–²π—‚π—‡π—€π—…π–Ύπ—π—ˆπ—‡=V
30 17 28 29 mpbir2an βŠ’π–²π—‚π—‡π—€π—…π–Ύπ—π—ˆπ—‡FnV