Theorem suplem2pr 6314

Description: The union of a set of positive reals (if a positive real) is its supremum (least upper bound). Part of Proposition 9-3.3 of [Gleason] p. 122.

Assertion

Ref	Expression
suplem2pr	|- (A C_ P. -> ((y e. A -> -. U.A <P y) /\ (y <P U.A -> E.z(z e. P. /\ (z e. A /\ y <P z)))))

Distinct variable group:   y,z,A

Proof of Theorem suplem2pr

Step	Hyp	Ref	Expression
1		npex 6243	. . . . . . 7 |- P. e. _V
2	1	ssex 3455	. . . . . 6 |- (A C_ P. -> A e. _V)
3		uniexg 3795	. . . . . 6 |- (A e. _V -> U.A e. _V)
4		ltrelpr 6253	. . . . . . . 8 |- <P C_ (P. X. P.)
5	4	brelg 4047	. . . . . . 7 |- (U.A e. _V -> (y <P U.A -> (y e. P. /\ U.A e. P.)))
6		simpl 346	. . . . . . 7 |- ((y e. P. /\ U.A e. P.) -> y e. P.)
7	5, 6	syl6 25	. . . . . 6 |- (U.A e. _V -> (y <P U.A -> y e. P.))
8	2, 3, 7	3syl 24	. . . . 5 |- (A C_ P. -> (y <P U.A -> y e. P.))
9		ltsopr 6288	. . . . . . . . . . . . . . . . 17 |- <P Or P.
10		sotric 3615	. . . . . . . . . . . . . . . . 17 |- (( <P Or P. /\ (y e. P. /\ z e. P.)) -> (y <P z <-> -. (y = z \/ z <P y)))
11	9, 10	mpan 759	. . . . . . . . . . . . . . . 16 |- ((y e. P. /\ z e. P.) -> (y <P z <-> -. (y = z \/ z <P y)))
12	11	con2bid 585	. . . . . . . . . . . . . . 15 |- ((y e. P. /\ z e. P.) -> ((y = z \/ z <P y) <-> -. y <P z))
13	12	ancoms 484	. . . . . . . . . . . . . 14 |- ((z e. P. /\ y e. P.) -> ((y = z \/ z <P y) <-> -. y <P z))
14		ltprord 6286	. . . . . . . . . . . . . . . 16 |- ((z e. P. /\ y e. P.) -> (z <P y <-> z C. y))
15	14	orbi2d 676	. . . . . . . . . . . . . . 15 |- ((z e. P. /\ y e. P.) -> ((y = z \/ z <P y) <-> (y = z \/ z C. y)))
16		sspss 2707	. . . . . . . . . . . . . . . 16 |- (z C_ y <-> (z C. y \/ z = y))
17		eqcom 1886	. . . . . . . . . . . . . . . . 17 |- (z = y <-> y = z)
18	17	orbi2i 275	. . . . . . . . . . . . . . . 16 |- ((z C. y \/ z = y) <-> (z C. y \/ y = z))
19		orcom 266	. . . . . . . . . . . . . . . 16 |- ((z C. y \/ y = z) <-> (y = z \/ z C. y))
20	16, 18, 19	3bitri 194	. . . . . . . . . . . . . . 15 |- (z C_ y <-> (y = z \/ z C. y))
21	15, 20	syl6bbr 597	. . . . . . . . . . . . . 14 |- ((z e. P. /\ y e. P.) -> ((y = z \/ z <P y) <-> z C_ y))
22	13, 21	bitr3d 589	. . . . . . . . . . . . 13 |- ((z e. P. /\ y e. P.) -> (-. y <P z <-> z C_ y))
23		ssel2 2616	. . . . . . . . . . . . 13 |- ((A C_ P. /\ z e. A) -> z e. P.)
24	22, 23	sylan 497	. . . . . . . . . . . 12 |- (((A C_ P. /\ z e. A) /\ y e. P.) -> (-. y <P z <-> z C_ y))
25	24	an1rs 547	. . . . . . . . . . 11 |- (((A C_ P. /\ y e. P.) /\ z e. A) -> (-. y <P z <-> z C_ y))
26	25	pm5.74da 646	. . . . . . . . . 10 |- ((A C_ P. /\ y e. P.) -> ((z e. A -> -. y <P z) <-> (z e. A -> z C_ y)))
27	26	albidv 1656	. . . . . . . . 9 |- ((A C_ P. /\ y e. P.) -> (A.z(z e. A -> -. y <P z) <-> A.z(z e. A -> z C_ y)))
28		alinexa 1389	. . . . . . . . 9 |- (A.z(z e. A -> -. y <P z) <-> -. E.z(z e. A /\ y <P z))
29		unissb 3208	. . . . . . . . . 10 |- (U.A C_ y <-> A.z e. A z C_ y)
30		df-ral 2109	. . . . . . . . . 10 |- (A.z e. A z C_ y <-> A.z(z e. A -> z C_ y))
31	29, 30	bitr2i 191	. . . . . . . . 9 |- (A.z(z e. A -> z C_ y) <-> U.A C_ y)
32	27, 28, 31	3bitr3g 613	. . . . . . . 8 |- ((A C_ P. /\ y e. P.) -> (-. E.z(z e. A /\ y <P z) <-> U.A C_ y))
33		ssnpss 2712	. . . . . . . . 9 |- (U.A C_ y -> -. y C. U.A)
34		visset 2295	. . . . . . . . . . 11 |- y e. _V
35	34	ssex 3455	. . . . . . . . . 10 |- (U.A C_ y -> U.A e. _V)
36		ltprord 6286	. . . . . . . . . . . 12 |- ((y e. P. /\ U.A e. P.) -> (y <P U.A <-> y C. U.A))
37	36	biimpd 170	. . . . . . . . . . 11 |- ((y e. P. /\ U.A e. P.) -> (y <P U.A -> y C. U.A))
38	5, 37	syli 65	. . . . . . . . . 10 |- (U.A e. _V -> (y <P U.A -> y C. U.A))
39	35, 38	syl 12	. . . . . . . . 9 |- (U.A C_ y -> (y <P U.A -> y C. U.A))
40	33, 39	mtod 123	. . . . . . . 8 |- (U.A C_ y -> -. y <P U.A)
41	32, 40	syl6bi 231	. . . . . . 7 |- ((A C_ P. /\ y e. P.) -> (-. E.z(z e. A /\ y <P z) -> -. y <P U.A))
42	41	con4d 91	. . . . . 6 |- ((A C_ P. /\ y e. P.) -> (y <P U.A -> E.z(z e. A /\ y <P z)))
43	42	ex 402	. . . . 5 |- (A C_ P. -> (y e. P. -> (y <P U.A -> E.z(z e. A /\ y <P z))))
44	8, 43	syld 30	. . . 4 |- (A C_ P. -> (y <P U.A -> (y <P U.A -> E.z(z e. A /\ y <P z))))
45	44	pm2.43d 79	. . 3 |- (A C_ P. -> (y <P U.A -> E.z(z e. A /\ y <P z)))
46		visset 2295	. . . . . . . 8 |- z e. _V
47	46, 4	brel 4048	. . . . . . 7 |- (y <P z -> (y e. P. /\ z e. P.))
48	47	simprd 352	. . . . . 6 |- (y <P z -> z e. P.)
49	48	adantl 424	. . . . 5 |- ((z e. A /\ y <P z) -> z e. P.)
50	49	ancri 321	. . . 4 |- ((z e. A /\ y <P z) -> (z e. P. /\ (z e. A /\ y <P z)))
51	50	eximi 1387	. . 3 |- (E.z(z e. A /\ y <P z) -> E.z(z e. P. /\ (z e. A /\ y <P z)))
52	45, 51	syl6 25	. 2 |- (A C_ P. -> (y <P U.A -> E.z(z e. P. /\ (z e. A /\ y <P z))))
53		elssuni 3206	. . . 4 |- (y e. A -> y C_ U.A)
54		ssnpss 2712	. . . 4 |- (y C_ U.A -> -. U.A C. y)
55	53, 54	syl 12	. . 3 |- (y e. A -> -. U.A C. y)
56	34, 4	brel 4048	. . . 4 |- (U.A <P y -> (U.A e. P. /\ y e. P.))
57		ltprord 6286	. . . . 5 |- ((U.A e. P. /\ y e. P.) -> (U.A <P y <-> U.A C. y))
58	57	biimpd 170	. . . 4 |- ((U.A e. P. /\ y e. P.) -> (U.A <P y -> U.A C. y))
59	56, 58	mpcom 60	. . 3 |- (U.A <P y -> U.A C. y)
60	55, 59	nsyl 131	. 2 |- (y e. A -> -. U.A <P y)
61	52, 60	jctil 316	1 |- (A C_ P. -> ((y e. A -> -. U.A <P y) /\ (y <P U.A -> E.z(z e. P. /\ (z e. A /\ y <P z)))))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   \/ wo 239   /\ wa 240  A.wal 1296   = wceq 1298   e. wcel 1300  E.wex 1326  A.wral 2105  _Vcvv 2292   C_ wss 2593   C. wpss 2594  U.cuni 3177   class class class wbr 3338   Or wor 3590  P.cnp 6137   <P cltp 6141

This theorem is referenced by:  supexpr 6315

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790  ax-inf2 5731

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-reu 2111  df-rab 2112  df-v 2294  df-sbc 2454  df-csb 2541  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-pss 2607  df-nul 2876  df-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-tp 3052  df-op 3053  df-uni 3178  df-int 3215  df-iun 3257  df-br 3339  df-opab 3396  df-tr 3412  df-eprel 3583  df-id 3586  df-po 3591  df-so 3604  df-fr 3625  df-we 3644  df-ord 3660  df-on 3661  df-lim 3662  df-suc 3663  df-om 3950  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-fv 4014  df-opr 4886  df-oprab 4887  df-1st 5020  df-2nd 5021  df-rdg 5140  df-1o 5177  df-oadd 5179  df-omul 5180  df-er 5318  df-ec 5320  df-qs 5323  df-ni 6152  df-mi 6154  df-lti 6155  df-enq 6189  df-nq 6190  df-ltq 6194  df-np 6238  df-ltp 6242

Copyright terms: Public domain