Theorem supsrlem6 4024

Description: Lemma for supremum theorem.

Hypotheses

Ref	Expression
supsrlem.1	|- C e. R.
supsrlem.2	|- B = {w | (C +R (w +R -1R)) e. A}

Assertion

Ref	Expression
supsrlem6	|- ((C e. A /\ E.x(x e. R. /\ A.y(y e. R. -> (y e. A -> y <R x)))) -> E.x(x e. R. /\ A.y(y e. R. -> ((y e. A -> -. x <R y) /\ (y <R x -> E.z(z e. R. /\ (z e. A /\ y <R z)))))))

Distinct variable group(s):   x,y,z,w,A   x,B,y,z,w   x,C,y,z,w

Proof of Theorem supsrlem6

Step	Hyp	Ref	Expression
1		eleq1 1149	. . . . . . 7 |- (x = v -> (x e. B <-> v e. B))
2		breq2 2066	. . . . . . 7 |- (x = v -> (0R <R x <-> 0R <R v))
3	1, 2	anbi12d 476	. . . . . 6 |- (x = v -> ((x e. B /\ 0R <R x) <-> (v e. B /\ 0R <R v)))
4	3	cbvabv 1424	. . . . 5 |- {x | (x e. B /\ 0R <R x)} = {v | (v e. B /\ 0R <R v)}
5	4	suppsr3 4018	. . . 4 |- ((E.v(v e. B /\ 0R <R v) /\ E.w(w e. R. /\ A.v(v e. R. -> (v e. B -> v <R w)))) -> E.w(w e. R. /\ A.v(v e. R. -> ((v e. B -> -. w <R v) /\ (v <R w -> E.u(u e. R. /\ (u e. B /\ v <R u)))))))
6		oprex 3018	. . . . 5 |- (C +R (w +R -1R)) e. V
7		breq1 2065	. . . . . . . . . . 11 |- ((C +R (w +R -1R)) = x -> ((C +R (w +R -1R)) <R y <-> x <R y))
8	7	negbid 463	. . . . . . . . . 10 |- ((C +R (w +R -1R)) = x -> (-. (C +R (w +R -1R)) <R y <-> -. x <R y))
9	8	imbi2d 464	. . . . . . . . 9 |- ((C +R (w +R -1R)) = x -> ((y e. A -> -. (C +R (w +R -1R)) <R y) <-> (y e. A -> -. x <R y)))
10		breq2 2066	. . . . . . . . . 10 |- ((C +R (w +R -1R)) = x -> (y <R (C +R (w +R -1R)) <-> y <R x))
11	10	imbi1d 465	. . . . . . . . 9 |- ((C +R (w +R -1R)) = x -> ((y <R (C +R (w +R -1R)) -> E.z(z e. R. /\ (z e. A /\ y <R z))) <-> (y <R x -> E.z(z e. R. /\ (z e. A /\ y <R z)))))
12	9, 11	anbi12d 476	. . . . . . . 8 |- ((C +R (w +R -1R)) = x -> (((y e. A -> -. (C +R (w +R -1R)) <R y) /\ (y <R (C +R (w +R -1R)) -> E.z(z e. R. /\ (z e. A /\ y <R z)))) <-> ((y e. A -> -. x <R y) /\ (y <R x -> E.z(z e. R. /\ (z e. A /\ y <R z))))))
13	12	imbi2d 464	. . . . . . 7 |- ((C +R (w +R -1R)) = x -> ((y e. R. -> ((y e. A -> -. (C +R (w +R -1R)) <R y) /\ (y <R (C +R (w +R -1R)) -> E.z(z e. R. /\ (z e. A /\ y <R z))))) <-> (y e. R. -> ((y e. A -> -. x <R y) /\ (y <R x -> E.z(z e. R. /\ (z e. A /\ y <R z)))))))
14	13	bialdv 935	. . . . . 6 |- ((C +R (w +R -1R)) = x -> (A.y(y e. R. -> ((y e. A -> -. (C +R (w +R -1R)) <R y) /\ (y <R (C +R (w +R -1R)) -> E.z(z e. R. /\ (z e. A /\ y <R z))))) <-> A.y(y e. R. -> ((y e. A -> -. x <R y) /\ (y <R x -> E.z(z e. R. /\ (z e. A /\ y <R z)))))))
15		oprex 3018	. . . . . . 7 |- (C +R (v +R -1R)) e. V
16		eleq1 1149	. . . . . . . . . 10 |- ((C +R (v +R -1R)) = y -> ((C +R (v +R -1R)) e. A <-> y e. A))
17		supsrlem.1	. . . . . . . . . . 11 |- C e. R.
18		supsrlem.2	. . . . . . . . . . 11 |- B = {w | (C +R (w +R -1R)) e. A}
19		visset 1350	. . . . . . . . . . 11 |- v e. V
20	17, 18, 19	supsrlem4 4022	. . . . . . . . . 10 |- (v e. B <-> (C +R (v +R -1R)) e. A)
21	16, 20	syl5bb 410	. . . . . . . . 9 |- ((C +R (v +R -1R)) = y -> (v e. B <-> y e. A))
22		breq2 2066	. . . . . . . . . . 11 |- ((C +R (v +R -1R)) = y -> ((C +R (w +R -1R)) <R (C +R (v +R -1R)) <-> (C +R (w +R -1R)) <R y))
23		visset 1350	. . . . . . . . . . . 12 |- w e. V
24	17, 23, 19	supsrlem3 4021	. . . . . . . . . . 11 |- ((C +R (w +R -1R)) <R (C +R (v +R -1R)) <-> w <R v)
25	22, 24	syl5bbr 412	. . . . . . . . . 10 |- ((C +R (v +R -1R)) = y -> (w <R v <-> (C +R (w +R -1R)) <R y))
26	25	negbid 463	. . . . . . . . 9 |- ((C +R (v +R -1R)) = y -> (-. w <R v <-> -. (C +R (w +R -1R)) <R y))
27	21, 26	imbi12d 474	. . . . . . . 8 |- ((C +R (v +R -1R)) = y -> ((v e. B -> -. w <R v) <-> (y e. A -> -. (C +R (w +R -1R)) <R y)))
28		breq1 2065	. . . . . . . . . 10 |- ((C +R (v +R -1R)) = y -> ((C +R (v +R -1R)) <R (C +R (w +R -1R)) <-> y <R (C +R (w +R -1R))))
29	17, 19, 23	supsrlem3 4021	. . . . . . . . . 10 |- ((C +R (v +R -1R)) <R (C +R (w +R -1R)) <-> v <R w)
30	28, 29	syl5bbr 412	. . . . . . . . 9 |- ((C +R (v +R -1R)) = y -> (v <R w <-> y <R (C +R (w +R -1R))))
31		breq1 2065	. . . . . . . . . . . . 13 |- ((C +R (v +R -1R)) = y -> ((C +R (v +R -1R)) <R z <-> y <R z))
32	31	anbi2d 468	. . . . . . . . . . . 12 |- ((C +R (v +R -1R)) = y -> ((z e. A /\ (C +R (v +R -1R)) <R z) <-> (z e. A /\ y <R z)))
33	32	anbi2d 468	. . . . . . . . . . 11 |- ((C +R (v +R -1R)) = y -> ((z e. R. /\ (z e. A /\ (C +R (v +R -1R)) <R z)) <-> (z e. R. /\ (z e. A /\ y <R z))))
34	33	biexdv 936	. . . . . . . . . 10 |- ((C +R (v +R -1R)) = y -> (E.z(z e. R. /\ (z e. A /\ (C +R (v +R -1R)) <R z)) <-> E.z(z e. R. /\ (z e. A /\ y <R z))))
35		oprex 3018	. . . . . . . . . . 11 |- (C +R (u +R -1R)) e. V
36		eleq1 1149	. . . . . . . . . . . . 13 |- ((C +R (u +R -1R)) = z -> ((C +R (u +R -1R)) e. A <-> z e. A))
37		visset 1350	. . . . . . . . . . . . . 14 |- u e. V
38	17, 18, 37	supsrlem4 4022	. . . . . . . . . . . . 13 |- (u e. B <-> (C +R (u +R -1R)) e. A)
39	36, 38	syl5bb 410	. . . . . . . . . . . 12 |- ((C +R (u +R -1R)) = z -> (u e. B <-> z e. A))
40		breq2 2066	. . . . . . . . . . . . 13 |- ((C +R (u +R -1R)) = z -> ((C +R (v +R -1R)) <R (C +R (u +R -1R)) <-> (C +R (v +R -1R)) <R z))
41	17, 19, 37	supsrlem3 4021	. . . . . . . . . . . . 13 |- ((C +R (v +R -1R)) <R (C +R (u +R -1R)) <-> v <R u)
42	40, 41	syl5bbr 412	. . . . . . . . . . . 12 |- ((C +R (u +R -1R)) = z -> (v <R u <-> (C +R (v +R -1R)) <R z))
43	39, 42	anbi12d 476	. . . . . . . . . . 11 |- ((C +R (u +R -1R)) = z -> ((u e. B /\ v <R u) <-> (z e. A /\ (C +R (v +R -1R)) <R z)))
44		eleq1 1149	. . . . . . . . . . . 12 |- ((C +R (u +R -1R)) = z -> ((C +R (u +R -1R)) e. R. <-> z e. R.))
45	17	supsrlem1 4019	. . . . . . . . . . . 12 |- ((C +R (u +R -1R)) e. R. <-> u e. R.)
46	44, 45	syl5bbr 412	. . . . . . . . . . 11 |- ((C +R (u +R -1R)) = z -> (u e. R. <-> z e. R.))
47	17	supsrlem2 4020	. . . . . . . . . . 11 |- (z e. R. <-> E.u(u e. R. /\ (C +R (u +R -1R)) = z))
48	35, 43, 46, 47	gencbvex 1372	. . . . . . . . . 10 |- (E.u(u e. R. /\ (u e. B /\ v <R u)) <-> E.z(z e. R. /\ (z e. A /\ (C +R (v +R -1R)) <R z)))
49	34, 48	syl5bb 410	. . . . . . . . 9 |- ((C +R (v +R -1R)) = y -> (E.u(u e. R. /\ (u e. B /\ v <R u)) <-> E.z(z e. R. /\ (z e. A /\ y <R z))))
50	30, 49	imbi12d 474	. . . . . . . 8 |- ((C +R (v +R -1R)) = y -> ((v <R w -> E.u(u e. R. /\ (u e. B /\ v <R u))) <-> (y <R (C +R (w +R -1R)) -> E.z(z e. R. /\ (z e. A /\ y <R z)))))
51	27, 50	anbi12d 476	. . . . . . 7 |- ((C +R (v +R -1R)) = y -> (((v e. B -> -. w <R v) /\ (v <R w -> E.u(u e. R. /\ (u e. B /\ v <R u)))) <-> ((y e. A -> -. (C +R (w +R -1R)) <R y) /\ (y <R (C +R (w +R -1R)) -> E.z(z e. R. /\ (z e. A