suplesup2

Description: If any element of A is less than or equal to an element in B , then the supremum of A is less than or equal to the supremum of B . (Contributed by Glauco Siliprandi, 8-Apr-2021)

	Ref	Expression
Hypotheses	suplesup2.a	⊢ ( 𝜑 → 𝐴 ⊆ ℝ^* )
	suplesup2.b	⊢ ( 𝜑 → 𝐵 ⊆ ℝ^* )
	suplesup2.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 ∈ 𝐵 𝑥 ≤ 𝑦 )
Assertion	suplesup2	⊢ ( 𝜑 → sup ( 𝐴 , ℝ^* , < ) ≤ sup ( 𝐵 , ℝ^* , < ) )

Proof

Step	Hyp	Ref	Expression
1		suplesup2.a	⊢ ( 𝜑 → 𝐴 ⊆ ℝ^* )
2		suplesup2.b	⊢ ( 𝜑 → 𝐵 ⊆ ℝ^* )
3		suplesup2.c	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ∃ 𝑦 ∈ 𝐵 𝑥 ≤ 𝑦 )
4	1	sselda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ∈ ℝ^* )
5	4	3ad2ant1	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ∧ 𝑥 ≤ 𝑦 ) → 𝑥 ∈ ℝ^* )
6		simp1l	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ∧ 𝑥 ≤ 𝑦 ) → 𝜑 )
7		simp2	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ∧ 𝑥 ≤ 𝑦 ) → 𝑦 ∈ 𝐵 )
8	2	sselda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ ℝ^* )
9	6 7 8	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ∧ 𝑥 ≤ 𝑦 ) → 𝑦 ∈ ℝ^* )
10		supxrcl	⊢ ( 𝐵 ⊆ ℝ^* → sup ( 𝐵 , ℝ^* , < ) ∈ ℝ^* )
11	2 10	syl	⊢ ( 𝜑 → sup ( 𝐵 , ℝ^* , < ) ∈ ℝ^* )
12	6 11	syl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ∧ 𝑥 ≤ 𝑦 ) → sup ( 𝐵 , ℝ^* , < ) ∈ ℝ^* )
13		simp3	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ∧ 𝑥 ≤ 𝑦 ) → 𝑥 ≤ 𝑦 )
14	2	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝐵 ⊆ ℝ^* )
15		simpr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ∈ 𝐵 )
16		supxrub	⊢ ( ( 𝐵 ⊆ ℝ^* ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ≤ sup ( 𝐵 , ℝ^* , < ) )
17	14 15 16	syl2anc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐵 ) → 𝑦 ≤ sup ( 𝐵 , ℝ^* , < ) )
18	6 7 17	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ∧ 𝑥 ≤ 𝑦 ) → 𝑦 ≤ sup ( 𝐵 , ℝ^* , < ) )
19	5 9 12 13 18	xrletrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐵 ∧ 𝑥 ≤ 𝑦 ) → 𝑥 ≤ sup ( 𝐵 , ℝ^* , < ) )
20	19	3exp	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝑦 ∈ 𝐵 → ( 𝑥 ≤ 𝑦 → 𝑥 ≤ sup ( 𝐵 , ℝ^* , < ) ) ) )
21	20	rexlimdv	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ∃ 𝑦 ∈ 𝐵 𝑥 ≤ 𝑦 → 𝑥 ≤ sup ( 𝐵 , ℝ^* , < ) ) )
22	3 21	mpd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝑥 ≤ sup ( 𝐵 , ℝ^* , < ) )
23	22	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐴 𝑥 ≤ sup ( 𝐵 , ℝ^* , < ) )
24		supxrleub	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ sup ( 𝐵 , ℝ^* , < ) ∈ ℝ^* ) → ( sup ( 𝐴 , ℝ^* , < ) ≤ sup ( 𝐵 , ℝ^* , < ) ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ sup ( 𝐵 , ℝ^* , < ) ) )
25	1 11 24	syl2anc	⊢ ( 𝜑 → ( sup ( 𝐴 , ℝ^* , < ) ≤ sup ( 𝐵 , ℝ^* , < ) ↔ ∀ 𝑥 ∈ 𝐴 𝑥 ≤ sup ( 𝐵 , ℝ^* , < ) ) )
26	23 25	mpbird	⊢ ( 𝜑 → sup ( 𝐴 , ℝ^* , < ) ≤ sup ( 𝐵 , ℝ^* , < ) )

Metamath Proof Explorer

Theorem suplesup2

Proof