supxrgere

Description: If a real number can be approximated from below by members of a set, then it is less than or equal to the supremum of the set. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	supxrgere.xph	⊢ Ⅎ 𝑥 𝜑
	supxrgere.a	⊢ ( 𝜑 → 𝐴 ⊆ ℝ^* )
	supxrgere.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
	supxrgere.y	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ⁺ ) → ∃ 𝑦 ∈ 𝐴 ( 𝐵 − 𝑥 ) < 𝑦 )
Assertion	supxrgere	⊢ ( 𝜑 → 𝐵 ≤ sup ( 𝐴 , ℝ^* , < ) )

Proof

Step	Hyp	Ref	Expression
1		supxrgere.xph	⊢ Ⅎ 𝑥 𝜑
2		supxrgere.a	⊢ ( 𝜑 → 𝐴 ⊆ ℝ^* )
3		supxrgere.b	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
4		supxrgere.y	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ⁺ ) → ∃ 𝑦 ∈ 𝐴 ( 𝐵 − 𝑥 ) < 𝑦 )
5		rexr	⊢ ( 𝐵 ∈ ℝ → 𝐵 ∈ ℝ^* )
6		pnfxr	⊢ +∞ ∈ ℝ^*
7	6	a1i	⊢ ( 𝐵 ∈ ℝ → +∞ ∈ ℝ^* )
8		ltpnf	⊢ ( 𝐵 ∈ ℝ → 𝐵 < +∞ )
9	5 7 8	xrltled	⊢ ( 𝐵 ∈ ℝ → 𝐵 ≤ +∞ )
10	3 9	syl	⊢ ( 𝜑 → 𝐵 ≤ +∞ )
11	10	adantr	⊢ ( ( 𝜑 ∧ sup ( 𝐴 , ℝ^* , < ) = +∞ ) → 𝐵 ≤ +∞ )
12		id	⊢ ( sup ( 𝐴 , ℝ^* , < ) = +∞ → sup ( 𝐴 , ℝ^* , < ) = +∞ )
13	12	eqcomd	⊢ ( sup ( 𝐴 , ℝ^* , < ) = +∞ → +∞ = sup ( 𝐴 , ℝ^* , < ) )
14	13	adantl	⊢ ( ( 𝜑 ∧ sup ( 𝐴 , ℝ^* , < ) = +∞ ) → +∞ = sup ( 𝐴 , ℝ^* , < ) )
15	11 14	breqtrd	⊢ ( ( 𝜑 ∧ sup ( 𝐴 , ℝ^* , < ) = +∞ ) → 𝐵 ≤ sup ( 𝐴 , ℝ^* , < ) )
16		simpl	⊢ ( ( 𝜑 ∧ ¬ sup ( 𝐴 , ℝ^* , < ) = +∞ ) → 𝜑 )
17		1rp	⊢ 1 ∈ ℝ⁺
18		nfcv	⊢ Ⅎ 𝑥 1
19		nfv	⊢ Ⅎ 𝑥 1 ∈ ℝ⁺
20	1 19	nfan	⊢ Ⅎ 𝑥 ( 𝜑 ∧ 1 ∈ ℝ⁺ )
21		nfv	⊢ Ⅎ 𝑥 ∃ 𝑦 ∈ 𝐴 ( 𝐵 − 1 ) < 𝑦
22	20 21	nfim	⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ 1 ∈ ℝ⁺ ) → ∃ 𝑦 ∈ 𝐴 ( 𝐵 − 1 ) < 𝑦 )
23		eleq1	⊢ ( 𝑥 = 1 → ( 𝑥 ∈ ℝ⁺ ↔ 1 ∈ ℝ⁺ ) )
24	23	anbi2d	⊢ ( 𝑥 = 1 → ( ( 𝜑 ∧ 𝑥 ∈ ℝ⁺ ) ↔ ( 𝜑 ∧ 1 ∈ ℝ⁺ ) ) )
25		oveq2	⊢ ( 𝑥 = 1 → ( 𝐵 − 𝑥 ) = ( 𝐵 − 1 ) )
26	25	breq1d	⊢ ( 𝑥 = 1 → ( ( 𝐵 − 𝑥 ) < 𝑦 ↔ ( 𝐵 − 1 ) < 𝑦 ) )
27	26	rexbidv	⊢ ( 𝑥 = 1 → ( ∃ 𝑦 ∈ 𝐴 ( 𝐵 − 𝑥 ) < 𝑦 ↔ ∃ 𝑦 ∈ 𝐴 ( 𝐵 − 1 ) < 𝑦 ) )
28	24 27	imbi12d	⊢ ( 𝑥 = 1 → ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ⁺ ) → ∃ 𝑦 ∈ 𝐴 ( 𝐵 − 𝑥 ) < 𝑦 ) ↔ ( ( 𝜑 ∧ 1 ∈ ℝ⁺ ) → ∃ 𝑦 ∈ 𝐴 ( 𝐵 − 1 ) < 𝑦 ) ) )
29	18 22 28 4	vtoclgf	⊢ ( 1 ∈ ℝ⁺ → ( ( 𝜑 ∧ 1 ∈ ℝ⁺ ) → ∃ 𝑦 ∈ 𝐴 ( 𝐵 − 1 ) < 𝑦 ) )
30	17 29	ax-mp	⊢ ( ( 𝜑 ∧ 1 ∈ ℝ⁺ ) → ∃ 𝑦 ∈ 𝐴 ( 𝐵 − 1 ) < 𝑦 )
31	17 30	mpan2	⊢ ( 𝜑 → ∃ 𝑦 ∈ 𝐴 ( 𝐵 − 1 ) < 𝑦 )
32	31	adantr	⊢ ( ( 𝜑 ∧ ¬ sup ( 𝐴 , ℝ^* , < ) = +∞ ) → ∃ 𝑦 ∈ 𝐴 ( 𝐵 − 1 ) < 𝑦 )
33		mnfxr	⊢ -∞ ∈ ℝ^*
34	33	a1i	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ ( 𝐵 − 1 ) < 𝑦 ) → -∞ ∈ ℝ^* )
35	2	sselda	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ ℝ^* )
36	35	3adant3	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ ( 𝐵 − 1 ) < 𝑦 ) → 𝑦 ∈ ℝ^* )
37		supxrcl	⊢ ( 𝐴 ⊆ ℝ^* → sup ( 𝐴 , ℝ^* , < ) ∈ ℝ^* )
38	2 37	syl	⊢ ( 𝜑 → sup ( 𝐴 , ℝ^* , < ) ∈ ℝ^* )
39	38	3ad2ant1	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ ( 𝐵 − 1 ) < 𝑦 ) → sup ( 𝐴 , ℝ^* , < ) ∈ ℝ^* )
40		peano2rem	⊢ ( 𝐵 ∈ ℝ → ( 𝐵 − 1 ) ∈ ℝ )
41	3 40	syl	⊢ ( 𝜑 → ( 𝐵 − 1 ) ∈ ℝ )
42	41	rexrd	⊢ ( 𝜑 → ( 𝐵 − 1 ) ∈ ℝ^* )
43	42	adantr	⊢ ( ( 𝜑 ∧ ¬ -∞ < 𝑦 ) → ( 𝐵 − 1 ) ∈ ℝ^* )
44	43	3ad2antl1	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ ( 𝐵 − 1 ) < 𝑦 ) ∧ ¬ -∞ < 𝑦 ) → ( 𝐵 − 1 ) ∈ ℝ^* )
45	36	adantr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ ( 𝐵 − 1 ) < 𝑦 ) ∧ ¬ -∞ < 𝑦 ) → 𝑦 ∈ ℝ^* )
46	33	a1i	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ ( 𝐵 − 1 ) < 𝑦 ) ∧ ¬ -∞ < 𝑦 ) → -∞ ∈ ℝ^* )
47		simpl3	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ ( 𝐵 − 1 ) < 𝑦 ) ∧ ¬ -∞ < 𝑦 ) → ( 𝐵 − 1 ) < 𝑦 )
48		simpr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ ¬ -∞ < 𝑦 ) → ¬ -∞ < 𝑦 )
49	35	adantr	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ ¬ -∞ < 𝑦 ) → 𝑦 ∈ ℝ^* )
50	33	a1i	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ ¬ -∞ < 𝑦 ) → -∞ ∈ ℝ^* )
51		xrlenlt	⊢ ( ( 𝑦 ∈ ℝ^* ∧ -∞ ∈ ℝ^* ) → ( 𝑦 ≤ -∞ ↔ ¬ -∞ < 𝑦 ) )
52	49 50 51	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ ¬ -∞ < 𝑦 ) → ( 𝑦 ≤ -∞ ↔ ¬ -∞ < 𝑦 ) )
53	48 52	mpbird	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ ¬ -∞ < 𝑦 ) → 𝑦 ≤ -∞ )
54	53	3adantl3	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ ( 𝐵 − 1 ) < 𝑦 ) ∧ ¬ -∞ < 𝑦 ) → 𝑦 ≤ -∞ )
55	44 45 46 47 54	xrltletrd	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ ( 𝐵 − 1 ) < 𝑦 ) ∧ ¬ -∞ < 𝑦 ) → ( 𝐵 − 1 ) < -∞ )
56		nltmnf	⊢ ( ( 𝐵 − 1 ) ∈ ℝ^* → ¬ ( 𝐵 − 1 ) < -∞ )
57	42 56	syl	⊢ ( 𝜑 → ¬ ( 𝐵 − 1 ) < -∞ )
58	57	adantr	⊢ ( ( 𝜑 ∧ ¬ -∞ < 𝑦 ) → ¬ ( 𝐵 − 1 ) < -∞ )
59	58	3ad2antl1	⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ ( 𝐵 − 1 ) < 𝑦 ) ∧ ¬ -∞ < 𝑦 ) → ¬ ( 𝐵 − 1 ) < -∞ )
60	55 59	condan	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ ( 𝐵 − 1 ) < 𝑦 ) → -∞ < 𝑦 )
61	2	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → 𝐴 ⊆ ℝ^* )
62		simpr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ 𝐴 )
63		supxrub	⊢ ( ( 𝐴 ⊆ ℝ^* ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ≤ sup ( 𝐴 , ℝ^* , < ) )
64	61 62 63	syl2anc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ≤ sup ( 𝐴 , ℝ^* , < ) )
65	64	3adant3	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ ( 𝐵 − 1 ) < 𝑦 ) → 𝑦 ≤ sup ( 𝐴 , ℝ^* , < ) )
66	34 36 39 60 65	xrltletrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ∧ ( 𝐵 − 1 ) < 𝑦 ) → -∞ < sup ( 𝐴 , ℝ^* , < ) )
67	66	3exp	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐴 → ( ( 𝐵 − 1 ) < 𝑦 → -∞ < sup ( 𝐴 , ℝ^* , < ) ) ) )
68	67	adantr	⊢ ( ( 𝜑 ∧ ¬ sup ( 𝐴 , ℝ^* , < ) = +∞ ) → ( 𝑦 ∈ 𝐴 → ( ( 𝐵 − 1 ) < 𝑦 → -∞ < sup ( 𝐴 , ℝ^* , < ) ) ) )
69	68	rexlimdv	⊢ ( ( 𝜑 ∧ ¬ sup ( 𝐴 , ℝ^* , < ) = +∞ ) → ( ∃ 𝑦 ∈ 𝐴 ( 𝐵 − 1 ) < 𝑦 → -∞ < sup ( 𝐴 , ℝ^* , < ) ) )
70	32 69	mpd	⊢ ( ( 𝜑 ∧ ¬ sup ( 𝐴 , ℝ^* , < ) = +∞ ) → -∞ < sup ( 𝐴 , ℝ^* , < ) )
71		simpr	⊢ ( ( 𝜑 ∧ ¬ sup ( 𝐴 , ℝ^* , < ) = +∞ ) → ¬ sup ( 𝐴 , ℝ^* , < ) = +∞ )
72		nltpnft	⊢ ( sup ( 𝐴 , ℝ^* , < ) ∈ ℝ^* → ( sup ( 𝐴 , ℝ^* , < ) = +∞ ↔ ¬ sup ( 𝐴 , ℝ^* , < ) < +∞ ) )
73	38 72	syl	⊢ ( 𝜑 → ( sup ( 𝐴 , ℝ^* , < ) = +∞ ↔ ¬ sup ( 𝐴 , ℝ^* , < ) < +∞ ) )
74	73	adantr	⊢ ( ( 𝜑 ∧ ¬ sup ( 𝐴 , ℝ^* , < ) = +∞ ) → ( sup ( 𝐴 , ℝ^* , < ) = +∞ ↔ ¬ sup ( 𝐴 , ℝ^* , < ) < +∞ ) )
75	71 74	mtbid	⊢ ( ( 𝜑 ∧ ¬ sup ( 𝐴 , ℝ^* , < ) = +∞ ) → ¬ ¬ sup ( 𝐴 , ℝ^* , < ) < +∞ )
76	75	notnotrd	⊢ ( ( 𝜑 ∧ ¬ sup ( 𝐴 , ℝ^* , < ) = +∞ ) → sup ( 𝐴 , ℝ^* , < ) < +∞ )
77	70 76	jca	⊢ ( ( 𝜑 ∧ ¬ sup ( 𝐴 , ℝ^* , < ) = +∞ ) → ( -∞ < sup ( 𝐴 , ℝ^* , < ) ∧ sup ( 𝐴 , ℝ^* , < ) < +∞ ) )
78	38	adantr	⊢ ( ( 𝜑 ∧ ¬ sup ( 𝐴 , ℝ^* , < ) = +∞ ) → sup ( 𝐴 , ℝ^* , < ) ∈ ℝ^* )
79		xrrebnd	⊢ ( sup ( 𝐴 , ℝ^* , < ) ∈ ℝ^* → ( sup ( 𝐴 , ℝ^* , < ) ∈ ℝ ↔ ( -∞ < sup ( 𝐴 , ℝ^* , < ) ∧ sup ( 𝐴 , ℝ^* , < ) < +∞ ) ) )
80	78 79	syl	⊢ ( ( 𝜑 ∧ ¬ sup ( 𝐴 , ℝ^* , < ) = +∞ ) → ( sup ( 𝐴 , ℝ^* , < ) ∈ ℝ ↔ ( -∞ < sup ( 𝐴 , ℝ^* , < ) ∧ sup ( 𝐴 , ℝ^* , < ) < +∞ ) ) )
81	77 80	mpbird	⊢ ( ( 𝜑 ∧ ¬ sup ( 𝐴 , ℝ^* , < ) = +∞ ) → sup ( 𝐴 , ℝ^* , < ) ∈ ℝ )
82		simpl	⊢ ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ^* , < ) ∈ ℝ ) ∧ ¬ 𝐵 ≤ sup ( 𝐴 , ℝ^* , < ) ) → ( 𝜑 ∧ sup ( 𝐴 , ℝ^* , < ) ∈ ℝ ) )
83		simpr	⊢ ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ^* , < ) ∈ ℝ ) ∧ ¬ 𝐵 ≤ sup ( 𝐴 , ℝ^* , < ) ) → ¬ 𝐵 ≤ sup ( 𝐴 , ℝ^* , < ) )
84	82	simprd	⊢ ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ^* , < ) ∈ ℝ ) ∧ ¬ 𝐵 ≤ sup ( 𝐴 , ℝ^* , < ) ) → sup ( 𝐴 , ℝ^* , < ) ∈ ℝ )
85	3	ad2antrr	⊢ ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ^* , < ) ∈ ℝ ) ∧ ¬ 𝐵 ≤ sup ( 𝐴 , ℝ^* , < ) ) → 𝐵 ∈ ℝ )
86	84 85	ltnled	⊢ ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ^* , < ) ∈ ℝ ) ∧ ¬ 𝐵 ≤ sup ( 𝐴 , ℝ^* , < ) ) → ( sup ( 𝐴 , ℝ^* , < ) < 𝐵 ↔ ¬ 𝐵 ≤ sup ( 𝐴 , ℝ^* , < ) ) )
87	83 86	mpbird	⊢ ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ^* , < ) ∈ ℝ ) ∧ ¬ 𝐵 ≤ sup ( 𝐴 , ℝ^* , < ) ) → sup ( 𝐴 , ℝ^* , < ) < 𝐵 )
88		simpll	⊢ ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ^* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ^* , < ) < 𝐵 ) → 𝜑 )
89	3	adantr	⊢ ( ( 𝜑 ∧ sup ( 𝐴 , ℝ^* , < ) ∈ ℝ ) → 𝐵 ∈ ℝ )
90		simpr	⊢ ( ( 𝜑 ∧ sup ( 𝐴 , ℝ^* , < ) ∈ ℝ ) → sup ( 𝐴 , ℝ^* , < ) ∈ ℝ )
91	89 90	resubcld	⊢ ( ( 𝜑 ∧ sup ( 𝐴 , ℝ^* , < ) ∈ ℝ ) → ( 𝐵 − sup ( 𝐴 , ℝ^* , < ) ) ∈ ℝ )
92	91	adantr	⊢ ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ^* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ^* , < ) < 𝐵 ) → ( 𝐵 − sup ( 𝐴 , ℝ^* , < ) ) ∈ ℝ )
93		simpr	⊢ ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ^* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ^* , < ) < 𝐵 ) → sup ( 𝐴 , ℝ^* , < ) < 𝐵 )
94	90	adantr	⊢ ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ^* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ^* , < ) < 𝐵 ) → sup ( 𝐴 , ℝ^* , < ) ∈ ℝ )
95	88 3	syl	⊢ ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ^* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ^* , < ) < 𝐵 ) → 𝐵 ∈ ℝ )
96	94 95	posdifd	⊢ ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ^* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ^* , < ) < 𝐵 ) → ( sup ( 𝐴 , ℝ^* , < ) < 𝐵 ↔ 0 < ( 𝐵 − sup ( 𝐴 , ℝ^* , < ) ) ) )
97	93 96	mpbid	⊢ ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ^* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ^* , < ) < 𝐵 ) → 0 < ( 𝐵 − sup ( 𝐴 , ℝ^* , < ) ) )
98	92 97	elrpd	⊢ ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ^* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ^* , < ) < 𝐵 ) → ( 𝐵 − sup ( 𝐴 , ℝ^* , < ) ) ∈ ℝ⁺ )
99		ovex	⊢ ( 𝐵 − sup ( 𝐴 , ℝ^* , < ) ) ∈ V
100		nfcv	⊢ Ⅎ 𝑥 ( 𝐵 − sup ( 𝐴 , ℝ^* , < ) )
101		nfv	⊢ Ⅎ 𝑥 ( 𝐵 − sup ( 𝐴 , ℝ^* , < ) ) ∈ ℝ⁺
102	1 101	nfan	⊢ Ⅎ 𝑥 ( 𝜑 ∧ ( 𝐵 − sup ( 𝐴 , ℝ^* , < ) ) ∈ ℝ⁺ )
103		nfv	⊢ Ⅎ 𝑥 ∃ 𝑦 ∈ 𝐴 ( 𝐵 − ( 𝐵 − sup ( 𝐴 , ℝ^* , < ) ) ) < 𝑦
104	102 103	nfim	⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ ( 𝐵 − sup ( 𝐴 , ℝ^* , < ) ) ∈ ℝ⁺ ) → ∃ 𝑦 ∈ 𝐴 ( 𝐵 − ( 𝐵 − sup ( 𝐴 , ℝ^* , < ) ) ) < 𝑦 )
105		eleq1	⊢ ( 𝑥 = ( 𝐵 − sup ( 𝐴 , ℝ^* , < ) ) → ( 𝑥 ∈ ℝ⁺ ↔ ( 𝐵 − sup ( 𝐴 , ℝ^* , < ) ) ∈ ℝ⁺ ) )
106	105	anbi2d	⊢ ( 𝑥 = ( 𝐵 − sup ( 𝐴 , ℝ^* , < ) ) → ( ( 𝜑 ∧ 𝑥 ∈ ℝ⁺ ) ↔ ( 𝜑 ∧ ( 𝐵 − sup ( 𝐴 , ℝ^* , < ) ) ∈ ℝ⁺ ) ) )
107		oveq2	⊢ ( 𝑥 = ( 𝐵 − sup ( 𝐴 , ℝ^* , < ) ) → ( 𝐵 − 𝑥 ) = ( 𝐵 − ( 𝐵 − sup ( 𝐴 , ℝ^* , < ) ) ) )
108	107	breq1d	⊢ ( 𝑥 = ( 𝐵 − sup ( 𝐴 , ℝ^* , < ) ) → ( ( 𝐵 − 𝑥 ) < 𝑦 ↔ ( 𝐵 − ( 𝐵 − sup ( 𝐴 , ℝ^* , < ) ) ) < 𝑦 ) )
109	108	rexbidv	⊢ ( 𝑥 = ( 𝐵 − sup ( 𝐴 , ℝ^* , < ) ) → ( ∃ 𝑦 ∈ 𝐴 ( 𝐵 − 𝑥 ) < 𝑦 ↔ ∃ 𝑦 ∈ 𝐴 ( 𝐵 − ( 𝐵 − sup ( 𝐴 , ℝ^* , < ) ) ) < 𝑦 ) )
110	106 109	imbi12d	⊢ ( 𝑥 = ( 𝐵 − sup ( 𝐴 , ℝ^* , < ) ) → ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ⁺ ) → ∃ 𝑦 ∈ 𝐴 ( 𝐵 − 𝑥 ) < 𝑦 ) ↔ ( ( 𝜑 ∧ ( 𝐵 − sup ( 𝐴 , ℝ^* , < ) ) ∈ ℝ⁺ ) → ∃ 𝑦 ∈ 𝐴 ( 𝐵 − ( 𝐵 − sup ( 𝐴 , ℝ^* , < ) ) ) < 𝑦 ) ) )
111	100 104 110 4	vtoclgf	⊢ ( ( 𝐵 − sup ( 𝐴 , ℝ^* , < ) ) ∈ V → ( ( 𝜑 ∧ ( 𝐵 − sup ( 𝐴 , ℝ^* , < ) ) ∈ ℝ⁺ ) → ∃ 𝑦 ∈ 𝐴 ( 𝐵 − ( 𝐵 − sup ( 𝐴 , ℝ^* , < ) ) ) < 𝑦 ) )
112	99 111	ax-mp	⊢ ( ( 𝜑 ∧ ( 𝐵 − sup ( 𝐴 , ℝ^* , < ) ) ∈ ℝ⁺ ) → ∃ 𝑦 ∈ 𝐴 ( 𝐵 − ( 𝐵 − sup ( 𝐴 , ℝ^* , < ) ) ) < 𝑦 )
113	88 98 112	syl2anc	⊢ ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ^* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ^* , < ) < 𝐵 ) → ∃ 𝑦 ∈ 𝐴 ( 𝐵 − ( 𝐵 − sup ( 𝐴 , ℝ^* , < ) ) ) < 𝑦 )
114	3	recnd	⊢ ( 𝜑 → 𝐵 ∈ ℂ )
115	114	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ^* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ^* , < ) < 𝐵 ) ∧ ( 𝐵 − ( 𝐵 − sup ( 𝐴 , ℝ^* , < ) ) ) < 𝑦 ) → 𝐵 ∈ ℂ )
116	90	recnd	⊢ ( ( 𝜑 ∧ sup ( 𝐴 , ℝ^* , < ) ∈ ℝ ) → sup ( 𝐴 , ℝ^* , < ) ∈ ℂ )
117	116	ad2antrr	⊢ ( ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ^* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ^* , < ) < 𝐵 ) ∧ ( 𝐵 − ( 𝐵 − sup ( 𝐴 , ℝ^* , < ) ) ) < 𝑦 ) → sup ( 𝐴 , ℝ^* , < ) ∈ ℂ )
118	115 117	nncand	⊢ ( ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ^* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ^* , < ) < 𝐵 ) ∧ ( 𝐵 − ( 𝐵 − sup ( 𝐴 , ℝ^* , < ) ) ) < 𝑦 ) → ( 𝐵 − ( 𝐵 − sup ( 𝐴 , ℝ^* , < ) ) ) = sup ( 𝐴 , ℝ^* , < ) )
119	118	eqcomd	⊢ ( ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ^* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ^* , < ) < 𝐵 ) ∧ ( 𝐵 − ( 𝐵 − sup ( 𝐴 , ℝ^* , < ) ) ) < 𝑦 ) → sup ( 𝐴 , ℝ^* , < ) = ( 𝐵 − ( 𝐵 − sup ( 𝐴 , ℝ^* , < ) ) ) )
120		simpr	⊢ ( ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ^* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ^* , < ) < 𝐵 ) ∧ ( 𝐵 − ( 𝐵 − sup ( 𝐴 , ℝ^* , < ) ) ) < 𝑦 ) → ( 𝐵 − ( 𝐵 − sup ( 𝐴 , ℝ^* , < ) ) ) < 𝑦 )
121	119 120	eqbrtrd	⊢ ( ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ^* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ^* , < ) < 𝐵 ) ∧ ( 𝐵 − ( 𝐵 − sup ( 𝐴 , ℝ^* , < ) ) ) < 𝑦 ) → sup ( 𝐴 , ℝ^* , < ) < 𝑦 )
122	121	ex	⊢ ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ^* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ^* , < ) < 𝐵 ) → ( ( 𝐵 − ( 𝐵 − sup ( 𝐴 , ℝ^* , < ) ) ) < 𝑦 → sup ( 𝐴 , ℝ^* , < ) < 𝑦 ) )
123	122	adantr	⊢ ( ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ^* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ^* , < ) < 𝐵 ) ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝐵 − ( 𝐵 − sup ( 𝐴 , ℝ^* , < ) ) ) < 𝑦 → sup ( 𝐴 , ℝ^* , < ) < 𝑦 ) )
124	123	reximdva	⊢ ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ^* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ^* , < ) < 𝐵 ) → ( ∃ 𝑦 ∈ 𝐴 ( 𝐵 − ( 𝐵 − sup ( 𝐴 , ℝ^* , < ) ) ) < 𝑦 → ∃ 𝑦 ∈ 𝐴 sup ( 𝐴 , ℝ^* , < ) < 𝑦 ) )
125	113 124	mpd	⊢ ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ^* , < ) ∈ ℝ ) ∧ sup ( 𝐴 , ℝ^* , < ) < 𝐵 ) → ∃ 𝑦 ∈ 𝐴 sup ( 𝐴 , ℝ^* , < ) < 𝑦 )
126	82 87 125	syl2anc	⊢ ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ^* , < ) ∈ ℝ ) ∧ ¬ 𝐵 ≤ sup ( 𝐴 , ℝ^* , < ) ) → ∃ 𝑦 ∈ 𝐴 sup ( 𝐴 , ℝ^* , < ) < 𝑦 )
127	61 37	syl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → sup ( 𝐴 , ℝ^* , < ) ∈ ℝ^* )
128	35 127	xrlenltd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑦 ≤ sup ( 𝐴 , ℝ^* , < ) ↔ ¬ sup ( 𝐴 , ℝ^* , < ) < 𝑦 ) )
129	64 128	mpbid	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ¬ sup ( 𝐴 , ℝ^* , < ) < 𝑦 )
130	129	ralrimiva	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐴 ¬ sup ( 𝐴 , ℝ^* , < ) < 𝑦 )
131		ralnex	⊢ ( ∀ 𝑦 ∈ 𝐴 ¬ sup ( 𝐴 , ℝ^* , < ) < 𝑦 ↔ ¬ ∃ 𝑦 ∈ 𝐴 sup ( 𝐴 , ℝ^* , < ) < 𝑦 )
132	130 131	sylib	⊢ ( 𝜑 → ¬ ∃ 𝑦 ∈ 𝐴 sup ( 𝐴 , ℝ^* , < ) < 𝑦 )
133	132	ad2antrr	⊢ ( ( ( 𝜑 ∧ sup ( 𝐴 , ℝ^* , < ) ∈ ℝ ) ∧ ¬ 𝐵 ≤ sup ( 𝐴 , ℝ^* , < ) ) → ¬ ∃ 𝑦 ∈ 𝐴 sup ( 𝐴 , ℝ^* , < ) < 𝑦 )
134	126 133	condan	⊢ ( ( 𝜑 ∧ sup ( 𝐴 , ℝ^* , < ) ∈ ℝ ) → 𝐵 ≤ sup ( 𝐴 , ℝ^* , < ) )
135	16 81 134	syl2anc	⊢ ( ( 𝜑 ∧ ¬ sup ( 𝐴 , ℝ^* , < ) = +∞ ) → 𝐵 ≤ sup ( 𝐴 , ℝ^* , < ) )
136	15 135	pm2.61dan	⊢ ( 𝜑 → 𝐵 ≤ sup ( 𝐴 , ℝ^* , < ) )

Metamath Proof Explorer

Theorem supxrgere

Proof