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

Theorem poseq 25533
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 5580 . . . . . . . . . . . . . . . 16  |-  ( x  =  b  ->  (
f : x --> A  <->  f :
b --> A ) )
43cbvrexv 2935 . . . . . . . . . . . . . . 15  |-  ( E. x  e.  On  f : x --> A  <->  E. b  e.  On  f : b --> A )
54abbii 2550 . . . . . . . . . . . . . 14  |-  { f  |  E. x  e.  On  f : x --> A }  =  {
f  |  E. b  e.  On  f : b --> A }
62, 5eqtri 2458 . . . . . . . . . . . . 13  |-  F  =  { f  |  E. b  e.  On  f : b --> A }
76orderseqlem 25532 . . . . . . . . . . . 12  |-  ( a  e.  F  ->  (
a `  x )  e.  ( A  u.  { (/)
} ) )
8 poirr 4517 . . . . . . . . . . . 12  |-  ( ( R  Po  ( A  u.  { (/) } )  /\  ( a `  x )  e.  ( A  u.  { (/) } ) )  ->  -.  ( a `  x
) R ( a `
 x ) )
91, 7, 8sylancr 646 . . . . . . . . . . 11  |-  ( a  e.  F  ->  -.  ( a `  x
) R ( a `
 x ) )
109intnand 884 . . . . . . . . . 10  |-  ( a  e.  F  ->  -.  ( A. y  e.  x  ( a `  y
)  =  ( a `
 y )  /\  ( a `  x
) R ( a `
 x ) ) )
1110adantr 453 . . . . . . . . 9  |-  ( ( a  e.  F  /\  x  e.  On )  ->  -.  ( A. y  e.  x  ( a `  y )  =  ( a `  y )  /\  ( a `  x ) R ( a `  x ) ) )
1211nrexdv 2811 . . . . . . . 8  |-  ( a  e.  F  ->  -.  E. x  e.  On  ( A. y  e.  x  ( a `  y
)  =  ( a `
 y )  /\  ( a `  x
) R ( a `
 x ) ) )
1312adantr 453 . . . . . . 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 413 . . . . . . 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 201 . . . . . 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 2961 . . . . . . 7  |-  a  e. 
_V
17 eleq1 2498 . . . . . . . . 9  |-  ( f  =  a  ->  (
f  e.  F  <->  a  e.  F ) )
1817anbi1d 687 . . . . . . . 8  |-  ( f  =  a  ->  (
( f  e.  F  /\  g  e.  F
)  <->  ( a  e.  F  /\  g  e.  F ) ) )
19 fveq1 5730 . . . . . . . . . . . 12  |-  ( f  =  a  ->  (
f `  y )  =  ( a `  y ) )
2019eqeq1d 2446 . . . . . . . . . . 11  |-  ( f  =  a  ->  (
( f `  y
)  =  ( g `
 y )  <->  ( a `  y )  =  ( g `  y ) ) )
2120ralbidv 2727 . . . . . . . . . 10  |-  ( f  =  a  ->  ( A. y  e.  x  ( f `  y
)  =  ( g `
 y )  <->  A. y  e.  x  ( a `  y )  =  ( g `  y ) ) )
22 fveq1 5730 . . . . . . . . . . 11  |-  ( f  =  a  ->  (
f `  x )  =  ( a `  x ) )
2322breq1d 4225 . . . . . . . . . 10  |-  ( f  =  a  ->  (
( f `  x
) R ( g `
 x )  <->  ( a `  x ) R ( g `  x ) ) )
2421, 23anbi12d 693 . . . . . . . . 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 2728 . . . . . . . 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 693 . . . . . . 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 2498 . . . . . . . . 9  |-  ( g  =  a  ->  (
g  e.  F  <->  a  e.  F ) )
2827anbi2d 686 . . . . . . . 8  |-  ( g  =  a  ->  (
( a  e.  F  /\  g  e.  F
)  <->  ( a  e.  F  /\  a  e.  F ) ) )
29 fveq1 5730 . . . . . . . . . . . 12  |-  ( g  =  a  ->  (
g `  y )  =  ( a `  y ) )
3029eqeq2d 2449 . . . . . . . . . . 11  |-  ( g  =  a  ->  (
( a `  y
)  =  ( g `
 y )  <->  ( a `  y )  =  ( a `  y ) ) )
3130ralbidv 2727 . . . . . . . . . 10  |-  ( g  =  a  ->  ( A. y  e.  x  ( a `  y
)  =  ( g `
 y )  <->  A. y  e.  x  ( a `  y )  =  ( a `  y ) ) )
32 fveq1 5730 . . . . . . . . . . 11  |-  ( g  =  a  ->  (
g `  x )  =  ( a `  x ) )
3332breq2d 4227 . . . . . . . . . 10  |-  ( g  =  a  ->  (
( a `  x
) R ( g `
 x )  <->  ( a `  x ) R ( a `  x ) ) )
3431, 33anbi12d 693 . . . . . . . . 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 2728 . . . . . . . 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 693 . . . . . . 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 4480 . . . . . 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 292 . . . . 5  |-  -.  a S a
40 vex 2961 . . . . . . . 8  |-  b  e. 
_V
41 raleq 2906 . . . . . . . . . . . 12  |-  ( x  =  z  ->  ( A. y  e.  x  ( f `  y
)  =  ( g `
 y )  <->  A. y  e.  z  ( f `  y )  =  ( g `  y ) ) )
42 fveq2 5731 . . . . . . . . . . . . 13  |-  ( x  =  z  ->  (
f `  x )  =  ( f `  z ) )
43 fveq2 5731 . . . . . . . . . . . . 13  |-  ( x  =  z  ->  (
g `  x )  =  ( g `  z ) )
4442, 43breq12d 4228 . . . . . . . . . . . 12  |-  ( x  =  z  ->  (
( f `  x
) R ( g `
 x )  <->  ( f `  z ) R ( g `  z ) ) )
4541, 44anbi12d 693 . . . . . . . . . . 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 2935 . . . . . . . . . 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 2727 . . . . . . . . . . . 12  |-  ( f  =  a  ->  ( A. y  e.  z 
( f `  y
)  =  ( g `
 y )  <->  A. y  e.  z  ( a `  y )  =  ( g `  y ) ) )
48 fveq1 5730 . . . . . . . . . . . . 13  |-  ( f  =  a  ->  (
f `  z )  =  ( a `  z ) )
4948breq1d 4225 . . . . . . . . . . . 12  |-  ( f  =  a  ->  (
( f `  z
) R ( g `
 z )  <->  ( a `  z ) R ( g `  z ) ) )
5047, 49anbi12d 693 . . . . . . . . . . 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 2728 . . . . . . . . . 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 250 . . . . . . . . 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 693 . . . . . . . 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 2498 . . . . . . . . . 10  |-  ( g  =  b  ->  (
g  e.  F  <->  b  e.  F ) )
5554anbi2d 686 . . . . . . . . 9  |-  ( g  =  b  ->  (
( a  e.  F  /\  g  e.  F
)  <->  ( a  e.  F  /\  b  e.  F ) ) )
56 fveq1 5730 . . . . . . . . . . . . 13  |-  ( g  =  b  ->  (
g `  y )  =  ( b `  y ) )
5756eqeq2d 2449 . . . . . . . . . . . 12  |-  ( g  =  b  ->  (
( a `  y
)  =  ( g `
 y )  <->  ( a `  y )  =  ( b `  y ) ) )
5857ralbidv 2727 . . . . . . . . . . 11  |-  ( g  =  b  ->  ( A. y  e.  z 
( a `  y
)  =  ( g `
 y )  <->  A. y  e.  z  ( a `  y )  =  ( b `  y ) ) )
59 fveq1 5730 . . . . . . . . . . . 12  |-  ( g  =  b  ->  (
g `  z )  =  ( b `  z ) )
6059breq2d 4227 . . . . . . . . . . 11  |-  ( g  =  b  ->  (
( a `  z
) R ( g `
 z )  <->  ( a `  z ) R ( b `  z ) ) )
6158, 60anbi12d 693 . . . . . . . . . 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 2728 . . . . . . . . 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 693 . . . . . . . 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 4480 . . . . . . 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 2961 . . . . . . . 8  |-  c  e. 
_V
66 eleq1 2498 . . . . . . . . . 10  |-  ( f  =  b  ->  (
f  e.  F  <->  b  e.  F ) )
6766anbi1d 687 . . . . . . . . 9  |-  ( f  =  b  ->  (
( f  e.  F  /\  g  e.  F
)  <->  ( b  e.  F  /\  g  e.  F ) ) )
68 raleq 2906 . . . . . . . . . . . 12  |-  ( x  =  w  ->  ( A. y  e.  x  ( f `  y
)  =  ( g `
 y )  <->  A. y  e.  w  ( f `  y )  =  ( g `  y ) ) )
69 fveq2 5731 . . . . . . . . . . . . 13  |-  ( x  =  w  ->  (
f `  x )  =  ( f `  w ) )
70 fveq2 5731 . . . . . . . . . . . . 13  |-  ( x  =  w  ->  (
g `  x )  =  ( g `  w ) )
7169, 70breq12d 4228 . . . . . . . . . . . 12  |-  ( x  =  w  ->  (
( f `  x
) R ( g `
 x )  <->  ( f `  w ) R ( g `  w ) ) )
7268, 71anbi12d 693 . . . . . . . . . . 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 2935 . . . . . . . . . 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 5730 . . . . . . . . . . . . . 14  |-  ( f  =  b  ->  (
f `  y )  =  ( b `  y ) )
7574eqeq1d 2446 . . . . . . . . . . . . 13  |-  ( f  =  b  ->  (
( f `  y
)  =  ( g `
 y )  <->  ( b `  y )  =  ( g `  y ) ) )
7675ralbidv 2727 . . . . . . . . . . . 12  |-  ( f  =  b  ->  ( A. y  e.  w  ( f `  y
)  =  ( g `
 y )  <->  A. y  e.  w  ( b `  y )  =  ( g `  y ) ) )
77 fveq1 5730 . . . . . . . . . . . . 13  |-  ( f  =  b  ->  (
f `  w )  =  ( b `  w ) )
7877breq1d 4225 . . . . . . . . . . . 12  |-  ( f  =  b  ->  (
( f `  w
) R ( g `
 w )  <->  ( b `  w ) R ( g `  w ) ) )
7976, 78anbi12d 693 . . . . . . . . . . 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 2728 . . . . . . . . . 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 250 . . . . . . . . 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 693 . . . . . . . 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 2498 . . . . . . . . . 10  |-  ( g  =  c  ->  (
g  e.  F  <->  c  e.  F ) )
8483anbi2d 686 . . . . . . . . 9  |-  ( g  =  c  ->  (
( b  e.  F  /\  g  e.  F
)  <->  ( b  e.  F  /\  c  e.  F ) ) )
85 fveq1 5730 . . . . . . . . . . . . 13  |-  ( g  =  c  ->  (
g `  y )  =  ( c `  y ) )
8685eqeq2d 2449 . . . . . . . . . . . 12  |-  ( g  =  c  ->  (
( b `  y
)  =  ( g `
 y )  <->  ( b `  y )  =  ( c `  y ) ) )
8786ralbidv 2727 . . . . . . . . . . 11  |-  ( g  =  c  ->  ( A. y  e.  w  ( b `  y
)  =  ( g `
 y )  <->  A. y  e.  w  ( b `  y )  =  ( c `  y ) ) )
88 fveq1 5730 . . . . . . . . . . . 12  |-  ( g  =  c  ->  (
g `  w )  =  ( c `  w ) )
8988breq2d 4227 . . . . . . . . . . 11  |-  ( g  =  c  ->  (
( b `  w
) R ( g `
 w )  <->  ( b `  w ) R ( c `  w ) ) )
9087, 89anbi12d 693 . . . . . . . . . 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 2728 . . . . . . . . 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 693 . . . . . . . 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 4480 . . . . . . 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 736 . . . . . . . . 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 739 . . . . . . . . 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 799 . . . . . . . . . . . . 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 2734 . . . . . . . . . . . 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 2877 . . . . . . . . . . . 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 242 . . . . . . . . . . 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 4594 . . . . . . . . . . . . . 14  |-  ( z  e.  On  ->  Ord  z )
101 eloni 4594 . . . . . . . . . . . . . 14  |-  ( w  e.  On  ->  Ord  w )
102 ordtri3or 4616 . . . . . . . . . . . . . 14  |-  ( ( Ord  z  /\  Ord  w )  ->  (
z  e.  w  \/  z  =  w  \/  w  e.  z ) )
103100, 101, 102syl2an 465 . . . . . . . . . . . . 13  |-  ( ( z  e.  On  /\  w  e.  On )  ->  ( z  e.  w  \/  z  =  w  \/  w  e.  z
) )
104 simp1l 982 . . . . . . . . . . . . . . . . 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 4626 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( w  e.  On  ->  (
z  e.  w  -> 
z  C_  w )
)
106105imp 420 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( w  e.  On  /\  z  e.  w )  ->  z  C_  w )
107106adantll 696 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( z  e.  On  /\  w  e.  On )  /\  z  e.  w
)  ->  z  C_  w )
108 ssralv 3409 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( z 
C_  w  ->  ( A. y  e.  w  ( b `  y
)  =  ( c `
 y )  ->  A. y  e.  z 
( b `  y
)  =  ( c `
 y ) ) )
109108anim2d 550 . . . . . . . . . . . . . . . . . . . . . 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 2840 . . . . . . . . . . . . . . . . . . . . . 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 220 . . . . . . . . . . . . . . . . . . . . 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 2455 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( a `  y
)  =  ( b `
 y )  /\  ( b `  y
)  =  ( c `
 y ) )  ->  ( a `  y )  =  ( c `  y ) )
113112ralimi 2783 . . . . . . . . . . . . . . . . . . . . 21  |-  ( A. y  e.  z  (
( a `  y
)  =  ( b `
 y )  /\  ( b `  y
)  =  ( c `
 y ) )  ->  A. y  e.  z  ( a `  y
)  =  ( c `
 y ) )
114111, 113syl6 32 . . . . . . . . . . . . . . . . . . . 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 456 . . . . . . . . . . . . . . . . . 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 1151 . . . . . . . . . . . . . . . . 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 5731 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  z  ->  (
b `  y )  =  ( b `  z ) )
119 fveq2 5731 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  z  ->  (
c `  y )  =  ( c `  z ) )
120118, 119eqeq12d 2452 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  =  z  ->  (
( b `  y
)  =  ( c `
 y )  <->  ( b `  z )  =  ( c `  z ) ) )
121120rspcv 3050 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( z  e.  w  ->  ( A. y  e.  w  ( b `  y
)  =  ( c `
 y )  -> 
( b `  z
)  =  ( c `
 z ) ) )
122 breq2 4219 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( b `  z )  =  ( c `  z )  ->  (
( a `  z
) R ( b `
 z )  <->  ( a `  z ) R ( c `  z ) ) )
123122biimpd 200 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( b `  z )  =  ( c `  z )  ->  (
( a `  z
) R ( b `
 z )  -> 
( a `  z
) R ( c `
 z ) ) )
124121, 123syl6 32 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( z  e.  w  ->  ( A. y  e.  w  ( b `  y
)  =  ( c `
 y )  -> 
( ( a `  z ) R ( b `  z )  ->  ( a `  z ) R ( c `  z ) ) ) )
125124com3l 78 . . . . . . . . . . . . . . . . . . . . 21  |-  ( A. y  e.  w  (
b `  y )  =  ( c `  y )  ->  (
( a `  z
) R ( b `
 z )  -> 
( z  e.  w  ->  ( a `  z
) R ( c `
 z ) ) ) )
126125imp 420 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A. y  e.  w  ( b `  y
)  =  ( c `
 y )  /\  ( a `  z
) R ( b `
 z ) )  ->  ( z  e.  w  ->  ( a `  z ) R ( c `  z ) ) )
127126ad2ant2lr 730 . . . . . . . . . . . . . . . . . . 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 421 . . . . . . . . . . . . . . . . . 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 976 . . . . . . . . . . . . . . . . 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 2906 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  z  ->  ( A. y  e.  t 
( a `  y
)  =  ( c `
 y )  <->  A. y  e.  z  ( a `  y )  =  ( c `  y ) ) )
131 fveq2 5731 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  =  z  ->  (
a `  t )  =  ( a `  z ) )
132 fveq2 5731 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  =  z  ->  (
c `  t )  =  ( c `  z ) )
133131, 132breq12d 4228 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  z  ->  (
( a `  t
) R ( c `
 t )  <->  ( a `  z ) R ( c `  z ) ) )
134130, 133anbi12d 693 . . . . . . . . . . . . . . . . . 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 3054 . . . . . . . . . . . . . . . . 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 1183 . . . . . . . . . . . . . . . 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 24 . . . . . . . . . . . . . . 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 1153 . . . . . . . . . . . . . 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 25532 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( a  e.  F  ->  (
a `  z )  e.  ( A  u.  { (/)
} ) )
140139ad2antrr 708 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( a  e.  F  /\  b  e.  F
)  /\  ( b  e.  F  /\  c  e.  F ) )  -> 
( a `  z
)  e.  ( A  u.  { (/) } ) )
1412orderseqlem 25532 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( b  e.  F  ->  (
b `  z )  e.  ( A  u.  { (/)
} ) )
142141ad2antlr 709 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( a  e.  F  /\  b  e.  F
)  /\  ( b  e.  F  /\  c  e.  F ) )  -> 
( b `  z
)  e.  ( A  u.  { (/) } ) )
1432orderseqlem 25532 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( c  e.  F  ->  (
c `  z )  e.  ( A  u.  { (/)
} ) )
144143ad2antll 711 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( a  e.  F  /\  b  e.  F
)  /\  ( b  e.  F  /\  c  e.  F ) )  -> 
( c `  z
)  e.  ( A  u.  { (/) } ) )
145140, 142, 1443jca 1135 . . . . . . . . . . . . . . . . . . . . . 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 4518 . . . . . . . . . . . . . . . . . . . . . 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 646 . . . . . . . . . . . . . . . . . . . . 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 421 . . . . . . . . . . . . . . . . . . . 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 551 . . . . . . . . . . . . . . . . . . 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 631 . . . . . . . . . . . . . . . . . 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 462 . . . . . . . . . . . . . . . . 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 590 . . . . . . . . . . . . . . . 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 2906 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  =  w  ->  ( A. y  e.  z 
( b `  y
)  =  ( c `
 y )  <->  A. y  e.  w  ( b `  y )  =  ( c `  y ) ) )
154153anbi2d 686 . . . . . . . . . . . . . . . . . . 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 250 . . . . . . . . . . . . . . . . . 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 5731 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  =  w  ->  (
b `  z )  =  ( b `  w ) )
157 fveq2 5731 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  =  w  ->  (
c `  z )  =  ( c `  w ) )
158156, 157breq12d 4228 . . . . . . . . . . . . . . . . . . 19  |-  ( z  =  w  ->  (
( b `  z
) R ( c `
 z )  <->  ( b `  w ) R ( c `  w ) ) )
159158anbi2d 686 . . . . . . . . . . . . . . . . . 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 693 . . . . . . . . . . . . . . . . 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 310 . . . . . . . . . . . . . . . 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 213 . . . . . . . . . . . . . . 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 453 . . . . . . . . . . . . . 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 983 . . . . . . . . . . . . . . . . 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 4626 . . . . . . . . . . . . . . . . . . . . 21  |-  ( z  e.  On  ->  (
w  e.  z  ->  w  C_  z ) )
166165imp 420 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( z  e.  On  /\  w  e.  z )  ->  w  C_  z )
167166adantlr 697 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( z  e.  On  /\  w  e.  On )  /\  w  e.  z )  ->  w  C_  z
)
168 ssralv 3409 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( w 
C_  z  ->  ( A. y  e.  z 
( a `  y
)  =  ( b `
 y )  ->  A. y  e.  w  ( a `  y
)  =  ( b `
 y ) ) )
169168anim1d 549 . . . . . . . . . . . . . . . . . . . . 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 2840 . . . . . . . . . . . . . . . . . . . . . 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 2783 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( A. y  e.  w  (
( a `  y
)  =  ( b `
 y )  /\  ( b `  y
)  =  ( c `
 y ) )  ->  A. y  e.  w  ( a `  y
)  =  ( c `
 y ) )
172170, 171sylbir 206 . . . . . . . . . . . . . . . . . . . . 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 32 . . . . . . . . . . . . . . . . . . . 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 456 . . . . . . . . . . . . . . . . . . 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 1151 . . . . . . . . . . . . . . . . 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 5731 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  w  ->  (
a `  y )  =  ( a `  w ) )
178 fveq2 5731 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  w  ->  (
b `  y )  =  ( b `  w ) )
179177, 178eqeq12d 2452 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  =  w  ->  (
( a `  y
)  =  ( b `
 y )  <->  ( a `  w )  =  ( b `  w ) ) )
180179rspcv 3050 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( w  e.  z  ->  ( A. y  e.  z 
( a `  y
)  =  ( b `
 y )  -> 
( a `  w
)  =  ( b `
 w ) ) )
181 breq1 4218 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( a `  w )  =  ( b `  w )  ->  (
( a `  w
) R ( c `
 w )  <->  ( b `  w ) R ( c `  w ) ) )
182181biimprd 216 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( a `  w )  =  ( b `  w )  ->  (
( b `  w
) R ( c `
 w )  -> 
( a `  w
) R ( c `
 w ) ) )
183180, 182syl6 32 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( w  e.  z  ->  ( A. y  e.  z 
( a `  y
)  =  ( b `
 y )  -> 
( ( b `  w ) R ( c `  w )  ->  ( a `  w ) R ( c `  w ) ) ) )
184183com3l 78 . . . . . . . . . . . . . . . . . . . . 21  |-  ( A. y  e.  z  (
a `  y )  =  ( b `  y )  ->  (
( b `  w
) R ( c `
 w )  -> 
( w  e.  z  ->  ( a `  w ) R ( c `  w ) ) ) )
185184imp 420 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A. y  e.  z  ( a `  y
)  =  ( b `
 y )  /\  ( b `  w
) R ( c `
 w ) )  ->  ( w  e.  z  ->  ( a `  w ) R ( c `  w ) ) )
186185ad2ant2rl 731 . . . . . . . . . . . . . . . . . . 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 421 . . . . . . . . . . . . . . . . . 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 976 . . . . . . . . . . . . . . . . 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 2906 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  w  ->  ( A. y  e.  t 
( a `  y
)  =  ( c `
 y )  <->  A. y  e.  w  ( a `  y )  =  ( c `  y ) ) )
190 fveq2 5731 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  =  w  ->  (
a `  t )  =  ( a `  w ) )
191 fveq2 5731 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  =  w  ->  (
c `  t )  =  ( c `  w ) )
192190, 191breq12d 4228 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  w  ->  (
( a `  t
) R ( c `
 t )  <->  ( a `  w ) R ( c `  w ) ) )
193189, 192anbi12d 693 . . . . . . . . . . . . . . . . . 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 3054 . . . . . . . . . . . . . . . . 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 1183 . . . . . . . . . . . . . . . 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 24 . . . . . . . . . . . . . . 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 1153 . . . . . . . . . . . . . 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 1249 . . . . . . . . . . . . 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 2837 . . . . . . . . . . 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 206 . . . . . . . . . 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 421 . . . . . . . . 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 522 . . . . . . . 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 801 . . . . . . 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 467 . . . . . 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 2906 . . . . . . . . . . 11  |-  ( x  =  t  ->  ( A. y  e.  x  ( f `  y
)  =  ( g `
 y )  <->  A. y  e.  t  ( f `  y )  =  ( g `  y ) ) )
207 fveq2 5731 . . . . . . . . . . . 12  |-  ( x  =  t  ->  (
f `  x )  =  ( f `  t ) )
208 fveq2 5731 . . . . . . . . . . . 12  |-  ( x  =  t  ->  (
g `  x )  =  ( g `  t ) )
209207, 208breq12d 4228 . . . . . . . . . . 11  |-  ( x  =  t  ->  (
( f `  x
) R ( g `
 x )  <->  ( f `  t ) R ( g `  t ) ) )
210206, 209anbi12d 693 . . . . . . . . . 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 2935 . . . . . . . . 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 2727 . . . . . . . . . . 11  |-  ( f  =  a  ->  ( A. y  e.  t 
( f `  y
)  =  ( g `
 y )  <->  A. y  e.  t  ( a `  y )  =  ( g `  y ) ) )
213 fveq1 5730 . . . . . . . . . . . 12  |-  ( f  =  a  ->  (
f `  t )  =  ( a `  t ) )
214213breq1d 4225 . . . . . . . . . . 11  |-  ( f  =  a  ->  (
( f `  t
) R ( g `
 t )  <->  ( a `  t ) R ( g `  t ) ) )
215212, 214anbi12d 693 . . . . . . . . . 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 2728 . . . . . . . . 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 250 . . . . . . . 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 693 . . . . . . 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 686 . . . . . . . 8  |-  ( g  =  c  ->  (
( a  e.  F  /\  g  e.  F
)  <->  ( a  e.  F  /\  c  e.  F ) ) )
22085eqeq2d 2449 . . . . . . . . . . 11  |-  ( g  =  c  ->  (
( a `  y
)  =  ( g `
 y )  <->  ( a `  y )  =  ( c `  y ) ) )
221220ralbidv 2727 . . . . . . . . . 10  |-  ( g  =  c  ->  ( A. y  e.  t 
( a `  y
)  =  ( g `
 y )  <->  A. y  e.  t  ( a `  y )  =  ( c `  y ) ) )
222 fveq1 5730 . . . . . . . . . . 11  |-  ( g  =  c  ->  (
g `  t )  =  ( c `  t ) )
223222breq2d 4227 . . . . . . . . . 10  |-  ( g  =  c  ->  (
( a `  t
) R ( g `
 t )  <->  ( a `  t ) R ( c `  t ) ) )
224221, 223anbi12d 693 . . . . . . . . 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 2728 . . . . . . . 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 693 . . . . . . 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 4480 . . . . . 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 205 . . . . 5  |-  ( ( a S b  /\  b S c )  -> 
a S c )
22939, 228pm3.2i 443 . . . 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 2805 . 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 4506 . 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 202 1  |-  S  Po  F
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 360    \/ w3o 936    /\ w3a 937    = wceq 1653    e. wcel 1726   {cab 2424   A.wral 2707   E.wrex 2708    u. cun 3320    C_ wss 3322   (/)c0 3630   {csn 3816   class class class wbr 4215   {copab 4268    Po wpo 4504   Ord word 4583   Oncon0 4584   -->wf 5453   ` cfv 5457
This theorem is referenced by:  soseq  25534
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4333  ax-nul 4341  ax-pow 4380  ax-pr 4406
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-rab 2716  df-v 2960  df-sbc 3164  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-pss 3338  df-nul 3631  df-if 3742  df-sn 3822  df-pr 3823  df-op 3825  df-uni 4018  df-br 4216  df-opab 4270  df-tr 4306  df-eprel 4497  df-po 4506  df-so 4507  df-fr 4544  df-we 4546  df-ord 4587  df-on 4588  df-rel 4888  df-cnv 4889  df-co 4890  df-dm 4891  df-rn 4892  df-iota 5421  df-fun 5459  df-fn 5460  df-f 5461  df-fv 5465
  Copyright terms: Public domain W3C validator