Theorem poseq

Description: A partial ordering of ordinal sequences. (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	bitrid	|- ( 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	bitrid	|- ( 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	imbitrrdi	|- ( 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	bitrid	|- ( 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	bitrid	|- ( 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