Theorem infsupneg 9609

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 9608. (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 4019	. . . . . . . 8 ⊢ (𝑎 = 𝑥 → (𝑦 < 𝑎 ↔ 𝑦 < 𝑥))
3	2	notbid 668	. . . . . . 7 ⊢ (𝑎 = 𝑥 → (¬ 𝑦 < 𝑎 ↔ ¬ 𝑦 < 𝑥))
4	3	ralbidv 2487	. . . . . 6 ⊢ (𝑎 = 𝑥 → (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑎 ↔ ∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥))
5		breq1 4018	. . . . . . . 8 ⊢ (𝑎 = 𝑥 → (𝑎 < 𝑦 ↔ 𝑥 < 𝑦))
6	5	imbi1d 231	. . . . . . 7 ⊢ (𝑎 = 𝑥 → ((𝑎 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦) ↔ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))
7	6	ralbidv 2487	. . . . . 6 ⊢ (𝑎 = 𝑥 → (∀𝑦 ∈ ℝ (𝑎 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦) ↔ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))
8	4, 7	anbi12d 473	. . . . 5 ⊢ (𝑎 = 𝑥 → ((∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑎 ∧ ∀𝑦 ∈ ℝ (𝑎 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)) ↔ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))))
9	8	cbvrexv 2716	. . . 4 ⊢ (∃𝑎 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑎 ∧ ∀𝑦 ∈ ℝ (𝑎 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)) ↔ ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))
10	1, 9	sylibr 134	. . 3 ⊢ (𝜑 → ∃𝑎 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑎 ∧ ∀𝑦 ∈ ℝ (𝑎 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))
11		breq1 4018	. . . . . . 7 ⊢ (𝑏 = 𝑦 → (𝑏 < 𝑎 ↔ 𝑦 < 𝑎))
12	11	notbid 668	. . . . . 6 ⊢ (𝑏 = 𝑦 → (¬ 𝑏 < 𝑎 ↔ ¬ 𝑦 < 𝑎))
13	12	cbvralv 2715	. . . . 5 ⊢ (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 ↔ ∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑎)
14		breq1 4018	. . . . . . . . 9 ⊢ (𝑐 = 𝑧 → (𝑐 < 𝑏 ↔ 𝑧 < 𝑏))
15	14	cbvrexv 2716	. . . . . . . 8 ⊢ (∃𝑐 ∈ 𝐴 𝑐 < 𝑏 ↔ ∃𝑧 ∈ 𝐴 𝑧 < 𝑏)
16	15	imbi2i 226	. . . . . . 7 ⊢ ((𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏) ↔ (𝑎 < 𝑏 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑏))
17	16	ralbii 2493	. . . . . 6 ⊢ (∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏) ↔ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑏))
18		breq2 4019	. . . . . . . 8 ⊢ (𝑏 = 𝑦 → (𝑎 < 𝑏 ↔ 𝑎 < 𝑦))
19		breq2 4019	. . . . . . . . 9 ⊢ (𝑏 = 𝑦 → (𝑧 < 𝑏 ↔ 𝑧 < 𝑦))
20	19	rexbidv 2488	. . . . . . . 8 ⊢ (𝑏 = 𝑦 → (∃𝑧 ∈ 𝐴 𝑧 < 𝑏 ↔ ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))
21	18, 20	imbi12d 234	. . . . . . 7 ⊢ (𝑏 = 𝑦 → ((𝑎 < 𝑏 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑏) ↔ (𝑎 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))
22	21	cbvralv 2715	. . . . . 6 ⊢ (∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑏) ↔ ∀𝑦 ∈ ℝ (𝑎 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))
23	17, 22	bitri 184	. . . . 5 ⊢ (∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏) ↔ ∀𝑦 ∈ ℝ (𝑎 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))
24	13, 23	anbi12i 460	. . . 4 ⊢ ((∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ↔ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑎 ∧ ∀𝑦 ∈ ℝ (𝑎 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))
25	24	rexbii 2494	. . 3 ⊢ (∃𝑎 ∈ ℝ (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ↔ ∃𝑎 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑎 ∧ ∀𝑦 ∈ ℝ (𝑎 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))
26	10, 25	sylibr 134	. 2 ⊢ (𝜑 → ∃𝑎 ∈ ℝ (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)))
27		renegcl 8231	. . . . . 6 ⊢ (𝑎 ∈ ℝ → -𝑎 ∈ ℝ)
28	27	ad2antlr 489	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏))) → -𝑎 ∈ ℝ)
29		simplr 528	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏))) → 𝑎 ∈ ℝ)
30		simprl 529	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏))) → ∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎)
31		elrabi 2902	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} → 𝑦 ∈ ℝ)
32		negeq 8163	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑦 → -𝑤 = -𝑦)
33	32	eleq1d 2256	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑦 → (-𝑤 ∈ 𝐴 ↔ -𝑦 ∈ 𝐴))
34	33	elrab3 2906	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℝ → (𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ↔ -𝑦 ∈ 𝐴))
35	34	biimpd 144	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℝ → (𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} → -𝑦 ∈ 𝐴))
36	31, 35	mpcom 36	. . . . . . . . . . 11 ⊢ (𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} → -𝑦 ∈ 𝐴)
37		breq1 4018	. . . . . . . . . . . . 13 ⊢ (𝑏 = -𝑦 → (𝑏 < 𝑎 ↔ -𝑦 < 𝑎))
38	37	notbid 668	. . . . . . . . . . . 12 ⊢ (𝑏 = -𝑦 → (¬ 𝑏 < 𝑎 ↔ ¬ -𝑦 < 𝑎))
39	38	rspcv 2849	. . . . . . . . . . 11 ⊢ (-𝑦 ∈ 𝐴 → (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 → ¬ -𝑦 < 𝑎))
40	36, 39	syl 14	. . . . . . . . . 10 ⊢ (𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} → (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 → ¬ -𝑦 < 𝑎))
41	40	adantr 276	. . . . . . . . 9 ⊢ ((𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ∧ 𝑎 ∈ ℝ) → (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 → ¬ -𝑦 < 𝑎))
42		ltnegcon1 8433	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (-𝑎 < 𝑦 ↔ -𝑦 < 𝑎))
43	42	ancoms 268	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℝ ∧ 𝑎 ∈ ℝ) → (-𝑎 < 𝑦 ↔ -𝑦 < 𝑎))
44	43	notbid 668	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℝ ∧ 𝑎 ∈ ℝ) → (¬ -𝑎 < 𝑦 ↔ ¬ -𝑦 < 𝑎))
45	31, 44	sylan 283	. . . . . . . . 9 ⊢ ((𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ∧ 𝑎 ∈ ℝ) → (¬ -𝑎 < 𝑦 ↔ ¬ -𝑦 < 𝑎))
46	41, 45	sylibrd 169	. . . . . . . 8 ⊢ ((𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ∧ 𝑎 ∈ ℝ) → (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 → ¬ -𝑎 < 𝑦))
47	46	ancoms 268	. . . . . . 7 ⊢ ((𝑎 ∈ ℝ ∧ 𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}) → (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 → ¬ -𝑎 < 𝑦))
48	47	ralrimdva 2567	. . . . . 6 ⊢ (𝑎 ∈ ℝ → (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 → ∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ -𝑎 < 𝑦))
49	29, 30, 48	sylc 62	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏))) → ∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ -𝑎 < 𝑦)
50		nfv 1538	. . . . . . . . . . . 12 ⊢ Ⅎ𝑐(𝜑 ∧ 𝑎 ∈ ℝ)
51		nfcv 2329	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑐ℝ
52		nfv 1538	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑐 𝑎 < 𝑏
53		nfre1 2530	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑐∃𝑐 ∈ 𝐴 𝑐 < 𝑏
54	52, 53	nfim 1582	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑐(𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)
55	51, 54	nfralya 2527	. . . . . . . . . . . 12 ⊢ Ⅎ𝑐∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)
56	50, 55	nfan 1575	. . . . . . . . . . 11 ⊢ Ⅎ𝑐((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏))
57		nfv 1538	. . . . . . . . . . 11 ⊢ Ⅎ𝑐 𝑦 ∈ ℝ
58	56, 57	nfan 1575	. . . . . . . . . 10 ⊢ Ⅎ𝑐(((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ)
59		nfv 1538	. . . . . . . . . 10 ⊢ Ⅎ𝑐 𝑦 < -𝑎
60	58, 59	nfan 1575	. . . . . . . . 9 ⊢ Ⅎ𝑐((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎)
61		simplr 528	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎) ∧ 𝑐 ∈ 𝐴) ∧ 𝑐 < -𝑦) → 𝑐 ∈ 𝐴)
62		infsupneg.ss	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ⊆ ℝ)
63	62	sseld 3166	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑐 ∈ 𝐴 → 𝑐 ∈ ℝ))
64	63	ad6antr 498	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎) ∧ 𝑐 ∈ 𝐴) ∧ 𝑐 < -𝑦) → (𝑐 ∈ 𝐴 → 𝑐 ∈ ℝ))
65	61, 64	mpd 13	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎) ∧ 𝑐 ∈ 𝐴) ∧ 𝑐 < -𝑦) → 𝑐 ∈ ℝ)
66	65	renegcld 8350	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎) ∧ 𝑐 ∈ 𝐴) ∧ 𝑐 < -𝑦) → -𝑐 ∈ ℝ)
67	65	recnd 7999	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎) ∧ 𝑐 ∈ 𝐴) ∧ 𝑐 < -𝑦) → 𝑐 ∈ ℂ)
68	67	negnegd 8272	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎) ∧ 𝑐 ∈ 𝐴) ∧ 𝑐 < -𝑦) → --𝑐 = 𝑐)
69	68, 61	eqeltrd 2264	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎) ∧ 𝑐 ∈ 𝐴) ∧ 𝑐 < -𝑦) → --𝑐 ∈ 𝐴)
70		negeq 8163	. . . . . . . . . . . . 13 ⊢ (𝑤 = -𝑐 → -𝑤 = --𝑐)
71	70	eleq1d 2256	. . . . . . . . . . . 12 ⊢ (𝑤 = -𝑐 → (-𝑤 ∈ 𝐴 ↔ --𝑐 ∈ 𝐴))
72	71	elrab 2905	. . . . . . . . . . 11 ⊢ (-𝑐 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ↔ (-𝑐 ∈ ℝ ∧ --𝑐 ∈ 𝐴))
73	66, 69, 72	sylanbrc 417	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎) ∧ 𝑐 ∈ 𝐴) ∧ 𝑐 < -𝑦) → -𝑐 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴})
74		simp-4r 542	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎) ∧ 𝑐 ∈ 𝐴) ∧ 𝑐 < -𝑦) → 𝑦 ∈ ℝ)
75		simpr 110	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎) ∧ 𝑐 ∈ 𝐴) ∧ 𝑐 < -𝑦) → 𝑐 < -𝑦)
76	65, 74, 75	ltnegcon2d 8496	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎) ∧ 𝑐 ∈ 𝐴) ∧ 𝑐 < -𝑦) → 𝑦 < -𝑐)
77		breq2 4019	. . . . . . . . . . 11 ⊢ (𝑧 = -𝑐 → (𝑦 < 𝑧 ↔ 𝑦 < -𝑐))
78	77	rspcev 2853	. . . . . . . . . 10 ⊢ ((-𝑐 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ∧ 𝑦 < -𝑐) → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧)
79	73, 76, 78	syl2anc 411	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎) ∧ 𝑐 ∈ 𝐴) ∧ 𝑐 < -𝑦) → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧)
80		simpllr 534	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) → 𝑎 ∈ ℝ)
81		simpr 110	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
82		simplr 528	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) → ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏))
83	80, 81, 82	jca31 309	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) → ((𝑎 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)))
84		ltnegcon2 8434	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ ℝ ∧ 𝑎 ∈ ℝ) → (𝑦 < -𝑎 ↔ 𝑎 < -𝑦))
85	84	ancoms 268	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑦 < -𝑎 ↔ 𝑎 < -𝑦))
86	85	adantr 276	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) → (𝑦 < -𝑎 ↔ 𝑎 < -𝑦))
87		renegcl 8231	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℝ → -𝑦 ∈ ℝ)
88		breq2 4019	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = -𝑦 → (𝑎 < 𝑏 ↔ 𝑎 < -𝑦))
89		breq2 4019	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = -𝑦 → (𝑐 < 𝑏 ↔ 𝑐 < -𝑦))
90	89	rexbidv 2488	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = -𝑦 → (∃𝑐 ∈ 𝐴 𝑐 < 𝑏 ↔ ∃𝑐 ∈ 𝐴 𝑐 < -𝑦))
91	88, 90	imbi12d 234	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = -𝑦 → ((𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏) ↔ (𝑎 < -𝑦 → ∃𝑐 ∈ 𝐴 𝑐 < -𝑦)))
92	91	rspcv 2849	. . . . . . . . . . . . . . 15 ⊢ (-𝑦 ∈ ℝ → (∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏) → (𝑎 < -𝑦 → ∃𝑐 ∈ 𝐴 𝑐 < -𝑦)))
93	87, 92	syl 14	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℝ → (∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏) → (𝑎 < -𝑦 → ∃𝑐 ∈ 𝐴 𝑐 < -𝑦)))
94	93	adantl 277	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏) → (𝑎 < -𝑦 → ∃𝑐 ∈ 𝐴 𝑐 < -𝑦)))
95	94	imp 124	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) → (𝑎 < -𝑦 → ∃𝑐 ∈ 𝐴 𝑐 < -𝑦))
96	86, 95	sylbid 150	. . . . . . . . . . 11 ⊢ (((𝑎 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) → (𝑦 < -𝑎 → ∃𝑐 ∈ 𝐴 𝑐 < -𝑦))
97	96	imp 124	. . . . . . . . . 10 ⊢ ((((𝑎 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 < -𝑎) → ∃𝑐 ∈ 𝐴 𝑐 < -𝑦)
98	83, 97	sylan 283	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎) → ∃𝑐 ∈ 𝐴 𝑐 < -𝑦)
99	60, 79, 98	r19.29af 2628	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎) → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧)
100	99	ex 115	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) → (𝑦 < -𝑎 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧))
101	100	ralrimiva 2560	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) → ∀𝑦 ∈ ℝ (𝑦 < -𝑎 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧))
102	101	adantrl 478	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏))) → ∀𝑦 ∈ ℝ (𝑦 < -𝑎 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧))
103		breq1 4018	. . . . . . . . 9 ⊢ (𝑥 = -𝑎 → (𝑥 < 𝑦 ↔ -𝑎 < 𝑦))
104	103	notbid 668	. . . . . . . 8 ⊢ (𝑥 = -𝑎 → (¬ 𝑥 < 𝑦 ↔ ¬ -𝑎 < 𝑦))
105	104	ralbidv 2487	. . . . . . 7 ⊢ (𝑥 = -𝑎 → (∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑥 < 𝑦 ↔ ∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ -𝑎 < 𝑦))
106		breq2 4019	. . . . . . . . 9 ⊢ (𝑥 = -𝑎 → (𝑦 < 𝑥 ↔ 𝑦 < -𝑎))
107	106	imbi1d 231	. . . . . . . 8 ⊢ (𝑥 = -𝑎 → ((𝑦 < 𝑥 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧) ↔ (𝑦 < -𝑎 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧)))
108	107	ralbidv 2487	. . . . . . 7 ⊢ (𝑥 = -𝑎 → (∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧) ↔ ∀𝑦 ∈ ℝ (𝑦 < -𝑎 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧)))
109	105, 108	anbi12d 473	. . . . . 6 ⊢ (𝑥 = -𝑎 → ((∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧)) ↔ (∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ -𝑎 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < -𝑎 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧))))
110	109	rspcev 2853	. . . . 5 ⊢ ((-𝑎 ∈ ℝ ∧ (∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ -𝑎 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < -𝑎 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧))) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧)))
111	28, 49, 102, 110	syl12anc 1246	. . . 4 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏))) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧)))
112	111	ex 115	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → ((∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧))))
113	112	rexlimdva 2604	. 2 ⊢ (𝜑 → (∃𝑎 ∈ ℝ (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧))))
114	26, 113	mpd 13	1 ⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1363   ∈ wcel 2158  ∀wral 2465  ∃wrex 2466  {crab 2469   ⊆ wss 3141   class class class wbr 4015  ℝcr 7823   < clt 8005  -cneg 8142

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-13 2160  ax-14 2161  ax-ext 2169  ax-sep 4133  ax-pow 4186  ax-pr 4221  ax-un 4445  ax-setind 4548  ax-cnex 7915  ax-resscn 7916  ax-1cn 7917  ax-1re 7918  ax-icn 7919  ax-addcl 7920  ax-addrcl 7921  ax-mulcl 7922  ax-addcom 7924  ax-addass 7926  ax-distr 7928  ax-i2m1 7929  ax-0id 7932  ax-rnegex 7933  ax-cnre 7935  ax-pre-ltadd 7940

This theorem depends on definitions:  df-bi 117  df-3an 981  df-tru 1366  df-fal 1369  df-nf 1471  df-sb 1773  df-eu 2039  df-mo 2040  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-ne 2358  df-nel 2453  df-ral 2470  df-rex 2471  df-reu 2472  df-rab 2474  df-v 2751  df-sbc 2975  df-dif 3143  df-un 3145  df-in 3147  df-ss 3154  df-pw 3589  df-sn 3610  df-pr 3611  df-op 3613  df-uni 3822  df-br 4016  df-opab 4077  df-id 4305  df-xp 4644  df-rel 4645  df-cnv 4646  df-co 4647  df-dm 4648  df-iota 5190  df-fun 5230  df-fv 5236  df-riota 5844  df-ov 5891  df-oprab 5892  df-mpo 5893  df-pnf 8007  df-mnf 8008  df-ltxr 8010  df-sub 8143  df-neg 8144

This theorem is referenced by:  infssuzcldc  11965