Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fnsingle Structured version   Visualization version   Unicode version

Theorem fnsingle 30686
Description: The singleton relationship is a function over the universe. (Contributed by Scott Fenton, 4-Apr-2014.) (Revised by Mario Carneiro, 19-Apr-2014.)
Assertion
Ref Expression
fnsingle  |- Singleton  Fn  _V

Proof of Theorem fnsingle
Dummy variables  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 difss 3560 . . . . 5  |-  ( ( _V  X.  _V )  \  ran  ( ( _V 
(x)  _E  )  /_\  (  _I 
(x)  _V ) ) ) 
C_  ( _V  X.  _V )
2 df-rel 4841 . . . . 5  |-  ( Rel  ( ( _V  X.  _V )  \  ran  (
( _V  (x)  _E  )  /_\  (  _I  (x)  _V ) ) )  <->  ( ( _V  X.  _V )  \  ran  ( ( _V  (x)  _E  )  /_\  (  _I  (x)  _V ) ) )  C_  ( _V  X.  _V )
)
31, 2mpbir 213 . . . 4  |-  Rel  (
( _V  X.  _V )  \  ran  ( ( _V  (x)  _E  )  /_\  (  _I  (x)  _V ) ) )
4 df-singleton 30628 . . . . 5  |- Singleton  =  ( ( _V  X.  _V )  \  ran  ( ( _V  (x)  _E  )  /_\  (  _I  (x)  _V ) ) )
54releqi 4918 . . . 4  |-  ( Rel Singleton  <->  Rel  ( ( _V  X.  _V )  \  ran  (
( _V  (x)  _E  )  /_\  (  _I  (x)  _V ) ) ) )
63, 5mpbir 213 . . 3  |-  Rel Singleton
7 vex 3048 . . . . . . 7  |-  x  e. 
_V
8 vex 3048 . . . . . . 7  |-  y  e. 
_V
97, 8brsingle 30684 . . . . . 6  |-  ( xSingleton
y  <->  y  =  {
x } )
10 vex 3048 . . . . . . 7  |-  z  e. 
_V
117, 10brsingle 30684 . . . . . 6  |-  ( xSingleton
z  <->  z  =  {
x } )
12 eqtr3 2472 . . . . . 6  |-  ( ( y  =  { x }  /\  z  =  {
x } )  -> 
y  =  z )
139, 11, 12syl2anb 482 . . . . 5  |-  ( ( xSingleton y  /\  xSingleton z )  ->  y  =  z )
1413ax-gen 1669 . . . 4  |-  A. z
( ( xSingleton y  /\  xSingleton z )  -> 
y  =  z )
1514gen2 1670 . . 3  |-  A. x A. y A. z ( ( xSingleton y  /\  xSingleton z )  ->  y  =  z )
16 dffun2 5592 . . 3  |-  ( Fun Singleton  <->  ( Rel Singleton 
/\  A. x A. y A. z ( ( xSingleton
y  /\  xSingleton z )  ->  y  =  z ) ) )
176, 15, 16mpbir2an 931 . 2  |-  Fun Singleton
18 eqv 3748 . . 3  |-  ( dom Singleton  =  _V  <->  A. x  x  e. 
dom Singleton )
19 eqid 2451 . . . . . 6  |-  { x }  =  { x }
20 snex 4641 . . . . . . 7  |-  { x }  e.  _V
217, 20brsingle 30684 . . . . . 6  |-  ( xSingleton { x }  <->  { x }  =  { x } )
2219, 21mpbir 213 . . . . 5  |-  xSingleton { x }
23 breq2 4406 . . . . . 6  |-  ( y  =  { x }  ->  ( xSingleton y  <->  xSingleton { x } ) )
2420, 23spcev 3141 . . . . 5  |-  ( xSingleton { x }  ->  E. y  xSingleton y )
2522, 24ax-mp 5 . . . 4  |-  E. y  xSingleton y
267eldm 5032 . . . 4  |-  ( x  e.  dom Singleton  <->  E. y  xSingleton y
)
2725, 26mpbir 213 . . 3  |-  x  e. 
dom Singleton
2818, 27mpgbir 1673 . 2  |-  dom Singleton  =  _V
29 df-fn 5585 . 2  |-  (Singleton  Fn  _V 
<->  ( Fun Singleton  /\  dom Singleton  =  _V ) )
3017, 28, 29mpbir2an 931 1  |- Singleton  Fn  _V
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 371   A.wal 1442    = wceq 1444   E.wex 1663    e. wcel 1887   _Vcvv 3045    \ cdif 3401    C_ wss 3404    /_\ csymdif 3662   {csn 3968   class class class wbr 4402    _E cep 4743    _I cid 4744    X. cxp 4832   dom cdm 4834   ran crn 4835   Rel wrel 4839   Fun wfun 5576    Fn wfn 5577    (x) ctxp 30596  Singletoncsingle 30604
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-rab 2746  df-v 3047  df-sbc 3268  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-symdif 3663  df-nul 3732  df-if 3882  df-sn 3969  df-pr 3971  df-op 3975  df-uni 4199  df-br 4403  df-opab 4462  df-mpt 4463  df-eprel 4745  df-id 4749  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-fo 5588  df-fv 5590  df-1st 6793  df-2nd 6794  df-txp 30620  df-singleton 30628
This theorem is referenced by:  fvsingle  30687
  Copyright terms: Public domain W3C validator