Theorem poseq 13954

Description: A partial ordering of sequences of ordinals.

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

Proof of Theorem poseq

Step	Hyp	Ref	Expression
1		poseq.2	. . . . . . . . . . . . . 14 |- F = {f | E.x e. On f:x-->A}
2		feq2 4552	. . . . . . . . . . . . . . . 16 |- (x = b -> (f:x-->A <-> f:b-->A))
3	2	cbvrexv 2281	. . . . . . . . . . . . . . 15 |- (E.x e. On f:x-->A <-> E.b e. On f:b-->A)
4	3	abbii 2006	. . . . . . . . . . . . . 14 |- {f | E.x e. On f:x-->A} = {f | E.b e. On f:b-->A}
5	1, 4	eqtri 1908	. . . . . . . . . . . . 13 |- F = {f | E.b e. On f:b-->A}
6	5	orderseqlem 13953	. . . . . . . . . . . 12 |- (a e. F -> (a` x) e. (A u. {(/)}))
7		poseq.1	. . . . . . . . . . . . 13 |- R Po (A u. {(/)})
8		poirr 3597	. . . . . . . . . . . . 13 |- ((R Po (A u. {(/)}) /\ (a` x) e. (A u. {(/)})) -> -. (a` x)R(a` x))
9	7, 8	mpan 759	. . . . . . . . . . . 12 |- ((a` x) e. (A u. {(/)}) -> -. (a` x)R(a` x))
10	6, 9	syl 12	. . . . . . . . . . 11 |- (a e. F -> -. (a` x)R(a` x))
11	10	intnand 757	. . . . . . . . . 10 |- (a e. F -> -. (A.y e. x (a` y) = (a` y) /\ (a` x)R(a` x)))
12	11	adantr 425	. . . . . . . . 9 |- ((a e. F /\ x e. On) -> -. (A.y e. x (a` y) = (a` y) /\ (a` x)R(a` x)))
13	12	nrexdv 2193	. . . . . . . 8 |- (a e. F -> -. E.x e. On (A.y e. x (a` y) = (a` y) /\ (a` x)R(a` x)))
14	13	adantr 425	. . . . . . 7 |- ((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 261	. . . . . . 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))))
16	14, 15	mpbi 206	. . . . . 6 |- -. ((a e. F /\ a e. F) /\ E.x e. On (A.y e. x (a` y) = (a` y) /\ (a` x)R(a` x)))
17		visset 2295	. . . . . . 7 |- a e. _V
18		eleq1 1957	. . . . . . . . 9 |- (f = a -> (f e. F <-> a e. F))
19	18	anbi1d 679	. . . . . . . 8 |- (f = a -> ((f e. F /\ g e. F) <-> (a e. F /\ g e. F)))
20		fveq1 4680	. . . . . . . . . . . 12 |- (f = a -> (f` y) = (a` y))
21	20	eqeq1d 1892	. . . . . . . . . . 11 |- (f = a -> ((f` y) = (g` y) <-> (a` y) = (g` y)))
22	21	ralbidv 2123	. . . . . . . . . 10 |- (f = a -> (A.y e. x (f` y) = (g` y) <-> A.y e. x (a` y) = (g` y)))
23		fveq1 4680	. . . . . . . . . . 11 |- (f = a -> (f` x) = (a` x))
24	23	breq1d 3348	. . . . . . . . . 10 |- (f = a -> ((f` x)R(g` x) <-> (a` x)R(g` x)))
25	22, 24	anbi12d 690	. . . . . . . . 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))))
26	25	rexbidv 2124	. . . . . . . 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))))
27	19, 26	anbi12d 690	. . . . . . 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)))))
28		eleq1 1957	. . . . . . . . 9 |- (g = a -> (g e. F <-> a e. F))
29	28	anbi2d 678	. . . . . . . 8 |- (g = a -> ((a e. F /\ g e. F) <-> (a e. F /\ a e. F)))
30		fveq1 4680	. . . . . . . . . . . 12 |- (g = a -> (g` y) = (a` y))
31	30	eqeq2d 1895	. . . . . . . . . . 11 |- (g = a -> ((a` y) = (g` y) <-> (a` y) = (a` y)))
32	31	ralbidv 2123	. . . . . . . . . 10 |- (g = a -> (A.y e. x (a` y) = (g` y) <-> A.y e. x (a` y) = (a` y)))
33		fveq1 4680	. . . . . . . . . . 11 |- (g = a -> (g` x) = (a` x))
34	33	breq2d 3350	. . . . . . . . . 10 |- (g = a -> ((a` x)R(g` x) <-> (a` x)R(a` x)))
35	32, 34	anbi12d 690	. . . . . . . . 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))))
36	35	rexbidv 2124	. . . . . . . 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))))
37	29, 36	anbi12d 690	. . . . . . 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)))))
38		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)))}
39	17, 17, 27, 37, 38	brab 3571	. . . . . 6 |- (aSa <-> ((a e. F /\ a e. F) /\ E.x e. On (A.y e. x (a` y) = (a` y) /\ (a` x)R(a` x))))
40	16, 39	mtbir 209	. . . . 5 |- -. aSa
41		simplll 452	. . . . . . . 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)
42		simplrr 455	. . . . . . . 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)))) -> c e. F)
43		an4 564	. . . . . . . . . . . 12 |- (((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))))
44	43	2rexbii 2130	. . . . . . . . . . 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 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))))
45		reeanv 2249	. . . . . . . . . . 11 |- (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))))
46	44, 45	bitri 190	. . . . . . . . . 10 |- (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))))
47		ordtri3or 3691	. . . . . . . . . . . . 13 |- ((Ord z /\ Ord w) -> (z e. w \/ z = w \/ w e. z))
48		eloni 3667	. . . . . . . . . . . . 13 |- (z e. On -> Ord z)
49		eloni 3667	. . . . . . . . . . . . 13 |- (w e. On -> Ord w)
50	47, 48, 49	syl2an 503	. . . . . . . . . . . 12 |- ((z e. On /\ w e. On) -> (z e. w \/ z = w \/ w e. z))
51		simp1l 900	. . . . . . . . . . . . . . . 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)))) -> z e. On)
52		onelss 3705	. . . . . . . . . . . . . . . . . . . . 21 |- (w e. On -> (z e. w -> z C_ w))
53	52	imp 377	. . . . . . . . . . . . . . . . . . . 20 |- ((w e. On /\ z e. w) -> z C_ w)
54	53	adantll 428	. . . . . . . . . . . . . . . . . . 19 |- (((z e. On /\ w e. On) /\ z e. w) -> z C_ w)
55		ssralv 2672	. . . . . . . . . . . . . . . . . . . . . 22 |- (z C_ w -> (A.y e. w (b` y) = (c` y) -> A.y e. z (b` y) = (c` y)))
56	55	anim2d 620	. . . . . . . . . . . . . . . . . . . . 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) /\ A.y e. z (b` y) = (c` y))))
57		r19.26 2219	. . . . . . . . . . . . . . . . . . . . 21 |- (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)))
58	56, 57	syl6ibr 230	. . . . . . . . . . . . . . . . . . . 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) = (b` y) /\ (b` y) = (c` y))))
59		eqtr 1904	. . . . . . . . . . . . . . . . . . . . 21 |- (((a` y) = (b` y) /\ (b` y) = (c` y)) -> (a` y) = (c` y))
60	59	ralimi 2168	. . . . . . . . . . . . . . . . . . . 20 |- (A.y e. z ((a` y) = (b` y) /\ (b` y) = (c` y)) -> A.y e. z (a` y) = (c` y))
61	58, 60	syl6 25	. . . . . . . . . . . . . . . . . . 19 |- (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)))
62	54, 61	syl 12	. . . . . . . . . . . . . . . . . 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.y e. z (a` y) = (c` y)))
63	62	adantrd 427	. . . . . . . . . . . . . . . . 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)))
64	63	3impia 1064	. . . . . . . . . . . . . . . 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)))) -> A.y e. z (a` y) = (c` y))
65		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (y = z -> (b` y) = (b` z))
66		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (y = z -> (c` y) = (c` z))
67	65, 66	eqeq12d 1899	. . . . . . . . . . . . . . . . . . . . . . 23 |- (y = z -> ((b` y) = (c` y) <-> (b` z) = (c` z)))
68	67	rcla4v 2376	. . . . . . . . . . . . . . . . . . . . . 22 |- (z e. w -> (A.y e. w (b` y) = (c` y) -> (b` z) = (c` z)))
69		breq2 3342	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((b` z) = (c` z) -> ((a` z)R(b` z) <-> (a` z)R(c` z)))
70	69	biimpd 170	. . . . . . . . . . . . . . . . . . . . . 22 |- ((b` z) = (c` z) -> ((a` z)R(b` z) -> (a` z)R(c` z)))
71	68, 70	syl6 25	. . . . . . . . . . . . . . . . . . . . 21 |- (z e. w -> (A.y e. w (b` y) = (c` y) -> ((a` z)R(b` z) -> (a` z)R(c` z))))
72	71	com3l 38	. . . . . . . . . . . . . . . . . . . 20 |- (A.y e. w (b` y) = (c` y) -> ((a` z)R(b` z) -> (z e. w -> (a` z)R(c` z))))
73	72	imp 377	. . . . . . . . . . . . . . . . . . 19 |- ((A.y e. w (b` y) = (c` y) /\ (a` z)R(b` z)) -> (z e. w -> (a` z)R(c` z)))
74	73	ad2ant2lr 446	. . . . . . . . . . . . . . . . . 18 |- (((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)))
75	74	impcom 378	. . . . . . . . . . . . . . . . 17 |- ((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))
76	75	3adant1 894	. . . . . . . . . . . . . . . 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)))) -> (a` z)R(c` z))
77		raleq 2266	. . . . . . . . . . . . . . . . . 18 |- (t = z -> (A.y e. t (a` y) = (c` y) <-> A.y e. z (a` y) = (c` y)))
78		fveq2 4681	. . . . . . . . . . . . . . . . . . 19 |- (t = z -> (a` t) = (a` z))
79		fveq2 4681	. . . . . . . . . . . . . . . . . . 19 |- (t = z -> (c` t) = (c` z))
80	78, 79	breq12d 3351	. . . . . . . . . . . . . . . . . 18 |- (t = z -> ((a` t)R(c` t) <-> (a` z)R(c` z)))
81	77, 80	anbi12d 690	. . . . . . . . . . . . . . . . 17 |- (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))))
82	81	rcla4ev 2381	. . . . . . . . . . . . . . . 16 |- ((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)))
83	51, 64, 76, 82	syl12anc 1098	. . . . . . . . . . . . . . 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)))) -> E.t e. On (A.y e. t (a` y) = (c` y) /\ (a` t)R(c` t)))
84	83	a1d 15	. . . . . . . . . . . . . 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))))
85	84	3exp 1066	. . . . . . . . . . . . 13 |- ((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))))))
86		raleq 2266	. . . . . . . . . . . . . . . . . . 19 |- (z = w -> (A.y e. z (b` y) = (c` y) <-> A.y e. w (b` y) = (c` y)))
87	86	anbi2d 678	. . . . . . . . . . . . . . . . . 18 |- (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))))
88	87, 57	syl5bb 591	. . . . . . . . . . . . . . . . 17 |- (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))))
89		fveq2 4681	. . . . . . . . . . . . . . . . . . 19 |- (z = w -> (b` z) = (b` w))
90		fveq2 4681	. . . . . . . . . . . . . . . . . . 19 |- (z = w -> (c` z) = (c` w))
91	89, 90	breq12d 3351	. . . . . . . . . . . . . . . . . 18 |- (z = w -> ((b` z)R(c` z) <-> (b` w)R(c` w)))
92	91	anbi2d 678	. . . . . . . . . . . . . . . . 17 |- (z = w -> (((a` z)R(b` z) /\ (b` z)R(c` z)) <-> ((a` z)R(b` z) /\ (b` w)R(c` w))))
93	88, 92	anbi12d 690	. . . . . . . . . . . . . . . 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.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)))))
94	93	imbi1d 675	. . . . . . . . . . . . . . 15 |- (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))))))
95		potr 3598	. . . . . . . . . . . . . . . . . . . . 21 |- ((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)))
96	1	orderseqlem 13953	. . . . . . . . . . . . . . . . . . . . . . 23 |- (a e. F -> (a` z) e. (A u. {(/)}))
97	96	ad2antrr 440	. . . . . . . . . . . . . . . . . . . . . 22 |- (((a e. F /\ b e. F) /\ (b e. F /\ c e. F)) -> (a` z) e. (A u. {(/)}))
98	1	orderseqlem 13953	. . . . . . . . . . . . . . . . . . . . . . 23 |- (b e. F -> (b` z) e. (A u. {(/)}))
99	98	ad2antlr 441	. . . . . . . . . . . . . . . . . . . . . 22 |- (((a e. F /\ b e. F) /\ (b e. F /\ c e. F)) -> (b` z) e. (A u. {(/)}))
100	1	orderseqlem 13953	. . . . . . . . . . . . . . . . . . . . . . 23 |- (c e. F -> (c` z) e. (A u. {(/)}))
101	100	ad2antll 443	. . . . . . . . . . . . . . . . . . . . . 22 |- (((a e. F /\ b e. F) /\ (b e. F /\ c e. F)) -> (c` z) e. (A u. {(/)}))
102	97, 99, 101	3jca 1050	. . . . . . . . . . . . . . . . . . . . 21 |- (((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. {(/)})))
103	95, 7, 102	sylancr 526	. . . . . . . . . . . . . . . . . . . 20 |- (((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)))
104	103	impcom 378	. . . . . . . . . . . . . . . . . . 19 |- ((((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))
105	60, 104	anim12i 360	. . . . . . . . . . . . . . . . . 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)))
106	105	anassrs 489	. . . . . . . . . . . . . . . . 17 |- (((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)))
107	82, 106	sylan2 500	. . . . . . . . . . . . . . . 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)))
108	107	exp32 408	. . . . . . . . . . . . . . 15 |- (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)))))
109	94, 108	syl5cbi 226	. . . . . . . . . . . . . 14 |- (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))))))
110	109	adantr 425	. . . . . . . . . . . . 13 |- ((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))))))
111		simp1r 901	. . . . . . . . . . . . . . . 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)))) -> w e. On)
112		onelss 3705	. . . . . . . . . . . . . . . . . . . 20 |- (z e. On -> (w e. z -> w C_ z))
113	112	imp 377	. . . . . . . . . . . . . . . . . . 19 |- ((z e. On /\ w e. z) -> w C_ z)
114	113	adantlr 429	. . . . . . . . . . . . . . . . . 18 |- (((z e. On /\ w e. On) /\ w e. z) -> w C_ z)
115		ssralv 2672	. . . . . . . . . . . . . . . . . . . . 21 |- (w C_ z -> (A.y e. z (a` y) = (b` y) -> A.y e. w (a` y) = (b` y)))
116	115	anim1d 619	. . . . . . . . . . . . . . . . . . . 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) = (b` y) /\ A.y e. w (b` y) = (c` y))))
117		r19.26 2219	. . . . . . . . . . . . . . . . . . . . 21 |- (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)))
118	59	ralimi 2168	. . . . . . . . . . . . . . . . . . . . 21 |- (A.y e. w ((a` y) = (b` y) /\ (b` y) = (c` y)) -> A.y e. w (a` y) = (c` y))
119	117, 118	sylbir 218	. . . . . . . . . . . . . . . . . . . 20 |- ((A.y e. w (a` y) = (b` y) /\ A.y e. w (b` y) = (c` y)) -> A.y e. w (a` y) = (c` y))
120	116, 119	syl6 25	. . . . . . . . . . . . . . . . . . 19 |- (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)))
121	120	adantrd 427	. . . . . . . . . . . . . . . . . 18 |- (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)))
122	114, 121	syl 12	. . . . . . . . . . . . . . . . 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)))
123	122	3impia 1064	. . . . . . . . . . . . . . . 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)))) -> A.y e. w (a` y) = (c` y))
124		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (y = w -> (a` y) = (a` w))
125		fveq2 4681	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (y = w -> (b` y) = (b` w))
126	124, 125	eqeq12d 1899	. . . . . . . . . . . . . . . . . . . . . . 23 |- (y = w -> ((a` y) = (b` y) <-> (a` w) = (b` w)))
127	126	rcla4v 2376	. . . . . . . . . . . . . . . . . . . . . 22 |- (w e. z -> (A.y e. z (a` y) = (b` y) -> (a` w) = (b` w)))
128		breq1 3341	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((a` w) = (b` w) -> ((a` w)R(c` w) <-> (b` w)R(c` w)))
129	128	biimprd 171	. . . . . . . . . . . . . . . . . . . . . 22 |- ((a` w) = (b` w) -> ((b` w)R(c` w) -> (a` w)R(c` w)))
130	127, 129	syl6 25	. . . . . . . . . . . . . . . . . . . . 21 |- (w e. z -> (A.y e. z (a` y) = (b` y) -> ((b` w)R(c` w) -> (a` w)R(c` w))))
131	130	com3l 38	. . . . . . . . . . . . . . . . . . . 20 |- (A.y e. z (a` y) = (b` y) -> ((b` w)R(c` w) -> (w e. z -> (a` w)R(c` w))))
132	131	imp 377	. . . . . . . . . . . . . . . . . . 19 |- ((A.y e. z (a` y) = (b` y) /\ (b` w)R(c` w)) -> (w e. z -> (a` w)R(c` w)))
133	132	ad2ant2rl 447	. . . . . . . . . . . . . . . . . 18 |- (((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)))
134	133	impcom 378	. . . . . . . . . . . . . . . . 17 |- ((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))
135	134	3adant1 894	. . . . . . . . . . . . . . . 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)))) -> (a` w)R(c` w))
136		raleq 2266	. . . . . . . . . . . . . . . . . 18 |- (t = w -> (A.y e. t (a` y) = (c` y) <-> A.y e. w (a` y) = (c` y)))
137		fveq2 4681	. . . . . . . . . . . . . . . . . . 19 |- (t = w -> (a` t) = (a` w))
138		fveq2 4681	. . . . . . . . . . . . . . . . . . 19 |- (t = w -> (c` t) = (c` w))
139	137, 138	breq12d 3351	. . . . . . . . . . . . . . . . . 18 |- (t = w -> ((a` t)R(c` t) <-> (a` w)R(c` w)))
140	136, 139	anbi12d 690	. . . . . . . . . . . . . . . . 17 |- (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))))
141	140	rcla4ev 2381	. . . . . . . . . . . . . . . 16 |- ((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)))
142	111, 123, 135, 141	syl12anc 1098	. . . . . . . . . . . . . . 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)))) -> E.t e. On (A.y e. t (a` y) = (c` y) /\ (a` t)R(c` t)))
143	142	a1d 15	. . . . . . . . . . . . . 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))))
144	143	3exp 1066	. . . . . . . . . . . . 13 |- ((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))))))
145	85, 110, 144	3jaod 1161	. . . . . . . . . . . 12 |- ((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))))))
146	50, 145	mpd 29	. . . . . . . . . . 11 |- ((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)))))
147	146	r19.23aivv 2217	. . . . . . . . . 10 |- (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))))
148	46, 147	sylbir 218	. . . . . . . . 9 |- ((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))))
149	148	impcom 378	. . . . . . . 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)))) -> E.t e. On (A.y e. t (a` y) = (c` y) /\ (a` t)R(c` t)))
150	41, 42, 149	jca31 311	. . . . . . 7 |- ((((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))))
151	150	an4s 566	. . . . . 6 |- ((((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))))
152		visset 2295	. . . . . . . 8 |- b e. _V
153	21	ralbidv 2123	. . . . . . . . . . . 12 |- (f = a -> (A.y e. z (f` y) = (g` y) <-> A.y e. z (a` y) = (g` y)))
154		fveq1 4680	. . . . . . . . . . . . 13 |- (f = a -> (f` z) = (a` z))
155	154	breq1d 3348	. . . . . . . . . . . 12 |- (f = a -> ((f` z)R(g` z) <-> (a` z)R(g` z)))
156	153, 155	anbi12d 690	. . . . . . . . . . 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))))
157	156	rexbidv 2124	. . . . . . . . . 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))))
158		raleq 2266	. . . . . . . . . . . 12 |- (x = z -> (A.y e. x (f` y) = (g` y) <-> A.y e. z (f` y) = (g` y)))
159		fveq2 4681	. . . . . . . . . . . . 13 |- (x = z -> (f` x) = (f` z))
160		fveq2 4681	. . . . . . . . . . . . 13 |- (x = z -> (g` x) = (g` z))
161	159, 160	breq12d 3351	. . . . . . . . . . . 12 |- (x = z -> ((f` x)R(g` x) <-> (f` z)R(g` z)))
162	158, 161	anbi12d 690	. . . . . . . . . . 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))))
163	162	cbvrexv 2281	. . . . . . . . . 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)))
164	157, 163	syl5bb 591	. . . . . . . . 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))))
165	19, 164	anbi12d 690	. . . . . . . 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)))))
166		eleq1 1957	. . . . . . . . . 10 |- (g = b -> (g e. F <-> b e. F))
167	166	anbi2d 678	. . . . . . . . 9 |- (g = b -> ((a e. F /\ g e. F) <-> (a e. F /\ b e. F)))
168		fveq1 4680	. . . . . . . . . . . . 13 |- (g = b -> (g` y) = (b` y))
169	168	eqeq2d 1895	. . . . . . . . . . . 12 |- (g = b -> ((a` y) = (g` y) <-> (a` y) = (b` y)))
170	169	ralbidv 2123	. . . . . . . . . . 11 |- (g = b -> (A.y e. z (a` y) = (g` y) <-> A.y e. z (a` y) = (b` y)))
171		fveq1 4680	. . . . . . . . . . . 12 |- (g = b -> (g` z) = (b` z))
172	171	breq2d 3350	. . . . . . . . . . 11 |- (g = b -> ((a` z)R(g` z) <-> (a` z)R(b` z)))
173	170, 172	anbi12d 690	. . . . . . . . . 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))))
174	173	rexbidv 2124	. . . . . . . . 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))))
175	167, 174	anbi12d 690	. . . . . . . 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)))))
176	17, 152, 165, 175, 38	brab 3571	. . . . . . 7 |- (aSb <-> ((a e. F /\ b e. F) /\ E.z e. On (A.y e. z (a` y) = (b` y) /\ (a` z)R(b` z))))
177		visset 2295	. . . . . . . 8 |- c e. _V
178		eleq1 1957	. . . . . . . . . 10 |- (f = b -> (f e. F <-> b e. F))
179	178	anbi1d 679	. . . . . . . . 9 |- (f = b -> ((f e. F /\ g e. F) <-> (b e. F /\ g e. F)))
180		fveq1 4680	. . . . . . . . . . . . . 14 |- (f = b -> (f` y) = (b` y))
181	180	eqeq1d 1892	. . . . . . . . . . . . 13 |- (f = b -> ((f` y) = (g` y) <-> (b` y) = (g` y)))
182	181	ralbidv 2123	. . . . . . . . . . . 12 |- (f = b -> (A.y e. w (f` y) = (g` y) <-> A.y e. w (b` y) = (g` y)))
183		fveq1 4680	. . . . . . . . . . . . 13 |- (f = b -> (f` w) = (b` w))
184	183	breq1d 3348	. . . . . . . . . . . 12 |- (f = b -> ((f` w)R(g` w) <-> (b` w)R(g` w)))
185	182, 184	anbi12d 690	. . . . . . . . . . 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))))
186	185	rexbidv 2124	. . . . . . . . . 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))))
187		raleq 2266	. . . . . . . . . . . 12 |- (x = w -> (A.y e. x (f` y) = (g` y) <-> A.y e. w (f` y) = (g` y)))
188		fveq2 4681	. . . . . . . . . . . . 13 |- (x = w -> (f` x) = (f` w))
189		fveq2 4681	. . . . . . . . . . . . 13 |- (x = w -> (g` x) = (g` w))
190	188, 189	breq12d 3351	. . . . . . . . . . . 12 |- (x = w -> ((f` x)R(g` x) <-> (f` w)R(g` w)))
191	187, 190	anbi12d 690	. . . . . . . . . . 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))))
192	191	cbvrexv 2281	. . . . . . . . . 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)))
193	186, 192	syl5bb 591	. . . . . . . . 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))))
194	179, 193	anbi12d 690	. . . . . . . 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)))))
195		eleq1 1957	. . . . . . . . . 10 |- (g = c -> (g e. F <-> c e. F))
196	195	anbi2d 678	. . . . . . . . 9 |- (g = c -> ((b e. F /\ g e. F) <-> (b e. F /\ c e. F)))
197		fveq1 4680	. . . . . . . . . . . . 13 |- (g = c -> (g` y) = (c` y))
198	197	eqeq2d 1895	. . . . . . . . . . . 12 |- (g = c -> ((b` y) = (g` y) <-> (b` y) = (c` y)))
199	198	ralbidv 2123	. . . . . . . . . . 11 |- (g = c -> (A.y e. w (b` y) = (g` y) <-> A.y e. w (b` y) = (c` y)))
200		fveq1 4680	. . . . . . . . . . . 12 |- (g = c -> (g` w) = (c` w))
201	200	breq2d 3350	. . . . . . . . . . 11 |- (g = c -> ((b` w)R(g` w) <-> (b` w)R(c` w)))
202	199, 201	anbi12d 690	. . . . . . . . . 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))))
203	202	rexbidv 2124	. . . . . . . . 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))))
204	196, 203	anbi12d 690	. . . . . . . 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)))))
205	152, 177, 194, 204, 38	brab 3571	. . . . . . 7 |- (bSc <-> ((b e. F /\ c e. F) /\ E.w e. On (A.y e. w (b` y) = (c` y) /\ (b` w)R(c` w))))
206	176, 205	anbi12i 540	. . . . . 6 |- ((aSb /\ bSc) <-> (((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)))))
207	21	ralbidv 2123	. . . . . . . . . . 11 |- (f = a -> (A.y e. t (f` y) = (g` y) <-> A.y e. t (a` y) = (g` y)))
208		fveq1 4680	. . . . . . . . . . . 12 |- (f = a -> (f` t) = (a` t))
209	208	breq1d 3348	. . . . . . . . . . 11 |- (f = a -> ((f` t)R(g` t) <-> (a` t)R(g` t)))
210	207, 209	anbi12d 690	. . . . . . . . . 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))))
211	210	rexbidv 2124	. . . . . . . . 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))))
212		raleq 2266	. . . . . . . . . . 11 |- (x = t -> (A.y e. x (f` y) = (g` y) <-> A.y e. t (f` y) = (g` y)))
213		fveq2 4681	. . . . . . . . . . . 12 |- (x = t -> (f` x) = (f` t))
214		fveq2 4681	. . . . . . . . . . . 12 |- (x = t -> (g` x) = (g` t))
215	213, 214	breq12d 3351	. . . . . . . . . . 11 |- (x = t -> ((f` x)R(g` x) <-> (f` t)R(g` t)))
216	212, 215	anbi12d 690	. . . . . . . . . 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))))
217	216	cbvrexv 2281	. . . . . . . . 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)))
218	211, 217	syl5bb 591	. . . . . . . 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))))
219	19, 218	anbi12d 690	. . . . . . 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)))))
220	195	anbi2d 678	. . . . . . . 8 |- (g = c -> ((a e. F /\ g e. F) <-> (a e. F /\ c e. F)))
221	197	eqeq2d 1895	. . . . . . . . . . 11 |- (g = c -> ((a` y) = (g` y) <-> (a` y) = (c` y)))
222	221	ralbidv 2123	. . . . . . . . . 10 |- (g = c -> (A.y e. t (a` y) = (g` y) <-> A.y e. t (a` y) = (c` y)))
223		fveq1 4680	. . . . . . . . . . 11 |- (g = c -> (g` t) = (c` t))
224	223	breq2d 3350	. . . . . . . . . 10 |- (g = c -> ((a` t)R(g` t) <-> (a` t)R(c` t)))
225	222, 224	anbi12d 690	. . . . . . . . 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))))
226	225	rexbidv 2124	. . . . . . . 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))))
227	220, 226	anbi12d 690	. . . . . . 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)))))
228	17, 177, 219, 227, 38	brab 3571	. . . . . 6 |- (aSc <-> ((a e. F /\ c e. F) /\ E.t e. On (A.y e. t (a` y) = (c` y) /\ (a` t)R(c` t))))
229	151, 206, 228	3imtr4i 236	. . . . 5 |- ((aSb /\ bSc) -> aSc)
230	40, 229	pm3.2i 307	. . . 4 |- (-. aSa /\ ((aSb /\ bSc) -> aSc))
231	230	a1i 8	. . 3 |- ((a e. F /\ b e. F /\ c e. F) -> (-. aSa /\ ((aSb /\ bSc) -> aSc)))
232	231	rgen3 2187	. 2 |- A.a e. F A.b e. F A.c e. F (-. aSa /\ ((aSb /\ bSc) -> aSc))
233		df-po 3591	. 2 |- (S Po F <-> A.a e. F A.b e. F A.c e. F (-. aSa /\ ((aSb /\ bSc) -> aSc)))
234	232, 233	mpbir 207	1 |- S Po F

Syntax hints:  -. wn 2   -> wi 3   /\ wa 240   \/ w3o 857   /\ w3a 858   = wceq 1298   e. wcel 1300  {cab 1871  A.wral 2105  E.wrex 2106   u. cun 2591   C_ wss 2593  (/)c0 2875  {csn 3044   class class class wbr 3338  {copab 3395   Po wpo 3589  Ord word 3656  Oncon0 3657  -->wf 3994  ` cfv 3998

This theorem is referenced by:  soseq 13955

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-fv 4014

Copyright terms: Public domain