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

Theorem r1sdom 7633
Description: Each stage in the cumulative hierarchy is strictly larger than the last. (Contributed by Mario Carneiro, 19-Apr-2013.)
Assertion
Ref Expression
r1sdom  |-  ( ( A  e.  On  /\  B  e.  A )  ->  ( R1 `  B
)  ~<  ( R1 `  A ) )

Proof of Theorem r1sdom
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eleq2 2448 . . . 4  |-  ( x  =  (/)  ->  ( B  e.  x  <->  B  e.  (/) ) )
2 fveq2 5668 . . . . 5  |-  ( x  =  (/)  ->  ( R1
`  x )  =  ( R1 `  (/) ) )
32breq2d 4165 . . . 4  |-  ( x  =  (/)  ->  ( ( R1 `  B ) 
~<  ( R1 `  x
)  <->  ( R1 `  B )  ~<  ( R1 `  (/) ) ) )
41, 3imbi12d 312 . . 3  |-  ( x  =  (/)  ->  ( ( B  e.  x  -> 
( R1 `  B
)  ~<  ( R1 `  x ) )  <->  ( B  e.  (/)  ->  ( R1 `  B )  ~<  ( R1 `  (/) ) ) ) )
5 eleq2 2448 . . . 4  |-  ( x  =  y  ->  ( B  e.  x  <->  B  e.  y ) )
6 fveq2 5668 . . . . 5  |-  ( x  =  y  ->  ( R1 `  x )  =  ( R1 `  y
) )
76breq2d 4165 . . . 4  |-  ( x  =  y  ->  (
( R1 `  B
)  ~<  ( R1 `  x )  <->  ( R1 `  B )  ~<  ( R1 `  y ) ) )
85, 7imbi12d 312 . . 3  |-  ( x  =  y  ->  (
( B  e.  x  ->  ( R1 `  B
)  ~<  ( R1 `  x ) )  <->  ( B  e.  y  ->  ( R1
`  B )  ~< 
( R1 `  y
) ) ) )
9 eleq2 2448 . . . 4  |-  ( x  =  suc  y  -> 
( B  e.  x  <->  B  e.  suc  y ) )
10 fveq2 5668 . . . . 5  |-  ( x  =  suc  y  -> 
( R1 `  x
)  =  ( R1
`  suc  y )
)
1110breq2d 4165 . . . 4  |-  ( x  =  suc  y  -> 
( ( R1 `  B )  ~<  ( R1 `  x )  <->  ( R1 `  B )  ~<  ( R1 `  suc  y ) ) )
129, 11imbi12d 312 . . 3  |-  ( x  =  suc  y  -> 
( ( B  e.  x  ->  ( R1 `  B )  ~<  ( R1 `  x ) )  <-> 
( B  e.  suc  y  ->  ( R1 `  B )  ~<  ( R1 `  suc  y ) ) ) )
13 eleq2 2448 . . . 4  |-  ( x  =  A  ->  ( B  e.  x  <->  B  e.  A ) )
14 fveq2 5668 . . . . 5  |-  ( x  =  A  ->  ( R1 `  x )  =  ( R1 `  A
) )
1514breq2d 4165 . . . 4  |-  ( x  =  A  ->  (
( R1 `  B
)  ~<  ( R1 `  x )  <->  ( R1 `  B )  ~<  ( R1 `  A ) ) )
1613, 15imbi12d 312 . . 3  |-  ( x  =  A  ->  (
( B  e.  x  ->  ( R1 `  B
)  ~<  ( R1 `  x ) )  <->  ( B  e.  A  ->  ( R1
`  B )  ~< 
( R1 `  A
) ) ) )
17 noel 3575 . . . 4  |-  -.  B  e.  (/)
1817pm2.21i 125 . . 3  |-  ( B  e.  (/)  ->  ( R1 `  B )  ~<  ( R1 `  (/) ) )
19 elsuci 4588 . . . . 5  |-  ( B  e.  suc  y  -> 
( B  e.  y  \/  B  =  y ) )
20 fvex 5682 . . . . . . . . . . 11  |-  ( R1
`  y )  e. 
_V
2120canth2 7196 . . . . . . . . . 10  |-  ( R1
`  y )  ~<  ~P ( R1 `  y
)
22 r1suc 7629 . . . . . . . . . 10  |-  ( y  e.  On  ->  ( R1 `  suc  y )  =  ~P ( R1
`  y ) )
2321, 22syl5breqr 4189 . . . . . . . . 9  |-  ( y  e.  On  ->  ( R1 `  y )  ~< 
( R1 `  suc  y ) )
24 sdomtr 7181 . . . . . . . . . 10  |-  ( ( ( R1 `  B
)  ~<  ( R1 `  y )  /\  ( R1 `  y )  ~< 
( R1 `  suc  y ) )  -> 
( R1 `  B
)  ~<  ( R1 `  suc  y ) )
2524expcom 425 . . . . . . . . 9  |-  ( ( R1 `  y ) 
~<  ( R1 `  suc  y )  ->  (
( R1 `  B
)  ~<  ( R1 `  y )  ->  ( R1 `  B )  ~< 
( R1 `  suc  y ) ) )
2623, 25syl 16 . . . . . . . 8  |-  ( y  e.  On  ->  (
( R1 `  B
)  ~<  ( R1 `  y )  ->  ( R1 `  B )  ~< 
( R1 `  suc  y ) ) )
2726com12 29 . . . . . . 7  |-  ( ( R1 `  B ) 
~<  ( R1 `  y
)  ->  ( y  e.  On  ->  ( R1 `  B )  ~<  ( R1 `  suc  y ) ) )
2827imim2i 14 . . . . . 6  |-  ( ( B  e.  y  -> 
( R1 `  B
)  ~<  ( R1 `  y ) )  -> 
( B  e.  y  ->  ( y  e.  On  ->  ( R1 `  B )  ~<  ( R1 `  suc  y ) ) ) )
29 fveq2 5668 . . . . . . . . 9  |-  ( B  =  y  ->  ( R1 `  B )  =  ( R1 `  y
) )
3029breq1d 4163 . . . . . . . 8  |-  ( B  =  y  ->  (
( R1 `  B
)  ~<  ( R1 `  suc  y )  <->  ( R1 `  y )  ~<  ( R1 `  suc  y ) ) )
3123, 30syl5ibr 213 . . . . . . 7  |-  ( B  =  y  ->  (
y  e.  On  ->  ( R1 `  B ) 
~<  ( R1 `  suc  y ) ) )
3231a1i 11 . . . . . 6  |-  ( ( B  e.  y  -> 
( R1 `  B
)  ~<  ( R1 `  y ) )  -> 
( B  =  y  ->  ( y  e.  On  ->  ( R1 `  B )  ~<  ( R1 `  suc  y ) ) ) )
3328, 32jaod 370 . . . . 5  |-  ( ( B  e.  y  -> 
( R1 `  B
)  ~<  ( R1 `  y ) )  -> 
( ( B  e.  y  \/  B  =  y )  ->  (
y  e.  On  ->  ( R1 `  B ) 
~<  ( R1 `  suc  y ) ) ) )
3419, 33syl5 30 . . . 4  |-  ( ( B  e.  y  -> 
( R1 `  B
)  ~<  ( R1 `  y ) )  -> 
( B  e.  suc  y  ->  ( y  e.  On  ->  ( R1 `  B )  ~<  ( R1 `  suc  y ) ) ) )
3534com3r 75 . . 3  |-  ( y  e.  On  ->  (
( B  e.  y  ->  ( R1 `  B )  ~<  ( R1 `  y ) )  ->  ( B  e. 
suc  y  ->  ( R1 `  B )  ~< 
( R1 `  suc  y ) ) ) )
36 limuni 4582 . . . . . . 7  |-  ( Lim  x  ->  x  =  U. x )
3736eleq2d 2454 . . . . . 6  |-  ( Lim  x  ->  ( B  e.  x  <->  B  e.  U. x
) )
38 eluni2 3961 . . . . . 6  |-  ( B  e.  U. x  <->  E. y  e.  x  B  e.  y )
3937, 38syl6bb 253 . . . . 5  |-  ( Lim  x  ->  ( B  e.  x  <->  E. y  e.  x  B  e.  y )
)
40 r19.29 2789 . . . . . . 7  |-  ( ( A. y  e.  x  ( B  e.  y  ->  ( R1 `  B
)  ~<  ( R1 `  y ) )  /\  E. y  e.  x  B  e.  y )  ->  E. y  e.  x  ( ( B  e.  y  ->  ( R1 `  B )  ~<  ( R1 `  y ) )  /\  B  e.  y ) )
41 fvex 5682 . . . . . . . . . 10  |-  ( R1
`  x )  e. 
_V
42 ssiun2 4075 . . . . . . . . . . 11  |-  ( y  e.  x  ->  ( R1 `  y )  C_  U_ y  e.  x  ( R1 `  y ) )
43 vex 2902 . . . . . . . . . . . . 13  |-  x  e. 
_V
44 r1lim 7631 . . . . . . . . . . . . 13  |-  ( ( x  e.  _V  /\  Lim  x )  ->  ( R1 `  x )  = 
U_ y  e.  x  ( R1 `  y ) )
4543, 44mpan 652 . . . . . . . . . . . 12  |-  ( Lim  x  ->  ( R1 `  x )  =  U_ y  e.  x  ( R1 `  y ) )
4645sseq2d 3319 . . . . . . . . . . 11  |-  ( Lim  x  ->  ( ( R1 `  y )  C_  ( R1 `  x )  <-> 
( R1 `  y
)  C_  U_ y  e.  x  ( R1 `  y ) ) )
4742, 46syl5ibr 213 . . . . . . . . . 10  |-  ( Lim  x  ->  ( y  e.  x  ->  ( R1
`  y )  C_  ( R1 `  x ) ) )
48 ssdomg 7089 . . . . . . . . . 10  |-  ( ( R1 `  x )  e.  _V  ->  (
( R1 `  y
)  C_  ( R1 `  x )  ->  ( R1 `  y )  ~<_  ( R1 `  x ) ) )
4941, 47, 48ee02 1383 . . . . . . . . 9  |-  ( Lim  x  ->  ( y  e.  x  ->  ( R1
`  y )  ~<_  ( R1 `  x ) ) )
50 id 20 . . . . . . . . . . 11  |-  ( ( B  e.  y  -> 
( R1 `  B
)  ~<  ( R1 `  y ) )  -> 
( B  e.  y  ->  ( R1 `  B )  ~<  ( R1 `  y ) ) )
5150imp 419 . . . . . . . . . 10  |-  ( ( ( B  e.  y  ->  ( R1 `  B )  ~<  ( R1 `  y ) )  /\  B  e.  y )  ->  ( R1 `  B )  ~<  ( R1 `  y ) )
52 sdomdomtr 7176 . . . . . . . . . . 11  |-  ( ( ( R1 `  B
)  ~<  ( R1 `  y )  /\  ( R1 `  y )  ~<_  ( R1 `  x ) )  ->  ( R1 `  B )  ~<  ( R1 `  x ) )
5352expcom 425 . . . . . . . . . 10  |-  ( ( R1 `  y )  ~<_  ( R1 `  x
)  ->  ( ( R1 `  B )  ~< 
( R1 `  y
)  ->  ( R1 `  B )  ~<  ( R1 `  x ) ) )
5451, 53syl5 30 . . . . . . . . 9  |-  ( ( R1 `  y )  ~<_  ( R1 `  x
)  ->  ( (
( B  e.  y  ->  ( R1 `  B )  ~<  ( R1 `  y ) )  /\  B  e.  y )  ->  ( R1 `  B )  ~<  ( R1 `  x ) ) )
5549, 54syl6 31 . . . . . . . 8  |-  ( Lim  x  ->  ( y  e.  x  ->  ( ( ( B  e.  y  ->  ( R1 `  B )  ~<  ( R1 `  y ) )  /\  B  e.  y )  ->  ( R1 `  B )  ~<  ( R1 `  x ) ) ) )
5655rexlimdv 2772 . . . . . . 7  |-  ( Lim  x  ->  ( E. y  e.  x  (
( B  e.  y  ->  ( R1 `  B )  ~<  ( R1 `  y ) )  /\  B  e.  y )  ->  ( R1 `  B )  ~<  ( R1 `  x ) ) )
5740, 56syl5 30 . . . . . 6  |-  ( Lim  x  ->  ( ( A. y  e.  x  ( B  e.  y  ->  ( R1 `  B
)  ~<  ( R1 `  y ) )  /\  E. y  e.  x  B  e.  y )  -> 
( R1 `  B
)  ~<  ( R1 `  x ) ) )
5857exp3acom23 1378 . . . . 5  |-  ( Lim  x  ->  ( E. y  e.  x  B  e.  y  ->  ( A. y  e.  x  ( B  e.  y  ->  ( R1 `  B ) 
~<  ( R1 `  y
) )  ->  ( R1 `  B )  ~< 
( R1 `  x
) ) ) )
5939, 58sylbid 207 . . . 4  |-  ( Lim  x  ->  ( B  e.  x  ->  ( A. y  e.  x  ( B  e.  y  ->  ( R1 `  B ) 
~<  ( R1 `  y
) )  ->  ( R1 `  B )  ~< 
( R1 `  x
) ) ) )
6059com23 74 . . 3  |-  ( Lim  x  ->  ( A. y  e.  x  ( B  e.  y  ->  ( R1 `  B ) 
~<  ( R1 `  y
) )  ->  ( B  e.  x  ->  ( R1 `  B ) 
~<  ( R1 `  x
) ) ) )
614, 8, 12, 16, 18, 35, 60tfinds 4779 . 2  |-  ( A  e.  On  ->  ( B  e.  A  ->  ( R1 `  B ) 
~<  ( R1 `  A
) ) )
6261imp 419 1  |-  ( ( A  e.  On  /\  B  e.  A )  ->  ( R1 `  B
)  ~<  ( R1 `  A ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 358    /\ wa 359    = wceq 1649    e. wcel 1717   A.wral 2649   E.wrex 2650   _Vcvv 2899    C_ wss 3263   (/)c0 3571   ~Pcpw 3742   U.cuni 3957   U_ciun 4035   class class class wbr 4153   Oncon0 4522   Lim wlim 4523   suc csuc 4524   ` cfv 5394    ~<_ cdom 7043    ~< csdm 7044   R1cr1 7621
This theorem is referenced by:  r111  7634  smobeth  8394  r1tskina  8590
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 2368  ax-rep 4261  ax-sep 4271  ax-nul 4279  ax-pow 4318  ax-pr 4344  ax-un 4641
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 2242  df-mo 2243  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ne 2552  df-ral 2654  df-rex 2655  df-reu 2656  df-rab 2658  df-v 2901  df-sbc 3105  df-csb 3195  df-dif 3266  df-un 3268  df-in 3270  df-ss 3277  df-pss 3279  df-nul 3572  df-if 3683  df-pw 3744  df-sn 3763  df-pr 3764  df-tp 3765  df-op 3766  df-uni 3958  df-iun 4037  df-br 4154  df-opab 4208  df-mpt 4209  df-tr 4244  df-eprel 4435  df-id 4439  df-po 4444  df-so 4445  df-fr 4482  df-we 4484  df-ord 4525  df-on 4526  df-lim 4527  df-suc 4528  df-xp 4824  df-rel 4825  df-cnv 4826  df-co 4827  df-dm 4828  df-rn 4829  df-res 4830  df-ima 4831  df-iota 5358  df-fun 5396  df-fn 5397  df-f 5398  df-f1 5399  df-fo 5400  df-f1o 5401  df-fv 5402  df-recs 6569  df-rdg 6604  df-er 6841  df-en 7046  df-dom 7047  df-sdom 7048  df-r1 7623
  Copyright terms: Public domain W3C validator