Theorem suplem1pr 3955

Description: The union of a non-empty, bounded set of positive reals is a positive real. Part of Proposition 9-3.3 of [Gleason] p. 122.

Assertion

Ref	Expression
suplem1pr	|- (((A (_ P. /\ -. A = (/)) /\ E.x(x e. P. /\ A.y(y e. P. -> (y e. A -> y <P x)))) -> U.A e. P.)

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

Proof of Theorem suplem1pr

Step	Hyp	Ref	Expression
1		ssel 1502	. . . . . . . . . . 11 |- (A (_ P. -> (z e. A -> z e. P.))
2		prn0 3887	. . . . . . . . . . . 12 |- (z e. P. -> -. z = (/))
3		n0 1714	. . . . . . . . . . . 12 |- (-. z = (/) <-> E.x x e. z)
4	2, 3	sylib 173	. . . . . . . . . . 11 |- (z e. P. -> E.x x e. z)
5	1, 4	syl6 23	. . . . . . . . . 10 |- (A (_ P. -> (z e. A -> E.x x e. z))
6	5	ancrd 247	. . . . . . . . 9 |- (A (_ P. -> (z e. A -> (E.x x e. z /\ z e. A)))
7		19.41v 963	. . . . . . . . 9 |- (E.x(x e. z /\ z e. A) <-> (E.x x e. z /\ z e. A))
8	6, 7	syl6ibr 186	. . . . . . . 8 |- (A (_ P. -> (z e. A -> E.x(x e. z /\ z e. A)))
9	8	19.22dv 947	. . . . . . 7 |- (A (_ P. -> (E.z z e. A -> E.zE.x(x e. z /\ z e. A)))
10		n0 1714	. . . . . . 7 |- (-. A = (/) <-> E.z z e. A)
11		0pss 1730	. . . . . . . . 9 |- ((/) (. U.A <-> -. U.A = (/))
12		n0 1714	. . . . . . . . 9 |- (-. U.A = (/) <-> E.x x e. U.A)
13	11, 12	bitr 151	. . . . . . . 8 |- ((/) (. U.A <-> E.x x e. U.A)
14		eluni 1922	. . . . . . . . 9 |- (x e. U.A <-> E.z(x e. z /\ z e. A))
15	14	biex 733	. . . . . . . 8 |- (E.x x e. U.A <-> E.xE.z(x e. z /\ z e. A))
16		excom 728	. . . . . . . 8 |- (E.xE.z(x e. z /\ z e. A) <-> E.zE.x(x e. z /\ z e. A))
17	13, 15, 16	3bitr 155	. . . . . . 7 |- ((/) (. U.A <-> E.zE.x(x e. z /\ z e. A))
18	9, 10, 17	3imtr4g 426	. . . . . 6 |- (A (_ P. -> (-. A = (/) -> (/) (. U.A))
19		prpssnq 3888	. . . . . . . . . 10 |- (x e. P. -> x (. Q.)
20	19	a1i 7	. . . . . . . . 9 |- (A (_ P. -> (x e. P. -> x (. Q.))
21		ssel 1502	. . . . . . . . . . . . 13 |- (A (_ P. -> (y e. A -> y e. P.))
22	21	syl4d 28	. . . . . . . . . . . 12 |- (A (_ P. -> ((y e. P. -> (y e. A -> y <P x)) -> (y e. A -> (y e. A -> y <P x))))
23		pm2.43 57	. . . . . . . . . . . . 13 |- ((y e. A -> (y e. A -> y <P x)) -> (y e. A -> y <P x))
24		visset 1350	. . . . . . . . . . . . . . 15 |- x e. V
25		ltrelpr 3895	. . . . . . . . . . . . . . 15 |- <P (_ (P. X. P.)
26	24, 25	brel 2459	. . . . . . . . . . . . . 14 |- (y <P x -> (y e. P. /\ x e. P.))
27		ltprord 3928	. . . . . . . . . . . . . . 15 |- ((y e. P. /\ x e. P.) -> (y <P x <-> y (. x))
28		pssss 1567	. . . . . . . . . . . . . . 15 |- (y (. x -> y (_ x)
29	27, 28	syl6bi 187	. . . . . . . . . . . . . 14 |- ((y e. P. /\ x e. P.) -> (y <P x -> y (_ x))
30	26, 29	mpcom 49	. . . . . . . . . . . . 13 |- (y <P x -> y (_ x)
31	23, 30	syl6 23	. . . . . . . . . . . 12 |- ((y e. A -> (y e. A -> y <P x)) -> (y e. A -> y (_ x))
32	22, 31	syl6 23	. . . . . . . . . . 11 |- (A (_ P. -> ((y e. P. -> (y e. A -> y <P x)) -> (y e. A -> y (_ x)))
33	32	19.20dv 946	. . . . . . . . . 10 |- (A (_ P. -> (A.y(y e. P. -> (y e. A -> y <P x)) -> A.y(y e. A -> y (_ x)))
34		unissb 1941	. . . . . . . . . . 11 |- (U.A (_ x <-> A.y e. A y (_ x)
35		df-ral 1205	. . . . . . . . . . 11 |- (A.y e. A y (_ x <-> A.y(y e. A -> y (_ x))
36	34, 35	bitr 151	. . . . . . . . . 10 |- (U.A (_ x <-> A.y(y e. A -> y (_ x))
37	33, 36	syl6ibr 186	. . . . . . . . 9 |- (A (_ P. -> (A.y(y e. P. -> (y e. A -> y <P x)) -> U.A (_ x))
38	20, 37	anim12d 431	. . . . . . . 8 |- (A (_ P. -> ((x e. P. /\ A.y(y e. P. -> (y e. A -> y <P x))) -> (x (. Q. /\ U.A (_ x)))
39		sspsstr 1575	. . . . . . . . 9 |- ((U.A (_ x /\ x (. Q.) -> U.A (. Q.)
40	39	ancoms 334	. . . . . . . 8 |- ((x (. Q. /\ U.A (_ x) -> U.A (. Q.)
41	38, 40	syl6 23	. . . . . . 7 |- (A (_ P. -> ((x e. P. /\ A.y(y e. P. -> (y e. A -> y <P x))) -> U.A (. Q.))
42	41	19.23adv 954	. . . . . 6 |- (A (_ P. -> (E.x(x e. P. /\ A.y(y e. P. -> (y e. A -> y <P x))) -> U.A (. Q.))
43	18, 42	anim12d 431	. . . . 5 |- (A (_ P. -> ((-. A = (/) /\ E.x(x e. P. /\ A.y(y e. P. -> (y e. A -> y <P x)))) -> ((/) (. U.A /\ U.A (. Q.)))
44		prcdpq 3891	. . . . . . . . . . . . . . . . . . . . 21 |- ((z e. P. /\ x e. z) -> (y <Q x -> y e. z))
45	44	exp 291	. . . . . . . . . . . . . . . . . . . 20 |- (z e. P. -> (x e. z -> (y <Q x -> y e. z)))
46	1, 45	syl6 23	. . . . . . . . . . . . . . . . . . 19 |- (A (_ P. -> (z e. A -> (x e. z -> (y <Q x -> y e. z))))
47	46	com24 37	. . . . . . . . . . . . . . . . . 18 |- (A (_ P. -> (y <Q x -> (x e. z -> (z e. A -> y e. z))))
48	47	imp31 280	. . . . . . . . . . . . . . . . 17 |- (((A (_ P. /\ y <Q x) /\ x e. z) -> (z e. A -> y e. z))
49	48	ancrd 247	. . . . . . . . . . . . . . . 16 |- (((A (_ P. /\ y <Q x) /\ x e. z) -> (z e. A -> (y e. z /\ z e. A)))
50		elunii 1924	. . . . . . . . . . . . . . . 16 |- ((y e. z /\ z e. A) -> y e. U.A)
51	49, 50	syl6 23	. . . . . . . . . . . . . . 15 |- (((A (_ P. /\ y <Q x) /\ x e. z) -> (z e. A -> y e. U.A))
52	51	exp 291	. . . . . . . . . . . . . 14 |- ((A (_ P. /\ y <Q x) -> (x e. z -> (z e. A -> y e. U.A)))
53	52	imp3a 279	. . . . . . . . . . . . 13 |- ((A (_ P. /\ y <Q x) -> ((x e. z /\ z e. A) -> y e. U.A))
54	53	19.23adv 954	. . . . . . . . . . . 12 |- ((A (_ P. /\ y <Q x) -> (E.z(x e. z /\ z e. A) -> y e. U.A))
55	54, 14	syl5ib 181	. . . . . . . . . . 11 |- ((A (_ P. /\ y <Q x) -> (x e. U.A -> y e. U.A))
56	55	exp 291	. . . . . . . . . 10 |- (A (_ P. -> (y <Q x -> (x e. U.A -> y e. U.A)))
57	56	com23 32	. . . . . . . . 9 |- (A (_ P. -> (x e. U.A -> (y <Q x -> y e. U.A)))
58	57	19.21adv 945	. . . . . . . 8 |- (A (_ P. -> (x e. U.A -> A.y(y <Q x -> y e. U.A)))
59		prnmax 3893	. . . . . . . . . . . . . . . . . 18 |- ((z e. P. /\ x e. z) -> E.y(y e. z /\ x <Q y))
60	59	exp 291	. . . . . . . . . . . . . . . . 17 |- (z e. P. -> (x e. z -> E.y(y e. z /\ x <Q y)))
61	1, 60	syl6 23	. . . . . . . . . . . . . . . 16 |- (A (_ P. -> (z e. A -> (x e. z -> E.y(y e. z /\ x <Q y))))
62	61	com23 32	. . . . . . . . . . . . . . 15 |- (A (_ P. -> (x e. z -> (z e. A -> E.y(y e. z /\ x <Q y))))
63	62	imp 277	. . . . . . . . . . . . . 14 |- ((A (_ P. /\ x e. z) -> (z e. A -> E.y(y e. z /\ x <Q y)))
64	63	ancrd 247	. . . . . . . . . . . . 13 |- ((A (_ P. /\ x e. z) -> (z e. A -> (E.y(y e. z /\ x <Q y) /\ z e. A)))
65		19.41v 963	. . . . . . . . . . . . . 14 |- (E.y((y e. z /\ x <Q y) /\ z e. A) <-> (E.y(y e. z /\ x <Q y) /\ z e. A))
66	50	anim1i 269	. . . . . . . . . . . . . . . 16 |- (((y e. z /\ z e. A) /\ x <Q y) -> (y e. U.A /\ x <Q y))
67	66	an1rs 373	. . . . . . . . . . . . . . 15 |- (((y e. z /\ x <Q y) /\ z e. A) -> (y e. U.A /\ x <Q y))
68	67	19.22i 723	. . . . . . . . . . . . . 14 |- (E.y((y e. z /\ x <Q y) /\ z e. A) -> E.y(y e. U.A /\ x <Q y))
69	65, 68	sylbir 176	. . . . . . . . . . . . 13 |- ((E.y(y e. z /\ x <Q y) /\ z e. A) -> E.y(y e. U.A /\ x <Q y))
70	64, 69	syl6 23	. . . . . . . . . . . 12 |- ((A (_ P. /\ x e. z) -> (z e. A -> E.y(y e. U.A /\ x <Q y)))
71	70	exp 291	. . . . . . . . . . 11 |- (A (_ P. -> (x e. z -> (z e. A -> E.y(y e. U.A /\ x <Q y))))
72	71	imp3a 279	. . . . . . . . . 10 |- (A (_ P. -> ((x e. z /\ z e. A) -> E.y(y e. U.A /\ x <Q y)))
73	72	19.23adv 954	. . . . . . . . 9 |- (A (_ P. -> (E.z(x e. z /\ z e. A) -> E.y(y e. U.A /\ x <Q y)))
74		df-rex 1206	. . . . . . . . 9 |- (E.y e. U. Ax <Q y <-> E.y(y e. U.A /\ x <Q y))
75	73, 14, 74	3imtr4g 426	. . . . . . . 8 |- (A (_ P. -> (x e. U.A -> E.y e. U. Ax <Q y))
76	58, 75	jcad 455	. . . . . . 7 |- (A (_ P. -> (x e. U.A -> (A.y(y <Q x -> y e. U.A) /\ E.y e. U. Ax <Q y)))
77	76	r19.21aiv 1259	. . . . . 6 |- (A (_ P. -> A.x e. U. A(A.y(y <Q x -> y e. U.A) /\ E.y e. U. Ax <Q y))
78	77	a1d 14	. . . . 5 |- (A (_ P. -> ((-. A = (/) /\ E.x(x e. P. /\ A.y(y e. P. -> (y <