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

Theorem poseq 24324
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 5392 . . . . . . . . . . . . . . . 16  |-  ( x  =  b  ->  (
f : x --> A  <->  f :
b --> A ) )
43cbvrexv 2778 . . . . . . . . . . . . . . 15  |-  ( E. x  e.  On  f : x --> A  <->  E. b  e.  On  f : b --> A )
54abbii 2408 . . . . . . . . . . . . . 14  |-  { f  |  E. x  e.  On  f : x --> A }  =  {
f  |  E. b  e.  On  f : b --> A }
62, 5eqtri 2316 . . . . . . . . . . . . 13  |-  F  =  { f  |  E. b  e.  On  f : b --> A }
76orderseqlem 24323 . . . . . . . . . . . 12  |-  ( a  e.  F  ->  (
a `  x )  e.  ( A  u.  { (/)
} ) )
8 poirr 4341 . . . . . . . . . . . 12  |-  ( ( R  Po  ( A  u.  { (/) } )  /\  ( a `  x )  e.  ( A  u.  { (/) } ) )  ->  -.  ( a `  x
) R ( a `
 x ) )
91, 7, 8sylancr 644 . . . . . . . . . . 11  |-  ( a  e.  F  ->  -.  ( a `  x
) R ( a `
 x ) )
109intnand 882 . . . . . . . . . 10  |-  ( a  e.  F  ->  -.  ( A. y  e.  x  ( a `  y
)  =  ( a `
 y )  /\  ( a `  x
) R ( a `
 x ) ) )
1110adantr 451 . . . . . . . . 9  |-  ( ( a  e.  F  /\  x  e.  On )  ->  -.  ( A. y  e.  x  ( a `  y )  =  ( a `  y )  /\  ( a `  x ) R ( a `  x ) ) )
1211nrexdv 2659 . . . . . . . 8  |-  ( a  e.  F  ->  -.  E. x  e.  On  ( A. y  e.  x  ( a `  y
)  =  ( a `
 y )  /\  ( a `  x
) R ( a `
 x ) ) )
1312adantr 451 . . . . . . 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 411 . . . . . . 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 199 . . . . . 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 2804 . . . . . . 7  |-  a  e. 
_V
17 eleq1 2356 . . . . . . . . 9  |-  ( f  =  a  ->  (
f  e.  F  <->  a  e.  F ) )
1817anbi1d 685 . . . . . . . 8  |-  ( f  =  a  ->  (
( f  e.  F  /\  g  e.  F
)  <->  ( a  e.  F  /\  g  e.  F ) ) )
19 fveq1 5540 . . . . . . . . . . . 12  |-  ( f  =  a  ->  (
f `  y )  =  ( a `  y ) )
2019eqeq1d 2304 . . . . . . . . . . 11  |-  ( f  =  a  ->  (
( f `  y
)  =  ( g `
 y )  <->  ( a `  y )  =  ( g `  y ) ) )
2120ralbidv 2576 . . . . . . . . . 10  |-  ( f  =  a  ->  ( A. y  e.  x  ( f `  y
)  =  ( g `
 y )  <->  A. y  e.  x  ( a `  y )  =  ( g `  y ) ) )
22 fveq1 5540 . . . . . . . . . . 11  |-  ( f  =  a  ->  (
f `  x )  =  ( a `  x ) )
2322breq1d 4049 . . . . . . . . . 10  |-  ( f  =  a  ->  (
( f `  x
) R ( g `
 x )  <->  ( a `  x ) R ( g `  x ) ) )
2421, 23anbi12d 691 . . . . . . . . 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 2577 . . . . . . . 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 691 . . . . . . 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 2356 . . . . . . . . 9  |-  ( g  =  a  ->  (
g  e.  F  <->  a  e.  F ) )
2827anbi2d 684 . . . . . . . 8  |-  ( g  =  a  ->  (
( a  e.  F  /\  g  e.  F
)  <->  ( a  e.  F  /\  a  e.  F ) ) )
29 fveq1 5540 . . . . . . . . . . . 12  |-  ( g  =  a  ->  (
g `  y )  =  ( a `  y ) )
3029eqeq2d 2307 . . . . . . . . . . 11  |-  ( g  =  a  ->  (
( a `  y
)  =  ( g `
 y )  <->  ( a `  y )  =  ( a `  y ) ) )
3130ralbidv 2576 . . . . . . . . . 10  |-  ( g  =  a  ->  ( A. y  e.  x  ( a `  y
)  =  ( g `
 y )  <->  A. y  e.  x  ( a `  y )  =  ( a `  y ) ) )
32 fveq1 5540 . . . . . . . . . . 11  |-  ( g  =  a  ->  (
g `  x )  =  ( a `  x ) )
3332breq2d 4051 . . . . . . . . . 10  |-  ( g  =  a  ->  (
( a `  x
) R ( g `
 x )  <->  ( a `  x ) R ( a `  x ) ) )
3431, 33anbi12d 691 . . . . . . . . 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 2577 . . . . . . . 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 691 . . . . . . 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 4303 . . . . . 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 290 . . . . 5  |-  -.  a S a
40 vex 2804 . . . . . . . 8  |-  b  e. 
_V
41 raleq 2749 . . . . . . . . . . . 12  |-  ( x  =  z  ->  ( A. y  e.  x  ( f `  y
)  =  ( g `
 y )  <->  A. y  e.  z  ( f `  y )  =  ( g `  y ) ) )
42 fveq2 5541 . . . . . . . . . . . . 13  |-  ( x  =  z  ->  (
f `  x )  =  ( f `  z ) )
43 fveq2 5541 . . . . . . . . . . . . 13  |-  ( x  =  z  ->  (
g `  x )  =  ( g `  z ) )
4442, 43breq12d 4052 . . . . . . . . . . . 12  |-  ( x  =  z  ->  (
( f `  x
) R ( g `
 x )  <->  ( f `  z ) R ( g `  z ) ) )
4541, 44anbi12d 691 . . . . . . . . . . 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 2778 . . . . . . . . . 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 2576 . . . . . . . . . . . 12  |-  ( f  =  a  ->  ( A. y  e.  z 
( f `  y
)  =  ( g `
 y )  <->  A. y  e.  z  ( a `  y )  =  ( g `  y ) ) )
48 fveq1 5540 . . . . . . . . . . . . 13  |-  ( f  =  a  ->  (
f `  z )  =  ( a `  z ) )
4948breq1d 4049 . . . . . . . . . . . 12  |-  ( f  =  a  ->  (
( f `  z
) R ( g `
 z )  <->  ( a `  z ) R ( g `  z ) ) )
5047, 49anbi12d 691 . . . . . . . . . . 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 2577 . . . . . . . . . 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 248 . . . . . . . . 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 691 . . . . . . . 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 2356 . . . . . . . . . 10  |-  ( g  =  b  ->  (
g  e.  F  <->  b  e.  F ) )
5554anbi2d 684 . . . . . . . . 9  |-  ( g  =  b  ->  (
( a  e.  F  /\  g  e.  F
)  <->  ( a  e.  F  /\  b  e.  F ) ) )
56 fveq1 5540 . . . . . . . . . . . . 13  |-  ( g  =  b  ->  (
g `  y )  =  ( b `  y ) )
5756eqeq2d 2307 . . . . . . . . . . . 12  |-  ( g  =  b  ->  (
( a `  y
)  =  ( g `
 y )  <->  ( a `  y )  =  ( b `  y ) ) )
5857ralbidv 2576 . . . . . . . . . . 11  |-  ( g  =  b  ->  ( A. y  e.  z 
( a `  y
)  =  ( g `
 y )  <->  A. y  e.  z  ( a `  y )  =  ( b `  y ) ) )
59 fveq1 5540 . . . . . . . . . . . 12  |-  ( g  =  b  ->  (
g `  z )  =  ( b `  z ) )
6059breq2d 4051 . . . . . . . . . . 11  |-  ( g  =  b  ->  (
( a `  z
) R ( g `
 z )  <->  ( a `  z ) R ( b `  z ) ) )
6158, 60anbi12d 691 . . . . . . . . . 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 2577 . . . . . . . . 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 691 . . . . . . . 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 4303 . . . . . . 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 2804 . . . . . . . 8  |-  c  e. 
_V
66 eleq1 2356 . . . . . . . . . 10  |-  ( f  =  b  ->  (
f  e.  F  <->  b  e.  F ) )
6766anbi1d 685 . . . . . . . . 9  |-  ( f  =  b  ->  (
( f  e.  F  /\  g  e.  F
)  <->  ( b  e.  F  /\  g  e.  F ) ) )
68 raleq 2749 . . . . . . . . . . . 12  |-  ( x  =  w  ->  ( A. y  e.  x  ( f `  y
)  =  ( g `
 y )  <->  A. y  e.  w  ( f `  y )  =  ( g `  y ) ) )
69 fveq2 5541 . . . . . . . . . . . . 13  |-  ( x  =  w  ->  (
f `  x )  =  ( f `  w ) )
70 fveq2 5541 . . . . . . . . . . . . 13  |-  ( x  =  w  ->  (
g `  x )  =  ( g `  w ) )
7169, 70breq12d 4052 . . . . . . . . . . . 12  |-  ( x  =  w  ->  (
( f `  x
) R ( g `
 x )  <->  ( f `  w ) R ( g `  w ) ) )
7268, 71anbi12d 691 . . . . . . . . . . 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 2778 . . . . . . . . . 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 5540 . . . . . . . . . . . . . 14  |-  ( f  =  b  ->  (
f `  y )  =  ( b `  y ) )
7574eqeq1d 2304 . . . . . . . . . . . . 13  |-  ( f  =  b  ->  (
( f `  y
)  =  ( g `
 y )  <->  ( b `  y )  =  ( g `  y ) ) )
7675ralbidv 2576 . . . . . . . . . . . 12  |-  ( f  =  b  ->  ( A. y  e.  w  ( f `  y
)  =  ( g `
 y )  <->  A. y  e.  w  ( b `  y )  =  ( g `  y ) ) )
77 fveq1 5540 . . . . . . . . . . . . 13  |-  ( f  =  b  ->  (
f `  w )  =  ( b `  w ) )
7877breq1d 4049 . . . . . . . . . . . 12  |-  ( f  =  b  ->  (
( f `  w
) R ( g `
 w )  <->  ( b `  w ) R ( g `  w ) ) )
7976, 78anbi12d 691 . . . . . . . . . . 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 2577 . . . . . . . . . 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 248 . . . . . . . . 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 691 . . . . . . . 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 2356 . . . . . . . . . 10  |-  ( g  =  c  ->  (
g  e.  F  <->  c  e.  F ) )
8483anbi2d 684 . . . . . . . . 9  |-  ( g  =  c  ->  (
( b  e.  F  /\  g  e.  F
)  <->  ( b  e.  F  /\  c  e.  F ) ) )
85 fveq1 5540 . . . . . . . . . . . . 13  |-  ( g  =  c  ->  (
g `  y )  =  ( c `  y ) )
8685eqeq2d 2307 . . . . . . . . . . . 12  |-  ( g  =  c  ->  (
( b `  y
)  =  ( g `
 y )  <->  ( b `  y )  =  ( c `  y ) ) )
8786ralbidv 2576 . . . . . . . . . . 11  |-  ( g  =  c  ->  ( A. y  e.  w  ( b `  y
)  =  ( g `
 y )  <->  A. y  e.  w  ( b `  y )  =  ( c `  y ) ) )
88 fveq1 5540 . . . . . . . . . . . 12  |-  ( g  =  c  ->  (
g `  w )  =  ( c `  w ) )
8988breq2d 4051 . . . . . . . . . . 11  |-  ( g  =  c  ->  (
( b `  w
) R ( g `
 w )  <->  ( b `  w ) R ( c `  w ) ) )
9087, 89anbi12d 691 . . . . . . . . . 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 2577 . . . . . . . . 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 691 . . . . . . . 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 4303 . . . . . . 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 734 . . . . . . . . 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 737 . . . . . . . . 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 797 . . . . . . . . . . . . 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 2583 . . . . . . . . . . . 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 2720 . . . . . . . . . . . 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 240 . . . . . . . . . . 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 4418 . . . . . . . . . . . . . 14  |-  ( z  e.  On  ->  Ord  z )
101 eloni 4418 . . . . . . . . . . . . . 14  |-  ( w  e.  On  ->  Ord  w )
102 ordtri3or 4440 . . . . . . . . . . . . . 14  |-  ( ( Ord  z  /\  Ord  w )  ->  (
z  e.  w  \/  z  =  w  \/  w  e.  z ) )
103100, 101, 102syl2an 463 . . . . . . . . . . . . 13  |-  ( ( z  e.  On  /\  w  e.  On )  ->  ( z  e.  w  \/  z  =  w  \/  w  e.  z
) )
104 simp1l 979 . . . . . . . . . . . . . . . . 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 4450 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( w  e.  On  ->  (
z  e.  w  -> 
z  C_  w )
)
106105imp 418 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( w  e.  On  /\  z  e.  w )  ->  z  C_  w )
107106adantll 694 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( z  e.  On  /\  w  e.  On )  /\  z  e.  w
)  ->  z  C_  w )
108 ssralv 3250 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( z 
C_  w  ->  ( A. y  e.  w  ( b `  y
)  =  ( c `
 y )  ->  A. y  e.  z 
( b `  y
)  =  ( c `
 y ) ) )
109108anim2d 548 . . . . . . . . . . . . . . . . . . . . . 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 2688 . . . . . . . . . . . . . . . . . . . . . 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 218 . . . . . . . . . . . . . . . . . . . . 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 2313 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( a `  y
)  =  ( b `
 y )  /\  ( b `  y
)  =  ( c `
 y ) )  ->  ( a `  y )  =  ( c `  y ) )
113112ralimi 2631 . . . . . . . . . . . . . . . . . . . . 21  |-  ( A. y  e.  z  (
( a `  y
)  =  ( b `
 y )  /\  ( b `  y
)  =  ( c `
 y ) )  ->  A. y  e.  z  ( a `  y
)  =  ( c `
 y ) )
114111, 113syl6 29 . . . . . . . . . . . . . . . . . . . 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 15 . . . . . . . . . . . . . . . . . . 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 454 . . . . . . . . . . . . . . . . . 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 1148 . . . . . . . . . . . . . . . . 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 5541 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  z  ->  (
b `  y )  =  ( b `  z ) )
119 fveq2 5541 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  z  ->  (
c `  y )  =  ( c `  z ) )
120118, 119eqeq12d 2310 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  =  z  ->  (
( b `  y
)  =  ( c `
 y )  <->  ( b `  z )  =  ( c `  z ) ) )
121120rspcv 2893 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( z  e.  w  ->  ( A. y  e.  w  ( b `  y
)  =  ( c `
 y )  -> 
( b `  z
)  =  ( c `
 z ) ) )
122 breq2 4043 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( b `  z )  =  ( c `  z )  ->  (
( a `  z
) R ( b `
 z )  <->  ( a `  z ) R ( c `  z ) ) )
123122biimpd 198 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( b `  z )  =  ( c `  z )  ->  (
( a `  z
) R ( b `
 z )  -> 
( a `  z
) R ( c `
 z ) ) )
124121, 123syl6 29 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( z  e.  w  ->  ( A. y  e.  w  ( b `  y
)  =  ( c `
 y )  -> 
( ( a `  z ) R ( b `  z )  ->  ( a `  z ) R ( c `  z ) ) ) )
125124com3l 75 . . . . . . . . . . . . . . . . . . . . 21  |-  ( A. y  e.  w  (
b `  y )  =  ( c `  y )  ->  (
( a `  z
) R ( b `
 z )  -> 
( z  e.  w  ->  ( a `  z
) R ( c `
 z ) ) ) )
126125imp 418 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A. y  e.  w  ( b `  y
)  =  ( c `
 y )  /\  ( a `  z
) R ( b `
 z ) )  ->  ( z  e.  w  ->  ( a `  z ) R ( c `  z ) ) )
127126ad2ant2lr 728 . . . . . . . . . . . . . . . . . . 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 419 . . . . . . . . . . . . . . . . . 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 973 . . . . . . . . . . . . . . . . 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 2749 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  z  ->  ( A. y  e.  t 
( a `  y
)  =  ( c `
 y )  <->  A. y  e.  z  ( a `  y )  =  ( c `  y ) ) )
131 fveq2 5541 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  =  z  ->  (
a `  t )  =  ( a `  z ) )
132 fveq2 5541 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  =  z  ->  (
c `  t )  =  ( c `  z ) )
133131, 132breq12d 4052 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  z  ->  (
( a `  t
) R ( c `
 t )  <->  ( a `  z ) R ( c `  z ) ) )
134130, 133anbi12d 691 . . . . . . . . . . . . . . . . . 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 2897 . . . . . . . . . . . . . . . . 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 1180 . . . . . . . . . . . . . . . 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 22 . . . . . . . . . . . . . . 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 1150 . . . . . . . . . . . . . 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 24323 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( a  e.  F  ->  (
a `  z )  e.  ( A  u.  { (/)
} ) )
140139ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( a  e.  F  /\  b  e.  F
)  /\  ( b  e.  F  /\  c  e.  F ) )  -> 
( a `  z
)  e.  ( A  u.  { (/) } ) )
1412orderseqlem 24323 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( b  e.  F  ->  (
b `  z )  e.  ( A  u.  { (/)
} ) )
142141ad2antlr 707 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( a  e.  F  /\  b  e.  F
)  /\  ( b  e.  F  /\  c  e.  F ) )  -> 
( b `  z
)  e.  ( A  u.  { (/) } ) )
1432orderseqlem 24323 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( c  e.  F  ->  (
c `  z )  e.  ( A  u.  { (/)
} ) )
144143ad2antll 709 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( a  e.  F  /\  b  e.  F
)  /\  ( b  e.  F  /\  c  e.  F ) )  -> 
( c `  z
)  e.  ( A  u.  { (/) } ) )
145140, 142, 1443jca 1132 . . . . . . . . . . . . . . . . . . . . . 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 4342 . . . . . . . . . . . . . . . . . . . . . 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 644 . . . . . . . . . . . . . . . . . . . . 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 419 . . . . . . . . . . . . . . . . . . . 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 549 . . . . . . . . . . . . . . . . . . 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 629 . . . . . . . . . . . . . . . . . 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 460 . . . . . . . . . . . . . . . . 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 588 . . . . . . . . . . . . . . . 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 2749 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  =  w  ->  ( A. y  e.  z 
( b `  y
)  =  ( c `
 y )  <->  A. y  e.  w  ( b `  y )  =  ( c `  y ) ) )
154153anbi2d 684 . . . . . . . . . . . . . . . . . . 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 248 . . . . . . . . . . . . . . . . . 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 5541 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  =  w  ->  (
b `  z )  =  ( b `  w ) )
157 fveq2 5541 . . . . . . . . . . . . . . . . . . . 20  |-  ( z  =  w  ->  (
c `  z )  =  ( c `  w ) )
158156, 157breq12d 4052 . . . . . . . . . . . . . . . . . . 19  |-  ( z  =  w  ->  (
( b `  z
) R ( c `
 z )  <->  ( b `  w ) R ( c `  w ) ) )
159158anbi2d 684 . . . . . . . . . . . . . . . . . 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 691 . . . . . . . . . . . . . . . . 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 308 . . . . . . . . . . . . . . . 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 211 . . . . . . . . . . . . . . 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 451 . . . . . . . . . . . . . 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 980 . . . . . . . . . . . . . . . . 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 4450 . . . . . . . . . . . . . . . . . . . . 21  |-  ( z  e.  On  ->  (
w  e.  z  ->  w  C_  z ) )
166165imp 418 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( z  e.  On  /\  w  e.  z )  ->  w  C_  z )
167166adantlr 695 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( z  e.  On  /\  w  e.  On )  /\  w  e.  z )  ->  w  C_  z
)
168 ssralv 3250 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( w 
C_  z  ->  ( A. y  e.  z 
( a `  y
)  =  ( b `
 y )  ->  A. y  e.  w  ( a `  y
)  =  ( b `
 y ) ) )
169168anim1d 547 . . . . . . . . . . . . . . . . . . . . 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 2688 . . . . . . . . . . . . . . . . . . . . . 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 2631 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( A. y  e.  w  (
( a `  y
)  =  ( b `
 y )  /\  ( b `  y
)  =  ( c `
 y ) )  ->  A. y  e.  w  ( a `  y
)  =  ( c `
 y ) )
172170, 171sylbir 204 . . . . . . . . . . . . . . . . . . . . 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 29 . . . . . . . . . . . . . . . . . . . 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 454 . . . . . . . . . . . . . . . . . . 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 15 . . . . . . . . . . . . . . . . . 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 1148 . . . . . . . . . . . . . . . . 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 5541 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  w  ->  (
a `  y )  =  ( a `  w ) )
178 fveq2 5541 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( y  =  w  ->  (
b `  y )  =  ( b `  w ) )
179177, 178eqeq12d 2310 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( y  =  w  ->  (
( a `  y
)  =  ( b `
 y )  <->  ( a `  w )  =  ( b `  w ) ) )
180179rspcv 2893 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( w  e.  z  ->  ( A. y  e.  z 
( a `  y
)  =  ( b `
 y )  -> 
( a `  w
)  =  ( b `
 w ) ) )
181 breq1 4042 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( a `  w )  =  ( b `  w )  ->  (
( a `  w
) R ( c `
 w )  <->  ( b `  w ) R ( c `  w ) ) )
182181biimprd 214 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( a `  w )  =  ( b `  w )  ->  (
( b `  w
) R ( c `
 w )  -> 
( a `  w
) R ( c `
 w ) ) )
183180, 182syl6 29 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( w  e.  z  ->  ( A. y  e.  z 
( a `  y
)  =  ( b `
 y )  -> 
( ( b `  w ) R ( c `  w )  ->  ( a `  w ) R ( c `  w ) ) ) )
184183com3l 75 . . . . . . . . . . . . . . . . . . . . 21  |-  ( A. y  e.  z  (
a `  y )  =  ( b `  y )  ->  (
( b `  w
) R ( c `
 w )  -> 
( w  e.  z  ->  ( a `  w ) R ( c `  w ) ) ) )
185184imp 418 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A. y  e.  z  ( a `  y
)  =  ( b `
 y )  /\  ( b `  w
) R ( c `
 w ) )  ->  ( w  e.  z  ->  ( a `  w ) R ( c `  w ) ) )
186185ad2ant2rl 729 . . . . . . . . . . . . . . . . . . 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 419 . . . . . . . . . . . . . . . . . 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 973 . . . . . . . . . . . . . . . . 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 2749 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  w  ->  ( A. y  e.  t 
( a `  y
)  =  ( c `
 y )  <->  A. y  e.  w  ( a `  y )  =  ( c `  y ) ) )
190 fveq2 5541 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  =  w  ->  (
a `  t )  =  ( a `  w ) )
191 fveq2 5541 . . . . . . . . . . . . . . . . . . . 20  |-  ( t  =  w  ->  (
c `  t )  =  ( c `  w ) )
192190, 191breq12d 4052 . . . . . . . . . . . . . . . . . . 19  |-  ( t  =  w  ->  (
( a `  t
) R ( c `
 t )  <->  ( a `  w ) R ( c `  w ) ) )
193189, 192anbi12d 691 . . . . . . . . . . . . . . . . . 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 2897 . . . . . . . . . . . . . . . . 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 1180 . . . . . . . . . . . . . . . 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 22 . . . . . . . . . . . . . . 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 1150 . . . . . . . . . . . . . 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 1246 . . . . . . . . . . . . 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 14 . . . . . . . . . . . 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 2685 . . . . . . . . . . 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 204 . . . . . . . . . 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 419 . . . . . . . . 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 520 . . . . . . . 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 799 . . . . . . 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 465 . . . . . 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 2749 . . . . . . . . . . 11  |-  ( x  =  t  ->  ( A. y  e.  x  ( f `  y
)  =  ( g `
 y )  <->  A. y  e.  t  ( f `  y )  =  ( g `  y ) ) )
207 fveq2 5541 . . . . . . . . . . . 12  |-  ( x  =  t  ->  (
f `  x )  =  ( f `  t ) )
208 fveq2 5541 . . . . . . . . . . . 12  |-  ( x  =  t  ->  (
g `  x )  =  ( g `  t ) )
209207, 208breq12d 4052 . . . . . . . . . . 11  |-  ( x  =  t  ->  (
( f `  x
) R ( g `
 x )  <->  ( f `  t ) R ( g `  t ) ) )
210206, 209anbi12d 691 . . . . . . . . . 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 2778 . . . . . . . . 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 2576 . . . . . . . . . . 11  |-  ( f  =  a  ->  ( A. y  e.  t 
( f `  y
)  =  ( g `
 y )  <->  A. y  e.  t  ( a `  y )  =  ( g `  y ) ) )
213 fveq1 5540 . . . . . . . . . . . 12  |-  ( f  =  a  ->  (
f `  t )  =  ( a `  t ) )
214213breq1d 4049 . . . . . . . . . . 11  |-  ( f  =  a  ->  (
( f `  t
) R ( g `
 t )  <->  ( a `  t ) R ( g `  t ) ) )
215212, 214anbi12d 691 . . . . . . . . . 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 2577 . . . . . . . . 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 248 . . . . . . . 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 691 . . . . . . 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 684 . . . . . . . 8  |-  ( g  =  c  ->  (
( a  e.  F  /\  g  e.  F
)  <->  ( a  e.  F  /\  c  e.  F ) ) )
22085eqeq2d 2307 . . . . . . . . . . 11  |-  ( g  =  c  ->  (
( a `  y
)  =  ( g `
 y )  <->  ( a `  y )  =  ( c `  y ) ) )
221220ralbidv 2576 . . . . . . . . . 10  |-  ( g  =  c  ->  ( A. y  e.  t 
( a `  y
)  =  ( g `
 y )  <->  A. y  e.  t  ( a `  y )  =  ( c `  y ) ) )
222 fveq1 5540 . . . . . . . . . . 11  |-  ( g  =  c  ->  (
g `  t )  =  ( c `  t ) )
223222breq2d 4051 . . . . . . . . . 10  |-  ( g  =  c  ->  (
( a `  t
) R ( g `
 t )  <->  ( a `  t ) R ( c `  t ) ) )
224221, 223anbi12d 691 . . . . . . . . 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 2577 . . . . . . . 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 691 . . . . . . 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 4303 . . . . . 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 203 . . . . 5  |-  ( ( a S b  /\  b S c )  -> 
a S c )
22939, 228pm3.2i 441 . . . 4  |-  ( -.  a S a  /\  ( ( a S b  /\  b S c )  ->  a S c ) )
230229a1i 10 . . 3  |-  ( ( a  e.  F  /\  b  e.  F  /\  c  e.  F )  ->  ( -.  a S a  /\  ( ( a S b  /\  b S c )  -> 
a S c ) ) )
231230rgen3 2653 . 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 4330 . 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 200 1  |-  S  Po  F
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    /\ wa 358    \/ w3o 933    /\ w3a 934    = wceq 1632    e. wcel 1696   {cab 2282   A.wral 2556   E.wrex 2557    u. cun 3163    C_ wss 3165   (/)c0 3468   {csn 3653   class class class wbr 4039   {copab 4092    Po wpo 4328   Ord word 4407   Oncon0 4408   -->wf 5267   ` cfv 5271
This theorem is referenced by:  soseq  24325
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pow 4204  ax-pr 4230
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-rab 2565  df-v 2803  df-sbc 3005  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-pss 3181  df-nul 3469  df-if 3579  df-sn 3659  df-pr 3660  df-op 3662  df-uni 3844  df-br 4040  df-opab 4094  df-tr 4130  df-eprel 4321  df-po 4330  df-so 4331  df-fr 4368  df-we 4370  df-ord 4411  df-on 4412  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-rn 4716  df-iota 5235  df-fun 5273  df-fn 5274  df-f 5275  df-fv 5279
  Copyright terms: Public domain W3C validator