Theorem infsupneg 9183

Description: If a set of real numbers has a greatest lower bound, the set of the negation of those numbers has a least upper bound. To go in the other direction see supinfneg 9182. (Contributed by Jim Kingdon, 15-Jan-2022.)

Hypotheses

Ref	Expression
infsupneg.ex	⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))
infsupneg.ss	⊢ (𝜑 → 𝐴 ⊆ ℝ)

Assertion

Ref	Expression
infsupneg	⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧)))

Distinct variable groups:   𝑦,𝐴,𝑧,𝑤,𝑥   𝜑,𝑦

Allowed substitution hints:   𝜑(𝑥,𝑧,𝑤)

Proof of Theorem infsupneg

Dummy variables 𝑎 𝑏 𝑐 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		infsupneg.ex	. . . 4 ⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))
2		breq2 3871	. . . . . . . 8 ⊢ (𝑎 = 𝑥 → (𝑦 < 𝑎 ↔ 𝑦 < 𝑥))
3	2	notbid 630	. . . . . . 7 ⊢ (𝑎 = 𝑥 → (¬ 𝑦 < 𝑎 ↔ ¬ 𝑦 < 𝑥))
4	3	ralbidv 2391	. . . . . 6 ⊢ (𝑎 = 𝑥 → (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑎 ↔ ∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥))
5		breq1 3870	. . . . . . . 8 ⊢ (𝑎 = 𝑥 → (𝑎 < 𝑦 ↔ 𝑥 < 𝑦))
6	5	imbi1d 230	. . . . . . 7 ⊢ (𝑎 = 𝑥 → ((𝑎 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦) ↔ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))
7	6	ralbidv 2391	. . . . . 6 ⊢ (𝑎 = 𝑥 → (∀𝑦 ∈ ℝ (𝑎 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦) ↔ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))
8	4, 7	anbi12d 458	. . . . 5 ⊢ (𝑎 = 𝑥 → ((∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑎 ∧ ∀𝑦 ∈ ℝ (𝑎 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)) ↔ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))))
9	8	cbvrexv 2605	. . . 4 ⊢ (∃𝑎 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑎 ∧ ∀𝑦 ∈ ℝ (𝑎 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)) ↔ ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))
10	1, 9	sylibr 133	. . 3 ⊢ (𝜑 → ∃𝑎 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑎 ∧ ∀𝑦 ∈ ℝ (𝑎 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))
11		breq1 3870	. . . . . . 7 ⊢ (𝑏 = 𝑦 → (𝑏 < 𝑎 ↔ 𝑦 < 𝑎))
12	11	notbid 630	. . . . . 6 ⊢ (𝑏 = 𝑦 → (¬ 𝑏 < 𝑎 ↔ ¬ 𝑦 < 𝑎))
13	12	cbvralv 2604	. . . . 5 ⊢ (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 ↔ ∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑎)
14		breq1 3870	. . . . . . . . 9 ⊢ (𝑐 = 𝑧 → (𝑐 < 𝑏 ↔ 𝑧 < 𝑏))
15	14	cbvrexv 2605	. . . . . . . 8 ⊢ (∃𝑐 ∈ 𝐴 𝑐 < 𝑏 ↔ ∃𝑧 ∈ 𝐴 𝑧 < 𝑏)
16	15	imbi2i 225	. . . . . . 7 ⊢ ((𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏) ↔ (𝑎 < 𝑏 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑏))
17	16	ralbii 2395	. . . . . 6 ⊢ (∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏) ↔ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑏))
18		breq2 3871	. . . . . . . 8 ⊢ (𝑏 = 𝑦 → (𝑎 < 𝑏 ↔ 𝑎 < 𝑦))
19		breq2 3871	. . . . . . . . 9 ⊢ (𝑏 = 𝑦 → (𝑧 < 𝑏 ↔ 𝑧 < 𝑦))
20	19	rexbidv 2392	. . . . . . . 8 ⊢ (𝑏 = 𝑦 → (∃𝑧 ∈ 𝐴 𝑧 < 𝑏 ↔ ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))
21	18, 20	imbi12d 233	. . . . . . 7 ⊢ (𝑏 = 𝑦 → ((𝑎 < 𝑏 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑏) ↔ (𝑎 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))
22	21	cbvralv 2604	. . . . . 6 ⊢ (∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑏) ↔ ∀𝑦 ∈ ℝ (𝑎 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))
23	17, 22	bitri 183	. . . . 5 ⊢ (∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏) ↔ ∀𝑦 ∈ ℝ (𝑎 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))
24	13, 23	anbi12i 449	. . . 4 ⊢ ((∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ↔ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑎 ∧ ∀𝑦 ∈ ℝ (𝑎 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))
25	24	rexbii 2396	. . 3 ⊢ (∃𝑎 ∈ ℝ (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ↔ ∃𝑎 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑎 ∧ ∀𝑦 ∈ ℝ (𝑎 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))
26	10, 25	sylibr 133	. 2 ⊢ (𝜑 → ∃𝑎 ∈ ℝ (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)))
27		renegcl 7840	. . . . . 6 ⊢ (𝑎 ∈ ℝ → -𝑎 ∈ ℝ)
28	27	ad2antlr 474	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏))) → -𝑎 ∈ ℝ)
29		simplr 498	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏))) → 𝑎 ∈ ℝ)
30		simprl 499	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏))) → ∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎)
31		elrabi 2782	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} → 𝑦 ∈ ℝ)
32		negeq 7772	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑦 → -𝑤 = -𝑦)
33	32	eleq1d 2163	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑦 → (-𝑤 ∈ 𝐴 ↔ -𝑦 ∈ 𝐴))
34	33	elrab3 2786	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℝ → (𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ↔ -𝑦 ∈ 𝐴))
35	34	biimpd 143	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℝ → (𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} → -𝑦 ∈ 𝐴))
36	31, 35	mpcom 36	. . . . . . . . . . 11 ⊢ (𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} → -𝑦 ∈ 𝐴)
37		breq1 3870	. . . . . . . . . . . . 13 ⊢ (𝑏 = -𝑦 → (𝑏 < 𝑎 ↔ -𝑦 < 𝑎))
38	37	notbid 630	. . . . . . . . . . . 12 ⊢ (𝑏 = -𝑦 → (¬ 𝑏 < 𝑎 ↔ ¬ -𝑦 < 𝑎))
39	38	rspcv 2732	. . . . . . . . . . 11 ⊢ (-𝑦 ∈ 𝐴 → (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 → ¬ -𝑦 < 𝑎))
40	36, 39	syl 14	. . . . . . . . . 10 ⊢ (𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} → (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 → ¬ -𝑦 < 𝑎))
41	40	adantr 271	. . . . . . . . 9 ⊢ ((𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ∧ 𝑎 ∈ ℝ) → (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 → ¬ -𝑦 < 𝑎))
42		ltnegcon1 8038	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (-𝑎 < 𝑦 ↔ -𝑦 < 𝑎))
43	42	ancoms 265	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℝ ∧ 𝑎 ∈ ℝ) → (-𝑎 < 𝑦 ↔ -𝑦 < 𝑎))
44	43	notbid 630	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℝ ∧ 𝑎 ∈ ℝ) → (¬ -𝑎 < 𝑦 ↔ ¬ -𝑦 < 𝑎))
45	31, 44	sylan 278	. . . . . . . . 9 ⊢ ((𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ∧ 𝑎 ∈ ℝ) → (¬ -𝑎 < 𝑦 ↔ ¬ -𝑦 < 𝑎))
46	41, 45	sylibrd 168	. . . . . . . 8 ⊢ ((𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ∧ 𝑎 ∈ ℝ) → (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 → ¬ -𝑎 < 𝑦))
47	46	ancoms 265	. . . . . . 7 ⊢ ((𝑎 ∈ ℝ ∧ 𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}) → (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 → ¬ -𝑎 < 𝑦))
48	47	ralrimdva 2465	. . . . . 6 ⊢ (𝑎 ∈ ℝ → (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 → ∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ -𝑎 < 𝑦))
49	29, 30, 48	sylc 62	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏))) → ∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ -𝑎 < 𝑦)
50		nfv 1473	. . . . . . . . . . . 12 ⊢ Ⅎ𝑐(𝜑 ∧ 𝑎 ∈ ℝ)
51		nfcv 2235	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑐ℝ
52		nfv 1473	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑐 𝑎 < 𝑏
53		nfre1 2430	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑐∃𝑐 ∈ 𝐴 𝑐 < 𝑏
54	52, 53	nfim 1516	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑐(𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)
55	51, 54	nfralya 2427	. . . . . . . . . . . 12 ⊢ Ⅎ𝑐∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)
56	50, 55	nfan 1509	. . . . . . . . . . 11 ⊢ Ⅎ𝑐((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏))
57		nfv 1473	. . . . . . . . . . 11 ⊢ Ⅎ𝑐 𝑦 ∈ ℝ
58	56, 57	nfan 1509	. . . . . . . . . 10 ⊢ Ⅎ𝑐(((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ)
59		nfv 1473	. . . . . . . . . 10 ⊢ Ⅎ𝑐 𝑦 < -𝑎
60	58, 59	nfan 1509	. . . . . . . . 9 ⊢ Ⅎ𝑐((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎)
61		simplr 498	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎) ∧ 𝑐 ∈ 𝐴) ∧ 𝑐 < -𝑦) → 𝑐 ∈ 𝐴)
62		infsupneg.ss	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ⊆ ℝ)
63	62	sseld 3038	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑐 ∈ 𝐴 → 𝑐 ∈ ℝ))
64	63	ad6antr 483	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎) ∧ 𝑐 ∈ 𝐴) ∧ 𝑐 < -𝑦) → (𝑐 ∈ 𝐴 → 𝑐 ∈ ℝ))
65	61, 64	mpd 13	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎) ∧ 𝑐 ∈ 𝐴) ∧ 𝑐 < -𝑦) → 𝑐 ∈ ℝ)
66	65	renegcld 7955	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎) ∧ 𝑐 ∈ 𝐴) ∧ 𝑐 < -𝑦) → -𝑐 ∈ ℝ)
67	65	recnd 7613	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎) ∧ 𝑐 ∈ 𝐴) ∧ 𝑐 < -𝑦) → 𝑐 ∈ ℂ)
68	67	negnegd 7881	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎) ∧ 𝑐 ∈ 𝐴) ∧ 𝑐 < -𝑦) → --𝑐 = 𝑐)
69	68, 61	eqeltrd 2171	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎) ∧ 𝑐 ∈ 𝐴) ∧ 𝑐 < -𝑦) → --𝑐 ∈ 𝐴)
70		negeq 7772	. . . . . . . . . . . . 13 ⊢ (𝑤 = -𝑐 → -𝑤 = --𝑐)
71	70	eleq1d 2163	. . . . . . . . . . . 12 ⊢ (𝑤 = -𝑐 → (-𝑤 ∈ 𝐴 ↔ --𝑐 ∈ 𝐴))
72	71	elrab 2785	. . . . . . . . . . 11 ⊢ (-𝑐 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ↔ (-𝑐 ∈ ℝ ∧ --𝑐 ∈ 𝐴))
73	66, 69, 72	sylanbrc 409	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎) ∧ 𝑐 ∈ 𝐴) ∧ 𝑐 < -𝑦) → -𝑐 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴})
74		simp-4r 510	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎) ∧ 𝑐 ∈ 𝐴) ∧ 𝑐 < -𝑦) → 𝑦 ∈ ℝ)
75		simpr 109	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎) ∧ 𝑐 ∈ 𝐴) ∧ 𝑐 < -𝑦) → 𝑐 < -𝑦)
76	65, 74, 75	ltnegcon2d 8100	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎) ∧ 𝑐 ∈ 𝐴) ∧ 𝑐 < -𝑦) → 𝑦 < -𝑐)
77		breq2 3871	. . . . . . . . . . 11 ⊢ (𝑧 = -𝑐 → (𝑦 < 𝑧 ↔ 𝑦 < -𝑐))
78	77	rspcev 2736	. . . . . . . . . 10 ⊢ ((-𝑐 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ∧ 𝑦 < -𝑐) → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧)
79	73, 76, 78	syl2anc 404	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎) ∧ 𝑐 ∈ 𝐴) ∧ 𝑐 < -𝑦) → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧)
80		simpllr 502	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) → 𝑎 ∈ ℝ)
81		simpr 109	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
82		simplr 498	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) → ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏))
83	80, 81, 82	jca31 303	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) → ((𝑎 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)))
84		ltnegcon2 8039	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ ℝ ∧ 𝑎 ∈ ℝ) → (𝑦 < -𝑎 ↔ 𝑎 < -𝑦))
85	84	ancoms 265	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑦 < -𝑎 ↔ 𝑎 < -𝑦))
86	85	adantr 271	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) → (𝑦 < -𝑎 ↔ 𝑎 < -𝑦))
87		renegcl 7840	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℝ → -𝑦 ∈ ℝ)
88		breq2 3871	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = -𝑦 → (𝑎 < 𝑏 ↔ 𝑎 < -𝑦))
89		breq2 3871	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = -𝑦 → (𝑐 < 𝑏 ↔ 𝑐 < -𝑦))
90	89	rexbidv 2392	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = -𝑦 → (∃𝑐 ∈ 𝐴 𝑐 < 𝑏 ↔ ∃𝑐 ∈ 𝐴 𝑐 < -𝑦))
91	88, 90	imbi12d 233	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = -𝑦 → ((𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏) ↔ (𝑎 < -𝑦 → ∃𝑐 ∈ 𝐴 𝑐 < -𝑦)))
92	91	rspcv 2732	. . . . . . . . . . . . . . 15 ⊢ (-𝑦 ∈ ℝ → (∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏) → (𝑎 < -𝑦 → ∃𝑐 ∈ 𝐴 𝑐 < -𝑦)))
93	87, 92	syl 14	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℝ → (∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏) → (𝑎 < -𝑦 → ∃𝑐 ∈ 𝐴 𝑐 < -𝑦)))
94	93	adantl 272	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏) → (𝑎 < -𝑦 → ∃𝑐 ∈ 𝐴 𝑐 < -𝑦)))
95	94	imp 123	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) → (𝑎 < -𝑦 → ∃𝑐 ∈ 𝐴 𝑐 < -𝑦))
96	86, 95	sylbid 149	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) → (𝑦 < -𝑎 → ∃𝑐 ∈ 𝐴 𝑐 < -𝑦))
97	96	imp 123	. . . . . . . . . 10 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 < -𝑎) → ∃𝑐 ∈ 𝐴 𝑐 < -𝑦)
98	83, 97	sylan 278	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎) → ∃𝑐 ∈ 𝐴 𝑐 < -𝑦)
99	60, 79, 98	r19.29af 2523	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎) → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧)
100	99	ex 114	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) → (𝑦 < -𝑎 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧))
101	100	ralrimiva 2458	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) → ∀𝑦 ∈ ℝ (𝑦 < -𝑎 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧))
102	101	adantrl 463	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏))) → ∀𝑦 ∈ ℝ (𝑦 < -𝑎 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧))
103		breq1 3870	. . . . . . . . 9 ⊢ (𝑥 = -𝑎 → (𝑥 < 𝑦 ↔ -𝑎 < 𝑦))
104	103	notbid 630	. . . . . . . 8 ⊢ (𝑥 = -𝑎 → (¬ 𝑥 < 𝑦 ↔ ¬ -𝑎 < 𝑦))
105	104	ralbidv 2391	. . . . . . 7 ⊢ (𝑥 = -𝑎 → (∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑥 < 𝑦 ↔ ∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ -𝑎 < 𝑦))
106		breq2 3871	. . . . . . . . 9 ⊢ (𝑥 = -𝑎 → (𝑦 < 𝑥 ↔ 𝑦 < -𝑎))
107	106	imbi1d 230	. . . . . . . 8 ⊢ (𝑥 = -𝑎 → ((𝑦 < 𝑥 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧) ↔ (𝑦 < -𝑎 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧)))
108	107	ralbidv 2391	. . . . . . 7 ⊢ (𝑥 = -𝑎 → (∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧) ↔ ∀𝑦 ∈ ℝ (𝑦 < -𝑎 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧)))
109	105, 108	anbi12d 458	. . . . . 6 ⊢ (𝑥 = -𝑎 → ((∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧)) ↔ (∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ -𝑎 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < -𝑎 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧))))
110	109	rspcev 2736	. . . . 5 ⊢ ((-𝑎 ∈ ℝ ∧ (∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ -𝑎 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < -𝑎 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧))) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧)))
111	28, 49, 102, 110	syl12anc 1179	. . . 4 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏))) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧)))
112	111	ex 114	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → ((∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧))))
113	112	rexlimdva 2502	. 2 ⊢ (𝜑 → (∃𝑎 ∈ ℝ (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧))))
114	26, 113	mpd 13	1 ⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   = wceq 1296   ∈ wcel 1445  ∀wral 2370  ∃wrex 2371  {crab 2374   ⊆ wss 3013   class class class wbr 3867  ℝcr 7446   < clt 7619  -cneg 7751

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 582  ax-in2 583  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-13 1456  ax-14 1457  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077  ax-sep 3978  ax-pow 4030  ax-pr 4060  ax-un 4284  ax-setind 4381  ax-cnex 7533  ax-resscn 7534  ax-1cn 7535  ax-1re 7536  ax-icn 7537  ax-addcl 7538  ax-addrcl 7539  ax-mulcl 7540  ax-addcom 7542  ax-addass 7544  ax-distr 7546  ax-i2m1 7547  ax-0id 7550  ax-rnegex 7551  ax-cnre 7553  ax-pre-ltadd 7558

This theorem depends on definitions:  df-bi 116  df-3an 929  df-tru 1299  df-fal 1302  df-nf 1402  df-sb 1700  df-eu 1958  df-mo 1959  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-ne 2263  df-nel 2358  df-ral 2375  df-rex 2376  df-reu 2377  df-rab 2379  df-v 2635  df-sbc 2855  df-dif 3015  df-un 3017  df-in 3019  df-ss 3026  df-pw 3451  df-sn 3472  df-pr 3473  df-op 3475  df-uni 3676  df-br 3868  df-opab 3922  df-id 4144  df-xp 4473  df-rel 4474  df-cnv 4475  df-co 4476  df-dm 4477  df-iota 5014  df-fun 5051  df-fv 5057  df-riota 5646  df-ov 5693  df-oprab 5694  df-mpt2 5695  df-pnf 7621  df-mnf 7622  df-ltxr 7624  df-sub 7752  df-neg 7753

This theorem is referenced by:  infssuzcldc  11389