Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-oriso Unicode version

Definition df-oriso 25210
Description: Order isomorphisms. Experimental. Bourbaki E.III.5 (Contributed by FL, 17-Nov-2014.)
Assertion
Ref Expression
df-oriso  |-  OrIso  =  ( r  e.  _V , 
s  e.  _V  |->  { f  |  ( f : ( Base `  r
)
-1-1-onto-> ( Base `  s )  /\  A. a  e.  (
Base `  r ) A. b  e.  ( Base `  r ) ( a ( le `  r ) b  <->  ( f `  a ) ( le
`  s ) ( f `  b ) ) ) } )
Distinct variable group:    s, r, f, a, b

Detailed syntax breakdown of Definition df-oriso
StepHypRef Expression
1 coriso 25208 . 2  class  OrIso
2 vr . . 3  set  r
3 vs . . 3  set  s
4 cvv 2788 . . 3  class  _V
52cv 1622 . . . . . . 7  class  r
6 cbs 13148 . . . . . . 7  class  Base
75, 6cfv 5255 . . . . . 6  class  ( Base `  r )
83cv 1622 . . . . . . 7  class  s
98, 6cfv 5255 . . . . . 6  class  ( Base `  s )
10 vf . . . . . . 7  set  f
1110cv 1622 . . . . . 6  class  f
127, 9, 11wf1o 5254 . . . . 5  wff  f : ( Base `  r
)
-1-1-onto-> ( Base `  s )
13 va . . . . . . . . . 10  set  a
1413cv 1622 . . . . . . . . 9  class  a
15 vb . . . . . . . . . 10  set  b
1615cv 1622 . . . . . . . . 9  class  b
17 cple 13215 . . . . . . . . . 10  class  le
185, 17cfv 5255 . . . . . . . . 9  class  ( le
`  r )
1914, 16, 18wbr 4023 . . . . . . . 8  wff  a ( le `  r ) b
2014, 11cfv 5255 . . . . . . . . 9  class  ( f `
 a )
2116, 11cfv 5255 . . . . . . . . 9  class  ( f `
 b )
228, 17cfv 5255 . . . . . . . . 9  class  ( le
`  s )
2320, 21, 22wbr 4023 . . . . . . . 8  wff  ( f `
 a ) ( le `  s ) ( f `  b
)
2419, 23wb 176 . . . . . . 7  wff  ( a ( le `  r
) b  <->  ( f `  a ) ( le
`  s ) ( f `  b ) )
2524, 15, 7wral 2543 . . . . . 6  wff  A. b  e.  ( Base `  r
) ( a ( le `  r ) b  <->  ( f `  a ) ( le
`  s ) ( f `  b ) )
2625, 13, 7wral 2543 . . . . 5  wff  A. a  e.  ( Base `  r
) A. b  e.  ( Base `  r
) ( a ( le `  r ) b  <->  ( f `  a ) ( le
`  s ) ( f `  b ) )
2712, 26wa 358 . . . 4  wff  ( f : ( Base `  r
)
-1-1-onto-> ( Base `  s )  /\  A. a  e.  (
Base `  r ) A. b  e.  ( Base `  r ) ( a ( le `  r ) b  <->  ( f `  a ) ( le
`  s ) ( f `  b ) ) )
2827, 10cab 2269 . . 3  class  { f  |  ( f : ( Base `  r
)
-1-1-onto-> ( Base `  s )  /\  A. a  e.  (
Base `  r ) A. b  e.  ( Base `  r ) ( a ( le `  r ) b  <->  ( f `  a ) ( le
`  s ) ( f `  b ) ) ) }
292, 3, 4, 4, 28cmpt2 5860 . 2  class  ( r  e.  _V ,  s  e.  _V  |->  { f  |  ( f : ( Base `  r
)
-1-1-onto-> ( Base `  s )  /\  A. a  e.  (
Base `  r ) A. b  e.  ( Base `  r ) ( a ( le `  r ) b  <->  ( f `  a ) ( le
`  s ) ( f `  b ) ) ) } )
301, 29wceq 1623 1  wff  OrIso  =  ( r  e.  _V , 
s  e.  _V  |->  { f  |  ( f : ( Base `  r
)
-1-1-onto-> ( Base `  s )  /\  A. a  e.  (
Base `  r ) A. b  e.  ( Base `  r ) ( a ( le `  r ) b  <->  ( f `  a ) ( le
`  s ) ( f `  b ) ) ) } )
Colors of variables: wff set class
This definition is referenced by:  isoriso  25212
  Copyright terms: Public domain W3C validator