Theorem suplem1pr 10463

Description: The union of a nonempty, bounded set of positive reals is a positive real. Part of Proposition 9-3.3 of [Gleason] p. 122. (Contributed by NM, 19-May-1996.) (Revised by Mario Carneiro, 12-Jun-2013.) (New usage is discouraged.)

Assertion

Ref	Expression
suplem1pr	⊢ ((𝐴 ≠ ∅ ∧ ∃𝑥 ∈ P ∀𝑦 ∈ 𝐴 𝑦<P 𝑥) → ∪ 𝐴 ∈ P)

Distinct variable group:   𝑥,𝑦,𝐴

Proof of Theorem suplem1pr

Dummy variable 𝑧 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ltrelpr 10409	. . . . . . . . 9 ⊢ <P ⊆ (P × P)
2	1	brel 5581	. . . . . . . 8 ⊢ (𝑦<P 𝑥 → (𝑦 ∈ P ∧ 𝑥 ∈ P))
3	2	simpld 498	. . . . . . 7 ⊢ (𝑦<P 𝑥 → 𝑦 ∈ P)
4	3	ralimi 3128	. . . . . 6 ⊢ (∀𝑦 ∈ 𝐴 𝑦<P 𝑥 → ∀𝑦 ∈ 𝐴 𝑦 ∈ P)
5		dfss3 3903	. . . . . 6 ⊢ (𝐴 ⊆ P ↔ ∀𝑦 ∈ 𝐴 𝑦 ∈ P)
6	4, 5	sylibr 237	. . . . 5 ⊢ (∀𝑦 ∈ 𝐴 𝑦<P 𝑥 → 𝐴 ⊆ P)
7	6	rexlimivw 3241	. . . 4 ⊢ (∃𝑥 ∈ P ∀𝑦 ∈ 𝐴 𝑦<P 𝑥 → 𝐴 ⊆ P)
8	7	adantl 485	. . 3 ⊢ ((𝐴 ≠ ∅ ∧ ∃𝑥 ∈ P ∀𝑦 ∈ 𝐴 𝑦<P 𝑥) → 𝐴 ⊆ P)
9		n0 4260	. . . . 5 ⊢ (𝐴 ≠ ∅ ↔ ∃𝑧 𝑧 ∈ 𝐴)
10		ssel 3908	. . . . . . 7 ⊢ (𝐴 ⊆ P → (𝑧 ∈ 𝐴 → 𝑧 ∈ P))
11		prn0 10400	. . . . . . . . . 10 ⊢ (𝑧 ∈ P → 𝑧 ≠ ∅)
12		0pss 4352	. . . . . . . . . 10 ⊢ (∅ ⊊ 𝑧 ↔ 𝑧 ≠ ∅)
13	11, 12	sylibr 237	. . . . . . . . 9 ⊢ (𝑧 ∈ P → ∅ ⊊ 𝑧)
14		elssuni 4830	. . . . . . . . 9 ⊢ (𝑧 ∈ 𝐴 → 𝑧 ⊆ ∪ 𝐴)
15		psssstr 4034	. . . . . . . . 9 ⊢ ((∅ ⊊ 𝑧 ∧ 𝑧 ⊆ ∪ 𝐴) → ∅ ⊊ ∪ 𝐴)
16	13, 14, 15	syl2an 598	. . . . . . . 8 ⊢ ((𝑧 ∈ P ∧ 𝑧 ∈ 𝐴) → ∅ ⊊ ∪ 𝐴)
17	16	expcom 417	. . . . . . 7 ⊢ (𝑧 ∈ 𝐴 → (𝑧 ∈ P → ∅ ⊊ ∪ 𝐴))
18	10, 17	sylcom 30	. . . . . 6 ⊢ (𝐴 ⊆ P → (𝑧 ∈ 𝐴 → ∅ ⊊ ∪ 𝐴))
19	18	exlimdv 1934	. . . . 5 ⊢ (𝐴 ⊆ P → (∃𝑧 𝑧 ∈ 𝐴 → ∅ ⊊ ∪ 𝐴))
20	9, 19	syl5bi 245	. . . 4 ⊢ (𝐴 ⊆ P → (𝐴 ≠ ∅ → ∅ ⊊ ∪ 𝐴))
21		prpssnq 10401	. . . . . . 7 ⊢ (𝑥 ∈ P → 𝑥 ⊊ Q)
22	21	adantl 485	. . . . . 6 ⊢ ((𝐴 ⊆ P ∧ 𝑥 ∈ P) → 𝑥 ⊊ Q)
23		ltprord 10441	. . . . . . . . . 10 ⊢ ((𝑦 ∈ P ∧ 𝑥 ∈ P) → (𝑦<P 𝑥 ↔ 𝑦 ⊊ 𝑥))
24		pssss 4023	. . . . . . . . . 10 ⊢ (𝑦 ⊊ 𝑥 → 𝑦 ⊆ 𝑥)
25	23, 24	syl6bi 256	. . . . . . . . 9 ⊢ ((𝑦 ∈ P ∧ 𝑥 ∈ P) → (𝑦<P 𝑥 → 𝑦 ⊆ 𝑥))
26	2, 25	mpcom 38	. . . . . . . 8 ⊢ (𝑦<P 𝑥 → 𝑦 ⊆ 𝑥)
27	26	ralimi 3128	. . . . . . 7 ⊢ (∀𝑦 ∈ 𝐴 𝑦<P 𝑥 → ∀𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥)
28		unissb 4832	. . . . . . 7 ⊢ (∪ 𝐴 ⊆ 𝑥 ↔ ∀𝑦 ∈ 𝐴 𝑦 ⊆ 𝑥)
29	27, 28	sylibr 237	. . . . . 6 ⊢ (∀𝑦 ∈ 𝐴 𝑦<P 𝑥 → ∪ 𝐴 ⊆ 𝑥)
30		sspsstr 4033	. . . . . . 7 ⊢ ((∪ 𝐴 ⊆ 𝑥 ∧ 𝑥 ⊊ Q) → ∪ 𝐴 ⊊ Q)
31	30	expcom 417	. . . . . 6 ⊢ (𝑥 ⊊ Q → (∪ 𝐴 ⊆ 𝑥 → ∪ 𝐴 ⊊ Q))
32	22, 29, 31	syl2im 40	. . . . 5 ⊢ ((𝐴 ⊆ P ∧ 𝑥 ∈ P) → (∀𝑦 ∈ 𝐴 𝑦<P 𝑥 → ∪ 𝐴 ⊊ Q))
33	32	rexlimdva 3243	. . . 4 ⊢ (𝐴 ⊆ P → (∃𝑥 ∈ P ∀𝑦 ∈ 𝐴 𝑦<P 𝑥 → ∪ 𝐴 ⊊ Q))
34	20, 33	anim12d 611	. . 3 ⊢ (𝐴 ⊆ P → ((𝐴 ≠ ∅ ∧ ∃𝑥 ∈ P ∀𝑦 ∈ 𝐴 𝑦<P 𝑥) → (∅ ⊊ ∪ 𝐴 ∧ ∪ 𝐴 ⊊ Q)))
35	8, 34	mpcom 38	. 2 ⊢ ((𝐴 ≠ ∅ ∧ ∃𝑥 ∈ P ∀𝑦 ∈ 𝐴 𝑦<P 𝑥) → (∅ ⊊ ∪ 𝐴 ∧ ∪ 𝐴 ⊊ Q))
36		prcdnq 10404	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ P ∧ 𝑥 ∈ 𝑧) → (𝑦 <Q 𝑥 → 𝑦 ∈ 𝑧))
37	36	ex 416	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ P → (𝑥 ∈ 𝑧 → (𝑦 <Q 𝑥 → 𝑦 ∈ 𝑧)))
38	37	com3r 87	. . . . . . . . . . 11 ⊢ (𝑦 <Q 𝑥 → (𝑧 ∈ P → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧)))
39	10, 38	sylan9 511	. . . . . . . . . 10 ⊢ ((𝐴 ⊆ P ∧ 𝑦 <Q 𝑥) → (𝑧 ∈ 𝐴 → (𝑥 ∈ 𝑧 → 𝑦 ∈ 𝑧)))
40	39	reximdvai 3231	. . . . . . . . 9 ⊢ ((𝐴 ⊆ P ∧ 𝑦 <Q 𝑥) → (∃𝑧 ∈ 𝐴 𝑥 ∈ 𝑧 → ∃𝑧 ∈ 𝐴 𝑦 ∈ 𝑧))
41		eluni2 4804	. . . . . . . . 9 ⊢ (𝑥 ∈ ∪ 𝐴 ↔ ∃𝑧 ∈ 𝐴 𝑥 ∈ 𝑧)
42		eluni2 4804	. . . . . . . . 9 ⊢ (𝑦 ∈ ∪ 𝐴 ↔ ∃𝑧 ∈ 𝐴 𝑦 ∈ 𝑧)
43	40, 41, 42	3imtr4g 299	. . . . . . . 8 ⊢ ((𝐴 ⊆ P ∧ 𝑦 <Q 𝑥) → (𝑥 ∈ ∪ 𝐴 → 𝑦 ∈ ∪ 𝐴))
44	43	ex 416	. . . . . . 7 ⊢ (𝐴 ⊆ P → (𝑦 <Q 𝑥 → (𝑥 ∈ ∪ 𝐴 → 𝑦 ∈ ∪ 𝐴)))
45	44	com23 86	. . . . . 6 ⊢ (𝐴 ⊆ P → (𝑥 ∈ ∪ 𝐴 → (𝑦 <Q 𝑥 → 𝑦 ∈ ∪ 𝐴)))
46	45	alrimdv 1930	. . . . 5 ⊢ (𝐴 ⊆ P → (𝑥 ∈ ∪ 𝐴 → ∀𝑦(𝑦 <Q 𝑥 → 𝑦 ∈ ∪ 𝐴)))
47		eluni 4803	. . . . . 6 ⊢ (𝑥 ∈ ∪ 𝐴 ↔ ∃𝑧(𝑥 ∈ 𝑧 ∧ 𝑧 ∈ 𝐴))
48		prnmax 10406	. . . . . . . . . . . . 13 ⊢ ((𝑧 ∈ P ∧ 𝑥 ∈ 𝑧) → ∃𝑦 ∈ 𝑧 𝑥 <Q 𝑦)
49	48	ex 416	. . . . . . . . . . . 12 ⊢ (𝑧 ∈ P → (𝑥 ∈ 𝑧 → ∃𝑦 ∈ 𝑧 𝑥 <Q 𝑦))
50	10, 49	syl6 35	. . . . . . . . . . 11 ⊢ (𝐴 ⊆ P → (𝑧 ∈ 𝐴 → (𝑥 ∈ 𝑧 → ∃𝑦 ∈ 𝑧 𝑥 <Q 𝑦)))
51	50	com23 86	. . . . . . . . . 10 ⊢ (𝐴 ⊆ P → (𝑥 ∈ 𝑧 → (𝑧 ∈ 𝐴 → ∃𝑦 ∈ 𝑧 𝑥 <Q 𝑦)))
52	51	imp 410	. . . . . . . . 9 ⊢ ((𝐴 ⊆ P ∧ 𝑥 ∈ 𝑧) → (𝑧 ∈ 𝐴 → ∃𝑦 ∈ 𝑧 𝑥 <Q 𝑦))
53		ssrexv 3982	. . . . . . . . . 10 ⊢ (𝑧 ⊆ ∪ 𝐴 → (∃𝑦 ∈ 𝑧 𝑥 <Q 𝑦 → ∃𝑦 ∈ ∪ 𝐴𝑥 <Q 𝑦))
54	14, 53	syl 17	. . . . . . . . 9 ⊢ (𝑧 ∈ 𝐴 → (∃𝑦 ∈ 𝑧 𝑥 <Q 𝑦 → ∃𝑦 ∈ ∪ 𝐴𝑥 <Q 𝑦))
55	52, 54	sylcom 30	. . . . . . . 8 ⊢ ((𝐴 ⊆ P ∧ 𝑥 ∈ 𝑧) → (𝑧 ∈ 𝐴 → ∃𝑦 ∈ ∪ 𝐴𝑥 <Q 𝑦))
56	55	expimpd 457	. . . . . . 7 ⊢ (𝐴 ⊆ P → ((𝑥 ∈ 𝑧 ∧ 𝑧 ∈ 𝐴) → ∃𝑦 ∈ ∪ 𝐴𝑥 <Q 𝑦))
57	56	exlimdv 1934	. . . . . 6 ⊢ (𝐴 ⊆ P → (∃𝑧(𝑥 ∈ 𝑧 ∧ 𝑧 ∈ 𝐴) → ∃𝑦 ∈ ∪ 𝐴𝑥 <Q 𝑦))
58	47, 57	syl5bi 245	. . . . 5 ⊢ (𝐴 ⊆ P → (𝑥 ∈ ∪ 𝐴 → ∃𝑦 ∈ ∪ 𝐴𝑥 <Q 𝑦))
59	46, 58	jcad 516	. . . 4 ⊢ (𝐴 ⊆ P → (𝑥 ∈ ∪ 𝐴 → (∀𝑦(𝑦 <Q 𝑥 → 𝑦 ∈ ∪ 𝐴) ∧ ∃𝑦 ∈ ∪ 𝐴𝑥 <Q 𝑦)))
60	59	ralrimiv 3148	. . 3 ⊢ (𝐴 ⊆ P → ∀𝑥 ∈ ∪ 𝐴(∀𝑦(𝑦 <Q 𝑥 → 𝑦 ∈ ∪ 𝐴) ∧ ∃𝑦 ∈ ∪ 𝐴𝑥 <Q 𝑦))
61	8, 60	syl 17	. 2 ⊢ ((𝐴 ≠ ∅ ∧ ∃𝑥 ∈ P ∀𝑦 ∈ 𝐴 𝑦<P 𝑥) → ∀𝑥 ∈ ∪ 𝐴(∀𝑦(𝑦 <Q 𝑥 → 𝑦 ∈ ∪ 𝐴) ∧ ∃𝑦 ∈ ∪ 𝐴𝑥 <Q 𝑦))
62		elnp 10398	. 2 ⊢ (∪ 𝐴 ∈ P ↔ ((∅ ⊊ ∪ 𝐴 ∧ ∪ 𝐴 ⊊ Q) ∧ ∀𝑥 ∈ ∪ 𝐴(∀𝑦(𝑦 <Q 𝑥 → 𝑦 ∈ ∪ 𝐴) ∧ ∃𝑦 ∈ ∪ 𝐴𝑥 <Q 𝑦)))
63	35, 61, 62	sylanbrc 586	1 ⊢ ((𝐴 ≠ ∅ ∧ ∃𝑥 ∈ P ∀𝑦 ∈ 𝐴 𝑦<P 𝑥) → ∪ 𝐴 ∈ P)

Syntax hints:   → wi 4   ∧ wa 399  ∀wal 1536  ∃wex 1781   ∈ wcel 2111   ≠ wne 2987  ∀wral 3106  ∃wrex 3107   ⊆ wss 3881   ⊊ wpss 3882  ∅c0 4243  ∪ cuni 4800   class class class wbr 5030  Qcnq 10263   <_Q cltq 10269  Pcnp 10270  <_P cltp 10274

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-inf2 9088

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3443  df-sbc 3721  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-br 5031  df-opab 5093  df-tr 5137  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-om 7561  df-ni 10283  df-nq 10323  df-ltnq 10329  df-np 10392  df-ltp 10396

This theorem is referenced by:  supexpr  10465