Theorem suplem1pr 5161

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:   x,y,A

Proof of Theorem suplem1pr

Step	Hyp	Ref	Expression
1		ssel 2063	. . . . . . . . . . 11 |- (A (_ P. -> (z e. A -> z e. P.))
2		prn0 5093	. . . . . . . . . . . 12 |- (z e. P. -> z =/= (/))
3		ne0 2288	. . . . . . . . . . . 12 |- (z =/= (/) <-> E.x x e. z)
4	2, 3	sylib 198	. . . . . . . . . . 11 |- (z e. P. -> E.x x e. z)
5	1, 4	syl6 22	. . . . . . . . . 10 |- (A (_ P. -> (z e. A -> E.x x e. z))
6	5	ancrd 299	. . . . . . . . 9 |- (A (_ P. -> (z e. A -> (E.x x e. z /\ z e. A)))
7		19.41v 1305	. . . . . . . . 9 |- (E.x(x e. z /\ z e. A) <-> (E.x x e. z /\ z e. A))
8	6, 7	syl6ibr 213	. . . . . . . 8 |- (A (_ P. -> (z e. A -> E.x(x e. z /\ z e. A)))
9	8	19.22dv 1290	. . . . . . 7 |- (A (_ P. -> (E.z z e. A -> E.zE.x(x e. z /\ z e. A)))
10		n0 2289	. . . . . . 7 |- (-. A = (/) <-> E.z z e. A)
11		0pss 2308	. . . . . . . . 9 |- ((/) (. U.A <-> U.A =/= (/))
12		ne0 2288	. . . . . . . . 9 |- (U.A =/= (/) <-> E.x x e. U.A)
13	11, 12	bitr 173	. . . . . . . 8 |- ((/) (. U.A <-> E.x x e. U.A)
14		eluni 2506	. . . . . . . . 9 |- (x e. U.A <-> E.z(x e. z /\ z e. A))
15	14	exbii 1051	. . . . . . . 8 |- (E.x x e. U.A <-> E.xE.z(x e. z /\ z e. A))
16		excom 1046	. . . . . . . 8 |- (E.xE.z(x e. z /\ z e. A) <-> E.zE.x(x e. z /\ z e. A))
17	13, 15, 16	3bitr 177	. . . . . . 7 |- ((/) (. U.A <-> E.zE.x(x e. z /\ z e. A))
18	9, 10, 17	3imtr4g 553	. . . . . 6 |- (A (_ P. -> (-. A = (/) -> (/) (. U.A))
19		prpssnq 5094	. . . . . . . . . 10 |- (x e. P. -> x (. Q.)
20	19	a1i 8	. . . . . . . . 9 |- (A (_ P. -> (x e. P. -> x (. Q.))
21		ssel 2063	. . . . . . . . . . . . 13 |- (A (_ P. -> (y e. A -> y e. P.))
22	21	imim1d 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 63	. . . . . . . . . . . . 13 |- ((y e. A -> (y e. A -> y <P x)) -> (y e. A -> y <P x))
24		visset 1813	. . . . . . . . . . . . . . 15 |- x e. V
25		ltrelpr 5101	. . . . . . . . . . . . . . 15 |- <P (_ (P. X. P.)
26	24, 25	brel 3223	. . . . . . . . . . . . . 14 |- (y <P x -> (y e. P. /\ x e. P.))
27		ltprord 5134	. . . . . . . . . . . . . . 15 |- ((y e. P. /\ x e. P.) -> (y <P x <-> y (. x))
28		pssss 2143	. . . . . . . . . . . . . . 15 |- (y (. x -> y (_ x)
29	27, 28	syl6bi 214	. . . . . . . . . . . . . 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 22	. . . . . . . . . . . 12 |- ((y e. A -> (y e. A -> y <P x)) -> (y e. A -> y (_ x))
32	22, 31	syl6 22	. . . . . . . . . . 11 |- (A (_ P. -> ((y e. P. -> (y e. A -> y <P x)) -> (y e. A -> y (_ x)))
33	32	19.20dv 1289	. . . . . . . . . 10 |- (A (_ P. -> (A.y(y e. P. -> (y e. A -> y <P x)) -> A.y(y e. A -> y (_ x)))
34		unissb 2528	. . . . . . . . . . 11 |- (U.A (_ x <-> A.y e. A y (_ x)
35		df-ral 1649	. . . . . . . . . . 11 |- (A.y e. A y (_ x <-> A.y(y e. A -> y (_ x))
36	34, 35	bitr 173	. . . . . . . . . 10 |- (U.A (_ x <-> A.y(y e. A -> y (_ x))
37	33, 36	syl6ibr 213	. . . . . . . . 9 |- (A (_ P. -> (A.y(y e. P. -> (y e. A -> y <P x)) -> U.A (_ x))
38	20, 37	anim12d 558	. . . . . . . 8 |- (A (_ P. -> ((x e. P. /\ A.y(y e. P. -> (y e. A -> y <P x))) -> (x (. Q. /\ U.A (_ x)))
39		sspsstr 2151	. . . . . . . . 9 |- ((U.A (_ x /\ x (. Q.) -> U.A (. Q.)
40	39	ancoms 436	. . . . . . . 8 |- ((x (. Q. /\ U.A (_ x) -> U.A (. Q.)
41	38, 40	syl6 22	. . . . . . 7 |- (A (_ P. -> ((x e. P. /\ A.y(y e. P. -> (y e. A -> y <P x))) -> U.A (. Q.))
42	41	19.23adv 1214	. . . . . 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 558	. . . . 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 5097	. . . . . . . . . . . . . . . . . . . 20 |- ((z e. P. /\ x e. z) -> (y <Q x -> y e. z))
45	44	ex 373	. . . . . . . . . . . . . . . . . . 19 |- (z e. P. -> (x e. z -> (y <Q x -> y e. z)))
46	1, 45	syl6 22	. . . . . . . . . . . . . . . . . 18 |- (A (_ P. -> (z e. A -> (x e. z -> (y <Q x -> y e. z))))
47	46	com24 37	. . . . . . . . . . . . . . . . 17 |- (A (_ P. -> (y <Q x -> (x e. z -> (z e. A -> y e. z))))
48	47	imp31 362	. . . . . . . . . . . . . . . 16 |- (((A (_ P. /\ y <Q x) /\ x e. z) -> (z e. A -> y e. z))
49	48	ancrd 299	. . . . . . . . . . . . . . 15 |- (((A (_ P. /\ y <Q x) /\ x e. z) -> (z e. A -> (y e. z /\ z e. A)))
50		elunii 2508	. . . . . . . . . . . . . . 15 |- ((y e. z /\ z e. A) -> y e. U.A)
51	49, 50	syl6 22	. . . . . . . . . . . . . 14 |- (((A (_ P. /\ y <Q x) /\ x e. z) -> (z e. A -> y e. U.A))
52	51	ex 373	. . . . . . . . . . . . 13 |- ((A (_ P. /\ y <Q x) -> (x e. z -> (z e. A -> y e. U.A)))
53	52	imp3a 361	. . . . . . . . . . . 12 |- ((A (_ P. /\ y <Q x) -> ((x e. z /\ z e. A) -> y e. U.A))
54	53	19.23adv 1214	. . . . . . . . . . 11 |- ((A (_ P. /\ y <Q x) -> (E.z(x e. z /\ z e. A) -> y e. U.A))
55	54, 14	syl5ib 206	. . . . . . . . . 10 |- ((A (_ P. /\ y <Q x) -> (x e. U.A -> y e. U.A))
56	55	ex 373	. . . . . . . . 9 |- (A (_ P. -> (y <Q x -> (x e. U.A -> y e. U.A)))
57	56	com23 32	. . . . . . . 8 |- (A (_ P. -> (x e. U.A -> (y <Q x -> y e. U.A)))
58	57	19.21adv 1288	. . . . . . 7 |- (A (_ P. -> (x e. U.A -> A.y(y <Q x -> y e. U.A)))
59		prnmax 5099	. . . . . . . . . . . . . . . . 17 |- ((z e. P. /\ x e. z) -> E.y(y e. z /\ x <Q y))
60	59	ex 373	. . . . . . . . . . . . . . . 16 |- (z e. P. -> (x e. z -> E.y(y e. z /\ x <Q y)))
61	1, 60	syl6 22	. . . . . . . . . . . . . . 15 |- (A (_ P. -> (z e. A -> (x e. z -> E.y(y e. z /\ x <Q y))))
62	61	com23 32	. . . . . . . . . . . . . 14 |- (A (_ P. -> (x e. z -> (z e. A -> E.y(y e. z /\ x <Q y))))
63	62	imp 350	. . . . . . . . . . . . 13 |- ((A (_ P. /\ x e. z) -> (z e. A -> E.y(y e. z /\ x <Q y)))
64	63	ancrd 299	. . . . . . . . . . . 12 |- ((A (_ P. /\ x e. z) -> (z e. A -> (E.y(y e. z /\ x <Q y) /\ z e. A)))
65		19.41v 1305	. . . . . . . . . . . . 13 |- (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 334	. . . . . . . . . . . . . . 15 |- (((y e. z /\ z e. A) /\ x <Q y) -> (y e. U.A /\ x <Q y))
67	66	an1rs 489	. . . . . . . . . . . . . 14 |- (((y e. z /\ x <Q y) /\ z e. A) -> (y e. U.A /\ x <Q y))
68	67	19.22i 1040	. . . . . . . . . . . . 13 |- (E.y((y e. z /\ x <Q y) /\ z e. A) -> E.y(y e. U.A /\ x <Q y))
69	65, 68	sylbir 201	. . . . . . . . . . . 12 |- ((E.y(y e. z /\ x <Q y) /\ z e. A) -> E.y(y e. U.A /\ x <Q y))
70	64, 69	syl6 22	. . . . . . . . . . 11 |- ((A (_ P. /\ x e. z) -> (z e. A -> E.y(y e. U.A /\ x <Q y)))
71	70	ex 373	. . . . . . . . . 10 |- (A (_ P. -> (x e. z -> (z e. A -> E.y(y e. U.A /\ x <Q y))))
72	71	imp3a 361	. . . . . . . . 9 |- (A (_ P. -> ((x e. z /\ z e. A) -> E.y(y e. U.A /\ x <Q y)))
73	72	19.23adv 1214	. . . . . . . 8 |- (A (_ P. -> (E.z(x e. z /\ z e. A) -> E.y(y e. U.A /\ x <Q y)))
74		df-rex 1650	. . . . . . . 8 |- (E.y e. U.Ax <Q y <-> E.y(y e. U.A /\ x <Q y))
75	73, 14, 74	3imtr4g 553	. . . . . . 7 |- (A (_ P. -> (x e. U.A -> E.y e. U.Ax <Q y))
76	58, 75	jcad 600	. . . . . 6 |- (A (_ P. -> (x e. U.A -> (A.