supxrun

Description: The supremum of the union of two sets of extended reals equals the largest of their suprema. (Contributed by NM, 19-Jan-2006)

		Ref	Expression
	Assertion	supxrun	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ 𝐵 ⊆ ℝ^* ∧ sup ( 𝐴 , ℝ^* , < ) ≤ sup ( 𝐵 , ℝ^* , < ) ) → sup ( ( 𝐴 ∪ 𝐵 ) , ℝ^* , < ) = sup ( 𝐵 , ℝ^* , < ) )

Proof

Step	Hyp	Ref	Expression
1		unss	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ 𝐵 ⊆ ℝ^* ) ↔ ( 𝐴 ∪ 𝐵 ) ⊆ ℝ^* )
2	1	biimpi	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ 𝐵 ⊆ ℝ^* ) → ( 𝐴 ∪ 𝐵 ) ⊆ ℝ^* )
3	2	3adant3	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ 𝐵 ⊆ ℝ^* ∧ sup ( 𝐴 , ℝ^* , < ) ≤ sup ( 𝐵 , ℝ^* , < ) ) → ( 𝐴 ∪ 𝐵 ) ⊆ ℝ^* )
4		supxrcl	⊢ ( 𝐵 ⊆ ℝ^* → sup ( 𝐵 , ℝ^* , < ) ∈ ℝ^* )
5	4	3ad2ant2	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ 𝐵 ⊆ ℝ^* ∧ sup ( 𝐴 , ℝ^* , < ) ≤ sup ( 𝐵 , ℝ^* , < ) ) → sup ( 𝐵 , ℝ^* , < ) ∈ ℝ^* )
6		elun	⊢ ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ↔ ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) )
7		xrltso	⊢ < Or ℝ^*
8	7	a1i	⊢ ( 𝐴 ⊆ ℝ^* → < Or ℝ^* )
9		xrsupss	⊢ ( 𝐴 ⊆ ℝ^* → ∃ 𝑦 ∈ ℝ^* ( ∀ 𝑧 ∈ 𝐴 ¬ 𝑦 < 𝑧 ∧ ∀ 𝑧 ∈ ℝ^* ( 𝑧 < 𝑦 → ∃ 𝑤 ∈ 𝐴 𝑧 < 𝑤 ) ) )
10	8 9	supub	⊢ ( 𝐴 ⊆ ℝ^* → ( 𝑥 ∈ 𝐴 → ¬ sup ( 𝐴 , ℝ^* , < ) < 𝑥 ) )
11	10	3ad2ant1	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ 𝐵 ⊆ ℝ^* ∧ sup ( 𝐴 , ℝ^* , < ) ≤ sup ( 𝐵 , ℝ^* , < ) ) → ( 𝑥 ∈ 𝐴 → ¬ sup ( 𝐴 , ℝ^* , < ) < 𝑥 ) )
12		supxrcl	⊢ ( 𝐴 ⊆ ℝ^* → sup ( 𝐴 , ℝ^* , < ) ∈ ℝ^* )
13	12	ad2antrr	⊢ ( ( ( 𝐴 ⊆ ℝ^* ∧ 𝐵 ⊆ ℝ^* ) ∧ 𝑥 ∈ 𝐴 ) → sup ( 𝐴 , ℝ^* , < ) ∈ ℝ^* )
14	4	ad2antlr	⊢ ( ( ( 𝐴 ⊆ ℝ^* ∧ 𝐵 ⊆ ℝ^* ) ∧ 𝑥 ∈ 𝐴 ) → sup ( 𝐵 , ℝ^* , < ) ∈ ℝ^* )
15		ssel2	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ^* )
16	15	adantlr	⊢ ( ( ( 𝐴 ⊆ ℝ^* ∧ 𝐵 ⊆ ℝ^* ) ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ^* )
17		xrlelttr	⊢ ( ( sup ( 𝐴 , ℝ^* , < ) ∈ ℝ^* ∧ sup ( 𝐵 , ℝ^* , < ) ∈ ℝ^* ∧ 𝑥 ∈ ℝ^* ) → ( ( sup ( 𝐴 , ℝ^* , < ) ≤ sup ( 𝐵 , ℝ^* , < ) ∧ sup ( 𝐵 , ℝ^* , < ) < 𝑥 ) → sup ( 𝐴 , ℝ^* , < ) < 𝑥 ) )
18	13 14 16 17	syl3anc	⊢ ( ( ( 𝐴 ⊆ ℝ^* ∧ 𝐵 ⊆ ℝ^* ) ∧ 𝑥 ∈ 𝐴 ) → ( ( sup ( 𝐴 , ℝ^* , < ) ≤ sup ( 𝐵 , ℝ^* , < ) ∧ sup ( 𝐵 , ℝ^* , < ) < 𝑥 ) → sup ( 𝐴 , ℝ^* , < ) < 𝑥 ) )
19	18	expdimp	⊢ ( ( ( ( 𝐴 ⊆ ℝ^* ∧ 𝐵 ⊆ ℝ^* ) ∧ 𝑥 ∈ 𝐴 ) ∧ sup ( 𝐴 , ℝ^* , < ) ≤ sup ( 𝐵 , ℝ^* , < ) ) → ( sup ( 𝐵 , ℝ^* , < ) < 𝑥 → sup ( 𝐴 , ℝ^* , < ) < 𝑥 ) )
20	19	con3d	⊢ ( ( ( ( 𝐴 ⊆ ℝ^* ∧ 𝐵 ⊆ ℝ^* ) ∧ 𝑥 ∈ 𝐴 ) ∧ sup ( 𝐴 , ℝ^* , < ) ≤ sup ( 𝐵 , ℝ^* , < ) ) → ( ¬ sup ( 𝐴 , ℝ^* , < ) < 𝑥 → ¬ sup ( 𝐵 , ℝ^* , < ) < 𝑥 ) )
21	20	exp41	⊢ ( 𝐴 ⊆ ℝ^* → ( 𝐵 ⊆ ℝ^* → ( 𝑥 ∈ 𝐴 → ( sup ( 𝐴 , ℝ^* , < ) ≤ sup ( 𝐵 , ℝ^* , < ) → ( ¬ sup ( 𝐴 , ℝ^* , < ) < 𝑥 → ¬ sup ( 𝐵 , ℝ^* , < ) < 𝑥 ) ) ) ) )
22	21	com34	⊢ ( 𝐴 ⊆ ℝ^* → ( 𝐵 ⊆ ℝ^* → ( sup ( 𝐴 , ℝ^* , < ) ≤ sup ( 𝐵 , ℝ^* , < ) → ( 𝑥 ∈ 𝐴 → ( ¬ sup ( 𝐴 , ℝ^* , < ) < 𝑥 → ¬ sup ( 𝐵 , ℝ^* , < ) < 𝑥 ) ) ) ) )
23	22	3imp	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ 𝐵 ⊆ ℝ^* ∧ sup ( 𝐴 , ℝ^* , < ) ≤ sup ( 𝐵 , ℝ^* , < ) ) → ( 𝑥 ∈ 𝐴 → ( ¬ sup ( 𝐴 , ℝ^* , < ) < 𝑥 → ¬ sup ( 𝐵 , ℝ^* , < ) < 𝑥 ) ) )
24	11 23	mpdd	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ 𝐵 ⊆ ℝ^* ∧ sup ( 𝐴 , ℝ^* , < ) ≤ sup ( 𝐵 , ℝ^* , < ) ) → ( 𝑥 ∈ 𝐴 → ¬ sup ( 𝐵 , ℝ^* , < ) < 𝑥 ) )
25	7	a1i	⊢ ( 𝐵 ⊆ ℝ^* → < Or ℝ^* )
26		xrsupss	⊢ ( 𝐵 ⊆ ℝ^* → ∃ 𝑦 ∈ ℝ^* ( ∀ 𝑧 ∈ 𝐵 ¬ 𝑦 < 𝑧 ∧ ∀ 𝑧 ∈ ℝ^* ( 𝑧 < 𝑦 → ∃ 𝑤 ∈ 𝐵 𝑧 < 𝑤 ) ) )
27	25 26	supub	⊢ ( 𝐵 ⊆ ℝ^* → ( 𝑥 ∈ 𝐵 → ¬ sup ( 𝐵 , ℝ^* , < ) < 𝑥 ) )
28	27	3ad2ant2	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ 𝐵 ⊆ ℝ^* ∧ sup ( 𝐴 , ℝ^* , < ) ≤ sup ( 𝐵 , ℝ^* , < ) ) → ( 𝑥 ∈ 𝐵 → ¬ sup ( 𝐵 , ℝ^* , < ) < 𝑥 ) )
29	24 28	jaod	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ 𝐵 ⊆ ℝ^* ∧ sup ( 𝐴 , ℝ^* , < ) ≤ sup ( 𝐵 , ℝ^* , < ) ) → ( ( 𝑥 ∈ 𝐴 ∨ 𝑥 ∈ 𝐵 ) → ¬ sup ( 𝐵 , ℝ^* , < ) < 𝑥 ) )
30	6 29	biimtrid	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ 𝐵 ⊆ ℝ^* ∧ sup ( 𝐴 , ℝ^* , < ) ≤ sup ( 𝐵 , ℝ^* , < ) ) → ( 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) → ¬ sup ( 𝐵 , ℝ^* , < ) < 𝑥 ) )
31	30	ralrimiv	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ 𝐵 ⊆ ℝ^* ∧ sup ( 𝐴 , ℝ^* , < ) ≤ sup ( 𝐵 , ℝ^* , < ) ) → ∀ 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ¬ sup ( 𝐵 , ℝ^* , < ) < 𝑥 )
32		rexr	⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℝ^* )
33		xrsupss	⊢ ( 𝐵 ⊆ ℝ^* → ∃ 𝑥 ∈ ℝ^* ( ∀ 𝑧 ∈ 𝐵 ¬ 𝑥 < 𝑧 ∧ ∀ 𝑧 ∈ ℝ^* ( 𝑧 < 𝑥 → ∃ 𝑦 ∈ 𝐵 𝑧 < 𝑦 ) ) )
34	25 33	suplub	⊢ ( 𝐵 ⊆ ℝ^* → ( ( 𝑥 ∈ ℝ^* ∧ 𝑥 < sup ( 𝐵 , ℝ^* , < ) ) → ∃ 𝑦 ∈ 𝐵 𝑥 < 𝑦 ) )
35	32 34	sylani	⊢ ( 𝐵 ⊆ ℝ^* → ( ( 𝑥 ∈ ℝ ∧ 𝑥 < sup ( 𝐵 , ℝ^* , < ) ) → ∃ 𝑦 ∈ 𝐵 𝑥 < 𝑦 ) )
36		elun2	⊢ ( 𝑦 ∈ 𝐵 → 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) )
37	36	anim1i	⊢ ( ( 𝑦 ∈ 𝐵 ∧ 𝑥 < 𝑦 ) → ( 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) ∧ 𝑥 < 𝑦 ) )
38	37	reximi2	⊢ ( ∃ 𝑦 ∈ 𝐵 𝑥 < 𝑦 → ∃ 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) 𝑥 < 𝑦 )
39	35 38	syl6	⊢ ( 𝐵 ⊆ ℝ^* → ( ( 𝑥 ∈ ℝ ∧ 𝑥 < sup ( 𝐵 , ℝ^* , < ) ) → ∃ 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) 𝑥 < 𝑦 ) )
40	39	expd	⊢ ( 𝐵 ⊆ ℝ^* → ( 𝑥 ∈ ℝ → ( 𝑥 < sup ( 𝐵 , ℝ^* , < ) → ∃ 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) 𝑥 < 𝑦 ) ) )
41	40	ralrimiv	⊢ ( 𝐵 ⊆ ℝ^* → ∀ 𝑥 ∈ ℝ ( 𝑥 < sup ( 𝐵 , ℝ^* , < ) → ∃ 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) 𝑥 < 𝑦 ) )
42	41	3ad2ant2	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ 𝐵 ⊆ ℝ^* ∧ sup ( 𝐴 , ℝ^* , < ) ≤ sup ( 𝐵 , ℝ^* , < ) ) → ∀ 𝑥 ∈ ℝ ( 𝑥 < sup ( 𝐵 , ℝ^* , < ) → ∃ 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) 𝑥 < 𝑦 ) )
43		supxr	⊢ ( ( ( ( 𝐴 ∪ 𝐵 ) ⊆ ℝ^* ∧ sup ( 𝐵 , ℝ^* , < ) ∈ ℝ^* ) ∧ ( ∀ 𝑥 ∈ ( 𝐴 ∪ 𝐵 ) ¬ sup ( 𝐵 , ℝ^* , < ) < 𝑥 ∧ ∀ 𝑥 ∈ ℝ ( 𝑥 < sup ( 𝐵 , ℝ^* , < ) → ∃ 𝑦 ∈ ( 𝐴 ∪ 𝐵 ) 𝑥 < 𝑦 ) ) ) → sup ( ( 𝐴 ∪ 𝐵 ) , ℝ^* , < ) = sup ( 𝐵 , ℝ^* , < ) )
44	3 5 31 42 43	syl22anc	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ 𝐵 ⊆ ℝ^* ∧ sup ( 𝐴 , ℝ^* , < ) ≤ sup ( 𝐵 , ℝ^* , < ) ) → sup ( ( 𝐴 ∪ 𝐵 ) , ℝ^* , < ) = sup ( 𝐵 , ℝ^* , < ) )

Metamath Proof Explorer

Theorem supxrun

Proof