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 = ∅) ∧ ∃x(x ∈ P ∧ ∀y(y ∈ P → (y ∈ A → y<P x)))) → ∪A ∈ P)

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

Proof of Theorem suplem1pr

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

Syntax hints:  ¬ wn 1   → wi 2   ∧ wa 196  ∀wal 672  ∃wex 678   ∈ wel 803   = wceq 1091   ∈ wcel 1092  ∀wral 1201  ∃wrex 1202   ⊆ wss 1487   ⊂ wpss 1488  ∅c0 1707  ∪cuni 1919   class class class wbr 2054  Qcnq 3773   <_Q cltq 3778  Pcnp 3779  <_P cltp 3783

This theorem is referenced by:  suppr 3957

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-7 676  ax-gen 677  ax-8 798  ax-9 799  ax-10 800  ax-11 801  ax-12 802  ax-13 804  ax-14 805  ax-16 922  ax-17 925  ax-ext 1074  ax-rep 1075  ax-un 1076  ax-pow 1077  ax-reg 1078  ax-inf 1079

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198  df-3or 582  df-3an 583  df-ex 679  df-sb 853  df-eu 1009  df-mo 1010  df-clab 1093  df-cleq 1097  df-clel 1099  df-ne 1192  df-ral 1205  df-rex 1206  df-rab 1208  df-v 1349  df-sbc 1441  df-dif 1489  df-un 1490  df-in 1491  df-ss 1492  df-pss 1494  df-nul 1708  df-if 1777  df-pw 1799  df-sn 1811  df-pr 1812  df-tp 1814  df-op 1815  df-uni 1920  df-tr 2042  df-br 2063  df-opab 2098  df-eprel 2122  df-id 2125  df-po 2128  df-so 2138  df-fr 2169  df-we 2186  df-ord 2202  df-on 2203  df-lim 2204  df-suc 2205  df-om 2373  df-xp 2424  df-rel 2425  df-cnv 2426  df-co 2427  df-dm 2428  df-rn 2429  df-res 2430  df-ima 2431  df-fun 2432  df-fn 2433  df-f 2434  df-f1 2435  df-fv 2438  df-rdg 2970  df-qs 3205  df-ni 3794  df-nq 3832  df-ltq 3836  df-np 3880  df-ltp 3884

metamath.org