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

Theorem r1tr 7381
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
StepHypRef Expression
1 r1funlim 7371 . . . . . 6  |-  ( Fun 
R1  /\  Lim  dom  R1 )
21simpri 450 . . . . 5  |-  Lim  dom  R1
3 limord 4388 . . . . 5  |-  ( Lim 
dom  R1  ->  Ord  dom  R1 )
4 ordsson 4518 . . . . 5  |-  ( Ord 
dom  R1  ->  dom  R1  C_  On )
52, 3, 4mp2b 11 . . . 4  |-  dom  R1  C_  On
65sseli 3118 . . 3  |-  ( A  e.  dom  R1  ->  A  e.  On )
7 fveq2 5423 . . . . . 6  |-  ( x  =  (/)  ->  ( R1
`  x )  =  ( R1 `  (/) ) )
8 r10 7373 . . . . . 6  |-  ( R1
`  (/) )  =  (/)
97, 8syl6eq 2304 . . . . 5  |-  ( x  =  (/)  ->  ( R1
`  x )  =  (/) )
10 treq 4059 . . . . 5  |-  ( ( R1 `  x )  =  (/)  ->  ( Tr  ( R1 `  x
)  <->  Tr  (/) ) )
119, 10syl 17 . . . 4  |-  ( x  =  (/)  ->  ( Tr  ( R1 `  x
)  <->  Tr  (/) ) )
12 fveq2 5423 . . . . 5  |-  ( x  =  y  ->  ( R1 `  x )  =  ( R1 `  y
) )
13 treq 4059 . . . . 5  |-  ( ( R1 `  x )  =  ( R1 `  y )  ->  ( Tr  ( R1 `  x
)  <->  Tr  ( R1 `  y ) ) )
1412, 13syl 17 . . . 4  |-  ( x  =  y  ->  ( Tr  ( R1 `  x
)  <->  Tr  ( R1 `  y ) ) )
15 fveq2 5423 . . . . 5  |-  ( x  =  suc  y  -> 
( R1 `  x
)  =  ( R1
`  suc  y )
)
16 treq 4059 . . . . 5  |-  ( ( R1 `  x )  =  ( R1 `  suc  y )  ->  ( Tr  ( R1 `  x
)  <->  Tr  ( R1 ` 
suc  y ) ) )
1715, 16syl 17 . . . 4  |-  ( x  =  suc  y  -> 
( Tr  ( R1
`  x )  <->  Tr  ( R1 `  suc  y ) ) )
18 fveq2 5423 . . . . 5  |-  ( x  =  A  ->  ( R1 `  x )  =  ( R1 `  A
) )
19 treq 4059 . . . . 5  |-  ( ( R1 `  x )  =  ( R1 `  A )  ->  ( Tr  ( R1 `  x
)  <->  Tr  ( R1 `  A ) ) )
2018, 19syl 17 . . . 4  |-  ( x  =  A  ->  ( Tr  ( R1 `  x
)  <->  Tr  ( R1 `  A ) ) )
21 tr0 4064 . . . 4  |-  Tr  (/)
22 limsuc 4577 . . . . . . . 8  |-  ( Lim 
dom  R1  ->  ( y  e.  dom  R1  <->  suc  y  e. 
dom  R1 ) )
232, 22ax-mp 10 . . . . . . 7  |-  ( y  e.  dom  R1  <->  suc  y  e. 
dom  R1 )
24 simpr 449 . . . . . . . . 9  |-  ( ( y  e.  On  /\  Tr  ( R1 `  y
) )  ->  Tr  ( R1 `  y ) )
25 pwtr 4164 . . . . . . . . 9  |-  ( Tr  ( R1 `  y
)  <->  Tr  ~P ( R1 `  y ) )
2624, 25sylib 190 . . . . . . . 8  |-  ( ( y  e.  On  /\  Tr  ( R1 `  y
) )  ->  Tr  ~P ( R1 `  y
) )
27 r1sucg 7374 . . . . . . . . 9  |-  ( y  e.  dom  R1  ->  ( R1 `  suc  y
)  =  ~P ( R1 `  y ) )
28 treq 4059 . . . . . . . . 9  |-  ( ( R1 `  suc  y
)  =  ~P ( R1 `  y )  -> 
( Tr  ( R1
`  suc  y )  <->  Tr 
~P ( R1 `  y ) ) )
2927, 28syl 17 . . . . . . . 8  |-  ( y  e.  dom  R1  ->  ( Tr  ( R1 `  suc  y )  <->  Tr  ~P ( R1 `  y ) ) )
3026, 29syl5ibrcom 215 . . . . . . 7  |-  ( ( y  e.  On  /\  Tr  ( R1 `  y
) )  ->  (
y  e.  dom  R1  ->  Tr  ( R1 `  suc  y ) ) )
3123, 30syl5bir 211 . . . . . 6  |-  ( ( y  e.  On  /\  Tr  ( R1 `  y
) )  ->  ( suc  y  e.  dom  R1 
->  Tr  ( R1 `  suc  y ) ) )
32 ndmfv 5451 . . . . . . . 8  |-  ( -. 
suc  y  e.  dom  R1 
->  ( R1 `  suc  y )  =  (/) )
33 treq 4059 . . . . . . . 8  |-  ( ( R1 `  suc  y
)  =  (/)  ->  ( Tr  ( R1 `  suc  y )  <->  Tr  (/) ) )
3432, 33syl 17 . . . . . . 7  |-  ( -. 
suc  y  e.  dom  R1 
->  ( Tr  ( R1
`  suc  y )  <->  Tr  (/) ) )
3521, 34mpbiri 226 . . . . . 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 425 . . . 4  |-  ( y  e.  On  ->  ( Tr  ( R1 `  y
)  ->  Tr  ( R1 `  suc  y ) ) )
38 triun 4066 . . . . . . . 8  |-  ( A. y  e.  x  Tr  ( R1 `  y )  ->  Tr  U_ y  e.  x  ( R1 `  y ) )
39 r1limg 7376 . . . . . . . . . 10  |-  ( ( x  e.  dom  R1  /\ 
Lim  x )  -> 
( R1 `  x
)  =  U_ y  e.  x  ( R1 `  y ) )
4039ancoms 441 . . . . . . . . 9  |-  ( ( Lim  x  /\  x  e.  dom  R1 )  -> 
( R1 `  x
)  =  U_ y  e.  x  ( R1 `  y ) )
41 treq 4059 . . . . . . . . 9  |-  ( ( R1 `  x )  =  U_ y  e.  x  ( R1 `  y )  ->  ( Tr  ( R1 `  x
)  <->  Tr  U_ y  e.  x  ( R1 `  y ) ) )
4240, 41syl 17 . . . . . . . 8  |-  ( ( Lim  x  /\  x  e.  dom  R1 )  -> 
( Tr  ( R1
`  x )  <->  Tr  U_ y  e.  x  ( R1 `  y ) ) )
4338, 42syl5ibr 214 . . . . . . 7  |-  ( ( Lim  x  /\  x  e.  dom  R1 )  -> 
( A. y  e.  x  Tr  ( R1
`  y )  ->  Tr  ( R1 `  x
) ) )
4443impancom 429 . . . . . 6  |-  ( ( Lim  x  /\  A. y  e.  x  Tr  ( R1 `  y ) )  ->  ( x  e.  dom  R1  ->  Tr  ( R1 `  x ) ) )
45 ndmfv 5451 . . . . . . . 8  |-  ( -.  x  e.  dom  R1  ->  ( R1 `  x
)  =  (/) )
4645, 10syl 17 . . . . . . 7  |-  ( -.  x  e.  dom  R1  ->  ( Tr  ( R1
`  x )  <->  Tr  (/) ) )
4721, 46mpbiri 226 . . . . . 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 425 . . . 4  |-  ( Lim  x  ->  ( A. y  e.  x  Tr  ( R1 `  y )  ->  Tr  ( R1 `  x ) ) )
5011, 14, 17, 20, 21, 37, 49tfinds 4587 . . 3  |-  ( A  e.  On  ->  Tr  ( R1 `  A ) )
516, 50syl 17 . 2  |-  ( A  e.  dom  R1  ->  Tr  ( R1 `  A
) )
52 ndmfv 5451 . . . 4  |-  ( -.  A  e.  dom  R1  ->  ( R1 `  A
)  =  (/) )
53 treq 4059 . . . 4  |-  ( ( R1 `  A )  =  (/)  ->  ( Tr  ( R1 `  A
)  <->  Tr  (/) ) )
5452, 53syl 17 . . 3  |-  ( -.  A  e.  dom  R1  ->  ( Tr  ( R1
`  A )  <->  Tr  (/) ) )
5521, 54mpbiri 226 . 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 5    <-> wb 178    /\ wa 360    = wceq 1619    e. wcel 1621   A.wral 2516    C_ wss 3094   (/)c0 3397   ~Pcpw 3566   U_ciun 3846   Tr wtr 4053   Ord word 4328   Oncon0 4329   Lim wlim 4330   suc csuc 4331   dom cdm 4626   Fun wfun 4632   ` cfv 4638   R1cr1 7367
This theorem is referenced by:  r1tr2  7382  r1ordg  7383  r1ord3g  7384  r1ord2  7386  r1sssuc  7388  r1pwss  7389  r1val1  7391  rankwflemb  7398  r1elwf  7401  r1elssi  7410  uniwf  7424  tcrank  7487  ackbij2lem3  7800  r1limwun  8291  tskr1om2  8323
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-13 1625  ax-14 1626  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2237  ax-sep 4081  ax-nul 4089  ax-pow 4126  ax-pr 4152  ax-un 4449
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 940  df-3an 941  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-eu 2121  df-mo 2122  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-ne 2421  df-ral 2520  df-rex 2521  df-reu 2522  df-rab 2523  df-v 2742  df-sbc 2936  df-csb 3024  df-dif 3097  df-un 3099  df-in 3101  df-ss 3108  df-pss 3110  df-nul 3398  df-if 3507  df-pw 3568  df-sn 3587  df-pr 3588  df-tp 3589  df-op 3590  df-uni 3769  df-iun 3848  df-br 3964  df-opab 4018  df-mpt 4019  df-tr 4054  df-eprel 4242  df-id 4246  df-po 4251  df-so 4252  df-fr 4289  df-we 4291  df-ord 4332  df-on 4333  df-lim 4334  df-suc 4335  df-om 4594  df-xp 4640  df-rel 4641  df-cnv 4642  df-co 4643  df-dm 4644  df-rn 4645  df-res 4646  df-ima 4647  df-fun 4648  df-fn 4649  df-f 4650  df-f1 4651  df-fo 4652  df-f1o 4653  df-fv 4654  df-recs 6321  df-rdg 6356  df-r1 7369
  Copyright terms: Public domain W3C validator