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

Theorem dfon2 24148
Description:  On consists of all sets that contain all its transitive proper subsets. This definition comes from J. R. Isbell, "A Definition of Ordinal Numbers," American Mathematical Monthly, vol 67 (1960), pp. 51-52. (Contributed by Scott Fenton, 20-Feb-2011.)
Assertion
Ref Expression
dfon2  |-  On  =  { x  |  A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x ) }
Distinct variable group:    x, y

Proof of Theorem dfon2
Dummy variables  z  w  t  u  v are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-on 4396 . 2  |-  On  =  { x  |  Ord  x }
2 tz7.7 4418 . . . . . . . . 9  |-  ( ( Ord  x  /\  Tr  y )  ->  (
y  e.  x  <->  ( y  C_  x  /\  y  =/=  x ) ) )
3 df-pss 3168 . . . . . . . . 9  |-  ( y 
C.  x  <->  ( y  C_  x  /\  y  =/=  x ) )
42, 3syl6bbr 254 . . . . . . . 8  |-  ( ( Ord  x  /\  Tr  y )  ->  (
y  e.  x  <->  y  C.  x ) )
54exbiri 605 . . . . . . 7  |-  ( Ord  x  ->  ( Tr  y  ->  ( y  C.  x  ->  y  e.  x
) ) )
65com23 72 . . . . . 6  |-  ( Ord  x  ->  ( y  C.  x  ->  ( Tr  y  ->  y  e.  x ) ) )
76imp3a 420 . . . . 5  |-  ( Ord  x  ->  ( (
y  C.  x  /\  Tr  y )  ->  y  e.  x ) )
87alrimiv 1617 . . . 4  |-  ( Ord  x  ->  A. y
( ( y  C.  x  /\  Tr  y )  ->  y  e.  x
) )
9 vex 2791 . . . . . . 7  |-  x  e. 
_V
10 dfon2lem3 24141 . . . . . . 7  |-  ( x  e.  _V  ->  ( A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x )  ->  ( Tr  x  /\  A. z  e.  x  -.  z  e.  z ) ) )
119, 10ax-mp 8 . . . . . 6  |-  ( A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x )  ->  ( Tr  x  /\  A. z  e.  x  -.  z  e.  z ) )
1211simpld 445 . . . . 5  |-  ( A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x )  ->  Tr  x )
139dfon2lem7 24145 . . . . . . . 8  |-  ( A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x )  ->  (
t  e.  x  ->  A. u ( ( u 
C.  t  /\  Tr  u )  ->  u  e.  t ) ) )
1413ralrimiv 2625 . . . . . . 7  |-  ( A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x )  ->  A. t  e.  x  A. u
( ( u  C.  t  /\  Tr  u )  ->  u  e.  t ) )
15 dfon2lem9 24147 . . . . . . . 8  |-  ( A. t  e.  x  A. u ( ( u 
C.  t  /\  Tr  u )  ->  u  e.  t )  ->  _E  Fr  x )
16 psseq2 3264 . . . . . . . . . . . . . . . 16  |-  ( t  =  z  ->  (
u  C.  t  <->  u  C.  z ) )
1716anbi1d 685 . . . . . . . . . . . . . . 15  |-  ( t  =  z  ->  (
( u  C.  t  /\  Tr  u )  <->  ( u  C.  z  /\  Tr  u
) ) )
18 elequ2 1689 . . . . . . . . . . . . . . 15  |-  ( t  =  z  ->  (
u  e.  t  <->  u  e.  z ) )
1917, 18imbi12d 311 . . . . . . . . . . . . . 14  |-  ( t  =  z  ->  (
( ( u  C.  t  /\  Tr  u )  ->  u  e.  t )  <->  ( ( u 
C.  z  /\  Tr  u )  ->  u  e.  z ) ) )
2019albidv 1611 . . . . . . . . . . . . 13  |-  ( t  =  z  ->  ( A. u ( ( u 
C.  t  /\  Tr  u )  ->  u  e.  t )  <->  A. u
( ( u  C.  z  /\  Tr  u )  ->  u  e.  z ) ) )
21 psseq1 3263 . . . . . . . . . . . . . . . 16  |-  ( u  =  v  ->  (
u  C.  z  <->  v  C.  z ) )
22 treq 4119 . . . . . . . . . . . . . . . 16  |-  ( u  =  v  ->  ( Tr  u  <->  Tr  v )
)
2321, 22anbi12d 691 . . . . . . . . . . . . . . 15  |-  ( u  =  v  ->  (
( u  C.  z  /\  Tr  u )  <->  ( v  C.  z  /\  Tr  v
) ) )
24 elequ1 1687 . . . . . . . . . . . . . . 15  |-  ( u  =  v  ->  (
u  e.  z  <->  v  e.  z ) )
2523, 24imbi12d 311 . . . . . . . . . . . . . 14  |-  ( u  =  v  ->  (
( ( u  C.  z  /\  Tr  u )  ->  u  e.  z )  <->  ( ( v 
C.  z  /\  Tr  v )  ->  v  e.  z ) ) )
2625cbvalv 1942 . . . . . . . . . . . . 13  |-  ( A. u ( ( u 
C.  z  /\  Tr  u )  ->  u  e.  z )  <->  A. v
( ( v  C.  z  /\  Tr  v )  ->  v  e.  z ) )
2720, 26syl6bb 252 . . . . . . . . . . . 12  |-  ( t  =  z  ->  ( A. u ( ( u 
C.  t  /\  Tr  u )  ->  u  e.  t )  <->  A. v
( ( v  C.  z  /\  Tr  v )  ->  v  e.  z ) ) )
2827rspccv 2881 . . . . . . . . . . 11  |-  ( A. t  e.  x  A. u ( ( u 
C.  t  /\  Tr  u )  ->  u  e.  t )  ->  (
z  e.  x  ->  A. v ( ( v 
C.  z  /\  Tr  v )  ->  v  e.  z ) ) )
29 psseq2 3264 . . . . . . . . . . . . . . . 16  |-  ( t  =  w  ->  (
u  C.  t  <->  u  C.  w ) )
3029anbi1d 685 . . . . . . . . . . . . . . 15  |-  ( t  =  w  ->  (
( u  C.  t  /\  Tr  u )  <->  ( u  C.  w  /\  Tr  u
) ) )
31 elequ2 1689 . . . . . . . . . . . . . . 15  |-  ( t  =  w  ->  (
u  e.  t  <->  u  e.  w ) )
3230, 31imbi12d 311 . . . . . . . . . . . . . 14  |-  ( t  =  w  ->  (
( ( u  C.  t  /\  Tr  u )  ->  u  e.  t )  <->  ( ( u 
C.  w  /\  Tr  u )  ->  u  e.  w ) ) )
3332albidv 1611 . . . . . . . . . . . . 13  |-  ( t  =  w  ->  ( A. u ( ( u 
C.  t  /\  Tr  u )  ->  u  e.  t )  <->  A. u
( ( u  C.  w  /\  Tr  u )  ->  u  e.  w
) ) )
34 psseq1 3263 . . . . . . . . . . . . . . . 16  |-  ( u  =  y  ->  (
u  C.  w  <->  y  C.  w ) )
35 treq 4119 . . . . . . . . . . . . . . . 16  |-  ( u  =  y  ->  ( Tr  u  <->  Tr  y )
)
3634, 35anbi12d 691 . . . . . . . . . . . . . . 15  |-  ( u  =  y  ->  (
( u  C.  w  /\  Tr  u )  <->  ( y  C.  w  /\  Tr  y
) ) )
37 elequ1 1687 . . . . . . . . . . . . . . 15  |-  ( u  =  y  ->  (
u  e.  w  <->  y  e.  w ) )
3836, 37imbi12d 311 . . . . . . . . . . . . . 14  |-  ( u  =  y  ->  (
( ( u  C.  w  /\  Tr  u )  ->  u  e.  w
)  <->  ( ( y 
C.  w  /\  Tr  y )  ->  y  e.  w ) ) )
3938cbvalv 1942 . . . . . . . . . . . . 13  |-  ( A. u ( ( u 
C.  w  /\  Tr  u )  ->  u  e.  w )  <->  A. y
( ( y  C.  w  /\  Tr  y )  ->  y  e.  w
) )
4033, 39syl6bb 252 . . . . . . . . . . . 12  |-  ( t  =  w  ->  ( A. u ( ( u 
C.  t  /\  Tr  u )  ->  u  e.  t )  <->  A. y
( ( y  C.  w  /\  Tr  y )  ->  y  e.  w
) ) )
4140rspccv 2881 . . . . . . . . . . 11  |-  ( A. t  e.  x  A. u ( ( u 
C.  t  /\  Tr  u )  ->  u  e.  t )  ->  (
w  e.  x  ->  A. y ( ( y 
C.  w  /\  Tr  y )  ->  y  e.  w ) ) )
4228, 41anim12d 546 . . . . . . . . . 10  |-  ( A. t  e.  x  A. u ( ( u 
C.  t  /\  Tr  u )  ->  u  e.  t )  ->  (
( z  e.  x  /\  w  e.  x
)  ->  ( A. v ( ( v 
C.  z  /\  Tr  v )  ->  v  e.  z )  /\  A. y ( ( y 
C.  w  /\  Tr  y )  ->  y  e.  w ) ) ) )
43 vex 2791 . . . . . . . . . . 11  |-  z  e. 
_V
44 vex 2791 . . . . . . . . . . 11  |-  w  e. 
_V
4543, 44dfon2lem5 24143 . . . . . . . . . 10  |-  ( ( A. v ( ( v  C.  z  /\  Tr  v )  ->  v  e.  z )  /\  A. y ( ( y 
C.  w  /\  Tr  y )  ->  y  e.  w ) )  -> 
( z  e.  w  \/  z  =  w  \/  w  e.  z
) )
4642, 45syl6 29 . . . . . . . . 9  |-  ( A. t  e.  x  A. u ( ( u 
C.  t  /\  Tr  u )  ->  u  e.  t )  ->  (
( z  e.  x  /\  w  e.  x
)  ->  ( z  e.  w  \/  z  =  w  \/  w  e.  z ) ) )
4746ralrimivv 2634 . . . . . . . 8  |-  ( A. t  e.  x  A. u ( ( u 
C.  t  /\  Tr  u )  ->  u  e.  t )  ->  A. z  e.  x  A. w  e.  x  ( z  e.  w  \/  z  =  w  \/  w  e.  z ) )
4815, 47jca 518 . . . . . . 7  |-  ( A. t  e.  x  A. u ( ( u 
C.  t  /\  Tr  u )  ->  u  e.  t )  ->  (  _E  Fr  x  /\  A. z  e.  x  A. w  e.  x  (
z  e.  w  \/  z  =  w  \/  w  e.  z ) ) )
4914, 48syl 15 . . . . . 6  |-  ( A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x )  ->  (  _E  Fr  x  /\  A. z  e.  x  A. w  e.  x  (
z  e.  w  \/  z  =  w  \/  w  e.  z ) ) )
50 dfwe2 4573 . . . . . . 7  |-  (  _E  We  x  <->  (  _E  Fr  x  /\  A. z  e.  x  A. w  e.  x  ( z  _E  w  \/  z  =  w  \/  w  _E  z ) ) )
51 epel 4308 . . . . . . . . . 10  |-  ( z  _E  w  <->  z  e.  w )
52 biid 227 . . . . . . . . . 10  |-  ( z  =  w  <->  z  =  w )
53 epel 4308 . . . . . . . . . 10  |-  ( w  _E  z  <->  w  e.  z )
5451, 52, 533orbi123i 1141 . . . . . . . . 9  |-  ( ( z  _E  w  \/  z  =  w  \/  w  _E  z )  <-> 
( z  e.  w  \/  z  =  w  \/  w  e.  z
) )
55542ralbii 2569 . . . . . . . 8  |-  ( A. z  e.  x  A. w  e.  x  (
z  _E  w  \/  z  =  w  \/  w  _E  z )  <->  A. z  e.  x  A. w  e.  x  ( z  e.  w  \/  z  =  w  \/  w  e.  z
) )
5655anbi2i 675 . . . . . . 7  |-  ( (  _E  Fr  x  /\  A. z  e.  x  A. w  e.  x  (
z  _E  w  \/  z  =  w  \/  w  _E  z ) )  <->  (  _E  Fr  x  /\  A. z  e.  x  A. w  e.  x  ( z  e.  w  \/  z  =  w  \/  w  e.  z ) ) )
5750, 56bitri 240 . . . . . 6  |-  (  _E  We  x  <->  (  _E  Fr  x  /\  A. z  e.  x  A. w  e.  x  ( z  e.  w  \/  z  =  w  \/  w  e.  z ) ) )
5849, 57sylibr 203 . . . . 5  |-  ( A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x )  ->  _E  We  x )
59 df-ord 4395 . . . . 5  |-  ( Ord  x  <->  ( Tr  x  /\  _E  We  x ) )
6012, 58, 59sylanbrc 645 . . . 4  |-  ( A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x )  ->  Ord  x )
618, 60impbii 180 . . 3  |-  ( Ord  x  <->  A. y ( ( y  C.  x  /\  Tr  y )  ->  y  e.  x ) )
6261abbii 2395 . 2  |-  { x  |  Ord  x }  =  { x  |  A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x ) }
631, 62eqtri 2303 1  |-  On  =  { x  |  A. y ( ( y 
C.  x  /\  Tr  y )  ->  y  e.  x ) }
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 358    \/ w3o 933   A.wal 1527    = wceq 1623    e. wcel 1684   {cab 2269    =/= wne 2446   A.wral 2543   _Vcvv 2788    C_ wss 3152    C. wpss 3153   class class class wbr 4023   Tr wtr 4113    _E cep 4303    Fr wfr 4349    We wwe 4351   Ord word 4391   Oncon0 4392
This theorem is referenced by:  dfon3  24432
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pr 4214  ax-un 4512
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-rab 2552  df-v 2790  df-sbc 2992  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pss 3168  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-tp 3648  df-op 3649  df-uni 3828  df-int 3863  df-iun 3907  df-br 4024  df-opab 4078  df-tr 4114  df-eprel 4305  df-po 4314  df-so 4315  df-fr 4352  df-we 4354  df-ord 4395  df-on 4396  df-suc 4398
  Copyright terms: Public domain W3C validator