Theorem suplem2pr

Description: The union of a set of positive reals (if a positive real) is its supremum (the least upper bound). 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.)

	Ref	Expression
Assertion	suplem2pr	⊢ ( 𝐴 ⊆ P → ( ( 𝑦 ∈ 𝐴 → ¬ ∪ 𝐴 <P 𝑦 ) ∧ ( 𝑦 <P ∪ 𝐴 → ∃ 𝑧 ∈ 𝐴 𝑦 <P 𝑧 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ltrelpr	⊢ <P ⊆ ( P × P )
2	1	brel	⊢ ( 𝑦 <P ∪ 𝐴 → ( 𝑦 ∈ P ∧ ∪ 𝐴 ∈ P ) )
3	2	simpld	⊢ ( 𝑦 <P ∪ 𝐴 → 𝑦 ∈ P )
4		ralnex	⊢ ( ∀ 𝑧 ∈ 𝐴 ¬ 𝑦 <P 𝑧 ↔ ¬ ∃ 𝑧 ∈ 𝐴 𝑦 <P 𝑧 )
5		ssel2	⊢ ( ( 𝐴 ⊆ P ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ P )
6		ltsopr	⊢ <P Or P
7		sotric	⊢ ( ( <P Or P ∧ ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) ) → ( 𝑦 <P 𝑧 ↔ ¬ ( 𝑦 = 𝑧 ∨ 𝑧 <P 𝑦 ) ) )
8	6 7	mpan	⊢ ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) → ( 𝑦 <P 𝑧 ↔ ¬ ( 𝑦 = 𝑧 ∨ 𝑧 <P 𝑦 ) ) )
9	8	con2bid	⊢ ( ( 𝑦 ∈ P ∧ 𝑧 ∈ P ) → ( ( 𝑦 = 𝑧 ∨ 𝑧 <P 𝑦 ) ↔ ¬ 𝑦 <P 𝑧 ) )
10	9	ancoms	⊢ ( ( 𝑧 ∈ P ∧ 𝑦 ∈ P ) → ( ( 𝑦 = 𝑧 ∨ 𝑧 <P 𝑦 ) ↔ ¬ 𝑦 <P 𝑧 ) )
11		ltprord	⊢ ( ( 𝑧 ∈ P ∧ 𝑦 ∈ P ) → ( 𝑧 <P 𝑦 ↔ 𝑧 ⊊ 𝑦 ) )
12	11	orbi2d	⊢ ( ( 𝑧 ∈ P ∧ 𝑦 ∈ P ) → ( ( 𝑦 = 𝑧 ∨ 𝑧 <P 𝑦 ) ↔ ( 𝑦 = 𝑧 ∨ 𝑧 ⊊ 𝑦 ) ) )
13		sspss	⊢ ( 𝑧 ⊆ 𝑦 ↔ ( 𝑧 ⊊ 𝑦 ∨ 𝑧 = 𝑦 ) )
14		equcom	⊢ ( 𝑧 = 𝑦 ↔ 𝑦 = 𝑧 )
15	14	orbi2i	⊢ ( ( 𝑧 ⊊ 𝑦 ∨ 𝑧 = 𝑦 ) ↔ ( 𝑧 ⊊ 𝑦 ∨ 𝑦 = 𝑧 ) )
16		orcom	⊢ ( ( 𝑧 ⊊ 𝑦 ∨ 𝑦 = 𝑧 ) ↔ ( 𝑦 = 𝑧 ∨ 𝑧 ⊊ 𝑦 ) )
17	13 15 16	3bitri	⊢ ( 𝑧 ⊆ 𝑦 ↔ ( 𝑦 = 𝑧 ∨ 𝑧 ⊊ 𝑦 ) )
18	12 17	bitr4di	⊢ ( ( 𝑧 ∈ P ∧ 𝑦 ∈ P ) → ( ( 𝑦 = 𝑧 ∨ 𝑧 <P 𝑦 ) ↔ 𝑧 ⊆ 𝑦 ) )
19	10 18	bitr3d	⊢ ( ( 𝑧 ∈ P ∧ 𝑦 ∈ P ) → ( ¬ 𝑦 <P 𝑧 ↔ 𝑧 ⊆ 𝑦 ) )
20	5 19	sylan	⊢ ( ( ( 𝐴 ⊆ P ∧ 𝑧 ∈ 𝐴 ) ∧ 𝑦 ∈ P ) → ( ¬ 𝑦 <P 𝑧 ↔ 𝑧 ⊆ 𝑦 ) )
21	20	an32s	⊢ ( ( ( 𝐴 ⊆ P ∧ 𝑦 ∈ P ) ∧ 𝑧 ∈ 𝐴 ) → ( ¬ 𝑦 <P 𝑧 ↔ 𝑧 ⊆ 𝑦 ) )
22	21	ralbidva	⊢ ( ( 𝐴 ⊆ P ∧ 𝑦 ∈ P ) → ( ∀ 𝑧 ∈ 𝐴 ¬ 𝑦 <P 𝑧 ↔ ∀ 𝑧 ∈ 𝐴 𝑧 ⊆ 𝑦 ) )
23	4 22	bitr3id	⊢ ( ( 𝐴 ⊆ P ∧ 𝑦 ∈ P ) → ( ¬ ∃ 𝑧 ∈ 𝐴 𝑦 <P 𝑧 ↔ ∀ 𝑧 ∈ 𝐴 𝑧 ⊆ 𝑦 ) )
24		unissb	⊢ ( ∪ 𝐴 ⊆ 𝑦 ↔ ∀ 𝑧 ∈ 𝐴 𝑧 ⊆ 𝑦 )
25	23 24	bitr4di	⊢ ( ( 𝐴 ⊆ P ∧ 𝑦 ∈ P ) → ( ¬ ∃ 𝑧 ∈ 𝐴 𝑦 <P 𝑧 ↔ ∪ 𝐴 ⊆ 𝑦 ) )
26		ssnpss	⊢ ( ∪ 𝐴 ⊆ 𝑦 → ¬ 𝑦 ⊊ ∪ 𝐴 )
27		ltprord	⊢ ( ( 𝑦 ∈ P ∧ ∪ 𝐴 ∈ P ) → ( 𝑦 <P ∪ 𝐴 ↔ 𝑦 ⊊ ∪ 𝐴 ) )
28	27	biimpd	⊢ ( ( 𝑦 ∈ P ∧ ∪ 𝐴 ∈ P ) → ( 𝑦 <P ∪ 𝐴 → 𝑦 ⊊ ∪ 𝐴 ) )
29	2 28	mpcom	⊢ ( 𝑦 <P ∪ 𝐴 → 𝑦 ⊊ ∪ 𝐴 )
30	26 29	nsyl	⊢ ( ∪ 𝐴 ⊆ 𝑦 → ¬ 𝑦 <P ∪ 𝐴 )
31	25 30	syl6bi	⊢ ( ( 𝐴 ⊆ P ∧ 𝑦 ∈ P ) → ( ¬ ∃ 𝑧 ∈ 𝐴 𝑦 <P 𝑧 → ¬ 𝑦 <P ∪ 𝐴 ) )
32	31	con4d	⊢ ( ( 𝐴 ⊆ P ∧ 𝑦 ∈ P ) → ( 𝑦 <P ∪ 𝐴 → ∃ 𝑧 ∈ 𝐴 𝑦 <P 𝑧 ) )
33	32	ex	⊢ ( 𝐴 ⊆ P → ( 𝑦 ∈ P → ( 𝑦 <P ∪ 𝐴 → ∃ 𝑧 ∈ 𝐴 𝑦 <P 𝑧 ) ) )
34	3 33	syl5	⊢ ( 𝐴 ⊆ P → ( 𝑦 <P ∪ 𝐴 → ( 𝑦 <P ∪ 𝐴 → ∃ 𝑧 ∈ 𝐴 𝑦 <P 𝑧 ) ) )
35	34	pm2.43d	⊢ ( 𝐴 ⊆ P → ( 𝑦 <P ∪ 𝐴 → ∃ 𝑧 ∈ 𝐴 𝑦 <P 𝑧 ) )
36		elssuni	⊢ ( 𝑦 ∈ 𝐴 → 𝑦 ⊆ ∪ 𝐴 )
37		ssnpss	⊢ ( 𝑦 ⊆ ∪ 𝐴 → ¬ ∪ 𝐴 ⊊ 𝑦 )
38	36 37	syl	⊢ ( 𝑦 ∈ 𝐴 → ¬ ∪ 𝐴 ⊊ 𝑦 )
39	1	brel	⊢ ( ∪ 𝐴 <P 𝑦 → ( ∪ 𝐴 ∈ P ∧ 𝑦 ∈ P ) )
40		ltprord	⊢ ( ( ∪ 𝐴 ∈ P ∧ 𝑦 ∈ P ) → ( ∪ 𝐴 <P 𝑦 ↔ ∪ 𝐴 ⊊ 𝑦 ) )
41	40	biimpd	⊢ ( ( ∪ 𝐴 ∈ P ∧ 𝑦 ∈ P ) → ( ∪ 𝐴 <P 𝑦 → ∪ 𝐴 ⊊ 𝑦 ) )
42	39 41	mpcom	⊢ ( ∪ 𝐴 <P 𝑦 → ∪ 𝐴 ⊊ 𝑦 )
43	38 42	nsyl	⊢ ( 𝑦 ∈ 𝐴 → ¬ ∪ 𝐴 <P 𝑦 )
44	35 43	jctil	⊢ ( 𝐴 ⊆ P → ( ( 𝑦 ∈ 𝐴 → ¬ ∪ 𝐴 <P 𝑦 ) ∧ ( 𝑦 <P ∪ 𝐴 → ∃ 𝑧 ∈ 𝐴 𝑦 <P 𝑧 ) ) )