MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  r1tr Unicode version

Theorem r1tr 7628
Description: The cumulative hierarchy of sets is transitive. Lemma 7T of [Enderton] p. 202. (Contributed by NM, 8-Sep-2003.) (Revised by Mario Carneiro, 16-Nov-2014.)
Assertion
Ref Expression
r1tr  |-  Tr  ( R1 `  A )

Proof of Theorem r1tr
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 r1funlim 7618 . . . . . 6  |-  ( Fun 
R1  /\  Lim  dom  R1 )
21simpri 449 . . . . 5  |-  Lim  dom  R1
3 limord 4574 . . . . 5  |-  ( Lim 
dom  R1  ->  Ord  dom  R1 )
4 ordsson 4703 . . . . 5  |-  ( Ord 
dom  R1  ->  dom  R1  C_  On )
52, 3, 4mp2b 10 . . . 4  |-  dom  R1  C_  On
65sseli 3280 . . 3  |-  ( A  e.  dom  R1  ->  A  e.  On )
7 fveq2 5661 . . . . . 6  |-  ( x  =  (/)  ->  ( R1
`  x )  =  ( R1 `  (/) ) )
8 r10 7620 . . . . . 6  |-  ( R1
`  (/) )  =  (/)
97, 8syl6eq 2428 . . . . 5  |-  ( x  =  (/)  ->  ( R1
`  x )  =  (/) )
10 treq 4242 . . . . 5  |-  ( ( R1 `  x )  =  (/)  ->  ( Tr  ( R1 `  x
)  <->  Tr  (/) ) )
119, 10syl 16 . . . 4  |-  ( x  =  (/)  ->  ( Tr  ( R1 `  x
)  <->  Tr  (/) ) )
12 fveq2 5661 . . . . 5  |-  ( x  =  y  ->  ( R1 `  x )  =  ( R1 `  y
) )
13 treq 4242 . . . . 5  |-  ( ( R1 `  x )  =  ( R1 `  y )  ->  ( Tr  ( R1 `  x
)  <->  Tr  ( R1 `  y ) ) )
1412, 13syl 16 . . . 4  |-  ( x  =  y  ->  ( Tr  ( R1 `  x
)  <->  Tr  ( R1 `  y ) ) )
15 fveq2 5661 . . . . 5  |-  ( x  =  suc  y  -> 
( R1 `  x
)  =  ( R1
`  suc  y )
)
16 treq 4242 . . . . 5  |-  ( ( R1 `  x )  =  ( R1 `  suc  y )  ->  ( Tr  ( R1 `  x
)  <->  Tr  ( R1 ` 
suc  y ) ) )
1715, 16syl 16 . . . 4  |-  ( x  =  suc  y  -> 
( Tr  ( R1
`  x )  <->  Tr  ( R1 `  suc  y ) ) )
18 fveq2 5661 . . . . 5  |-  ( x  =  A  ->  ( R1 `  x )  =  ( R1 `  A
) )
19 treq 4242 . . . . 5  |-  ( ( R1 `  x )  =  ( R1 `  A )  ->  ( Tr  ( R1 `  x
)  <->  Tr  ( R1 `  A ) ) )
2018, 19syl 16 . . . 4  |-  ( x  =  A  ->  ( Tr  ( R1 `  x
)  <->  Tr  ( R1 `  A ) ) )
21 tr0 4247 . . . 4  |-  Tr  (/)
22 limsuc 4762 . . . . . . . 8  |-  ( Lim 
dom  R1  ->  ( y  e.  dom  R1  <->  suc  y  e. 
dom  R1 ) )
232, 22ax-mp 8 . . . . . . 7  |-  ( y  e.  dom  R1  <->  suc  y  e. 
dom  R1 )
24 simpr 448 . . . . . . . . 9  |-  ( ( y  e.  On  /\  Tr  ( R1 `  y
) )  ->  Tr  ( R1 `  y ) )
25 pwtr 4350 . . . . . . . . 9  |-  ( Tr  ( R1 `  y
)  <->  Tr  ~P ( R1 `  y ) )
2624, 25sylib 189 . . . . . . . 8  |-  ( ( y  e.  On  /\  Tr  ( R1 `  y
) )  ->  Tr  ~P ( R1 `  y
) )
27 r1sucg 7621 . . . . . . . . 9  |-  ( y  e.  dom  R1  ->  ( R1 `  suc  y
)  =  ~P ( R1 `  y ) )
28 treq 4242 . . . . . . . . 9  |-  ( ( R1 `  suc  y
)  =  ~P ( R1 `  y )  -> 
( Tr  ( R1
`  suc  y )  <->  Tr 
~P ( R1 `  y ) ) )
2927, 28syl 16 . . . . . . . 8  |-  ( y  e.  dom  R1  ->  ( Tr  ( R1 `  suc  y )  <->  Tr  ~P ( R1 `  y ) ) )
3026, 29syl5ibrcom 214 . . . . . . 7  |-  ( ( y  e.  On  /\  Tr  ( R1 `  y
) )  ->  (
y  e.  dom  R1  ->  Tr  ( R1 `  suc  y ) ) )
3123, 30syl5bir 210 . . . . . 6  |-  ( ( y  e.  On  /\  Tr  ( R1 `  y
) )  ->  ( suc  y  e.  dom  R1 
->  Tr  ( R1 `  suc  y ) ) )
32 ndmfv 5688 . . . . . . . 8  |-  ( -. 
suc  y  e.  dom  R1 
->  ( R1 `  suc  y )  =  (/) )
33 treq 4242 . . . . . . . 8  |-  ( ( R1 `  suc  y
)  =  (/)  ->  ( Tr  ( R1 `  suc  y )  <->  Tr  (/) ) )
3432, 33syl 16 . . . . . . 7  |-  ( -. 
suc  y  e.  dom  R1 
->  ( Tr  ( R1
`  suc  y )  <->  Tr  (/) ) )
3521, 34mpbiri 225 . . . . . 6  |-  ( -. 
suc  y  e.  dom  R1 
->  Tr  ( R1 `  suc  y ) )
3631, 35pm2.61d1 153 . . . . 5  |-  ( ( y  e.  On  /\  Tr  ( R1 `  y
) )  ->  Tr  ( R1 `  suc  y
) )
3736ex 424 . . . 4  |-  ( y  e.  On  ->  ( Tr  ( R1 `  y
)  ->  Tr  ( R1 `  suc  y ) ) )
38 triun 4249 . . . . . . . 8  |-  ( A. y  e.  x  Tr  ( R1 `  y )  ->  Tr  U_ y  e.  x  ( R1 `  y ) )
39 r1limg 7623 . . . . . . . . . 10  |-  ( ( x  e.  dom  R1  /\ 
Lim  x )  -> 
( R1 `  x
)  =  U_ y  e.  x  ( R1 `  y ) )
4039ancoms 440 . . . . . . . . 9  |-  ( ( Lim  x  /\  x  e.  dom  R1 )  -> 
( R1 `  x
)  =  U_ y  e.  x  ( R1 `  y ) )
41 treq 4242 . . . . . . . . 9  |-  ( ( R1 `  x )  =  U_ y  e.  x  ( R1 `  y )  ->  ( Tr  ( R1 `  x
)  <->  Tr  U_ y  e.  x  ( R1 `  y ) ) )
4240, 41syl 16 . . . . . . . 8  |-  ( ( Lim  x  /\  x  e.  dom  R1 )  -> 
( Tr  ( R1
`  x )  <->  Tr  U_ y  e.  x  ( R1 `  y ) ) )
4338, 42syl5ibr 213 . . . . . . 7  |-  ( ( Lim  x  /\  x  e.  dom  R1 )  -> 
( A. y  e.  x  Tr  ( R1
`  y )  ->  Tr  ( R1 `  x
) ) )
4443impancom 428 . . . . . 6  |-  ( ( Lim  x  /\  A. y  e.  x  Tr  ( R1 `  y ) )  ->  ( x  e.  dom  R1  ->  Tr  ( R1 `  x ) ) )
45 ndmfv 5688 . . . . . . . 8  |-  ( -.  x  e.  dom  R1  ->  ( R1 `  x
)  =  (/) )
4645, 10syl 16 . . . . . . 7  |-  ( -.  x  e.  dom  R1  ->  ( Tr  ( R1
`  x )  <->  Tr  (/) ) )
4721, 46mpbiri 225 . . . . . 6  |-  ( -.  x  e.  dom  R1  ->  Tr  ( R1 `  x ) )
4844, 47pm2.61d1 153 . . . . 5  |-  ( ( Lim  x  /\  A. y  e.  x  Tr  ( R1 `  y ) )  ->  Tr  ( R1 `  x ) )
4948ex 424 . . . 4  |-  ( Lim  x  ->  ( A. y  e.  x  Tr  ( R1 `  y )  ->  Tr  ( R1 `  x ) ) )
5011, 14, 17, 20, 21, 37, 49tfinds 4772 . . 3  |-  ( A  e.  On  ->  Tr  ( R1 `  A ) )
516, 50syl 16 . 2  |-  ( A  e.  dom  R1  ->  Tr  ( R1 `  A
) )
52 ndmfv 5688 . . . 4  |-  ( -.  A  e.  dom  R1  ->  ( R1 `  A
)  =  (/) )
53 treq 4242 . . . 4  |-  ( ( R1 `  A )  =  (/)  ->  ( Tr  ( R1 `  A
)  <->  Tr  (/) ) )
5452, 53syl 16 . . 3  |-  ( -.  A  e.  dom  R1  ->  ( Tr  ( R1
`  A )  <->  Tr  (/) ) )
5521, 54mpbiri 225 . 2  |-  ( -.  A  e.  dom  R1  ->  Tr  ( R1 `  A ) )
5651, 55pm2.61i 158 1  |-  Tr  ( R1 `  A )
Colors of variables: wff set class
Syntax hints:   -. wn 3    <-> wb 177    /\ wa 359    = wceq 1649    e. wcel 1717   A.wral 2642    C_ wss 3256   (/)c0 3564   ~Pcpw 3735   U_ciun 4028   Tr wtr 4236   Ord word 4514   Oncon0 4515   Lim wlim 4516   suc csuc 4517   dom cdm 4811   Fun wfun 5381   ` cfv 5387   R1cr1 7614
This theorem is referenced by:  r1tr2  7629  r1ordg  7630  r1ord3g  7631  r1ord2  7633  r1sssuc  7635  r1pwss  7636  r1val1  7638  rankwflemb  7645  r1elwf  7648  r1elssi  7657  uniwf  7671  tcrank  7734  ackbij2lem3  8047  r1limwun  8537  tskr1om2  8569
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-13 1719  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361  ax-sep 4264  ax-nul 4272  ax-pow 4311  ax-pr 4337  ax-un 4634
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2235  df-mo 2236  df-clab 2367  df-cleq 2373  df-clel 2376  df-nfc 2505  df-ne 2545  df-ral 2647  df-rex 2648  df-reu 2649  df-rab 2651  df-v 2894  df-sbc 3098  df-csb 3188  df-dif 3259  df-un 3261  df-in 3263  df-ss 3270  df-pss 3272  df-nul 3565  df-if 3676  df-pw 3737  df-sn 3756  df-pr 3757  df-tp 3758  df-op 3759  df-uni 3951  df-iun 4030  df-br 4147  df-opab 4201  df-mpt 4202  df-tr 4237  df-eprel 4428  df-id 4432  df-po 4437  df-so 4438  df-fr 4475  df-we 4477  df-ord 4518  df-on 4519  df-lim 4520  df-suc 4521  df-om 4779  df-xp 4817  df-rel 4818  df-cnv 4819  df-co 4820  df-dm 4821  df-rn 4822  df-res 4823  df-ima 4824  df-iota 5351  df-fun 5389  df-fn 5390  df-f 5391  df-f1 5392  df-fo 5393  df-f1o 5394  df-fv 5395  df-recs 6562  df-rdg 6597  df-r1 7616
  Copyright terms: Public domain W3C validator