Theorem poseq 31750

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.

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

Syntax hints:   -. wn 3   -> wi 4   /\ wa 384   \/ w3o 1036   /\ w3a 1037   = wceq 1483   e. wcel 1990   {cab 2608   A.wral 2912   E.wrex 2913   u. cun 3572   C_ wss 3574   (/)c0 3915   {csn 4177   class class class wbr 4653   {copab 4712   Po wpo 5033   Ord word 5722   Oncon0 5723   -->wf 5884   ` cfv 5888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-ral 2917  df-rex 2918  df-rab 2921  df-v 3202  df-sbc 3436  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-uni 4437  df-br 4654  df-opab 4713  df-tr 4753  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-we 5075  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-ord 5726  df-on 5727  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-fv 5896

This theorem is referenced by:  soseq  31751