Metamath Proof Explorer


Theorem poseq

Description: A partial ordering of sequences of ordinals. (Contributed by Scott Fenton, 8-Jun-2011)

Ref Expression
Hypotheses 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 poseq
|- S Po F

Proof

Step Hyp Ref Expression
1 poseq.1
 |-  R Po ( A u. { (/) } )
2 poseq.2
 |-  F = { f | E. x e. On f : x --> A }
3 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 ) ) ) }
4 feq2
 |-  ( x = b -> ( f : x --> A <-> f : b --> A ) )
5 4 cbvrexvw
 |-  ( E. x e. On f : x --> A <-> E. b e. On f : b --> A )
6 5 abbii
 |-  { f | E. x e. On f : x --> A } = { f | E. b e. On f : b --> A }
7 2 6 eqtri
 |-  F = { f | E. b e. On f : b --> A }
8 7 orderseqlem
 |-  ( a e. F -> ( a ` x ) e. ( A u. { (/) } ) )
9 poirr
 |-  ( ( R Po ( A u. { (/) } ) /\ ( a ` x ) e. ( A u. { (/) } ) ) -> -. ( a ` x ) R ( a ` x ) )
10 1 8 9 sylancr
 |-  ( a e. F -> -. ( a ` x ) R ( a ` x ) )
11 10 intnand
 |-  ( a e. F -> -. ( A. y e. x ( a ` y ) = ( a ` y ) /\ ( a ` x ) R ( a ` x ) ) )
12 11 adantr
 |-  ( ( a e. F /\ x e. On ) -> -. ( A. y e. x ( a ` y ) = ( a ` y ) /\ ( a ` x ) R ( a ` x ) ) )
13 12 nrexdv
 |-  ( a e. F -> -. E. x e. On ( A. y e. x ( a ` y ) = ( a ` y ) /\ ( a ` x ) R ( a ` x ) ) )
14 13 adantr
 |-  ( ( a e. F /\ a e. F ) -> -. E. x e. On ( A. y e. x ( a ` y ) = ( a ` y ) /\ ( a ` x ) R ( a ` x ) ) )
15 imnan
 |-  ( ( ( 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 ) ) ) )
16 14 15 mpbi
 |-  -. ( ( a e. F /\ a e. F ) /\ E. x e. On ( A. y e. x ( a ` y ) = ( a ` y ) /\ ( a ` x ) R ( a ` x ) ) )
17 vex
 |-  a e. _V
18 eleq1w
 |-  ( f = a -> ( f e. F <-> a e. F ) )
19 18 anbi1d
 |-  ( f = a -> ( ( f e. F /\ g e. F ) <-> ( a e. F /\ g e. F ) ) )
20 fveq1
 |-  ( f = a -> ( f ` y ) = ( a ` y ) )
21 20 eqeq1d
 |-  ( f = a -> ( ( f ` y ) = ( g ` y ) <-> ( a ` y ) = ( g ` y ) ) )
22 21 ralbidv
 |-  ( f = a -> ( A. y e. x ( f ` y ) = ( g ` y ) <-> A. y e. x ( a ` y ) = ( g ` y ) ) )
23 fveq1
 |-  ( f = a -> ( f ` x ) = ( a ` x ) )
24 23 breq1d
 |-  ( f = a -> ( ( f ` x ) R ( g ` x ) <-> ( a ` x ) R ( g ` x ) ) )
25 22 24 anbi12d
 |-  ( 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 ) ) ) )
26 25 rexbidv
 |-  ( 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 ) ) ) )
27 19 26 anbi12d
 |-  ( 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 ) ) ) ) )
28 eleq1w
 |-  ( g = a -> ( g e. F <-> a e. F ) )
29 28 anbi2d
 |-  ( g = a -> ( ( a e. F /\ g e. F ) <-> ( a e. F /\ a e. F ) ) )
30 fveq1
 |-  ( g = a -> ( g ` y ) = ( a ` y ) )
31 30 eqeq2d
 |-  ( g = a -> ( ( a ` y ) = ( g ` y ) <-> ( a ` y ) = ( a ` y ) ) )
32 31 ralbidv
 |-  ( g = a -> ( A. y e. x ( a ` y ) = ( g ` y ) <-> A. y e. x ( a ` y ) = ( a ` y ) ) )
33 fveq1
 |-  ( g = a -> ( g ` x ) = ( a ` x ) )
34 33 breq2d
 |-  ( g = a -> ( ( a ` x ) R ( g ` x ) <-> ( a ` x ) R ( a ` x ) ) )
35 32 34 anbi12d
 |-  ( 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 ) ) ) )
36 35 rexbidv
 |-  ( 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 ) ) ) )
37 29 36 anbi12d
 |-  ( 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 ) ) ) ) )
38 17 17 27 37 3 brab
 |-  ( 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 ) ) ) )
39 16 38 mtbir
 |-  -. a S a
40 vex
 |-  b e. _V
41 raleq
 |-  ( x = z -> ( A. y e. x ( f ` y ) = ( g ` y ) <-> A. y e. z ( f ` y ) = ( g ` y ) ) )
42 fveq2
 |-  ( x = z -> ( f ` x ) = ( f ` z ) )
43 fveq2
 |-  ( x = z -> ( g ` x ) = ( g ` z ) )
44 42 43 breq12d
 |-  ( x = z -> ( ( f ` x ) R ( g ` x ) <-> ( f ` z ) R ( g ` z ) ) )
45 41 44 anbi12d
 |-  ( 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 ) ) ) )
46 45 cbvrexvw
 |-  ( 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 ) ) )
47 21 ralbidv
 |-  ( f = a -> ( A. y e. z ( f ` y ) = ( g ` y ) <-> A. y e. z ( a ` y ) = ( g ` y ) ) )
48 fveq1
 |-  ( f = a -> ( f ` z ) = ( a ` z ) )
49 48 breq1d
 |-  ( f = a -> ( ( f ` z ) R ( g ` z ) <-> ( a ` z ) R ( g ` z ) ) )
50 47 49 anbi12d
 |-  ( 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 ) ) ) )
51 50 rexbidv
 |-  ( 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 ) ) ) )
52 46 51 syl5bb
 |-  ( 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 ) ) ) )
53 19 52 anbi12d
 |-  ( 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 eleq1w
 |-  ( g = b -> ( g e. F <-> b e. F ) )
55 54 anbi2d
 |-  ( g = b -> ( ( a e. F /\ g e. F ) <-> ( a e. F /\ b e. F ) ) )
56 fveq1
 |-  ( g = b -> ( g ` y ) = ( b ` y ) )
57 56 eqeq2d
 |-  ( g = b -> ( ( a ` y ) = ( g ` y ) <-> ( a ` y ) = ( b ` y ) ) )
58 57 ralbidv
 |-  ( g = b -> ( A. y e. z ( a ` y ) = ( g ` y ) <-> A. y e. z ( a ` y ) = ( b ` y ) ) )
59 fveq1
 |-  ( g = b -> ( g ` z ) = ( b ` z ) )
60 59 breq2d
 |-  ( g = b -> ( ( a ` z ) R ( g ` z ) <-> ( a ` z ) R ( b ` z ) ) )
61 58 60 anbi12d
 |-  ( 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 ) ) ) )
62 61 rexbidv
 |-  ( 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 ) ) ) )
63 55 62 anbi12d
 |-  ( 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 ) ) ) ) )
64 17 40 53 63 3 brab
 |-  ( 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
 |-  c e. _V
66 eleq1w
 |-  ( f = b -> ( f e. F <-> b e. F ) )
67 66 anbi1d
 |-  ( f = b -> ( ( f e. F /\ g e. F ) <-> ( b e. F /\ g e. F ) ) )
68 raleq
 |-  ( x = w -> ( A. y e. x ( f ` y ) = ( g ` y ) <-> A. y e. w ( f ` y ) = ( g ` y ) ) )
69 fveq2
 |-  ( x = w -> ( f ` x ) = ( f ` w ) )
70 fveq2
 |-  ( x = w -> ( g ` x ) = ( g ` w ) )
71 69 70 breq12d
 |-  ( x = w -> ( ( f ` x ) R ( g ` x ) <-> ( f ` w ) R ( g ` w ) ) )
72 68 71 anbi12d
 |-  ( 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 ) ) ) )
73 72 cbvrexvw
 |-  ( 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
 |-  ( f = b -> ( f ` y ) = ( b ` y ) )
75 74 eqeq1d
 |-  ( f = b -> ( ( f ` y ) = ( g ` y ) <-> ( b ` y ) = ( g ` y ) ) )
76 75 ralbidv
 |-  ( f = b -> ( A. y e. w ( f ` y ) = ( g ` y ) <-> A. y e. w ( b ` y ) = ( g ` y ) ) )
77 fveq1
 |-  ( f = b -> ( f ` w ) = ( b ` w ) )
78 77 breq1d
 |-  ( f = b -> ( ( f ` w ) R ( g ` w ) <-> ( b ` w ) R ( g ` w ) ) )
79 76 78 anbi12d
 |-  ( 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 ) ) ) )
80 79 rexbidv
 |-  ( 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 ) ) ) )
81 73 80 syl5bb
 |-  ( 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 ) ) ) )
82 67 81 anbi12d
 |-  ( 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 eleq1w
 |-  ( g = c -> ( g e. F <-> c e. F ) )
84 83 anbi2d
 |-  ( g = c -> ( ( b e. F /\ g e. F ) <-> ( b e. F /\ c e. F ) ) )
85 fveq1
 |-  ( g = c -> ( g ` y ) = ( c ` y ) )
86 85 eqeq2d
 |-  ( g = c -> ( ( b ` y ) = ( g ` y ) <-> ( b ` y ) = ( c ` y ) ) )
87 86 ralbidv
 |-  ( g = c -> ( A. y e. w ( b ` y ) = ( g ` y ) <-> A. y e. w ( b ` y ) = ( c ` y ) ) )
88 fveq1
 |-  ( g = c -> ( g ` w ) = ( c ` w ) )
89 88 breq2d
 |-  ( g = c -> ( ( b ` w ) R ( g ` w ) <-> ( b ` w ) R ( c ` w ) ) )
90 87 89 anbi12d
 |-  ( 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 ) ) ) )
91 90 rexbidv
 |-  ( 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 ) ) ) )
92 84 91 anbi12d
 |-  ( 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 ) ) ) ) )
93 40 65 82 92 3 brab
 |-  ( 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
 |-  ( ( ( ( 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
 |-  ( ( ( ( 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
 |-  ( ( ( 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 ) ) ) )
97 96 2rexbii
 |-  ( 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
 |-  ( 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 ) ) ) )
99 97 98 bitri
 |-  ( 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
 |-  ( z e. On -> Ord z )
101 eloni
 |-  ( w e. On -> Ord w )
102 ordtri3or
 |-  ( ( Ord z /\ Ord w ) -> ( z e. w \/ z = w \/ w e. z ) )
103 100 101 102 syl2an
 |-  ( ( z e. On /\ w e. On ) -> ( z e. w \/ z = w \/ w e. z ) )
104 simp1l
 |-  ( ( ( 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
 |-  ( w e. On -> ( z e. w -> z C_ w ) )
106 105 imp
 |-  ( ( w e. On /\ z e. w ) -> z C_ w )
107 106 adantll
 |-  ( ( ( z e. On /\ w e. On ) /\ z e. w ) -> z C_ w )
108 ssralv
 |-  ( z C_ w -> ( A. y e. w ( b ` y ) = ( c ` y ) -> A. y e. z ( b ` y ) = ( c ` y ) ) )
109 108 anim2d
 |-  ( 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
 |-  ( 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 ) ) )
111 109 110 syl6ibr
 |-  ( 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
 |-  ( ( ( a ` y ) = ( b ` y ) /\ ( b ` y ) = ( c ` y ) ) -> ( a ` y ) = ( c ` y ) )
113 112 ralimi
 |-  ( A. y e. z ( ( a ` y ) = ( b ` y ) /\ ( b ` y ) = ( c ` y ) ) -> A. y e. z ( a ` y ) = ( c ` y ) )
114 111 113 syl6
 |-  ( 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 ) ) )
115 107 114 syl
 |-  ( ( ( 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 ) ) )
116 115 adantrd
 |-  ( ( ( 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 ) ) )
117 116 3impia
 |-  ( ( ( 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
 |-  ( y = z -> ( b ` y ) = ( b ` z ) )
119 fveq2
 |-  ( y = z -> ( c ` y ) = ( c ` z ) )
120 118 119 eqeq12d
 |-  ( y = z -> ( ( b ` y ) = ( c ` y ) <-> ( b ` z ) = ( c ` z ) ) )
121 120 rspcv
 |-  ( z e. w -> ( A. y e. w ( b ` y ) = ( c ` y ) -> ( b ` z ) = ( c ` z ) ) )
122 breq2
 |-  ( ( b ` z ) = ( c ` z ) -> ( ( a ` z ) R ( b ` z ) <-> ( a ` z ) R ( c ` z ) ) )
123 122 biimpd
 |-  ( ( b ` z ) = ( c ` z ) -> ( ( a ` z ) R ( b ` z ) -> ( a ` z ) R ( c ` z ) ) )
124 121 123 syl6
 |-  ( z e. w -> ( A. y e. w ( b ` y ) = ( c ` y ) -> ( ( a ` z ) R ( b ` z ) -> ( a ` z ) R ( c ` z ) ) ) )
125 124 com3l
 |-  ( A. y e. w ( b ` y ) = ( c ` y ) -> ( ( a ` z ) R ( b ` z ) -> ( z e. w -> ( a ` z ) R ( c ` z ) ) ) )
126 125 imp
 |-  ( ( A. y e. w ( b ` y ) = ( c ` y ) /\ ( a ` z ) R ( b ` z ) ) -> ( z e. w -> ( a ` z ) R ( c ` z ) ) )
127 126 ad2ant2lr
 |-  ( ( ( 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 ) ) )
128 127 impcom
 |-  ( ( 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 ) )
129 128 3adant1
 |-  ( ( ( 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
 |-  ( t = z -> ( A. y e. t ( a ` y ) = ( c ` y ) <-> A. y e. z ( a ` y ) = ( c ` y ) ) )
131 fveq2
 |-  ( t = z -> ( a ` t ) = ( a ` z ) )
132 fveq2
 |-  ( t = z -> ( c ` t ) = ( c ` z ) )
133 131 132 breq12d
 |-  ( t = z -> ( ( a ` t ) R ( c ` t ) <-> ( a ` z ) R ( c ` z ) ) )
134 130 133 anbi12d
 |-  ( 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 ) ) ) )
135 134 rspcev
 |-  ( ( 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 ) ) )
136 104 117 129 135 syl12anc
 |-  ( ( ( 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 ) ) )
137 136 a1d
 |-  ( ( ( 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 ) ) ) )
138 137 3exp
 |-  ( ( 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 ) ) ) ) ) )
139 2 orderseqlem
 |-  ( a e. F -> ( a ` z ) e. ( A u. { (/) } ) )
140 139 ad2antrr
 |-  ( ( ( a e. F /\ b e. F ) /\ ( b e. F /\ c e. F ) ) -> ( a ` z ) e. ( A u. { (/) } ) )
141 2 orderseqlem
 |-  ( b e. F -> ( b ` z ) e. ( A u. { (/) } ) )
142 141 ad2antlr
 |-  ( ( ( a e. F /\ b e. F ) /\ ( b e. F /\ c e. F ) ) -> ( b ` z ) e. ( A u. { (/) } ) )
143 2 orderseqlem
 |-  ( c e. F -> ( c ` z ) e. ( A u. { (/) } ) )
144 143 ad2antll
 |-  ( ( ( a e. F /\ b e. F ) /\ ( b e. F /\ c e. F ) ) -> ( c ` z ) e. ( A u. { (/) } ) )
145 140 142 144 3jca
 |-  ( ( ( 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
 |-  ( ( 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 ) ) )
147 1 145 146 sylancr
 |-  ( ( ( 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 ) ) )
148 147 impcom
 |-  ( ( ( ( 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 ) )
149 113 148 anim12i
 |-  ( ( 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 ) ) )
150 149 anassrs
 |-  ( ( ( 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 ) ) )
151 150 135 sylan2
 |-  ( ( 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 ) ) )
152 151 exp32
 |-  ( 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
 |-  ( z = w -> ( A. y e. z ( b ` y ) = ( c ` y ) <-> A. y e. w ( b ` y ) = ( c ` y ) ) )
154 153 anbi2d
 |-  ( 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 ) ) ) )
155 110 154 syl5bb
 |-  ( 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
 |-  ( z = w -> ( b ` z ) = ( b ` w ) )
157 fveq2
 |-  ( z = w -> ( c ` z ) = ( c ` w ) )
158 156 157 breq12d
 |-  ( z = w -> ( ( b ` z ) R ( c ` z ) <-> ( b ` w ) R ( c ` w ) ) )
159 158 anbi2d
 |-  ( z = w -> ( ( ( a ` z ) R ( b ` z ) /\ ( b ` z ) R ( c ` z ) ) <-> ( ( a ` z ) R ( b ` z ) /\ ( b ` w ) R ( c ` w ) ) ) )
160 155 159 anbi12d
 |-  ( 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 ) ) ) ) )
161 160 imbi1d
 |-  ( 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 ) ) ) ) ) )
162 152 161 syl5ibcom
 |-  ( 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 ) ) ) ) ) )
163 162 adantr
 |-  ( ( 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
 |-  ( ( ( 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
 |-  ( z e. On -> ( w e. z -> w C_ z ) )
166 165 imp
 |-  ( ( z e. On /\ w e. z ) -> w C_ z )
167 166 adantlr
 |-  ( ( ( z e. On /\ w e. On ) /\ w e. z ) -> w C_ z )
168 ssralv
 |-  ( w C_ z -> ( A. y e. z ( a ` y ) = ( b ` y ) -> A. y e. w ( a ` y ) = ( b ` y ) ) )
169 168 anim1d
 |-  ( 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
 |-  ( 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 ) ) )
171 112 ralimi
 |-  ( A. y e. w ( ( a ` y ) = ( b ` y ) /\ ( b ` y ) = ( c ` y ) ) -> A. y e. w ( a ` y ) = ( c ` y ) )
172 170 171 sylbir
 |-  ( ( A. y e. w ( a ` y ) = ( b ` y ) /\ A. y e. w ( b ` y ) = ( c ` y ) ) -> A. y e. w ( a ` y ) = ( c ` y ) )
173 169 172 syl6
 |-  ( 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 ) ) )
174 173 adantrd
 |-  ( 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 ) ) )
175 167 174 syl
 |-  ( ( ( 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 ) ) )
176 175 3impia
 |-  ( ( ( 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
 |-  ( y = w -> ( a ` y ) = ( a ` w ) )
178 fveq2
 |-  ( y = w -> ( b ` y ) = ( b ` w ) )
179 177 178 eqeq12d
 |-  ( y = w -> ( ( a ` y ) = ( b ` y ) <-> ( a ` w ) = ( b ` w ) ) )
180 179 rspcv
 |-  ( w e. z -> ( A. y e. z ( a ` y ) = ( b ` y ) -> ( a ` w ) = ( b ` w ) ) )
181 breq1
 |-  ( ( a ` w ) = ( b ` w ) -> ( ( a ` w ) R ( c ` w ) <-> ( b ` w ) R ( c ` w ) ) )
182 181 biimprd
 |-  ( ( a ` w ) = ( b ` w ) -> ( ( b ` w ) R ( c ` w ) -> ( a ` w ) R ( c ` w ) ) )
183 180 182 syl6
 |-  ( w e. z -> ( A. y e. z ( a ` y ) = ( b ` y ) -> ( ( b ` w ) R ( c ` w ) -> ( a ` w ) R ( c ` w ) ) ) )
184 183 com3l
 |-  ( A. y e. z ( a ` y ) = ( b ` y ) -> ( ( b ` w ) R ( c ` w ) -> ( w e. z -> ( a ` w ) R ( c ` w ) ) ) )
185 184 imp
 |-  ( ( A. y e. z ( a ` y ) = ( b ` y ) /\ ( b ` w ) R ( c ` w ) ) -> ( w e. z -> ( a ` w ) R ( c ` w ) ) )
186 185 ad2ant2rl
 |-  ( ( ( 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 ) ) )
187 186 impcom
 |-  ( ( 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 ) )
188 187 3adant1
 |-  ( ( ( 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
 |-  ( t = w -> ( A. y e. t ( a ` y ) = ( c ` y ) <-> A. y e. w ( a ` y ) = ( c ` y ) ) )
190 fveq2
 |-  ( t = w -> ( a ` t ) = ( a ` w ) )
191 fveq2
 |-  ( t = w -> ( c ` t ) = ( c ` w ) )
192 190 191 breq12d
 |-  ( t = w -> ( ( a ` t ) R ( c ` t ) <-> ( a ` w ) R ( c ` w ) ) )
193 189 192 anbi12d
 |-  ( 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 ) ) ) )
194 193 rspcev
 |-  ( ( 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 ) ) )
195 164 176 188 194 syl12anc
 |-  ( ( ( 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 ) ) )
196 195 a1d
 |-  ( ( ( 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 ) ) ) )
197 196 3exp
 |-  ( ( 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 ) ) ) ) ) )
198 138 163 197 3jaod
 |-  ( ( 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 ) ) ) ) ) )
199 103 198 mpd
 |-  ( ( 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 ) ) ) ) )
200 199 rexlimivv
 |-  ( 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 ) ) ) )
201 99 200 sylbir
 |-  ( ( 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 ) ) ) )
202 201 impcom
 |-  ( ( ( ( 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 ) ) )
203 94 95 202 jca31
 |-  ( ( ( ( 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 ) ) ) )
204 203 an4s
 |-  ( ( ( ( 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 ) ) ) )
205 64 93 204 syl2anb
 |-  ( ( 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
 |-  ( x = t -> ( A. y e. x ( f ` y ) = ( g ` y ) <-> A. y e. t ( f ` y ) = ( g ` y ) ) )
207 fveq2
 |-  ( x = t -> ( f ` x ) = ( f ` t ) )
208 fveq2
 |-  ( x = t -> ( g ` x ) = ( g ` t ) )
209 207 208 breq12d
 |-  ( x = t -> ( ( f ` x ) R ( g ` x ) <-> ( f ` t ) R ( g ` t ) ) )
210 206 209 anbi12d
 |-  ( 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 ) ) ) )
211 210 cbvrexvw
 |-  ( 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 ) ) )
212 21 ralbidv
 |-  ( f = a -> ( A. y e. t ( f ` y ) = ( g ` y ) <-> A. y e. t ( a ` y ) = ( g ` y ) ) )
213 fveq1
 |-  ( f = a -> ( f ` t ) = ( a ` t ) )
214 213 breq1d
 |-  ( f = a -> ( ( f ` t ) R ( g ` t ) <-> ( a ` t ) R ( g ` t ) ) )
215 212 214 anbi12d
 |-  ( 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 ) ) ) )
216 215 rexbidv
 |-  ( 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 ) ) ) )
217 211 216 syl5bb
 |-  ( 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 ) ) ) )
218 19 217 anbi12d
 |-  ( 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 ) ) ) ) )
219 83 anbi2d
 |-  ( g = c -> ( ( a e. F /\ g e. F ) <-> ( a e. F /\ c e. F ) ) )
220 85 eqeq2d
 |-  ( g = c -> ( ( a ` y ) = ( g ` y ) <-> ( a ` y ) = ( c ` y ) ) )
221 220 ralbidv
 |-  ( g = c -> ( A. y e. t ( a ` y ) = ( g ` y ) <-> A. y e. t ( a ` y ) = ( c ` y ) ) )
222 fveq1
 |-  ( g = c -> ( g ` t ) = ( c ` t ) )
223 222 breq2d
 |-  ( g = c -> ( ( a ` t ) R ( g ` t ) <-> ( a ` t ) R ( c ` t ) ) )
224 221 223 anbi12d
 |-  ( 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 ) ) ) )
225 224 rexbidv
 |-  ( 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 ) ) ) )
226 219 225 anbi12d
 |-  ( 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 ) ) ) ) )
227 17 65 218 226 3 brab
 |-  ( 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 ) ) ) )
228 205 227 sylibr
 |-  ( ( a S b /\ b S c ) -> a S c )
229 39 228 pm3.2i
 |-  ( -. a S a /\ ( ( a S b /\ b S c ) -> a S c ) )
230 229 a1i
 |-  ( ( a e. F /\ b e. F /\ c e. F ) -> ( -. a S a /\ ( ( a S b /\ b S c ) -> a S c ) ) )
231 230 rgen3
 |-  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
 |-  ( 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 ) ) )
233 231 232 mpbir
 |-  S Po F