Theorem axsup 4088

Description: A non-empty, bounded-above set of reals has a supremum. One of the 28 axioms for real and complex numbers, derived from ZF set theory.

Assertion

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

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

Proof of Theorem axsup

Step	Hyp	Ref	Expression
1		ssel 1502	. . . . . . . . . . . . . . . 16 |- (A (_ RR -> (y e. A -> y e. RR))
2	1	syl4d 28	. . . . . . . . . . . . . . 15 |- (A (_ RR -> ((y e. RR -> (y e. A -> -. x < y)) -> (y e. A -> (y e. A -> -. x < y))))
3		pm2.43 57	. . . . . . . . . . . . . . 15 |- ((y e. A -> (y e. A -> -. x < y)) -> (y e. A -> -. x < y))
4	2, 3	syl6 23	. . . . . . . . . . . . . 14 |- (A (_ RR -> ((y e. RR -> (y e. A -> -. x < y)) -> (y e. A -> -. x < y)))
5	4	19.20dv 946	. . . . . . . . . . . . 13 |- (A (_ RR -> (A.y(y e. RR -> (y e. A -> -. x < y)) -> A.y(y e. A -> -. x < y)))
6		df-ral 1205	. . . . . . . . . . . . 13 |- (A.y e. A -. x < y <-> A.y(y e. A -> -. x < y))
7	5, 6	syl6ibr 186	. . . . . . . . . . . 12 |- (A (_ RR -> (A.y(y e. RR -> (y e. A -> -. x < y)) -> A.y e. A -. x < y))
8		pm3.27 260	. . . . . . . . . . . . . . . . . . 19 |- ((z e. RR /\ (z e. A /\ y < z)) -> (z e. A /\ y < z))
9	8	19.22i 723	. . . . . . . . . . . . . . . . . 18 |- (E.z(z e. RR /\ (z e. A /\ y < z)) -> E.z(z e. A /\ y < z))
10		df-rex 1206	. . . . . . . . . . . . . . . . . 18 |- (E.z e. A y < z <-> E.z(z e. A /\ y < z))
11	9, 10	sylibr 175	. . . . . . . . . . . . . . . . 17 |- (E.z(z e. RR /\ (z e. A /\ y < z)) -> E.z e. A y < z)
12	11	syl3 18	. . . . . . . . . . . . . . . 16 |- ((y < x -> E.z(z e. RR /\ (z e. A /\ y < z))) -> (y < x -> E.z e. A y < z))
13	12	syl3 18	. . . . . . . . . . . . . . 15 |- ((y e. RR -> (y < x -> E.z(z e. RR /\ (z e. A /\ y < z)))) -> (y e. RR -> (y < x -> E.z e. A y < z)))
14	13	19.20i 691	. . . . . . . . . . . . . 14 |- (A.y(y e. RR -> (y < x -> E.z(z e. RR /\ (z e. A /\ y < z)))) -> A.y(y e. RR -> (y < x -> E.z e. A y < z)))
15		df-ral 1205	. . . . . . . . . . . . . 14 |- (A.y e. RR (y < x -> E.z e. A y < z) <-> A.y(y e. RR -> (y < x -> E.z e. A y < z)))
16	14, 15	sylibr 175	. . . . . . . . . . . . 13 |- (A.y(y e. RR -> (y < x -> E.z(z e. RR /\ (z e. A /\ y < z)))) -> A.y e. RR (y < x -> E.z e. A y < z))
17	16	a1i 7	. . . . . . . . . . . 12 |- (A (_ RR -> (A.y(y e. RR -> (y < x -> E.z(z e. RR /\ (z e. A /\ y < z)))) -> A.y e. RR (y < x -> E.z e. A y < z)))
18	7, 17	anim12d 431	. . . . . . . . . . 11 |- (A (_ RR -> ((A.y(y e. RR -> (y e. A -> -. x < y)) /\ A.y(y e. RR -> (y < x -> E.z(z e. RR /\ (z e. A /\ y < z))))) -> (A.y e. A -. x < y /\ A.y e. RR (y < x -> E.z e. A y < z))))
19		jcab 454	. . . . . . . . . . . . 13 |- ((y e. RR -> ((y e. A -> -. x < y) /\ (y < x -> E.z(z e. RR /\ (z e. A /\ y < z))))) <-> ((y e. RR -> (y e. A -> -. x < y)) /\ (y e. RR -> (y < x -> E.z(z e. RR /\ (z e. A /\ y < z))))))
20	19	bial 695	. . . . . . . . . . . 12 |- (A.y(y e. RR -> ((y e. A -> -. x < y) /\ (y < x -> E.z(z e. RR /\ (z e. A /\ y < z))))) <-> A.y((y e. RR -> (y e. A -> -. x < y)) /\ (y e. RR -> (y < x -> E.z(z e. RR /\ (z e. A /\ y < z))))))
21		19.26 749	. . . . . . . . . . . 12 |- (A.y((y e. RR -> (y e. A -> -. x < y)) /\ (y e. RR -> (y < x -> E.z(z e. RR /\ (z e. A /\ y < z))))) <-> (A.y(y e. RR -> (y e. A -> -. x < y)) /\ A.y(y e. RR -> (y < x -> E.z(z e. RR /\ (z e. A /\ y < z))))))
22	20, 21	bitr 151	. . . . . . . . . . 11 |- (A.y(y e. RR -> ((y e. A -> -. x < y) /\ (y < x -> E.z(z e. RR /\ (z e. A /\ y < z))))) <-> (A.y(y e. RR -> (y e. A -> -. x < y)) /\ A.y(y e. RR -> (y < x -> E.z(z e. RR /\ (z e. A /\ y < z))))))
23	18, 22	syl5ib 181	. . . . . . . . . 10 |- (A (_ RR -> (A.y(y e. RR -> ((y e. A -> -. x < y) /\ (y < x -> E.z(z e. RR /\ (z e. A /\ y < z))))) -> (A.y e. A -. x < y /\ A.y e. RR (y < x -> E.z e. A y < z))))
24	23	anim2d 433	. . . . . . . . 9 |- (A (_ RR -> ((x e. RR /\ A.y(y e. RR -> ((y e. A -> -. x < y) /\ (y < x -> E.z(z e. RR /\ (z e. A /\ y < z)))))) -> (x e. RR /\ (A.y e. A -. x < y /\ A.y e. RR (y < x -> E.z e. A y < z)))))
25	24	19.22dv 947	. . . . . . . 8 |- (A (_ RR -> (E.x(x e. RR /\ A.y(y e. RR -> ((y e. A -> -. x < y) /\ (y < x -> E.z(z e. RR /\ (z e. A /\ y < z)))))) -> E.x(x e. RR /\ (A.y e. A -. x < y /\ A.y e. RR (y < x -> E.z e. A y < z)))))
26		df-rex 1206	. . . . . . . 8 |- (E.x e. RR (A.y e. A -. x < y /\ A.y e. RR (y < x -> E.z e. A y < z)) <-> E.x(x e. RR /\ (A.y e. A -. x < y /\ A.y e. RR (y < x -> E.z e. A y < z))))
27	25, 26	syl6ibr 186	. . . . . . 7 |- (A (_ RR -> (E.x(x e. RR /\ A.y(y e. RR -> ((y e. A -> -. x < y) /\ (y < x -> E.z(z e. RR /\ (z e. A /\ y < z)))))) -> E.x e. RR (A.y e. A -. x < y /\ A.y e. RR (y < x -> E.z e. A y < z))))
28	27	adantr 306	. . . . . 6 |- ((A (_ RR /\ -. A = (/)) -> (E.x(x e. RR /\ A.y(y e. RR -> ((y e. A -> -. x < y) /\ (y < x -> E.z(z e. RR /\ (z e. A /\ y < z)))))) -> E.x e. RR (A.y e. A -. x < y /\ A.y e. RR (y < x -> E.z e. A y < z))))
29		opeq1 1876	. . . . . . . . 9 |- (v = w -> <.v, 0R>. = <.w, 0R>.)
30	29	eleq1d 1155	. . . . . . . 8 |- (v = w -> (<.v, 0R>. e. A <-> <.w, 0R>. e. A))
31	30	cbvabv 1424	. . . . . . 7 |- {v | <.v, 0R>. e. A} = {w | <.w, 0R>. e. A}
32	31	supre 4054	. . . . . 6 |- (((A (_ RR /\ -. A = (/)) /\ E.x(x e. RR /\ A.y(y e. RR -> (y e. A -> y < x)))) -> E.x(x e. RR /\ A.y(y e. RR -> ((y e. A -> -. x < y) /\ (y < x -> E.z(z e. RR /\ (z e. A /\ y < z)))))))
33	28, 32	syl5 22	. . . . 5 |- ((A (_ RR /\ -. A = (/)) -> (((A (_ RR /\ -. A = (/)) /\ E.x(x e. RR /\ A.y(y e. RR -> (y e. A -> y < x)))) -> E.x e. RR (A.y e. A -. x < y /\ A.y e. RR (y < x -> E.z e. A y < z))))
34	33	anabsi5 377	. . . 4 |- (((A (_ RR /\ -. A = (/)) /\ E.x(x e. RR /\ A.y(y e. RR -> (y e. A -> y < x)))) -> E.x e. RR (A.y e. A -. x < y /\ A.y e. RR (y < x -> E.z e. A y < z)))
35		df-rex 1206	. . . . 5 |- (E.x e. RR A.y e. A y < x <-> E.x(x e. RR /\ A.y e. A y < x))
36		df-ral 1205	. . . . . . . 8 |- (A.y e. A y < x <-> A.y(y e. A -> y < x))
37		ax-1 3	. . . . . . . . 9 |- ((y e. A -> y < x) -> (y e. RR -> (y e. A -> y < x)))
38	37	19.20i 691	. . . . . . . 8 |- (A.y(y e. A -> y < x