Theorem lbinfm 6005

Description: If a set of reals contains a lower bound, the lower bound is its infimum.

Assertion

Ref	Expression
lbinfm	|- ((S (_ RR /\ E.x e. S A.y e. S x <_ y) -> sup(S, RR, `' < ) = U.{x e. S | A.y e. S x <_ y})

Distinct variable group:   x,y,S

Proof of Theorem lbinfm

Step	Hyp	Ref	Expression
1		lble 6004	. . . . . . . 8 |- ((S (_ RR /\ E.x e. S A.y e. S x <_ y /\ z e. S) -> U.{x e. S | A.y e. S x <_ y} <_ z)
2	1	3expa 832	. . . . . . 7 |- (((S (_ RR /\ E.x e. S A.y e. S x <_ y) /\ z e. S) -> U.{x e. S | A.y e. S x <_ y} <_ z)
3		lenltt 5493	. . . . . . . 8 |- ((U.{x e. S | A.y e. S x <_ y} e. RR /\ z e. RR) -> (U.{x e. S | A.y e. S x <_ y} <_ z <-> -. z < U.{x e. S | A.y e. S x <_ y}))
4		lbcl 6003	. . . . . . . . . 10 |- ((S (_ RR /\ E.x e. S A.y e. S x <_ y) -> U.{x e. S | A.y e. S x <_ y} e. S)
5		ssel2 2061	. . . . . . . . . 10 |- ((S (_ RR /\ U.{x e. S | A.y e. S x <_ y} e. S) -> U.{x e. S | A.y e. S x <_ y} e. RR)
6	4, 5	syldan 467	. . . . . . . . 9 |- ((S (_ RR /\ E.x e. S A.y e. S x <_ y) -> U.{x e. S | A.y e. S x <_ y} e. RR)
7	6	adantr 389	. . . . . . . 8 |- (((S (_ RR /\ E.x e. S A.y e. S x <_ y) /\ z e. S) -> U.{x e. S | A.y e. S x <_ y} e. RR)
8		ssel2 2061	. . . . . . . . 9 |- ((S (_ RR /\ z e. S) -> z e. RR)
9	8	adantlr 393	. . . . . . . 8 |- (((S (_ RR /\ E.x e. S A.y e. S x <_ y) /\ z e. S) -> z e. RR)
10	3, 7, 9	sylanc 471	. . . . . . 7 |- (((S (_ RR /\ E.x e. S A.y e. S x <_ y) /\ z e. S) -> (U.{x e. S | A.y e. S x <_ y} <_ z <-> -. z < U.{x e. S | A.y e. S x <_ y}))
11	2, 10	mpbid 195	. . . . . 6 |- (((S (_ RR /\ E.x e. S A.y e. S x <_ y) /\ z e. S) -> -. z < U.{x e. S | A.y e. S x <_ y})
12		reex 5295	. . . . . . . . . . 11 |- RR e. V
13	12	ssex 2715	. . . . . . . . . 10 |- (S (_ RR -> S e. V)
14		rabexg 2720	. . . . . . . . . 10 |- (S e. V -> {x e. S | A.y e. S x <_ y} e. V)
15	13, 14	syl 10	. . . . . . . . 9 |- (S (_ RR -> {x e. S | A.y e. S x <_ y} e. V)
16		uniexg 2867	. . . . . . . . 9 |- ({x e. S | A.y e. S x <_ y} e. V -> U.{x e. S | A.y e. S x <_ y} e. V)
17		visset 1810	. . . . . . . . . 10 |- z e. V
18		brcnvg 3293	. . . . . . . . . 10 |- ((U.{x e. S | A.y e. S x <_ y} e. V /\ z e. V) -> (U.{x e. S | A.y e. S x <_ y}`' < z <-> z < U.{x e. S | A.y e. S x <_ y}))
19	17, 18	mpan2 695	. . . . . . . . 9 |- (U.{x e. S | A.y e. S x <_ y} e. V -> (U.{x e. S | A.y e. S x <_ y}`' < z <-> z < U.{x e. S | A.y e. S x <_ y}))
20	15, 16, 19	3syl 20	. . . . . . . 8 |- (S (_ RR -> (U.{x e. S | A.y e. S x <_ y}`' < z <-> z < U.{x e. S | A.y e. S x <_ y}))
21	20	negbid 610	. . . . . . 7 |- (S (_ RR -> (-. U.{x e. S | A.y e. S x <_ y}`' < z <-> -. z < U.{x e. S | A.y e. S x <_ y}))
22	21	ad2antrr 404	. . . . . 6 |- (((S (_ RR /\ E.x e. S A.y e. S x <_ y) /\ z e. S) -> (-. U.{x e. S | A.y e. S x <_ y}`' < z <-> -. z < U.{x e. S | A.y e. S x <_ y}))
23	11, 22	mpbird 196	. . . . 5 |- (((S (_ RR /\ E.x e. S A.y e. S x <_ y) /\ z e. S) -> -. U.{x e. S | A.y e. S x <_ y}`' < z)
24	23	r19.21aiva 1712	. . . 4 |- ((S (_ RR /\ E.x e. S A.y e. S x <_ y) -> A.z e. S -. U.{x e. S | A.y e. S x <_ y}`' < z)
25	4	a1d 12	. . . . . . . 8 |- ((S (_ RR /\ E.x e. S A.y e. S x <_ y) -> (z`' < U.{x e. S | A.y e. S x <_ y} -> U.{x e. S | A.y e. S x <_ y} e. S))
26	25	ancrd 299	. . . . . . 7 |- ((S (_ RR /\ E.x e. S A.y e. S x <_ y) -> (z`' < U.{x e. S | A.y e. S x <_ y} -> (U.{x e. S | A.y e. S x <_ y} e. S /\ z`' < U.{x e. S | A.y e. S x <_ y})))
27		breq2 2619	. . . . . . . 8 |- (w = U.{x e. S | A.y e. S x <_ y} -> (z`' < w <-> z`' < U.{x e. S | A.y e. S x <_ y}))
28	27	rcla4ev 1874	. . . . . . 7 |- ((U.{x e. S | A.y e. S x <_ y} e. S /\ z`' < U.{x e. S | A.y e. S x <_ y}) -> E.w e. S z`' < w)
29	26, 28	syl6 22	. . . . . 6 |- ((S (_ RR /\ E.x e. S A.y e. S x <_ y) -> (z`' < U.{x e. S | A.y e. S x <_ y} -> E.w e. S z`' < w))
30	29	a1d 12	. . . . 5 |- ((S (_ RR /\ E.x e. S A.y e. S x <_ y) -> (z e. RR -> (z`' < U.{x e. S | A.y e. S x <_ y} -> E.w e. S z`' < w)))
31	30	r19.21aiv 1711	. . . 4 |- ((S (_ RR /\ E.x e. S A.y e. S x <_ y) -> A.z e. RR (z`' < U.{x e. S | A.y e. S x <_ y} -> E.w e. S z`' < w))
32	24, 31	jca 288	. . 3 |- ((S (_ RR /\ E.x e. S A.y e. S x <_ y) -> (A.z e. S -. U.{x e. S | A.y e. S x <_ y}`' < z /\ A.z e. RR (z`' < U.{x e. S | A.y e. S x <_ y} -> E.w e. S z`' < w)))
33		breq1 2618	. . . . . . . 8 |- (v = U.{x e. S | A.y e. S x <_ y} -> (v`' < z <-> U.{x e. S | A.y e. S x <_ y}`' < z))
34	33	negbid 610	. . . . . . 7 |- (v = U.{x e. S | A.y e. S x <_ y} -> (-. v`' < z <-> -. U.{x e. S | A.y e. S x <_ y}`' < z))
35	34	ralbidv 1661	. . . . . 6 |- (v = U.{x e. S | A.y e. S x <_ y} -> (A.z e. S -. v`' < z <-> A.z e. S -. U.{x e. S | A.y e. S x <_ y}`' < z))
36		breq2 2619	. . . . . . . 8 |- (v = U.{x e. S | A.y e. S x <_ y} -> (z`' < v <-> z`' < U.{x e. S | A.y e. S x <_ y}))
37	36	imbi1d 612	. . . . . . 7 |- (v = U.{x e. S | A.y e. S x <_ y} -> ((z`' < v -> E.w e. S z`' < w) <-> (z`' < U.{x e. S | A.y e. S x <_ y} -> E.w e. S z`' < w)))
38	37	ralbidv 1661	. . . . . 6 |- (v = U.{x e. S | A.y e. S x <_ y} -> (A.z e. RR (z`' < v -> E.w e. S z`' < w) <-> A.z e. RR (z`' < U.{x e. S | A.y e. S x <_ y} -> E.w e. S z`' < w)))
39	35, 38	anbi12d 627	. . . . 5 |- (v = U.{x e. S | A.y e. S x <_ y} -> ((A.z e. S -. v`' < z /\ A.z e. RR (z`' < v -> E.w e. S z`' < w)) <-> (A.z e. S -. U.{x e. S | A.y e. S x <_ y}`' < z /\ A.z e. RR (z`' < U.{x e. S | A.y e. S x <_ y} -> E.w e. S z`' < w))))
40	39	reuuni2 2880	. . . 4 |- ((U.{x e. S | A.y e. S x <_ y} e. RR /\ E!v e. RR (A.z e. S -. v`' < z /\ A.z e. RR (z`' < v -> E.w e. S z`' < w))) -> ((A.z e. S -. U.{x e. S | A.y e. S x <_ y}`' < z /\ A.z e. RR (z`' < U.{x e. S | A.y e. S x <_ y} -> E.w e. S z`' < w)) <-> U.{v e. RR | (A.z e. S -. v`' < z /\ A.z e. RR (z`' < v -> E.w e. S z`' < w))} = U.{x e. S | A.y e. S x <_ y}))
41		ssel 2060	. . . . . 6 |- (S (_ RR -> (U.{x e. S | A.y e. S x <_ y} e. S -> U.{x e.