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

Theorem poseq 28938
Description: A partial ordering of sequences of ordinals. (Contributed by Scott Fenton, 8-Jun-2011.)
Hypotheses
Ref Expression
poseq.1  |-  R  Po  ( A  u.  { (/) } )
poseq.2  |-  F  =  { f  |  E. x  e.  On  f : x --> A }
poseq.3  |-  S  =  { <. f ,  g
>.  |  ( (
f  e.  F  /\  g  e.  F )  /\  E. x  e.  On  ( A. y  e.  x  ( f `  y
)  =  ( g `
 y )  /\  ( f `  x
) R ( g `
 x ) ) ) }
Assertion
Ref Expression
poseq  |-  S  Po  F
Distinct variable groups:    A, f, x    f, g, y, x   
f, F, g, x    R, f, g, x
Allowed substitution hints:    A( y, g)    R( y)    S( x, y, f, g)    F( y)

Proof of Theorem poseq
Dummy variables  b 
a  c  t  w  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 poseq.1 . . . . . . . . . . . 12  |-  R  Po  ( A  u.  { (/) } )
2 poseq.2 . . . . . . . . . . . . . 14  |-  F  =  { f  |  E. x  e.  On  f : x --> A }
3 feq2 5714 . . . . . . . . . . . . . . . 16  |-  ( x  =  b  ->  (
f : x --> A  <->  f :
b --> A ) )
43cbvrexv 3089 . . . . . . . . . . . . . . 15  |-  ( E. x  e.  On  f : x --> A  <->  E. b  e.  On  f : b --> A )
54abbii 2601 . . . . . . . . . . . . . 14  |-  { f  |  E. x  e.  On  f : x --> A }  =  {
f  |  E. b  e.  On  f : b --> A }
62, 5eqtri 2496 . . . . . . . . . . . . 13  |-  F  =  { f  |  E. b  e.  On  f : b --> A }
76orderseqlem 28937 . . . . . . . . . . . 12  |-  ( a  e.  F  ->  (
a `  x )  e.  ( A  u.  { (/)
} ) )
8 poirr 4811 . . . . . . . . . . . 12  |-  ( ( R  Po  ( A  u.  { (/) } )  /\  ( a `  x )  e.  ( A  u.  { (/) } ) )  ->  -.  ( a `  x
) R ( a `
 x ) )
91, 7, 8sylancr 663 . . . . . . . . . . 11  |-  ( a  e.  F  ->  -.  ( a `  x
) R ( a `
 x ) )
109intnand 914 . . . . . . . . . 10  |-  ( a  e.  F  ->  -.  ( A. y  e.  x  ( a `  y
)  =  ( a `
 y )  /\  ( a `  x
) R ( a `
 x ) ) )
1110adantr 465 . . . . . . . . 9  |-  ( ( a  e.  F  /\  x  e.  On )  ->  -.  ( A. y  e.  x  ( a `  y )  =  ( a `  y )  /\  ( a `  x ) R ( a `  x ) ) )
1211nrexdv 2920 . . . . . . . 8  |-  ( a  e.  F  ->  -.  E. x  e.  On  ( A. y  e.  x  ( a `  y
)  =  ( a `
 y )  /\  ( a `  x
) R ( a `
 x ) ) )
1312adantr 465 . . . . . . 7  |-  ( ( a  e.  F  /\  a  e.  F )  ->  -.  E. x  e.  On  ( A. y  e.  x  ( a `  y )  =  ( a `  y )  /\  ( a `  x ) R ( a `  x ) ) )
14 imnan 422 . . . . . . 7  |-  ( ( ( a  e.  F  /\  a  e.  F
)  ->  -.  E. x  e.  On  ( A. y  e.  x  ( a `  y )  =  ( a `  y )  /\  ( a `  x ) R ( a `  x ) ) )  <->  -.  (
( a  e.  F  /\  a  e.  F
)  /\  E. x  e.  On  ( A. y  e.  x  ( a `  y )  =  ( a `  y )  /\  ( a `  x ) R ( a `  x ) ) ) )
1513, 14mpbi 208 . . . . . 6  |-  -.  (
( a  e.  F  /\  a  e.  F
)  /\  E. x  e.  On  ( A. y  e.  x  ( a `  y )  =  ( a `  y )  /\  ( a `  x ) R ( a `  x ) ) )
16 vex 3116 . . . . . . 7  |-  a  e. 
_V
17 eleq1 2539 . . . . . . . . 9  |-  ( f  =  a  ->  (
f  e.  F  <->  a  e.  F ) )
1817anbi1d 704 . . . . . . . 8  |-  ( f  =  a  ->  (
( f  e.  F  /\  g  e.  F
)  <->  ( a  e.  F  /\  g  e.  F ) ) )
19 fveq1 5865 . . . . . . . . . . . 12  |-  ( f  =  a  ->  (
f `  y )  =  ( a `  y ) )
2019eqeq1d 2469 . . . . . . . . . . 11  |-  ( f  =  a  ->  (
( f `  y
)  =  ( g `
 y )  <->  ( a `  y )  =  ( g `  y ) ) )
2120ralbidv 2903 . . . . . . . . . 10  |-  ( f  =  a  ->  ( A. y  e.  x  ( f `  y
)  =  ( g `
 y )  <->  A. y  e.  x  ( a `  y )  =  ( g `  y ) ) )
22 fveq1 5865 . . . . . . . . . . 11  |-  ( f  =  a  ->  (
f `  x )  =  ( a `  x ) )
2322breq1d 4457 . . . . . . . . . 10  |-  ( f  =  a  ->  (
( f `  x
) R ( g `
 x )  <->  ( a `  x ) R ( g `  x ) ) )
2421, 23anbi12d 710 . . . . . . . . 9  |-  ( f  =  a  ->  (
( A. y  e.  x  ( f `  y )  =  ( g `  y )  /\  ( f `  x ) R ( g `  x ) )  <->  ( A. y  e.  x  ( a `  y )  =  ( g `  y )  /\  ( a `  x ) R ( g `  x ) ) ) )
2524rexbidv 2973 . . . . . . . 8  |-  ( f  =  a  ->  ( E. x  e.  On  ( A. y  e.  x  ( f `  y
)  =  ( g `
 y )  /\  ( f `  x
) R ( g `
 x ) )  <->  E. x  e.  On  ( A. y  e.  x  ( a `  y
)  =  ( g `
 y )  /\  ( a `  x
) R ( g `
 x ) ) ) )
2618, 25anbi12d 710 . . . . . . 7  |-  ( f  =  a  ->  (
( ( f  e.  F  /\  g  e.  F )  /\  E. x  e.  On  ( A. y  e.  x  ( f `  y
)  =  ( g `
 y )  /\  ( f `  x
) R ( g `
 x ) ) )  <->  ( ( a  e.  F  /\  g  e.  F )  /\  E. x  e.  On  ( A. y  e.  x  ( a `  y
)  =  ( g `
 y )  /\  ( a `  x
) R ( g `
 x ) ) ) ) )
27 eleq1 2539 . . . . . . . . 9  |-  ( g  =  a  ->  (
g  e.  F  <->  a  e.  F ) )
2827anbi2d 703 . . . . . . . 8  |-  ( g  =  a  ->  (
( a  e.  F  /\  g  e.  F
)  <->  ( a  e.  F  /\  a  e.  F ) ) )
29 fveq1 5865 . . . . . . . . . . . 12  |-  ( g  =  a  ->  (
g `  y )  =  ( a `  y ) )
3029eqeq2d 2481 . . . . . . . . . . 11  |-  ( g  =  a  ->  (
( a `  y
)  =  ( g `
 y )  <->  ( a `  y )  =  ( a `  y ) ) )
3130ralbidv 2903 . . . . . . . . . 10  |-  ( g  =  a  ->  ( A. y  e.  x  ( a `  y
)  =  ( g `
 y )  <->  A. y  e.  x  ( a `  y )  =  ( a `  y ) ) )
32 fveq1 5865 . . . . . . . . . . 11  |-  ( g  =  a  ->  (
g `  x )  =  ( a `  x ) )
3332breq2d 4459 . . . . . . . . . 10  |-  ( g  =  a  ->  (
( a `  x
) R ( g `
 x )  <->  ( a `  x ) R ( a `  x ) ) )
3431, 33anbi12d 710 . . . . . . . . 9  |-  ( g  =  a  ->  (
( A. y  e.  x  ( a `  y )  =  ( g `  y )  /\  ( a `  x ) R ( g `  x ) )  <->  ( A. y  e.  x  ( a `  y )  =  ( a `  y )  /\  ( a `  x ) R ( a `  x ) ) ) )
3534rexbidv 2973 . . . . . . . 8  |-  ( g  =  a  ->  ( E. x  e.  On  ( A. y  e.  x  ( a `  y
)  =  ( g `
 y )  /\  ( a `  x
) R ( g `
 x ) )  <->  E. x  e.  On  ( A. y  e.  x  ( a `  y
)  =  ( a `
 y )  /\  ( a `  x
) R ( a `
 x ) ) ) )
3628, 35anbi12d 710 . . . . . . 7  |-  ( g  =  a  ->  (
( ( a  e.  F  /\  g  e.  F )  /\  E. x  e.  On  ( A. y  e.  x  ( a `  y
)  =  ( g `
 y )  /\  ( a `  x
) R ( g `
 x ) ) )  <->  ( ( a  e.  F  /\  a  e.  F )  /\  E. x  e.  On  ( A. y  e.  x  ( a `  y
)  =  ( a `
 y )  /\  ( a `  x
) R ( a `
 x ) ) ) ) )
37 poseq.3 . . . . . . 7  |-  S  =  { <. f ,  g
>.  |  ( (
f  e.  F  /\  g  e.  F )  /\  E. x  e.  On  ( A. y  e.  x  ( f `  y
)  =  ( g `
 y )  /\  ( f `  x
) R ( g `
 x ) ) ) }
3816, 16, 26, 36, 37brab 4770 . . . . . 6  |-  ( a S a  <->  ( (
a  e.  F  /\  a  e.  F )  /\  E. x  e.  On  ( A. y  e.  x  ( a `  y
)  =  ( a `
 y )  /\  ( a `  x
) R ( a `
 x ) ) ) )
3915, 38mtbir 299 . . . . 5  |-  -.  a S a
40 vex 3116 . . . . . . . 8  |-  b  e. 
_V
41 raleq 3058 . . . . . . . . . . . 12  |-  ( x  =  z  ->  ( A. y  e.  x  ( f `  y
)  =  ( g `
 y )  <->  A. y  e.  z  ( f `  y )  =  ( g `  y ) ) )
42 fveq2 5866 . . . . . . . . . . . . 13  |-  ( x  =  z  ->  (
f `  x )  =  ( f `  z ) )
43 fveq2 5866 . . . . . . . . . . . . 13  |-  ( x  =  z  ->  (
g `  x )  =  ( g `  z ) )
4442, 43breq12d 4460 . . . . . . . . . . . 12  |-  ( x  =  z  ->  (
( f `  x
) R ( g `
 x )  <->  ( f `  z ) R ( g `  z ) ) )
4541, 44anbi12d 710 . . . . . . . . . . 11  |-  ( x  =  z  ->  (
( A. y  e.  x  ( f `  y )  =  ( g `  y )  /\  ( f `  x ) R ( g `  x ) )  <->  ( A. y  e.  z  ( f `  y )  =  ( g `  y )  /\  ( f `  z ) R ( g `  z ) ) ) )
4645cbvrexv 3089 . . . . . . . . . 10  |-  ( E. x  e.  On  ( A. y  e.  x  ( f `  y
)  =  ( g `
 y )  /\  ( f `  x
) R ( g `
 x ) )  <->  E. z  e.  On  ( A. y  e.  z  ( f `  y
)  =  ( g `
 y )  /\  ( f `  z
) R ( g `
 z ) ) )
4720ralbidv 2903 . . . . . . . . . . . 12  |-  ( f  =  a  ->  ( A. y  e.  z 
( f `  y
)  =  ( g `
 y )  <->  A. y  e.  z  ( a `  y )  =  ( g `  y ) ) )
48 fveq1 5865 . . . . . . . . . . . . 13  |-  ( f  =  a  ->  (
f `  z )  =  ( a `  z ) )
4948breq1d 4457 . . . . . . . . . . . 12  |-  ( f  =  a  ->  (
( f `  z
) R ( g `
 z )  <->  ( a `  z ) R ( g `  z ) ) )
5047, 49anbi12d 710 . . . . . . . . . . 11  |-  ( f  =  a  ->  (
( A. y  e.  z  ( f `  y )  =  ( g `  y )  /\  ( f `  z ) R ( g `  z ) )  <->  ( A. y  e.  z  ( a `  y )  =  ( g `  y )  /\  ( a `  z ) R ( g `  z ) ) ) )
5150rexbidv 2973 . . . . . . . . . 10  |-  ( f  =  a  ->  ( E. z  e.  On  ( A. y  e.  z  ( f `  y
)  =  ( g `
 y )  /\  ( f `  z
) R ( g `
 z ) )  <->  E. z  e.  On  ( A. y  e.  z  ( a `  y
)  =  ( g `
 y )  /\  ( a `  z
) R ( g `
 z ) ) ) )
5246, 51syl5bb 257 . . . . . . . . 9  |-  ( f  =  a  ->  ( E. x  e.  On  ( A. y  e.  x  ( f `  y
)  =  ( g `
 y )  /\  ( f `  x
) R ( g `
 x ) )  <->  E. z  e.  On  ( A. y  e.  z  ( a `  y
)  =  ( g `
 y )  /\  ( a `  z
) R ( g `
 z ) ) ) )
5318, 52anbi12d 710 . . . . . . . 8  |-  ( f  =  a  ->  (
( ( f  e.  F  /\  g  e.  F )  /\  E. x  e.  On  ( A. y  e.  x  ( f `  y
)  =  ( g `
 y )  /\  ( f `  x
) R ( g `
 x ) ) )  <->  ( ( a  e.  F  /\  g  e.  F )  /\  E. z  e.  On  ( A. y  e.  z 
( a `  y
)  =  ( g `
 y )  /\  ( a `  z
) R ( g `
 z ) ) ) ) )
54 eleq1 2539 . . . . . . . . . 10  |-  ( g  =  b  ->  (
g  e.  F  <->  b  e.  F ) )
5554anbi2d 703 . . . . . . . . 9  |-  ( g  =  b  ->  (
( a  e.  F  /\  g  e.  F
)  <->  ( a  e.  F  /\  b  e.  F ) ) )
56 fveq1 5865 . . . . . . . . . . . . 13  |-  ( g  =  b  ->  (
g `  y )  =  ( b `  y ) )
5756eqeq2d 2481 . . . . . . . . . . . 12  |-  ( g  =  b  ->  (
( a `  y
)  =  ( g `
 y )  <->  ( a `  y )  =  ( b `  y ) ) )
5857ralbidv 2903 . . . . . . . . . . 11  |-  ( g  =  b  ->  ( A. y  e.  z 
( a `  y
)  =  ( g `
 y )  <->  A. y  e.  z  ( a `  y )  =  ( b `  y ) ) )
59 fveq1 5865 . . . . . . . . . . . 12  |-  ( g  =  b  ->  (
g `  z )  =  ( b `  z ) )
6059breq2d 4459 . . . . . . . . . . 11  |-  ( g  =  b  ->  (
( a `  z
) R ( g `
 z )  <->  ( a `  z ) R ( b `  z ) ) )
6158, 60anbi12d 710 . . . . . . . . . 10  |-  ( g  =  b  ->  (
( A. y  e.  z  ( a `  y )  =  ( g `  y )  /\  ( a `  z ) R ( g `  z ) )  <->  ( A. y  e.  z  ( a `  y )  =  ( b `  y )  /\  ( a `  z ) R ( b `  z ) ) ) )
6261rexbidv 2973 . . . . . . . . 9  |-  ( g  =  b  ->  ( E. z  e.  On  ( A. y  e.  z  ( a `  y
)  =  ( g `
 y )  /\  ( a `  z
) R ( g `
 z ) )  <->  E. z  e.  On  ( A. y  e.  z  ( a `  y
)  =  ( b `
 y )  /\  ( a `  z
) R ( b `
 z ) ) ) )
6355, 62anbi12d 710 . . . . . . . 8  |-  ( g  =  b  ->  (
( ( a  e.  F  /\  g  e.  F )  /\  E. z  e.  On  ( A. y  e.  z 
( a `  y
)  =  ( g `
 y )  /\  ( a `  z
) R ( g `
 z ) ) )  <->  ( ( a  e.  F  /\  b  e.  F )  /\  E. z  e.  On  ( A. y  e.  z 
( a `  y
)  =  ( b `
 y )  /\  ( a `  z
) R ( b `
 z ) ) ) ) )
6416, 40, 53, 63, 37brab 4770 . . . . . . 7  |-  ( a S b  <->  ( (
a  e.  F  /\  b  e.  F )  /\  E. z  e.  On  ( A. y  e.  z  ( a `  y
)  =  ( b `
 y )  /\  ( a `  z
) R ( b `
 z ) ) ) )
65 vex 3116 . . . . . . . 8  |-  c  e. 
_V
66 eleq1 2539 . . . . . . . . . 10  |-  ( f  =  b  ->  (
f  e.  F  <->  b  e.  F ) )
6766anbi1d 704 . . . . . . . . 9  |-  ( f  =  b  ->  (
( f  e.  F  /\  g  e.  F
)  <->  ( b  e.  F  /\  g  e.  F ) ) )
68 raleq 3058 . . . . . . . . . . . 12  |-  ( x  =  w  ->  ( A. y  e.  x  ( f `  y
)  =  ( g `
 y )  <->  A. y  e.  w  ( f `  y )  =  ( g `  y ) ) )
69 fveq2 5866 . . . . . . . . . . . . 13  |-  ( x  =  w  ->  (
f `  x )  =  ( f `  w ) )
70 fveq2 5866 . . . . . . . . . . . . 13  |-  ( x  =  w  ->  (
g `  x )  =  ( g `  w ) )
7169, 70breq12d 4460 . . . . . . . . . . . 12  |-  ( x  =  w  ->  (
( f `  x
) R ( g `
 x )  <->  ( f `  w ) R ( g `  w ) ) )
7268, 71anbi12d 710 . . . . . . . . . . 11  |-  ( x  =  w  ->  (
( A. y  e.  x  ( f `  y )  =  ( g `  y )  /\  ( f `  x ) R ( g `  x ) )  <->  ( A. y  e.  w  ( f `  y )  =  ( g `  y )  /\  ( f `  w ) R ( g `  w ) ) ) )
7372cbvrexv 3089 . . . . . . . . . 10  |-  ( E. x  e.  On  ( A. y  e.  x  ( f `  y
)  =  ( g `
 y )  /\  ( f `  x
) R ( g `
 x ) )  <->  E. w  e.  On  ( A. y  e.  w  ( f `  y
)  =  ( g `
 y )  /\  ( f `  w
) R ( g `
 w ) ) )
74 fveq1 5865 . . . . . . . . . . . . . 14  |-  ( f  =  b  ->  (
f `  y )  =  ( b `  y ) )
7574eqeq1d 2469 . . . . . . . . . . . . 13  |-  ( f  =  b  ->  (
( f `  y
)  =  ( g `
 y )  <->  ( b `  y )  =  ( g `  y ) ) )
7675ralbidv 2903 . . . . . . . . . . . 12  |-  ( f  =  b  ->  ( A. y  e.  w  ( f `  y
)  =  ( g `
 y )  <->  A. y  e.  w  ( b `  y )  =  ( g `  y ) ) )
77 fveq1 5865 . . . . . . . . . . . . 13  |-  ( f  =  b  ->  (
f `  w )  =  ( b `  w ) )
7877breq1d 4457 . . . . . . . . . . . 12  |-  ( f  =  b  ->  (
( f `  w
) R ( g `
 w )  <->  ( b `  w ) R ( g `  w ) ) )
7976, 78anbi12d 710 . . . . . . . . . . 11  |-  ( f  =  b  ->  (
( A. y  e.  w  ( f `  y )  =  ( g `  y )  /\  ( f `  w ) R ( g `  w ) )  <->  ( A. y  e.  w  ( b `  y )  =  ( g `  y )  /\  ( b `  w ) R ( g `  w ) ) ) )
8079rexbidv 2973 . . . . . . . . . 10  |-  ( f  =  b  ->  ( E. w  e.  On  ( A. y  e.  w  ( f `  y
)  =  ( g `
 y )  /\  ( f `  w
) R ( g `
 w ) )  <->  E. w  e.  On  ( A. y  e.  w  ( b `  y
)  =  ( g `
 y )  /\  ( b `  w
) R ( g `
 w ) ) ) )
8173, 80syl5bb 257 . . . . . . . . 9  |-  ( f  =  b  ->  ( E. x  e.  On  ( A. y  e.  x  ( f `  y
)  =  ( g `
 y )  /\  ( f `  x
) R ( g `
 x ) )  <->  E. w  e.  On  ( A. y  e.  w  ( b `  y
)  =  ( g `
 y )  /\  ( b `  w
) R ( g `
 w ) ) ) )
8267, 81anbi12d 710 . . . . . . . 8  |-  ( f  =  b  ->  (
( ( f  e.  F  /\  g  e.  F )  /\  E. x  e.  On  ( A. y  e.  x  ( f `  y
)  =  ( g `
 y )  /\  ( f `  x
) R ( g `
 x ) ) )  <->  ( ( b  e.  F  /\  g  e.  F )  /\  E. w  e.  On  ( A. y  e.  w  ( b `  y
)  =  ( g `
 y )  /\  ( b `  w
) R ( g `
 w ) ) ) ) )
83 eleq1 2539 . . . . . . . . . 10  |-  ( g  =  c  ->  (
g  e.  F  <->  c  e.  F ) )
8483anbi2d 703 . . . . . . . . 9  |-  ( g  =  c  ->  (
( b  e.  F  /\  g  e.  F
)  <->  ( b  e.  F  /\  c  e.  F ) ) )
85 fveq1 5865 . . . . . . . . . . . . 13  |-  ( g  =  c  ->  (
g `  y )  =  ( c `  y ) )
8685eqeq2d 2481 . . . . . . . . . . . 12  |-  ( g  =  c  ->  (
( b `  y
)  =  ( g `
 y )  <->  ( b `  y )  =  ( c `  y ) ) )
8786ralbidv 2903 . . . . . . . . . . 11  |-  ( g  =  c  ->  ( A. y  e.  w  ( b `  y
)  =  ( g `
 y )  <->  A. y  e.  w  ( b `  y )  =  ( c `  y ) ) )
88 fveq1 5865 . . . . . . . . . . . 12  |-  ( g  =  c  ->  (
g `  w )  =  ( c `  w ) )
8988breq2d 4459 . . . . . . . . . . 11  |-  ( g  =  c  ->  (
( b `  w
) R ( g `
 w )  <->  ( b `  w ) R ( c `  w ) ) )
9087, 89anbi12d 710 . . . . . . . . . 10  |-  ( g  =  c  ->  (
( A. y  e.  w  ( b `  y )  =  ( g `  y )  /\  ( b `  w ) R ( g `  w ) )  <->  ( A. y  e.  w  ( b `  y )  =  ( c `  y )  /\  ( b `  w ) R ( c `  w ) ) ) )
9190rexbidv 2973 . . . . . . . . 9  |-  ( g  =  c  ->  ( E. w  e.  On  ( A. y  e.  w  ( b `  y
)  =  ( g `
 y )  /\  ( b `  w
) R ( g `
 w ) )  <->  E. w  e.  On  ( A. y  e.  w  ( b `  y
)  =  ( c `
 y )  /\  ( b `  w
) R ( c `
 w ) ) ) )
9284, 91anbi12d 710 . . . . . . . 8  |-  ( g  =  c  ->  (
( ( b  e.  F  /\  g  e.  F )  /\  E. w  e.  On  ( A. y  e.  w  ( b `  y
)  =  ( g `
 y )  /\  ( b `  w
) R ( g `
 w ) ) )  <->  ( ( b  e.  F  /\  c  e.  F )  /\  E. w  e.  On  ( A. y  e.  w  ( b `  y
)  =  ( c `
 y )  /\  ( b `  w
) R ( c `
 w ) ) ) ) )
9340, 65, 82, 92, 37brab 4770 . . . . . . 7  |-  ( b S c  <->  ( (
b  e.  F  /\  c  e.  F )  /\  E. w  e.  On  ( A. y  e.  w  ( b `  y
)  =  ( c `
 y )  /\  ( b `  w
) R ( c `
 w ) ) ) )
94 simplll 757 . . . . . . . . 9  |-  ( ( ( ( a  e.  F  /\  b  e.  F )  /\  (
b  e.  F  /\  c  e.  F )
)  /\  ( E. z  e.  On  ( A. y  e.  z 
( a `  y
)  =  ( b `
 y )  /\  ( a `  z
) R ( b `
 z ) )  /\  E. w  e.  On  ( A. y  e.  w  ( b `  y )  =  ( c `  y )  /\  ( b `  w ) R ( c `  w ) ) ) )  -> 
a  e.  F )
95 simplrr 760 . . . . . . . . 9  |-  ( ( ( ( a  e.  F  /\  b  e.  F )  /\  (
b  e.  F  /\  c  e.  F )
)  /\  ( E. z  e.  On  ( A. y  e.  z 
( a `  y
)  =  ( b `
 y )  /\  ( a `  z
) R ( b `
 z ) )  /\  E. w  e.  On  ( A. y  e.  w  ( b `  y )  =  ( c `  y )  /\  ( b `  w ) R ( c `  w ) ) ) )  -> 
c  e.  F )
96 an4 822 . . . . . . . . . . . . 13  |-  ( ( ( A. y  e.  z  ( a `  y )  =  ( b `  y )  /\  A. y  e.  w  ( b `  y )  =  ( c `  y ) )  /\  ( ( a `  z ) R ( b `  z )  /\  (
b `  w ) R ( c `  w ) ) )  <-> 
( ( A. y  e.  z  ( a `  y )  =  ( b `  y )  /\  ( a `  z ) R ( b `  z ) )  /\  ( A. y  e.  w  (
b `  y )  =  ( c `  y )  /\  (
b `  w ) R ( c `  w ) ) ) )
97962rexbii 2966 . . . . . . . . . . . 12  |-  ( E. z  e.  On  E. w  e.  On  (
( A. y  e.  z  ( a `  y )  =  ( b `  y )  /\  A. y  e.  w  ( b `  y )  =  ( c `  y ) )  /\  ( ( a `  z ) R ( b `  z )  /\  (
b `  w ) R ( c `  w ) ) )  <->  E. z  e.  On  E. w  e.  On  (
( A. y  e.  z  ( a `  y )  =  ( b `  y )  /\  ( a `  z ) R ( b `  z ) )  /\  ( A. y  e.  w  (
b `  y )  =  ( c `  y )  /\  (
b `  w ) R ( c `  w ) ) ) )
98 reeanv 3029 . . . . . . . . . . . 12  |-  ( E. z  e.  On  E. w  e.  On  (
( A. y  e.  z  ( a `  y )  =  ( b `  y )  /\  ( a `  z ) R ( b `  z ) )  /\  ( A. y  e.  w  (
b `  y )  =  ( c `  y )  /\  (
b `  w ) R ( c `  w ) ) )  <-> 
( E. z  e.  On  ( A. y  e.  z  ( a `  y )  =  ( b `  y )  /\  ( a `  z ) R ( b `  z ) )  /\  E. w  e.  On  ( A. y  e.  w  ( b `  y )  =  ( c `  y )  /\  ( b `  w ) R ( c `  w ) ) ) )
9997, 98bitri 249 . . . . . . . . . . 11  |-  ( E. z  e.  On  E. w  e.  On  (
( A. y  e.  z  ( a `  y )  =  ( b `  y )  /\  A. y  e.  w  ( b `  y )  =  ( c `  y ) )  /\  ( ( a `  z ) R ( b `  z )  /\  (
b `  w ) R ( c `  w ) ) )  <-> 
( E. z  e.  On  ( A. y  e.  z  ( a `  y )  =  ( b `  y )  /\  ( a `  z ) R ( b `  z ) )  /\  E. w  e.  On  ( A. y  e.  w  ( b `  y )  =  ( c `  y )  /\  ( b `  w ) R ( c `  w ) ) ) )
100 eloni 4888 . . . . . . . . . . . . . 14  |-  ( z  e.  On  ->  Ord  z )
101 eloni 4888 . . . . . . . . . . . . . 14  |-  ( w  e.  On  ->  Ord  w )
102 ordtri3or 4910 . . . . . . . . . . . . . 14  |-  ( ( Ord  z  /\  Ord  w )  ->  (
z  e.  w  \/  z  =  w  \/  w  e.  z ) )
103100, 101, 102syl2an 477 . . . . . . . . . . . . 13  |-  ( ( z  e.  On  /\  w  e.  On )  ->  ( z  e.  w  \/  z  =  w  \/  w  e.  z
) )
104 simp1l 1020 . . . . . . . . . . . . . . . . 17  |-  ( ( ( z  e.  On  /\  w  e.  On )  /\  z  e.  w  /\  ( ( A. y  e.  z  ( a `  y )  =  ( b `  y )  /\  A. y  e.  w  ( b `  y )  =  ( c `  y ) )  /\  ( ( a `  z ) R ( b `  z )  /\  (
b `  w ) R ( c `  w ) ) ) )  ->  z  e.  On )
105 onelss 4920 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( w  e.  On  ->  (
z  e.  w  -> 
z  C_  w )
)
106105imp 429 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( w  e.  On  /\  z  e.  w )  ->  z  C_  w )
107106adantll 713 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( z  e.  On  /\  w  e.  On )  /\  z  e.  w
)  ->  z  C_  w )
108 ssralv 3564 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( z 
C_  w  ->  ( A. y  e.  w  ( b `  y
)  =  ( c `
 y )  ->  A. y  e.  z 
( b `  y
)  =  ( c `
 y ) ) )
109108anim2d 565 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( z 
C_  w  ->  (
( A. y  e.  z  ( a `  y )  =  ( b `  y )  /\  A. y  e.  w  ( b `  y )  =  ( c `  y ) )  ->  ( A. y  e.  z  (
a `  y )  =  ( b `  y )  /\  A. y  e.  z  (
b `  y )  =  ( c `  y ) ) ) )
110 r19.26 2989 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( A. y  e.  z  (
( a `  y
)  =  ( b `
 y )  /\  ( b `  y
)  =  ( c `
 y ) )  <-> 
( A. y  e.  z  ( a `  y )  =  ( b `  y )  /\  A. y  e.  z  ( b `  y )  =  ( c `  y ) ) )
111109, 110syl6ibr 227 . . . . . . . . . . . . . . . . . . . . 21  |-  ( z 
C_  w  ->  (
( A. y  e.  z  ( a `  y )  =  ( b `  y )  /\  A. y  e.  w  ( b `  y )  =  ( c `  y ) )  ->  A. y  e.  z  ( (
a `  y )  =  ( b `  y )  /\  (
b `  y )  =  ( c `  y ) ) ) )
112 eqtr 2493 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( a `  y
)  =  ( b `
 y )  /\  ( b `  y
)  =  ( c `
 y ) )  ->  ( a `  y )  =  ( c `  y ) )
113112ralimi 2857 . . . . . . . . . . . . . . . . . . . . 21  |-  ( A. y  e.  z  (
( a `  y
)  =  ( b `
 y )  /\  ( b `  y
)  =  ( c `
 y ) )  ->  A. y  e.  z  ( a `  y
)  =  ( c `
 y ) )
114111, 113syl6 33 . . . . . . . . . . . . . . . . . . . 20  |-  ( z 
C_  w  ->  (
( A. y  e.  z  ( a `  y )  =  ( b `  y )  /\  A. y  e.  w  ( b `  y )  =  ( c `  y ) )  ->  A. y  e.  z  ( a `  y )  =  ( c `  y ) ) )
115107, 114syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( z  e.  On  /\  w  e.  On )  /\  z  e.  w
)  ->  ( ( A. y  e.  z 
( a `  y
)  =  ( b `
 y )  /\  A. y  e.  w  ( b `  y )  =  ( c `  y ) )  ->  A. y  e.  z 
( a `  y
)  =  ( c `
 y ) ) )
116115adantrd 468 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( z  e.  On  /\  w  e.  On )  /\  z  e.  w
)  ->  ( (
( A. y  e.  z  ( a `  y )  =  ( b `  y )  /\  A. y  e.  w  ( b `  y )  =  ( c `  y ) )  /\  ( ( a `  z ) R ( b `  z )  /\  (
b `  w ) R ( c `  w ) ) )  ->  A. y  e.  z  ( a `  y
)  =  ( c `
 y ) ) )
1171163impia 1193 . . . . . . . . . . . . . . . . 17  |-  ( ( ( z  e.  On  /\  w  e.  On )  /\  z  e.  w  /\  ( ( A. y  e.  z  ( a `  y )  =  ( b `  y )  /\  A. y  e.  w  ( b `  y )  =  ( c `  y ) )  /\  ( ( a `  z ) R ( b `  z )  /\  (
b `  w ) R ( c `  w ) ) ) )  ->  A. y  e.  z  ( a `  y )  =  ( c `  y ) )
118 fveq2 5866 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  z  ->  (
b `  y )  =  ( b `  z ) )
119 fveq2 5866 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  z  ->  (
c `  y )  =  ( c `  z ) )
120118, 119eqeq12d 2489 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  =  z  ->  (
( b `  y
)  =  ( c `
 y )  <->  ( b `  z )  =  ( c `  z ) ) )
121120rspcv 3210 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( z  e.  w  ->  ( A. y  e.  w  ( b `  y
)  =  ( c `
 y )  -> 
( b `  z
)  =  ( c `
 z ) ) )
122 breq2 4451 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( b `  z )  =  ( c `  z )  ->  (
( a `  z
) R ( b `
 z )  <->  ( a `  z ) R ( c `  z ) ) )
123122biimpd 207 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( b `  z )  =  ( c `  z )  ->  (
( a `  z
) R ( b `
 z )  -> 
( a `  z
) R ( c `
 z ) ) )
124121, 123syl6 33 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( z  e.  w  ->  ( A. y  e.  w  ( b `  y
)  =  ( c `
 y )  -> 
( ( a `  z ) R ( b `  z )  ->  ( a `  z ) R ( c `  z ) ) ) )
125124com3l 81 . . . . . . . . . . . . . . . . . . . . 21  |-  ( A. y  e.  w  (
b `  y )  =  ( c `  y )  ->  (
( a `  z
) R ( b `
 z )  -> 
( z  e.  w  ->  ( a `  z
) R ( c `
 z ) ) ) )
126125imp 429 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A. y  e.  w  ( b `  y
)  =  ( c `
 y )  /\  ( a `  z
) R ( b `
 z ) )  ->  ( z  e.  w  ->  ( a `  z ) R ( c `  z ) ) )
127126ad2ant2lr 747 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( A. y  e.  z  ( a `  y )  =  ( b `  y )  /\  A. y  e.  w  ( b `  y )  =  ( c `  y ) )  /\  ( ( a `  z ) R ( b `  z )  /\  (
b `  w ) R ( c `  w ) ) )  ->  ( z  e.  w  ->  ( a `  z ) R ( c `  z ) ) )
128127impcom 430 . . . . . . . . . . . . . . . . . 18  |-  ( ( z  e.  w  /\  ( ( A. y  e.  z  ( a `  y )  =  ( b `  y )  /\  A. y  e.  w  ( b `  y )  =  ( c `  y ) )  /\  ( ( a `  z ) R ( b `  z )  /\  (
b `  w ) R ( c `  w ) ) ) )  ->  ( a `  z ) R ( c `  z ) )
1291283adant1 1014 . . . . . . . . . . . . . . . . 17  |-  ( ( ( z  e.  On  /\  w  e.  On )  /\  z  e.  w  /\  ( ( A. y  e.  z  ( a `  y )  =  ( b `  y )  /\  A. y  e.  w  ( b `  y )  =  ( c `  y ) )  /\  ( ( a `  z ) R ( b `  z )  /\  (
b `  w ) R ( c `  w ) ) ) )  ->  ( a `  z ) R ( c `  z ) )
130 raleq 3058 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  z  ->  ( A. y  e.  t 
( a `  y
)  =  ( c `
 y )  <->  A. y  e.  z  ( a `  y )  =  ( c `  y ) ) )
131 fveq2 5866 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  =  z  ->  (
a `  t )  =  ( a `  z ) )
132 fveq2 5866 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  =  z  ->  (
c `  t )  =  ( c `  z ) )
133131, 132breq12d 4460 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  z  ->  (
( a `  t
) R ( c `
 t )  <->  ( a `  z ) R ( c `  z ) ) )
134130, 133anbi12d 710 . . . . . . . . . . . . . . . . . 18  |-  ( t  =  z  ->  (
( A. y  e.  t  ( a `  y )  =  ( c `  y )  /\  ( a `  t ) R ( c `  t ) )  <->  ( A. y  e.  z  ( a `  y )  =  ( c `  y )  /\  ( a `  z ) R ( c `  z ) ) ) )
135134rspcev 3214 . . . . . . . . . . . . . . . . 17  |-  ( ( z  e.  On  /\  ( A. y  e.  z  ( a `  y
)  =  ( c `
 y )  /\  ( a `  z
) R ( c `
 z ) ) )  ->  E. t  e.  On  ( A. y  e.  t  ( a `  y )  =  ( c `  y )  /\  ( a `  t ) R ( c `  t ) ) )
136104, 117, 129, 135syl12anc 1226 . . . . . . . . . . . . . . . 16  |-  ( ( ( z  e.  On  /\  w  e.  On )  /\  z  e.  w  /\  ( ( A. y  e.  z  ( a `  y )  =  ( b `  y )  /\  A. y  e.  w  ( b `  y )  =  ( c `  y ) )  /\  ( ( a `  z ) R ( b `  z )  /\  (
b `  w ) R ( c `  w ) ) ) )  ->  E. t  e.  On  ( A. y  e.  t  ( a `  y )  =  ( c `  y )  /\  ( a `  t ) R ( c `  t ) ) )
137136a1d 25 . . . . . . . . . . . . . . 15  |-  ( ( ( z  e.  On  /\  w  e.  On )  /\  z  e.  w  /\  ( ( A. y  e.  z  ( a `  y )  =  ( b `  y )  /\  A. y  e.  w  ( b `  y )  =  ( c `  y ) )  /\  ( ( a `  z ) R ( b `  z )  /\  (
b `  w ) R ( c `  w ) ) ) )  ->  ( (
( a  e.  F  /\  b  e.  F
)  /\  ( b  e.  F  /\  c  e.  F ) )  ->  E. t  e.  On  ( A. y  e.  t  ( a `  y
)  =  ( c `
 y )  /\  ( a `  t
) R ( c `
 t ) ) ) )
1381373exp 1195 . . . . . . . . . . . . . 14  |-  ( ( z  e.  On  /\  w  e.  On )  ->  ( z  e.  w  ->  ( ( ( A. y  e.  z  (
a `  y )  =  ( b `  y )  /\  A. y  e.  w  (
b `  y )  =  ( c `  y ) )  /\  ( ( a `  z ) R ( b `  z )  /\  ( b `  w ) R ( c `  w ) ) )  ->  (
( ( a  e.  F  /\  b  e.  F )  /\  (
b  e.  F  /\  c  e.  F )
)  ->  E. t  e.  On  ( A. y  e.  t  ( a `  y )  =  ( c `  y )  /\  ( a `  t ) R ( c `  t ) ) ) ) ) )
1392orderseqlem 28937 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( a  e.  F  ->  (
a `  z )  e.  ( A  u.  { (/)
} ) )
140139ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( a  e.  F  /\  b  e.  F
)  /\  ( b  e.  F  /\  c  e.  F ) )  -> 
( a `  z
)  e.  ( A  u.  { (/) } ) )
1412orderseqlem 28937 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( b  e.  F  ->  (
b `  z )  e.  ( A  u.  { (/)
} ) )
142141ad2antlr 726 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( a  e.  F  /\  b  e.  F
)  /\  ( b  e.  F  /\  c  e.  F ) )  -> 
( b `  z
)  e.  ( A  u.  { (/) } ) )
1432orderseqlem 28937 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( c  e.  F  ->  (
c `  z )  e.  ( A  u.  { (/)
} ) )
144143ad2antll 728 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( a  e.  F  /\  b  e.  F
)  /\  ( b  e.  F  /\  c  e.  F ) )  -> 
( c `  z
)  e.  ( A  u.  { (/) } ) )
145140, 142, 1443jca 1176 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( a  e.  F  /\  b  e.  F
)  /\  ( b  e.  F  /\  c  e.  F ) )  -> 
( ( a `  z )  e.  ( A  u.  { (/) } )  /\  ( b `
 z )  e.  ( A  u.  { (/)
} )  /\  (
c `  z )  e.  ( A  u.  { (/)
} ) ) )
146 potr 4812 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( R  Po  ( A  u.  { (/) } )  /\  ( ( a `
 z )  e.  ( A  u.  { (/)
} )  /\  (
b `  z )  e.  ( A  u.  { (/)
} )  /\  (
c `  z )  e.  ( A  u.  { (/)
} ) ) )  ->  ( ( ( a `  z ) R ( b `  z )  /\  (
b `  z ) R ( c `  z ) )  -> 
( a `  z
) R ( c `
 z ) ) )
1471, 145, 146sylancr 663 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( a  e.  F  /\  b  e.  F
)  /\  ( b  e.  F  /\  c  e.  F ) )  -> 
( ( ( a `
 z ) R ( b `  z
)  /\  ( b `  z ) R ( c `  z ) )  ->  ( a `  z ) R ( c `  z ) ) )
148147impcom 430 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( a `  z ) R ( b `  z )  /\  ( b `  z ) R ( c `  z ) )  /\  ( ( a  e.  F  /\  b  e.  F )  /\  ( b  e.  F  /\  c  e.  F
) ) )  -> 
( a `  z
) R ( c `
 z ) )
149113, 148anim12i 566 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A. y  e.  z  ( ( a `  y )  =  ( b `  y )  /\  ( b `  y )  =  ( c `  y ) )  /\  ( ( ( a `  z
) R ( b `
 z )  /\  ( b `  z
) R ( c `
 z ) )  /\  ( ( a  e.  F  /\  b  e.  F )  /\  (
b  e.  F  /\  c  e.  F )
) ) )  -> 
( A. y  e.  z  ( a `  y )  =  ( c `  y )  /\  ( a `  z ) R ( c `  z ) ) )
150149anassrs 648 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( A. y  e.  z  ( ( a `
 y )  =  ( b `  y
)  /\  ( b `  y )  =  ( c `  y ) )  /\  ( ( a `  z ) R ( b `  z )  /\  (
b `  z ) R ( c `  z ) ) )  /\  ( ( a  e.  F  /\  b  e.  F )  /\  (
b  e.  F  /\  c  e.  F )
) )  ->  ( A. y  e.  z 
( a `  y
)  =  ( c `
 y )  /\  ( a `  z
) R ( c `
 z ) ) )
151150, 135sylan2 474 . . . . . . . . . . . . . . . . 17  |-  ( ( z  e.  On  /\  ( ( A. y  e.  z  ( (
a `  y )  =  ( b `  y )  /\  (
b `  y )  =  ( c `  y ) )  /\  ( ( a `  z ) R ( b `  z )  /\  ( b `  z ) R ( c `  z ) ) )  /\  (
( a  e.  F  /\  b  e.  F
)  /\  ( b  e.  F  /\  c  e.  F ) ) ) )  ->  E. t  e.  On  ( A. y  e.  t  ( a `  y )  =  ( c `  y )  /\  ( a `  t ) R ( c `  t ) ) )
152151exp32 605 . . . . . . . . . . . . . . . 16  |-  ( z  e.  On  ->  (
( A. y  e.  z  ( ( a `
 y )  =  ( b `  y
)  /\  ( b `  y )  =  ( c `  y ) )  /\  ( ( a `  z ) R ( b `  z )  /\  (
b `  z ) R ( c `  z ) ) )  ->  ( ( ( a  e.  F  /\  b  e.  F )  /\  ( b  e.  F  /\  c  e.  F
) )  ->  E. t  e.  On  ( A. y  e.  t  ( a `  y )  =  ( c `  y )  /\  ( a `  t ) R ( c `  t ) ) ) ) )
153 raleq 3058 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  =  w  ->  ( A. y  e.  z 
( b `  y
)  =  ( c `
 y )  <->  A. y  e.  w  ( b `  y )  =  ( c `  y ) ) )
154153anbi2d 703 . . . . . . . . . . . . . . . . . . 19  |-  ( z  =  w  ->  (
( A. y  e.  z  ( a `  y )  =  ( b `  y )  /\  A. y  e.  z  ( b `  y )  =  ( c `  y ) )  <->  ( A. y  e.  z  ( a `  y )  =  ( b `  y )  /\  A. y  e.  w  ( b `  y )  =  ( c `  y ) ) ) )
155110, 154syl5bb 257 . . . . . . . . . . . . . . . . . 18  |-  ( z  =  w  ->  ( A. y  e.  z 
( ( a `  y )  =  ( b `  y )  /\  ( b `  y )  =  ( c `  y ) )  <->  ( A. y  e.  z  ( a `  y )  =  ( b `  y )  /\  A. y  e.  w  ( b `  y )  =  ( c `  y ) ) ) )
156 fveq2 5866 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  =  w  ->  (
b `  z )  =  ( b `  w ) )
157 fveq2 5866 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  =  w  ->  (
c `  z )  =  ( c `  w ) )
158156, 157breq12d 4460 . . . . . . . . . . . . . . . . . . 19  |-  ( z  =  w  ->  (
( b `  z
) R ( c `
 z )  <->  ( b `  w ) R ( c `  w ) ) )
159158anbi2d 703 . . . . . . . . . . . . . . . . . 18  |-  ( z  =  w  ->  (
( ( a `  z ) R ( b `  z )  /\  ( b `  z ) R ( c `  z ) )  <->  ( ( a `
 z ) R ( b `  z
)  /\  ( b `  w ) R ( c `  w ) ) ) )
160155, 159anbi12d 710 . . . . . . . . . . . . . . . . 17  |-  ( z  =  w  ->  (
( A. y  e.  z  ( ( a `
 y )  =  ( b `  y
)  /\  ( b `  y )  =  ( c `  y ) )  /\  ( ( a `  z ) R ( b `  z )  /\  (
b `  z ) R ( c `  z ) ) )  <-> 
( ( A. y  e.  z  ( a `  y )  =  ( b `  y )  /\  A. y  e.  w  ( b `  y )  =  ( c `  y ) )  /\  ( ( a `  z ) R ( b `  z )  /\  (
b `  w ) R ( c `  w ) ) ) ) )
161160imbi1d 317 . . . . . . . . . . . . . . . 16  |-  ( z  =  w  ->  (
( ( A. y  e.  z  ( (
a `  y )  =  ( b `  y )  /\  (
b `  y )  =  ( c `  y ) )  /\  ( ( a `  z ) R ( b `  z )  /\  ( b `  z ) R ( c `  z ) ) )  ->  (
( ( a  e.  F  /\  b  e.  F )  /\  (
b  e.  F  /\  c  e.  F )
)  ->  E. t  e.  On  ( A. y  e.  t  ( a `  y )  =  ( c `  y )  /\  ( a `  t ) R ( c `  t ) ) ) )  <->  ( (
( A. y  e.  z  ( a `  y )  =  ( b `  y )  /\  A. y  e.  w  ( b `  y )  =  ( c `  y ) )  /\  ( ( a `  z ) R ( b `  z )  /\  (
b `  w ) R ( c `  w ) ) )  ->  ( ( ( a  e.  F  /\  b  e.  F )  /\  ( b  e.  F  /\  c  e.  F
) )  ->  E. t  e.  On  ( A. y  e.  t  ( a `  y )  =  ( c `  y )  /\  ( a `  t ) R ( c `  t ) ) ) ) ) )
162152, 161syl5ibcom 220 . . . . . . . . . . . . . . 15  |-  ( z  e.  On  ->  (
z  =  w  -> 
( ( ( A. y  e.  z  (
a `  y )  =  ( b `  y )  /\  A. y  e.  w  (
b `  y )  =  ( c `  y ) )  /\  ( ( a `  z ) R ( b `  z )  /\  ( b `  w ) R ( c `  w ) ) )  ->  (
( ( a  e.  F  /\  b  e.  F )  /\  (
b  e.  F  /\  c  e.  F )
)  ->  E. t  e.  On  ( A. y  e.  t  ( a `  y )  =  ( c `  y )  /\  ( a `  t ) R ( c `  t ) ) ) ) ) )
163162adantr 465 . . . . . . . . . . . . . 14  |-  ( ( z  e.  On  /\  w  e.  On )  ->  ( z  =  w  ->  ( ( ( A. y  e.  z  ( a `  y
)  =  ( b `
 y )  /\  A. y  e.  w  ( b `  y )  =  ( c `  y ) )  /\  ( ( a `  z ) R ( b `  z )  /\  ( b `  w ) R ( c `  w ) ) )  ->  (
( ( a  e.  F  /\  b  e.  F )  /\  (
b  e.  F  /\  c  e.  F )
)  ->  E. t  e.  On  ( A. y  e.  t  ( a `  y )  =  ( c `  y )  /\  ( a `  t ) R ( c `  t ) ) ) ) ) )
164 simp1r 1021 . . . . . . . . . . . . . . . . 17  |-  ( ( ( z  e.  On  /\  w  e.  On )  /\  w  e.  z  /\  ( ( A. y  e.  z  (
a `  y )  =  ( b `  y )  /\  A. y  e.  w  (
b `  y )  =  ( c `  y ) )  /\  ( ( a `  z ) R ( b `  z )  /\  ( b `  w ) R ( c `  w ) ) ) )  ->  w  e.  On )
165 onelss 4920 . . . . . . . . . . . . . . . . . . . . 21  |-  ( z  e.  On  ->  (
w  e.  z  ->  w  C_  z ) )
166165imp 429 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( z  e.  On  /\  w  e.  z )  ->  w  C_  z )
167166adantlr 714 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( z  e.  On  /\  w  e.  On )  /\  w  e.  z )  ->  w  C_  z
)
168 ssralv 3564 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( w 
C_  z  ->  ( A. y  e.  z 
( a `  y
)  =  ( b `
 y )  ->  A. y  e.  w  ( a `  y
)  =  ( b `
 y ) ) )
169168anim1d 564 . . . . . . . . . . . . . . . . . . . . 21  |-  ( w 
C_  z  ->  (
( A. y  e.  z  ( a `  y )  =  ( b `  y )  /\  A. y  e.  w  ( b `  y )  =  ( c `  y ) )  ->  ( A. y  e.  w  (
a `  y )  =  ( b `  y )  /\  A. y  e.  w  (
b `  y )  =  ( c `  y ) ) ) )
170 r19.26 2989 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( A. y  e.  w  (
( a `  y
)  =  ( b `
 y )  /\  ( b `  y
)  =  ( c `
 y ) )  <-> 
( A. y  e.  w  ( a `  y )  =  ( b `  y )  /\  A. y  e.  w  ( b `  y )  =  ( c `  y ) ) )
171112ralimi 2857 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( A. y  e.  w  (
( a `  y
)  =  ( b `
 y )  /\  ( b `  y
)  =  ( c `
 y ) )  ->  A. y  e.  w  ( a `  y
)  =  ( c `
 y ) )
172170, 171sylbir 213 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( A. y  e.  w  ( a `  y
)  =  ( b `
 y )  /\  A. y  e.  w  ( b `  y )  =  ( c `  y ) )  ->  A. y  e.  w  ( a `  y
)  =  ( c `
 y ) )
173169, 172syl6 33 . . . . . . . . . . . . . . . . . . . 20  |-  ( w 
C_  z  ->  (
( A. y  e.  z  ( a `  y )  =  ( b `  y )  /\  A. y  e.  w  ( b `  y )  =  ( c `  y ) )  ->  A. y  e.  w  ( a `  y )  =  ( c `  y ) ) )
174173adantrd 468 . . . . . . . . . . . . . . . . . . 19  |-  ( w 
C_  z  ->  (
( ( A. y  e.  z  ( a `  y )  =  ( b `  y )  /\  A. y  e.  w  ( b `  y )  =  ( c `  y ) )  /\  ( ( a `  z ) R ( b `  z )  /\  (
b `  w ) R ( c `  w ) ) )  ->  A. y  e.  w  ( a `  y
)  =  ( c `
 y ) ) )
175167, 174syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( z  e.  On  /\  w  e.  On )  /\  w  e.  z )  ->  ( (
( A. y  e.  z  ( a `  y )  =  ( b `  y )  /\  A. y  e.  w  ( b `  y )  =  ( c `  y ) )  /\  ( ( a `  z ) R ( b `  z )  /\  (
b `  w ) R ( c `  w ) ) )  ->  A. y  e.  w  ( a `  y
)  =  ( c `
 y ) ) )
1761753impia 1193 . . . . . . . . . . . . . . . . 17  |-  ( ( ( z  e.  On  /\  w  e.  On )  /\  w  e.  z  /\  ( ( A. y  e.  z  (
a `  y )  =  ( b `  y )  /\  A. y  e.  w  (
b `  y )  =  ( c `  y ) )  /\  ( ( a `  z ) R ( b `  z )  /\  ( b `  w ) R ( c `  w ) ) ) )  ->  A. y  e.  w  ( a `  y
)  =  ( c `
 y ) )
177 fveq2 5866 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  w  ->  (
a `  y )  =  ( a `  w ) )
178 fveq2 5866 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  w  ->  (
b `  y )  =  ( b `  w ) )
179177, 178eqeq12d 2489 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  =  w  ->  (
( a `  y
)  =  ( b `
 y )  <->  ( a `  w )  =  ( b `  w ) ) )
180179rspcv 3210 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( w  e.  z  ->  ( A. y  e.  z 
( a `  y
)  =  ( b `
 y )  -> 
( a `  w
)  =  ( b `
 w ) ) )
181 breq1 4450 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( a `  w )  =  ( b `  w )  ->  (
( a `  w
) R ( c `
 w )  <->  ( b `  w ) R ( c `  w ) ) )
182181biimprd 223 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( a `  w )  =  ( b `  w )  ->  (
( b `  w
) R ( c `
 w )  -> 
( a `  w
) R ( c `
 w ) ) )
183180, 182syl6 33 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( w  e.  z  ->  ( A. y  e.  z 
( a `  y
)  =  ( b `
 y )  -> 
( ( b `  w ) R ( c `  w )  ->  ( a `  w ) R ( c `  w ) ) ) )
184183com3l 81 . . . . . . . . . . . . . . . . . . . . 21  |-  ( A. y  e.  z  (
a `  y )  =  ( b `  y )  ->  (
( b `  w
) R ( c `
 w )  -> 
( w  e.  z  ->  ( a `  w ) R ( c `  w ) ) ) )
185184imp 429 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A. y  e.  z  ( a `  y
)  =  ( b `
 y )  /\  ( b `  w
) R ( c `
 w ) )  ->  ( w  e.  z  ->  ( a `  w ) R ( c `  w ) ) )
186185ad2ant2rl 748 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( A. y  e.  z  ( a `  y )  =  ( b `  y )  /\  A. y  e.  w  ( b `  y )  =  ( c `  y ) )  /\  ( ( a `  z ) R ( b `  z )  /\  (
b `  w ) R ( c `  w ) ) )  ->  ( w  e.  z  ->  ( a `  w ) R ( c `  w ) ) )
187186impcom 430 . . . . . . . . . . . . . . . . . 18  |-  ( ( w  e.  z  /\  ( ( A. y  e.  z  ( a `  y )  =  ( b `  y )  /\  A. y  e.  w  ( b `  y )  =  ( c `  y ) )  /\  ( ( a `  z ) R ( b `  z )  /\  (
b `  w ) R ( c `  w ) ) ) )  ->  ( a `  w ) R ( c `  w ) )
1881873adant1 1014 . . . . . . . . . . . . . . . . 17  |-  ( ( ( z  e.  On  /\  w  e.  On )  /\  w  e.  z  /\  ( ( A. y  e.  z  (
a `  y )  =  ( b `  y )  /\  A. y  e.  w  (
b `  y )  =  ( c `  y ) )  /\  ( ( a `  z ) R ( b `  z )  /\  ( b `  w ) R ( c `  w ) ) ) )  -> 
( a `  w
) R ( c `
 w ) )
189 raleq 3058 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  w  ->  ( A. y  e.  t 
( a `  y
)  =  ( c `
 y )  <->  A. y  e.  w  ( a `  y )  =  ( c `  y ) ) )
190 fveq2 5866 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  =  w  ->  (
a `  t )  =  ( a `  w ) )
191 fveq2 5866 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  =  w  ->  (
c `  t )  =  ( c `  w ) )
192190, 191breq12d 4460 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  w  ->  (
( a `  t
) R ( c `
 t )  <->  ( a `  w ) R ( c `  w ) ) )
193189, 192anbi12d 710 . . . . . . . . . . . . . . . . . 18  |-  ( t  =  w  ->  (
( A. y  e.  t  ( a `  y )  =  ( c `  y )  /\  ( a `  t ) R ( c `  t ) )  <->  ( A. y  e.  w  ( a `  y )  =  ( c `  y )  /\  ( a `  w ) R ( c `  w ) ) ) )
194193rspcev 3214 . . . . . . . . . . . . . . . . 17  |-  ( ( w  e.  On  /\  ( A. y  e.  w  ( a `  y
)  =  ( c `
 y )  /\  ( a `  w
) R ( c `
 w ) ) )  ->  E. t  e.  On  ( A. y  e.  t  ( a `  y )  =  ( c `  y )  /\  ( a `  t ) R ( c `  t ) ) )
195164, 176, 188, 194syl12anc 1226 . . . . . . . . . . . . . . . 16  |-  ( ( ( z  e.  On  /\  w  e.  On )  /\  w  e.  z  /\  ( ( A. y  e.  z  (
a `  y )  =  ( b `  y )  /\  A. y  e.  w  (
b `  y )  =  ( c `  y ) )  /\  ( ( a `  z ) R ( b `  z )  /\  ( b `  w ) R ( c `  w ) ) ) )  ->  E. t  e.  On  ( A. y  e.  t  ( a `  y
)  =  ( c `
 y )  /\  ( a `  t
) R ( c `
 t ) ) )
196195a1d 25 . . . . . . . . . . . . . . 15  |-  ( ( ( z  e.  On  /\  w  e.  On )  /\  w  e.  z  /\  ( ( A. y  e.  z  (
a `  y )  =  ( b `  y )  /\  A. y  e.  w  (
b `  y )  =  ( c `  y ) )  /\  ( ( a `  z ) R ( b `  z )  /\  ( b `  w ) R ( c `  w ) ) ) )  -> 
( ( ( a  e.  F  /\  b  e.  F )  /\  (
b  e.  F  /\  c  e.  F )
)  ->  E. t  e.  On  ( A. y  e.  t  ( a `  y )  =  ( c `  y )  /\  ( a `  t ) R ( c `  t ) ) ) )
1971963exp 1195 . . . . . . . . . . . . . 14  |-  ( ( z  e.  On  /\  w  e.  On )  ->  ( w  e.  z  ->  ( ( ( A. y  e.  z  ( a `  y
)  =  ( b `
 y )  /\  A. y  e.  w  ( b `  y )  =  ( c `  y ) )  /\  ( ( a `  z ) R ( b `  z )  /\  ( b `  w ) R ( c `  w ) ) )  ->  (
( ( a  e.  F  /\  b  e.  F )  /\  (
b  e.  F  /\  c  e.  F )
)  ->  E. t  e.  On  ( A. y  e.  t  ( a `  y )  =  ( c `  y )  /\  ( a `  t ) R ( c `  t ) ) ) ) ) )
198138, 163, 1973jaod 1292 . . . . . . . . . . . . 13  |-  ( ( z  e.  On  /\  w  e.  On )  ->  ( ( z  e.  w  \/  z  =  w  \/  w  e.  z )  ->  (
( ( A. y  e.  z  ( a `  y )  =  ( b `  y )  /\  A. y  e.  w  ( b `  y )  =  ( c `  y ) )  /\  ( ( a `  z ) R ( b `  z )  /\  (
b `  w ) R ( c `  w ) ) )  ->  ( ( ( a  e.  F  /\  b  e.  F )  /\  ( b  e.  F  /\  c  e.  F
) )  ->  E. t  e.  On  ( A. y  e.  t  ( a `  y )  =  ( c `  y )  /\  ( a `  t ) R ( c `  t ) ) ) ) ) )
199103, 198mpd 15 . . . . . . . . . . . 12  |-  ( ( z  e.  On  /\  w  e.  On )  ->  ( ( ( A. y  e.  z  (
a `  y )  =  ( b `  y )  /\  A. y  e.  w  (
b `  y )  =  ( c `  y ) )  /\  ( ( a `  z ) R ( b `  z )  /\  ( b `  w ) R ( c `  w ) ) )  ->  (
( ( a  e.  F  /\  b  e.  F )  /\  (
b  e.  F  /\  c  e.  F )
)  ->  E. t  e.  On  ( A. y  e.  t  ( a `  y )  =  ( c `  y )  /\  ( a `  t ) R ( c `  t ) ) ) ) )
200199rexlimivv 2960 . . . . . . . . . . 11  |-  ( E. z  e.  On  E. w  e.  On  (
( A. y  e.  z  ( a `  y )  =  ( b `  y )  /\  A. y  e.  w  ( b `  y )  =  ( c `  y ) )  /\  ( ( a `  z ) R ( b `  z )  /\  (
b `  w ) R ( c `  w ) ) )  ->  ( ( ( a  e.  F  /\  b  e.  F )  /\  ( b  e.  F  /\  c  e.  F
) )  ->  E. t  e.  On  ( A. y  e.  t  ( a `  y )  =  ( c `  y )  /\  ( a `  t ) R ( c `  t ) ) ) )
20199, 200sylbir 213 . . . . . . . . . 10  |-  ( ( E. z  e.  On  ( A. y  e.  z  ( a `  y
)  =  ( b `
 y )  /\  ( a `  z
) R ( b `
 z ) )  /\  E. w  e.  On  ( A. y  e.  w  ( b `  y )  =  ( c `  y )  /\  ( b `  w ) R ( c `  w ) ) )  ->  (
( ( a  e.  F  /\  b  e.  F )  /\  (
b  e.  F  /\  c  e.  F )
)  ->  E. t  e.  On  ( A. y  e.  t  ( a `  y )  =  ( c `  y )  /\  ( a `  t ) R ( c `  t ) ) ) )
202201impcom 430 . . . . . . . . 9  |-  ( ( ( ( a  e.  F  /\  b  e.  F )  /\  (
b  e.  F  /\  c  e.  F )
)  /\  ( E. z  e.  On  ( A. y  e.  z 
( a `  y
)  =  ( b `
 y )  /\  ( a `  z
) R ( b `
 z ) )  /\  E. w  e.  On  ( A. y  e.  w  ( b `  y )  =  ( c `  y )  /\  ( b `  w ) R ( c `  w ) ) ) )  ->  E. t  e.  On  ( A. y  e.  t  ( a `  y
)  =  ( c `
 y )  /\  ( a `  t
) R ( c `
 t ) ) )
20394, 95, 202jca31 534 . . . . . . . 8  |-  ( ( ( ( a  e.  F  /\  b  e.  F )  /\  (
b  e.  F  /\  c  e.  F )
)  /\  ( E. z  e.  On  ( A. y  e.  z 
( a `  y
)  =  ( b `
 y )  /\  ( a `  z
) R ( b `
 z ) )  /\  E. w  e.  On  ( A. y  e.  w  ( b `  y )  =  ( c `  y )  /\  ( b `  w ) R ( c `  w ) ) ) )  -> 
( ( a  e.  F  /\  c  e.  F )  /\  E. t  e.  On  ( A. y  e.  t 
( a `  y
)  =  ( c `
 y )  /\  ( a `  t
) R ( c `
 t ) ) ) )
204203an4s 824 . . . . . . 7  |-  ( ( ( ( a  e.  F  /\  b  e.  F )  /\  E. z  e.  On  ( A. y  e.  z 
( a `  y
)  =  ( b `
 y )  /\  ( a `  z
) R ( b `
 z ) ) )  /\  ( ( b  e.  F  /\  c  e.  F )  /\  E. w  e.  On  ( A. y  e.  w  ( b `  y
)  =  ( c `
 y )  /\  ( b `  w
) R ( c `
 w ) ) ) )  ->  (
( a  e.  F  /\  c  e.  F
)  /\  E. t  e.  On  ( A. y  e.  t  ( a `  y )  =  ( c `  y )  /\  ( a `  t ) R ( c `  t ) ) ) )
20564, 93, 204syl2anb 479 . . . . . 6  |-  ( ( a S b  /\  b S c )  -> 
( ( a  e.  F  /\  c  e.  F )  /\  E. t  e.  On  ( A. y  e.  t 
( a `  y
)  =  ( c `
 y )  /\  ( a `  t
) R ( c `
 t ) ) ) )
206 raleq 3058 . . . . . . . . . . 11  |-  ( x  =  t  ->  ( A. y  e.  x  ( f `  y
)  =  ( g `
 y )  <->  A. y  e.  t  ( f `  y )  =  ( g `  y ) ) )
207 fveq2 5866 . . . . . . . . . . . 12  |-  ( x  =  t  ->  (
f `  x )  =  ( f `  t ) )
208 fveq2 5866 . . . . . . . . . . . 12  |-  ( x  =  t  ->  (
g `  x )  =  ( g `  t ) )
209207, 208breq12d 4460 . . . . . . . . . . 11  |-  ( x  =  t  ->  (
( f `  x
) R ( g `
 x )  <->  ( f `  t ) R ( g `  t ) ) )
210206, 209anbi12d 710 . . . . . . . . . 10  |-  ( x  =  t  ->  (
( A. y  e.  x  ( f `  y )  =  ( g `  y )  /\  ( f `  x ) R ( g `  x ) )  <->  ( A. y  e.  t  ( f `  y )  =  ( g `  y )  /\  ( f `  t ) R ( g `  t ) ) ) )
211210cbvrexv 3089 . . . . . . . . 9  |-  ( E. x  e.  On  ( A. y  e.  x  ( f `  y
)  =  ( g `
 y )  /\  ( f `  x
) R ( g `
 x ) )  <->  E. t  e.  On  ( A. y  e.  t  ( f `  y
)  =  ( g `
 y )  /\  ( f `  t
) R ( g `
 t ) ) )
21220ralbidv 2903 . . . . . . . . . . 11  |-  ( f  =  a  ->  ( A. y  e.  t 
( f `  y
)  =  ( g `
 y )  <->  A. y  e.  t  ( a `  y )  =  ( g `  y ) ) )
213 fveq1 5865 . . . . . . . . . . . 12  |-  ( f  =  a  ->  (
f `  t )  =  ( a `  t ) )
214213breq1d 4457 . . . . . . . . . . 11  |-  ( f  =  a  ->  (
( f `  t
) R ( g `
 t )  <->  ( a `  t ) R ( g `  t ) ) )
215212, 214anbi12d 710 . . . . . . . . . 10  |-  ( f  =  a  ->  (
( A. y  e.  t  ( f `  y )  =  ( g `  y )  /\  ( f `  t ) R ( g `  t ) )  <->  ( A. y  e.  t  ( a `  y )  =  ( g `  y )  /\  ( a `  t ) R ( g `  t ) ) ) )
216215rexbidv 2973 . . . . . . . . 9  |-  ( f  =  a  ->  ( E. t  e.  On  ( A. y  e.  t  ( f `  y
)  =  ( g `
 y )  /\  ( f `  t
) R ( g `
 t ) )  <->  E. t  e.  On  ( A. y  e.  t  ( a `  y
)  =  ( g `
 y )  /\  ( a `  t
) R ( g `
 t ) ) ) )
217211, 216syl5bb 257 . . . . . . . 8  |-  ( f  =  a  ->  ( E. x  e.  On  ( A. y  e.  x  ( f `  y
)  =  ( g `
 y )  /\  ( f `  x
) R ( g `
 x ) )  <->  E. t  e.  On  ( A. y  e.  t  ( a `  y
)  =  ( g `
 y )  /\  ( a `  t
) R ( g `
 t ) ) ) )
21818, 217anbi12d 710 . . . . . . 7  |-  ( f  =  a  ->  (
( ( f  e.  F  /\  g  e.  F )  /\  E. x  e.  On  ( A. y  e.  x  ( f `  y
)  =  ( g `
 y )  /\  ( f `  x
) R ( g `
 x ) ) )  <->  ( ( a  e.  F  /\  g  e.  F )  /\  E. t  e.  On  ( A. y  e.  t 
( a `  y
)  =  ( g `
 y )  /\  ( a `  t
) R ( g `
 t ) ) ) ) )
21983anbi2d 703 . . . . . . . 8  |-  ( g  =  c  ->  (
( a  e.  F  /\  g  e.  F
)  <->  ( a  e.  F  /\  c  e.  F ) ) )
22085eqeq2d 2481 . . . . . . . . . . 11  |-  ( g  =  c  ->  (
( a `  y
)  =  ( g `
 y )  <->  ( a `  y )  =  ( c `  y ) ) )
221220ralbidv 2903 . . . . . . . . . 10  |-  ( g  =  c  ->  ( A. y  e.  t 
( a `  y
)  =  ( g `
 y )  <->  A. y  e.  t  ( a `  y )  =  ( c `  y ) ) )
222 fveq1 5865 . . . . . . . . . . 11  |-  ( g  =  c  ->  (
g `  t )  =  ( c `  t ) )
223222breq2d 4459 . . . . . . . . . 10  |-  ( g  =  c  ->  (
( a `  t
) R ( g `
 t )  <->  ( a `  t ) R ( c `  t ) ) )
224221, 223anbi12d 710 . . . . . . . . 9  |-  ( g  =  c  ->  (
( A. y  e.  t  ( a `  y )  =  ( g `  y )  /\  ( a `  t ) R ( g `  t ) )  <->  ( A. y  e.  t  ( a `  y )  =  ( c `  y )  /\  ( a `  t ) R ( c `  t ) ) ) )
225224rexbidv 2973 . . . . . . . 8  |-  ( g  =  c  ->  ( E. t  e.  On  ( A. y  e.  t  ( a `  y
)  =  ( g `
 y )  /\  ( a `  t
) R ( g `
 t ) )  <->  E. t  e.  On  ( A. y  e.  t  ( a `  y
)  =  ( c `
 y )  /\  ( a `  t
) R ( c `
 t ) ) ) )
226219, 225anbi12d 710 . . . . . . 7  |-  ( g  =  c  ->  (
( ( a  e.  F  /\  g  e.  F )  /\  E. t  e.  On  ( A. y  e.  t 
( a `  y
)  =  ( g `
 y )  /\  ( a `  t
) R ( g `
 t ) ) )  <->  ( ( a  e.  F  /\  c  e.  F )  /\  E. t  e.  On  ( A. y  e.  t 
( a `  y
)  =  ( c `
 y )  /\  ( a `  t
) R ( c `
 t ) ) ) ) )
22716, 65, 218, 226, 37brab 4770 . . . . . 6  |-  ( a S c  <->  ( (
a  e.  F  /\  c  e.  F )  /\  E. t  e.  On  ( A. y  e.  t  ( a `  y
)  =  ( c `
 y )  /\  ( a `  t
) R ( c `
 t ) ) ) )
228205, 227sylibr 212 . . . . 5  |-  ( ( a S b  /\  b S c )  -> 
a S c )
22939, 228pm3.2i 455 . . . 4  |-  ( -.  a S a  /\  ( ( a S b  /\  b S c )  ->  a S c ) )
230229a1i 11 . . 3  |-  ( ( a  e.  F  /\  b  e.  F  /\  c  e.  F )  ->  ( -.  a S a  /\  ( ( a S b  /\  b S c )  -> 
a S c ) ) )
231230rgen3 2890 . 2  |-  A. a  e.  F  A. b  e.  F  A. c  e.  F  ( -.  a S a  /\  (
( a S b  /\  b S c )  ->  a S
c ) )
232 df-po 4800 . 2  |-  ( S  Po  F  <->  A. a  e.  F  A. b  e.  F  A. c  e.  F  ( -.  a S a  /\  (
( a S b  /\  b S c )  ->  a S
c ) ) )
233231, 232mpbir 209 1  |-  S  Po  F
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 369    \/ w3o 972    /\ w3a 973    = wceq 1379    e. wcel 1767   {cab 2452   A.wral 2814   E.wrex 2815    u. cun 3474    C_ wss 3476   (/)c0 3785   {csn 4027   class class class wbr 4447   {copab 4504    Po wpo 4798   Ord word 4877   Oncon0 4878   -->wf 5584   ` cfv 5588
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-8 1769  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4568  ax-nul 4576  ax-pow 4625  ax-pr 4686
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 974  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2819  df-rex 2820  df-rab 2823  df-v 3115  df-sbc 3332  df-dif 3479  df-un 3481  df-in 3483  df-ss 3490  df-pss 3492  df-nul 3786  df-if 3940  df-sn 4028  df-pr 4030  df-op 4034  df-uni 4246  df-br 4448  df-opab 4506  df-tr 4541  df-eprel 4791  df-po 4800  df-so 4801  df-fr 4838  df-we 4840  df-ord 4881  df-on 4882  df-rel 5006  df-cnv 5007  df-co 5008  df-dm 5009  df-rn 5010  df-iota 5551  df-fun 5590  df-fn 5591  df-f 5592  df-fv 5596
This theorem is referenced by:  soseq  28939
  Copyright terms: Public domain W3C validator