Theorem infm3 6001

Description: The completeness axiom for reals in terms of infimum: a non-empty, bounded-below set of reals has a infimum. (This theorem is the dual of sup3 5999.)

Assertion

Ref	Expression
infm3	|- ((A (_ RR /\ A =/= (/) /\ E.x e. RR A.y e. A x <_ y) -> E.x e. RR (A.y e. A -. y < x /\ A.y e. RR (x < y -> E.z e. A z < y)))

Distinct variable group:   x,y,z,A

Proof of Theorem infm3

Step	Hyp	Ref	Expression
1		ssel 2053	. . . . . . . . 9 |- (A (_ RR -> (v e. A -> v e. RR))
2	1	pm4.71rd 637	. . . . . . . 8 |- (A (_ RR -> (v e. A <-> (v e. RR /\ v e. A)))
3	2	exbidv 1274	. . . . . . 7 |- (A (_ RR -> (E.v v e. A <-> E.v(v e. RR /\ v e. A)))
4		df-rex 1642	. . . . . . . 8 |- (E.v e. RR v e. A <-> E.v(v e. RR /\ v e. A))
5		renegclt 5409	. . . . . . . . 9 |- (w e. RR -> -uw e. RR)
6		infm3lem 6000	. . . . . . . . 9 |- (v e. RR -> E.w e. RR v = -uw)
7		eleq1 1526	. . . . . . . . 9 |- (v = -uw -> (v e. A <-> -uw e. A))
8	5, 6, 7	rexxfr 2891	. . . . . . . 8 |- (E.v e. RR v e. A <-> E.w e. RR -uw e. A)
9	4, 8	bitr3 175	. . . . . . 7 |- (E.v(v e. RR /\ v e. A) <-> E.w e. RR -uw e. A)
10	3, 9	syl6bb 534	. . . . . 6 |- (A (_ RR -> (E.v v e. A <-> E.w e. RR -uw e. A))
11		ne0 2278	. . . . . 6 |- (A =/= (/) <-> E.v v e. A)
12		rabn0 2282	. . . . . 6 |- ({w e. RR | -uw e. A} =/= (/) <-> E.w e. RR -uw e. A)
13	10, 11, 12	3bitr4g 553	. . . . 5 |- (A (_ RR -> (A =/= (/) <-> {w e. RR | -uw e. A} =/= (/)))
14		ssel 2053	. . . . . . . . . . . 12 |- (A (_ RR -> (y e. A -> y e. RR))
15	14	pm4.71rd 637	. . . . . . . . . . 11 |- (A (_ RR -> (y e. A <-> (y e. RR /\ y e. A)))
16	15	imbi1d 611	. . . . . . . . . 10 |- (A (_ RR -> ((y e. A -> x <_ y) <-> ((y e. RR /\ y e. A) -> x <_ y)))
17		impexp 347	. . . . . . . . . 10 |- (((y e. RR /\ y e. A) -> x <_ y) <-> (y e. RR -> (y e. A -> x <_ y)))
18	16, 17	syl6bb 534	. . . . . . . . 9 |- (A (_ RR -> ((y e. A -> x <_ y) <-> (y e. RR -> (y e. A -> x <_ y))))
19	18	albidv 1273	. . . . . . . 8 |- (A (_ RR -> (A.y(y e. A -> x <_ y) <-> A.y(y e. RR -> (y e. A -> x <_ y))))
20		df-ral 1641	. . . . . . . 8 |- (A.y e. A x <_ y <-> A.y(y e. A -> x <_ y))
21		renegclt 5409	. . . . . . . . . 10 |- (v e. RR -> -uv e. RR)
22		infm3lem 6000	. . . . . . . . . 10 |- (y e. RR -> E.v e. RR y = -uv)
23		eleq1 1526	. . . . . . . . . . 11 |- (y = -uv -> (y e. A <-> -uv e. A))
24		breq2 2613	. . . . . . . . . . 11 |- (y = -uv -> (x <_ y <-> x <_ -uv))
25	23, 24	imbi12d 624	. . . . . . . . . 10 |- (y = -uv -> ((y e. A -> x <_ y) <-> (-uv e. A -> x <_ -uv)))
26	21, 22, 25	ralxfr 2889	. . . . . . . . 9 |- (A.y e. RR (y e. A -> x <_ y) <-> A.v e. RR (-uv e. A -> x <_ -uv))
27		df-ral 1641	. . . . . . . . 9 |- (A.y e. RR (y e. A -> x <_ y) <-> A.y(y e. RR -> (y e. A -> x <_ y)))
28	26, 27	bitr3 175	. . . . . . . 8 |- (A.v e. RR (-uv e. A -> x <_ -uv) <-> A.y(y e. RR -> (y e. A -> x <_ y)))
29	19, 20, 28	3bitr4g 553	. . . . . . 7 |- (A (_ RR -> (A.y e. A x <_ y <-> A.v e. RR (-uv e. A -> x <_ -uv)))
30	29	rexbidv 1656	. . . . . 6 |- (A (_ RR -> (E.x e. RR A.y e. A x <_ y <-> E.x e. RR A.v e. RR (-uv e. A -> x <_ -uv)))
31		renegclt 5409	. . . . . . . 8 |- (u e. RR -> -uu e. RR)
32		infm3lem 6000	. . . . . . . 8 |- (x e. RR -> E.u e. RR x = -uu)
33		breq1 2612	. . . . . . . . . 10 |- (x = -uu -> (x <_ -uv <-> -uu <_ -uv))
34	33	imbi2d 610	. . . . . . . . 9 |- (x = -uu -> ((-uv e. A -> x <_ -uv) <-> (-uv e. A -> -uu <_ -uv)))
35	34	ralbidv 1655	. . . . . . . 8 |- (x = -uu -> (A.v e. RR (-uv e. A -> x <_ -uv) <-> A.v e. RR (-uv e. A -> -uu <_ -uv)))
36	31, 32, 35	rexxfr 2891	. . . . . . 7 |- (E.x e. RR A.v e. RR (-uv e. A -> x <_ -uv) <-> E.u e. RR A.v e. RR (-uv e. A -> -uu <_ -uv))
37		lenegt 5630	. . . . . . . . . . . 12 |- ((v e. RR /\ u e. RR) -> (v <_ u <-> -uu <_ -uv))
38	37	ancoms 436	. . . . . . . . . . 11 |- ((u e. RR /\ v e. RR) -> (v <_ u <-> -uu <_ -uv))
39	38	imbi2d 610	. . . . . . . . . 10 |- ((u e. RR /\ v e. RR) -> ((-uv e. A -> v <_ u) <-> (-uv e. A -> -uu <_ -uv)))
40	39	ralbidva 1651	. . . . . . . . 9 |- (u e. RR -> (A.v e. RR (-uv e. A -> v <_ u) <-> A.v e. RR (-uv e. A -> -uu <_ -uv)))
41		negeq 5331	. . . . . . . . . . . . . . 15 |- (w = v -> -uw = -uv)
42	41	eleq1d 1532	. . . . . . . . . . . . . 14 |- (w = v -> (-uw e. A <-> -uv e. A))
43	42	elrab 1896	. . . . . . . . . . . . 13 |- (v e. {w e. RR | -uw e. A} <-> (v e. RR /\ -uv e. A))
44	43	imbi1i 186	. . . . . . . . . . . 12 |- ((v e. {w e. RR | -uw e. A} -> v <_ u) <-> ((v e. RR /\ -uv e. A) -> v <_ u))
45		impexp 347	. . . . . . . . . . . 12 |- (((v e. RR /\ -uv e. A) -> v <_ u) <-> (v e. RR -> (-uv e. A -> v <_ u)))
46	44, 45	bitr 173	. . . . . . . . . . 11 |- ((v e. {w e. RR | -uw e. A} -> v <_ u) <-> (v e. RR -> (-uv e. A -> v <_ u)))
47	46	albii 996	. . . . . . . . . 10 |- (A.v(v e. {w e. RR | -uw e. A} -> v <_ u) <-> A.v(v e. RR -> (-uv e. A -> v <_ u)))
48		df-ral 1641	. . . . . . . . . 10 |- (A.v e. {w e. RR | -uw e. A}v <_ u <-> A.v(v e. {w e. RR | -uw e. A} -> v <_ u))
49		df-ral 1641	. . . . . . . . . 10 |- (A.v e. RR (-uv e. A -> v <_ u) <-> A.v(v e. RR -> (-uv e. A -> v <_ u)))
50	47, 48, 49	3bitr4r 184	. . . . . . . . 9 |- (A.v e. RR (-uv e. A -> v <_ u) <-> A.v e. {w e. RR | -uw e. A}v <_ u)
51	40, 50	syl5bbr 532	. . . . . . . 8 |- (u e. RR -> (A.v e. {w e. RR | -uw e. A}v <_ u <-> A.v e. RR (-uv e. A -> -uu <_ -uv)))
52	51	rexbiia 1666	. . . . . . 7 |- (E.u e. RR A.v e. {w e. RR | -uw e. A}v <_ u <-> E.u e. RR A.v e. RR (-uv e. A -> -uu <_ -uv))
53	36, 52	bitr4 176	. . . . . 6 |- (E.x e. RR A.v e. RR (-uv e. A -> x <_ -uv) <-> E.u e. RR A.v e. {w e. RR | -uw e. A}v <_ u)
54	30, 53	syl6bb 534	. . . . 5 |- (A (_ RR -> (E.x e. RR A.y e. A x <_ y <-> E.u e. RR A.v e. {w e. RR | -uw e. A}v <_ u))
55	13, 54	anbi12d 626	. . . 4 |- (A (_ RR -> ((A =/= (/) /\ E.x e. RR A.y e. A x <_ y) <-> ({w e. RR | -uw e. A} =/= (/) /\ E.u e. RR A.v e. {w e. RR | -uw e. A}v <_ u)))
56		ssrab2 2121	. . . . 5 |- {w e. RR | -uw e. A} (_ RR
57		sup3 5999	. . . . 5 |- (({w e. RR | -uw e. A} (_ RR /\ {w e. RR | -uw e. A} =/= (/) /\ E.u e. RR A.v e. {w e. RR | -uw e. A}v <_ u) -> E.u e. RR (A.v e. {w e. RR | -uw e. A} -. u < v /\ A.v e. RR (v < u -> E.t e. {w e. RR | -uw e. A}v < t)))
58	56, 57	mp3an1 900	. . . 4 |- (({w e. RR | -uw e. A} =/= (/) /\ E.u e. RR A.v e. {w e. RR | -uw e. A}v <_ u) -> E.u e. RR (A.v e. {w e. RR | -uw e. A} -. u < v /\ A.v e. RR (v < u -> E.t e. {w e. RR | -uw e. A}v < t)))
59	55, 58	syl6bi 214	. . 3 |- (A (_ RR -> ((A =/= (/) /\ E.x e. RR A.y e. A x <_ y) -> E.u e. RR (A.v e. {w e. RR | -uw e. A} -. u < v /\ A.v e. RR (v < u -> E.t e. {w e. RR | -uw e. A}v < t))))
60	15	imbi1d 611	. . . . . . . . 9 |- (A (_ RR -> ((y e. A -> -. y < x) <-> ((y e. RR /\ y e. A) -> -. y < x)))
61		impexp 347	. . . . . . . . 9 |- (((y e. RR /\ y e.