ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  fsn Unicode version

Theorem fsn 5278
Description: A function maps a singleton to a singleton iff it is the singleton of an ordered pair. (Contributed by NM, 10-Dec-2003.)
Hypotheses
Ref Expression
fsn.1  _V
fsn.2  _V
Assertion
Ref Expression
fsn  F : { } --> { }  F  { <. ,  >. }

Proof of Theorem fsn
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 opelf 5005 . . . . . . . 8  F : { }
--> { }  <. ,  >.  F  { }  { }
2 elsn 3382 . . . . . . . . 9  { }
3 elsn 3382 . . . . . . . . 9  { }
42, 3anbi12i 433 . . . . . . . 8  { }  { }
51, 4sylib 127 . . . . . . 7  F : { }
--> { }  <. ,  >.  F
65ex 108 . . . . . 6  F : { } --> { }  <. ,  >.  F
7 fsn.1 . . . . . . . . . 10  _V
87snid 3394 . . . . . . . . 9  { }
9 feu 5015 . . . . . . . . 9  F : { }
--> { }  { }  { } <. ,  >.  F
108, 9mpan2 401 . . . . . . . 8  F : { } --> { }  { } <. , 
>.  F
113anbi1i 431 . . . . . . . . . . 11  { }  <. , 
>.  F  <. ,  >.  F
12 opeq2 3541 . . . . . . . . . . . . . 14  <. ,  >.  <. ,  >.
1312eleq1d 2103 . . . . . . . . . . . . 13  <. ,  >.  F  <. ,  >.  F
1413pm5.32i 427 . . . . . . . . . . . 12  <. ,  >.  F  <. ,  >.  F
15 ancom 253 . . . . . . . . . . . 12 
<. ,  >.  F  <. ,  >.  F
1614, 15bitr4i 176 . . . . . . . . . . 11  <. ,  >.  F  <. ,  >.  F
1711, 16bitr2i 174 . . . . . . . . . 10 
<. ,  >.  F  { }  <. , 
>.  F
1817eubii 1906 . . . . . . . . 9  <. ,  >.  F 
{ }  <. ,  >.  F
19 fsn.2 . . . . . . . . . . . 12  _V
2019eueq1 2707 . . . . . . . . . . 11
2120biantru 286 . . . . . . . . . 10  <. ,  >.  F  <. ,  >.  F
22 euanv 1954 . . . . . . . . . 10  <. ,  >.  F  <. ,  >.  F
2321, 22bitr4i 176 . . . . . . . . 9  <. ,  >.  F  <. ,  >.  F
24 df-reu 2307 . . . . . . . . 9  { } <. , 
>.  F  { }  <. ,  >.  F
2518, 23, 243bitr4i 201 . . . . . . . 8  <. ,  >.  F  { } <. , 
>.  F
2610, 25sylibr 137 . . . . . . 7  F : { } --> { }  <. ,  >.  F
27 opeq12 3542 . . . . . . . 8  <. , 
>.  <. ,  >.
2827eleq1d 2103 . . . . . . 7  <. , 
>.  F  <. ,  >.  F
2926, 28syl5ibrcom 146 . . . . . 6  F : { } --> { }  <. , 
>.  F
306, 29impbid 120 . . . . 5  F : { } --> { }  <. ,  >.  F
31 vex 2554 . . . . . . . 8 
_V
32 vex 2554 . . . . . . . 8 
_V
3331, 32opex 3957 . . . . . . 7  <. ,  >.  _V
3433elsnc 3390 . . . . . 6  <. ,  >.  { <. ,  >. } 
<. ,  >. 
<. ,  >.
357, 19opth2 3968 . . . . . 6  <. ,  >.  <. ,  >.
3634, 35bitr2i 174 . . . . 5  <. ,  >. 
{ <. ,  >. }
3730, 36syl6bb 185 . . . 4  F : { } --> { }  <. ,  >.  F  <. , 
>.  { <. ,  >. }
3837alrimivv 1752 . . 3  F : { } --> { }  <. ,  >.  F  <. ,  >. 
{ <. ,  >. }
39 frel 4992 . . . 4  F : { } --> { }  Rel  F
407, 19relsnop 4387 . . . 4  Rel  { <. ,  >. }
41 eqrel 4372 . . . 4  Rel  F  Rel  {
<. ,  >. }  F  { <. ,  >. }  <. ,  >.  F  <. ,  >. 
{ <. ,  >. }
4239, 40, 41sylancl 392 . . 3  F : { } --> { }  F  { <. ,  >. }  <. ,  >.  F  <. ,  >. 
{ <. ,  >. }
4338, 42mpbird 156 . 2  F : { } --> { }  F  { <. ,  >. }
447, 19f1osn 5109 . . . 4  { <. ,  >. } : { } -1-1-onto-> { }
45 f1oeq1 5060 . . . 4  F  { <. ,  >. }  F : { } -1-1-onto-> { }  { <. ,  >. } : { } -1-1-onto-> { }
4644, 45mpbiri 157 . . 3  F  { <. ,  >. }  F : { } -1-1-onto-> { }
47 f1of 5069 . . 3  F : { } -1-1-onto-> { }  F : { } --> { }
4846, 47syl 14 . 2  F  { <. ,  >. }  F : { } --> { }
4943, 48impbii 117 1  F : { } --> { }  F  { <. ,  >. }
Colors of variables: wff set class
Syntax hints:   wa 97   wb 98  wal 1240   wceq 1242   wcel 1390  weu 1897  wreu 2302   _Vcvv 2551   {csn 3367   <.cop 3370   Rel wrel 4293   -->wf 4841   -1-1-onto->wf1o 4844
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bndl 1396  ax-4 1397  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3866  ax-pow 3918  ax-pr 3935
This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-reu 2307  df-v 2553  df-un 2916  df-in 2918  df-ss 2925  df-pw 3353  df-sn 3373  df-pr 3374  df-op 3376  df-br 3756  df-opab 3810  df-id 4021  df-xp 4294  df-rel 4295  df-cnv 4296  df-co 4297  df-dm 4298  df-rn 4299  df-fun 4847  df-fn 4848  df-f 4849  df-f1 4850  df-fo 4851  df-f1o 4852
This theorem is referenced by:  fsng  5279
  Copyright terms: Public domain W3C validator