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

Theorem poseq 27736
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 5564 . . . . . . . . . . . . . . . 16  |-  ( x  =  b  ->  (
f : x --> A  <->  f :
b --> A ) )
43cbvrexv 2969 . . . . . . . . . . . . . . 15  |-  ( E. x  e.  On  f : x --> A  <->  E. b  e.  On  f : b --> A )
54abbii 2561 . . . . . . . . . . . . . 14  |-  { f  |  E. x  e.  On  f : x --> A }  =  {
f  |  E. b  e.  On  f : b --> A }
62, 5eqtri 2463 . . . . . . . . . . . . 13  |-  F  =  { f  |  E. b  e.  On  f : b --> A }
76orderseqlem 27735 . . . . . . . . . . . 12  |-  ( a  e.  F  ->  (
a `  x )  e.  ( A  u.  { (/)
} ) )
8 poirr 4673 . . . . . . . . . . . 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 907 . . . . . . . . . 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 2840 . . . . . . . 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 2996 . . . . . . 7  |-  a  e. 
_V
17 eleq1 2503 . . . . . . . . 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 5711 . . . . . . . . . . . 12  |-  ( f  =  a  ->  (
f `  y )  =  ( a `  y ) )
2019eqeq1d 2451 . . . . . . . . . . 11  |-  ( f  =  a  ->  (
( f `  y
)  =  ( g `
 y )  <->  ( a `  y )  =  ( g `  y ) ) )
2120ralbidv 2756 . . . . . . . . . 10  |-  ( f  =  a  ->  ( A. y  e.  x  ( f `  y
)  =  ( g `
 y )  <->  A. y  e.  x  ( a `  y )  =  ( g `  y ) ) )
22 fveq1 5711 . . . . . . . . . . 11  |-  ( f  =  a  ->  (
f `  x )  =  ( a `  x ) )
2322breq1d 4323 . . . . . . . . . 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 2757 . . . . . . . 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 2503 . . . . . . . . 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 5711 . . . . . . . . . . . 12  |-  ( g  =  a  ->  (
g `  y )  =  ( a `  y ) )
3029eqeq2d 2454 . . . . . . . . . . 11  |-  ( g  =  a  ->  (
( a `  y
)  =  ( g `
 y )  <->  ( a `  y )  =  ( a `  y ) ) )
3130ralbidv 2756 . . . . . . . . . 10  |-  ( g  =  a  ->  ( A. y  e.  x  ( a `  y
)  =  ( g `
 y )  <->  A. y  e.  x  ( a `  y )  =  ( a `  y ) ) )
32 fveq1 5711 . . . . . . . . . . 11  |-  ( g  =  a  ->  (
g `  x )  =  ( a `  x ) )
3332breq2d 4325 . . . . . . . . . 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 2757 . . . . . . . 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 4632 . . . . . 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 2996 . . . . . . . 8  |-  b  e. 
_V
41 raleq 2938 . . . . . . . . . . . 12  |-  ( x  =  z  ->  ( A. y  e.  x  ( f `  y
)  =  ( g `
 y )  <->  A. y  e.  z  ( f `  y )  =  ( g `  y ) ) )
42 fveq2 5712 . . . . . . . . . . . . 13  |-  ( x  =  z  ->  (
f `  x )  =  ( f `  z ) )
43 fveq2 5712 . . . . . . . . . . . . 13  |-  ( x  =  z  ->  (
g `  x )  =  ( g `  z ) )
4442, 43breq12d 4326 . . . . . . . . . . . 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 2969 . . . . . . . . . 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 2756 . . . . . . . . . . . 12  |-  ( f  =  a  ->  ( A. y  e.  z 
( f `  y
)  =  ( g `
 y )  <->  A. y  e.  z  ( a `  y )  =  ( g `  y ) ) )
48 fveq1 5711 . . . . . . . . . . . . 13  |-  ( f  =  a  ->  (
f `  z )  =  ( a `  z ) )
4948breq1d 4323 . . . . . . . . . . . 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 2757 . . . . . . . . . 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 2503 . . . . . . . . . 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 5711 . . . . . . . . . . . . 13  |-  ( g  =  b  ->  (
g `  y )  =  ( b `  y ) )
5756eqeq2d 2454 . . . . . . . . . . . 12  |-  ( g  =  b  ->  (
( a `  y
)  =  ( g `
 y )  <->  ( a `  y )  =  ( b `  y ) ) )
5857ralbidv 2756 . . . . . . . . . . 11  |-  ( g  =  b  ->  ( A. y  e.  z 
( a `  y
)  =  ( g `
 y )  <->  A. y  e.  z  ( a `  y )  =  ( b `  y ) ) )
59 fveq1 5711 . . . . . . . . . . . 12  |-  ( g  =  b  ->  (
g `  z )  =  ( b `  z ) )
6059breq2d 4325 . . . . . . . . . . 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 2757 . . . . . . . . 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 4632 . . . . . . 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 2996 . . . . . . . 8  |-  c  e. 
_V
66 eleq1 2503 . . . . . . . . . 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 2938 . . . . . . . . . . . 12  |-  ( x  =  w  ->  ( A. y  e.  x  ( f `  y
)  =  ( g `
 y )  <->  A. y  e.  w  ( f `  y )  =  ( g `  y ) ) )
69 fveq2 5712 . . . . . . . . . . . . 13  |-  ( x  =  w  ->  (
f `  x )  =  ( f `  w ) )
70 fveq2 5712 . . . . . . . . . . . . 13  |-  ( x  =  w  ->  (
g `  x )  =  ( g `  w ) )
7169, 70breq12d 4326 . . . . . . . . . . . 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 2969 . . . . . . . . . 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 5711 . . . . . . . . . . . . . 14  |-  ( f  =  b  ->  (
f `  y )  =  ( b `  y ) )
7574eqeq1d 2451 . . . . . . . . . . . . 13  |-  ( f  =  b  ->  (
( f `  y
)  =  ( g `
 y )  <->  ( b `  y )  =  ( g `  y ) ) )
7675ralbidv 2756 . . . . . . . . . . . 12  |-  ( f  =  b  ->  ( A. y  e.  w  ( f `  y
)  =  ( g `
 y )  <->  A. y  e.  w  ( b `  y )  =  ( g `  y ) ) )
77 fveq1 5711 . . . . . . . . . . . . 13  |-  ( f  =  b  ->  (
f `  w )  =  ( b `  w ) )
7877breq1d 4323 . . . . . . . . . . . 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 2757 . . . . . . . . . 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 2503 . . . . . . . . . 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 5711 . . . . . . . . . . . . 13  |-  ( g  =  c  ->  (
g `  y )  =  ( c `  y ) )
8685eqeq2d 2454 . . . . . . . . . . . 12  |-  ( g  =  c  ->  (
( b `  y
)  =  ( g `
 y )  <->  ( b `  y )  =  ( c `  y ) ) )
8786ralbidv 2756 . . . . . . . . . . 11  |-  ( g  =  c  ->  ( A. y  e.  w  ( b `  y
)  =  ( g `
 y )  <->  A. y  e.  w  ( b `  y )  =  ( c `  y ) ) )
88 fveq1 5711 . . . . . . . . . . . 12  |-  ( g  =  c  ->  (
g `  w )  =  ( c `  w ) )
8988breq2d 4325 . . . . . . . . . . 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 2757 . . . . . . . . 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 4632 . . . . . . 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 820 . . . . . . . . . . . . 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 2763 . . . . . . . . . . . 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 2909 . . . . . . . . . . . 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 4750 . . . . . . . . . . . . . 14  |-  ( z  e.  On  ->  Ord  z )
101 eloni 4750 . . . . . . . . . . . . . 14  |-  ( w  e.  On  ->  Ord  w )
102 ordtri3or 4772 . . . . . . . . . . . . . 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 1012 . . . . . . . . . . . . . . . . 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 4782 . . . . . . . . . . . . . . . . . . . . . 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 3437 . . . . . . . . . . . . . . . . . . . . . . 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 2870 . . . . . . . . . . . . . . . . . . . . . 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 2460 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( a `  y
)  =  ( b `
 y )  /\  ( b `  y
)  =  ( c `
 y ) )  ->  ( a `  y )  =  ( c `  y ) )
113112ralimi 2812 . . . . . . . . . . . . . . . . . . . . 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 1184 . . . . . . . . . . . . . . . . 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 5712 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  z  ->  (
b `  y )  =  ( b `  z ) )
119 fveq2 5712 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  z  ->  (
c `  y )  =  ( c `  z ) )
120118, 119eqeq12d 2457 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  =  z  ->  (
( b `  y
)  =  ( c `
 y )  <->  ( b `  z )  =  ( c `  z ) ) )
121120rspcv 3090 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( z  e.  w  ->  ( A. y  e.  w  ( b `  y
)  =  ( c `
 y )  -> 
( b `  z
)  =  ( c `
 z ) ) )
122 breq2 4317 . . . . . . . . . . . . . . . . . . . . . . . 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 1006 . . . . . . . . . . . . . . . . 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 2938 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  z  ->  ( A. y  e.  t 
( a `  y
)  =  ( c `
 y )  <->  A. y  e.  z  ( a `  y )  =  ( c `  y ) ) )
131 fveq2 5712 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  =  z  ->  (
a `  t )  =  ( a `  z ) )
132 fveq2 5712 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  =  z  ->  (
c `  t )  =  ( c `  z ) )
133131, 132breq12d 4326 . . . . . . . . . . . . . . . . . . 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 3094 . . . . . . . . . . . . . . . . 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 1216 . . . . . . . . . . . . . . . 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 1186 . . . . . . . . . . . . . 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 27735 . . . . . . . . . . . . . . . . . . . . . . . 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 27735 . . . . . . . . . . . . . . . . . . . . . . . 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 27735 . . . . . . . . . . . . . . . . . . . . . . . 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 1168 . . . . . . . . . . . . . . . . . . . . . 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 4674 . . . . . . . . . . . . . . . . . . . . . 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 2938 . . . . . . . . . . . . . . . . . . . 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 5712 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  =  w  ->  (
b `  z )  =  ( b `  w ) )
157 fveq2 5712 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  =  w  ->  (
c `  z )  =  ( c `  w ) )
158156, 157breq12d 4326 . . . . . . . . . . . . . . . . . . 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 1013 . . . . . . . . . . . . . . . . 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 4782 . . . . . . . . . . . . . . . . . . . . 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 3437 . . . . . . . . . . . . . . . . . . . . . 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 2870 . . . . . . . . . . . . . . . . . . . . . 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 2812 . . . . . . . . . . . . . . . . . . . . . 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 1184 . . . . . . . . . . . . . . . . 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 5712 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  w  ->  (
a `  y )  =  ( a `  w ) )
178 fveq2 5712 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  w  ->  (
b `  y )  =  ( b `  w ) )
179177, 178eqeq12d 2457 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  =  w  ->  (
( a `  y
)  =  ( b `
 y )  <->  ( a `  w )  =  ( b `  w ) ) )
180179rspcv 3090 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( w  e.  z  ->  ( A. y  e.  z 
( a `  y
)  =  ( b `
 y )  -> 
( a `  w
)  =  ( b `
 w ) ) )
181 breq1 4316 . . . . . . . . . . . . . . . . . . . . . . . 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 1006 . . . . . . . . . . . . . . . . 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 2938 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  w  ->  ( A. y  e.  t 
( a `  y
)  =  ( c `
 y )  <->  A. y  e.  w  ( a `  y )  =  ( c `  y ) ) )
190 fveq2 5712 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  =  w  ->  (
a `  t )  =  ( a `  w ) )
191 fveq2 5712 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  =  w  ->  (
c `  t )  =  ( c `  w ) )
192190, 191breq12d 4326 . . . . . . . . . . . . . . . . . . 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 3094 . . . . . . . . . . . . . . . . 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 1216 . . . . . . . . . . . . . . . 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 1186 . . . . . . . . . . . . . 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 1282 . . . . . . . . . . . . 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 2867 . . . . . . . . . . 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 822 . . . . . . 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 2938 . . . . . . . . . . 11  |-  ( x  =  t  ->  ( A. y  e.  x  ( f `  y
)  =  ( g `
 y )  <->  A. y  e.  t  ( f `  y )  =  ( g `  y ) ) )
207 fveq2 5712 . . . . . . . . . . . 12  |-  ( x  =  t  ->  (
f `  x )  =  ( f `  t ) )
208 fveq2 5712 . . . . . . . . . . . 12  |-  ( x  =  t  ->  (
g `  x )  =  ( g `  t ) )
209207, 208breq12d 4326 . . . . . . . . . . 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 2969 . . . . . . . . 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 2756 . . . . . . . . . . 11  |-  ( f  =  a  ->  ( A. y  e.  t 
( f `  y
)  =  ( g `
 y )  <->  A. y  e.  t  ( a `  y )  =  ( g `  y ) ) )
213 fveq1 5711 . . . . . . . . . . . 12  |-  ( f  =  a  ->  (
f `  t )  =  ( a `  t ) )
214213breq1d 4323 . . . . . . . . . . 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 2757 . . . . . . . . 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 2454 . . . . . . . . . . 11  |-  ( g  =  c  ->  (
( a `  y
)  =  ( g `
 y )  <->  ( a `  y )  =  ( c `  y ) ) )
221220ralbidv 2756 . . . . . . . . . 10  |-  ( g  =  c  ->  ( A. y  e.  t 
( a `  y
)  =  ( g `
 y )  <->  A. y  e.  t  ( a `  y )  =  ( c `  y ) ) )
222 fveq1 5711 . . . . . . . . . . 11  |-  ( g  =  c  ->  (
g `  t )  =  ( c `  t ) )
223222breq2d 4325 . . . . . . . . . 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 2757 . . . . . . . 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 4632 . . . . . 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 2834 . 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 4662 . 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 964    /\ w3a 965    = wceq 1369    e. wcel 1756   {cab 2429   A.wral 2736   E.wrex 2737    u. cun 3347    C_ wss 3349   (/)c0 3658   {csn 3898   class class class wbr 4313   {copab 4370    Po wpo 4660   Ord word 4739   Oncon0 4740   -->wf 5435   ` cfv 5439
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4434  ax-nul 4442  ax-pow 4491  ax-pr 4552
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2741  df-rex 2742  df-rab 2745  df-v 2995  df-sbc 3208  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-pss 3365  df-nul 3659  df-if 3813  df-sn 3899  df-pr 3901  df-op 3905  df-uni 4113  df-br 4314  df-opab 4372  df-tr 4407  df-eprel 4653  df-po 4662  df-so 4663  df-fr 4700  df-we 4702  df-ord 4743  df-on 4744  df-rel 4868  df-cnv 4869  df-co 4870  df-dm 4871  df-rn 4872  df-iota 5402  df-fun 5441  df-fn 5442  df-f 5443  df-fv 5447
This theorem is referenced by:  soseq  27737
  Copyright terms: Public domain W3C validator