Theorem pre-axsup 5214

Description: A non-empty, bounded-above set of reals has a supremum. Axiom 25 of 25 for real and complex numbers, derived from ZF set theory. Note: The more general version with ordering on extended reals is axsup 5430.

Assertion

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

Distinct variable group:   x,y,z,A

Proof of Theorem pre-axsup

Step	Hyp	Ref	Expression
1		ssel 2034	. . . . . . . . . . . . . . . 16 |- (A (_ RR -> (y e. A -> y e. RR))
2	1	imim1d 28	. . . . . . . . . . . . . . 15 |- (A (_ RR -> ((y e. RR -> (y e. A -> -. x <R y)) -> (y e. A -> (y e. A -> -. x <R y))))
3		pm2.43 63	. . . . . . . . . . . . . . 15 |- ((y e. A -> (y e. A -> -. x <R y)) -> (y e. A -> -. x <R y))
4	2, 3	syl6 22	. . . . . . . . . . . . . 14 |- (A (_ RR -> ((y e. RR -> (y e. A -> -. x <R y)) -> (y e. A -> -. x <R y)))
5	4	19.20dv 1271	. . . . . . . . . . . . 13 |- (A (_ RR -> (A.y(y e. RR -> (y e. A -> -. x <R y)) -> A.y(y e. A -> -. x <R y)))
6		df-ral 1625	. . . . . . . . . . . . 13 |- (A.y e. A -. x <R y <-> A.y(y e. A -> -. x <R y))
7	5, 6	syl6ibr 213	. . . . . . . . . . . 12 |- (A (_ RR -> (A.y(y e. RR -> (y e. A -> -. x <R y)) -> A.y e. A -. x <R y))
8		pm3.27 323	. . . . . . . . . . . . . . . . . . 19 |- ((z e. RR /\ (z e. A /\ y <R z)) -> (z e. A /\ y <R z))
9	8	19.22i 1016	. . . . . . . . . . . . . . . . . 18 |- (E.z(z e. RR /\ (z e. A /\ y <R z)) -> E.z(z e. A /\ y <R z))
10		df-rex 1626	. . . . . . . . . . . . . . . . . 18 |- (E.z e. A y <R z <-> E.z(z e. A /\ y <R z))
11	9, 10	sylibr 200	. . . . . . . . . . . . . . . . 17 |- (E.z(z e. RR /\ (z e. A /\ y <R z)) -> E.z e. A y <R z)
12	11	imim2i 17	. . . . . . . . . . . . . . . 16 |- ((y <R x -> E.z(z e. RR /\ (z e. A /\ y <R z))) -> (y <R x -> E.z e. A y <R z))
13	12	imim2i 17	. . . . . . . . . . . . . . 15 |- ((y e. RR -> (y <R x -> E.z(z e. RR /\ (z e. A /\ y <R z)))) -> (y e. RR -> (y <R x -> E.z e. A y <R z)))
14	13	19.20i 968	. . . . . . . . . . . . . 14 |- (A.y(y e. RR -> (y <R x -> E.z(z e. RR /\ (z e. A /\ y <R z)))) -> A.y(y e. RR -> (y <R x -> E.z e. A y <R z)))
15		df-ral 1625	. . . . . . . . . . . . . 14 |- (A.y e. RR (y <R x -> E.z e. A y <R z) <-> A.y(y e. RR -> (y <R x -> E.z e. A y <R z)))
16	14, 15	sylibr 200	. . . . . . . . . . . . 13 |- (A.y(y e. RR -> (y <R x -> E.z(z e. RR /\ (z e. A /\ y <R z)))) -> A.y e. RR (y <R x -> E.z e. A y <R z))
17	16	a1i 8	. . . . . . . . . . . 12 |- (A (_ RR -> (A.y(y e. RR -> (y <R x -> E.z(z e. RR /\ (z e. A /\ y <R z)))) -> A.y e. RR (y <R x -> E.z e. A y <R z)))
18	7, 17	anim12d 556	. . . . . . . . . . 11 |- (A (_ RR -> ((A.y(y e. RR -> (y e. A -> -. x <R y)) /\ A.y(y e. RR -> (y <R x -> E.z(z e. RR /\ (z e. A /\ y <R z))))) -> (A.y e. A -. x <R y /\ A.y e. RR (y <R x -> E.z e. A y <R z))))
19		jcab 596	. . . . . . . . . . . . 13 |- ((y e. RR -> ((y e. A -> -. x <R y) /\ (y <R x -> E.z(z e. RR /\ (z e. A /\ y <R z))))) <-> ((y e. RR -> (y e. A -> -. x <R y)) /\ (y e. RR -> (y <R x -> E.z(z e. RR /\ (z e. A /\ y <R z))))))
20	19	albii 975	. . . . . . . . . . . 12 |- (A.y(y e. RR -> ((y e. A -> -. x <R y) /\ (y <R x -> E.z(z e. RR /\ (z e. A /\ y <R z))))) <-> A.y((y e. RR -> (y e. A -> -. x <R y)) /\ (y e. RR -> (y <R x -> E.z(z e. RR /\ (z e. A /\ y <R z))))))
21		19.26 1043	. . . . . . . . . . . 12 |- (A.y((y e. RR -> (y e. A -> -. x <R y)) /\ (y e. RR -> (y <R x -> E.z(z e. RR /\ (z e. A /\ y <R z))))) <-> (A.y(y e. RR -> (y e. A -> -. x <R y)) /\ A.y(y e. RR -> (y <R x -> E.z(z e. RR /\ (z e. A /\ y <R z))))))
22	20, 21	bitr 173	. . . . . . . . . . 11 |- (A.y(y e. RR -> ((y e. A -> -. x <R y) /\ (y <R x -> E.z(z e. RR /\ (z e. A /\ y <R z))))) <-> (A.y(y e. RR -> (y e. A -> -. x <R y)) /\ A.y(y e. RR -> (y <R x -> E.z(z e. RR /\ (z e. A /\ y <R z))))))
23	18, 22	syl5ib 206	. . . . . . . . . 10 |- (A (_ RR -> (A.y(y e. RR -> ((y e. A -> -. x <R y) /\ (y <R x -> E.z(z e. RR /\ (z e. A /\ y <R z))))) -> (A.y e. A -. x <R y /\ A.y e. RR (y <R x -> E.z e. A y <R z))))
24	23	anim2d 559	. . . . . . . . 9 |- (A (_ RR -> ((x e. RR /\ A.y(y e. RR -> ((y e. A -> -. x <R y) /\ (y <R x -> E.z(z e. RR /\ (z e. A /\ y <R z)))))) -> (x e. RR /\ (A.y e. A -. x <R y /\ A.y e. RR (y <R x -> E.z e. A y <R z)))))
25	24	19.22dv 1272	. . . . . . . 8 |- (A (_ RR -> (E.x(x e. RR /\ A.y(y e. RR -> ((y e. A -> -. x <R y) /\ (y <R x -> E.z(z e. RR /\ (z e. A /\ y <R z)))))) -> E.x(x e. RR /\ (A.y e. A -. x <R y /\ A.y e. RR (y <R x -> E.z e. A y <R z)))))
26		df-rex 1626	. . . . . . . 8 |- (E.x e. RR (A.y e. A -. x <R y /\ A.y e. RR (y <R x -> E.z e. A y <R z)) <-> E.x(x e. RR /\ (A.y e. A -. x <R y /\ A.y e. RR (y <R x -> E.z e. A y <R z))))
27	25, 26	syl6ibr 213	. . . . . . 7 |- (A (_ RR -> (E.x(x e. RR /\ A.y(y e. RR -> ((y e. A -> -. x <R y) /\ (y <R x -> E.z(z e. RR /\ (z e. A /\ y <R z)))))) -> E.x e. RR (A.y e. A -. x <R y /\ A.y e. RR (y <R x -> E.z e. A y <R z))))
28	27	adantr 389	. . . . . 6 |- ((A (_ RR /\ -. A = (/)) -> (E.x(x e. RR /\ A.y(y e. RR -> ((y e. A -> -. x <R y) /\ (y <R x -> E.z(z e. RR /\ (z e. A /\ y <R z)))))) -> E.x e. RR (A.y e. A -. x <R y /\ A.y e. RR (y <R x -> E.z e. A y <R z))))
29		opeq1 2456	. . . . . . . . 9 |- (v = w -> <.v, 0R>. = <.w, 0R>.)
30	29	eleq1d 1516	. . . . . . . 8 |- (v = w -> (<.v, 0R>. e. A <-> <.w, 0R>. e. A))
31	30	cbvabv 1881	. . . . . . 7 |- {v | <.v, 0R>. e. A} = {w | <.w, 0R>. e. A}
32	31	supre 5183	. . . . . 6 |- (((A (_ RR /\ -. A = (/)) /\ E.x(x e. RR /\ A.y(y e. RR -> (y e. A -> y <R x)))) -> E.x(x e. RR /\ A.y(y e. RR -> ((y e. A -> -. x <R y) /\ (y <R x -> E.z(z e. RR /\ (z e. A /\ y <R z)))))))
33	28, 32	syl5 21	. . . . 5 |- ((A (_ RR /\ -. A = (/)) -> (((A (_ RR /\ -. A = (/)) /\ E.x(x e. RR /\ A.y(y e. RR -> (y e. A -> y <R x)))) -> E.x e. RR (A.y e. A -. x <R y /\ A.y e. RR (y <R x -> E.z e. A y <R z))))
34	33	anabsi5 494	. . . 4 |- (((A (_ RR /\ -. A = (/)) /\ E.x(x e. RR /\ A.y(y e. RR -> (y e. A -> y <R x)))) -> E.x e. RR (A.y e. A -. x <R y /\ A.y e. RR (y <R x -> E.z e. A y <R z)))
35		df-rex 1626	. . . . 5 |- (E.x e. RR A.y e. A y <R x <-> E.x(x e. RR /\ A.y e. A y <R x))
36		df-ral 1625	. .