Theorem infsupneg 9820

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 9819. (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 4090	. . . . . . . 8 ⊢ (𝑎 = 𝑥 → (𝑦 < 𝑎 ↔ 𝑦 < 𝑥))
3	2	notbid 671	. . . . . . 7 ⊢ (𝑎 = 𝑥 → (¬ 𝑦 < 𝑎 ↔ ¬ 𝑦 < 𝑥))
4	3	ralbidv 2530	. . . . . 6 ⊢ (𝑎 = 𝑥 → (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑎 ↔ ∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥))
5		breq1 4089	. . . . . . . 8 ⊢ (𝑎 = 𝑥 → (𝑎 < 𝑦 ↔ 𝑥 < 𝑦))
6	5	imbi1d 231	. . . . . . 7 ⊢ (𝑎 = 𝑥 → ((𝑎 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦) ↔ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))
7	6	ralbidv 2530	. . . . . 6 ⊢ (𝑎 = 𝑥 → (∀𝑦 ∈ ℝ (𝑎 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦) ↔ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))
8	4, 7	anbi12d 473	. . . . 5 ⊢ (𝑎 = 𝑥 → ((∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑎 ∧ ∀𝑦 ∈ ℝ (𝑎 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)) ↔ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))))
9	8	cbvrexv 2766	. . . 4 ⊢ (∃𝑎 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑎 ∧ ∀𝑦 ∈ ℝ (𝑎 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)) ↔ ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))
10	1, 9	sylibr 134	. . 3 ⊢ (𝜑 → ∃𝑎 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑎 ∧ ∀𝑦 ∈ ℝ (𝑎 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))
11		breq1 4089	. . . . . . 7 ⊢ (𝑏 = 𝑦 → (𝑏 < 𝑎 ↔ 𝑦 < 𝑎))
12	11	notbid 671	. . . . . 6 ⊢ (𝑏 = 𝑦 → (¬ 𝑏 < 𝑎 ↔ ¬ 𝑦 < 𝑎))
13	12	cbvralv 2765	. . . . 5 ⊢ (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 ↔ ∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑎)
14		breq1 4089	. . . . . . . . 9 ⊢ (𝑐 = 𝑧 → (𝑐 < 𝑏 ↔ 𝑧 < 𝑏))
15	14	cbvrexv 2766	. . . . . . . 8 ⊢ (∃𝑐 ∈ 𝐴 𝑐 < 𝑏 ↔ ∃𝑧 ∈ 𝐴 𝑧 < 𝑏)
16	15	imbi2i 226	. . . . . . 7 ⊢ ((𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏) ↔ (𝑎 < 𝑏 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑏))
17	16	ralbii 2536	. . . . . 6 ⊢ (∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏) ↔ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑏))
18		breq2 4090	. . . . . . . 8 ⊢ (𝑏 = 𝑦 → (𝑎 < 𝑏 ↔ 𝑎 < 𝑦))
19		breq2 4090	. . . . . . . . 9 ⊢ (𝑏 = 𝑦 → (𝑧 < 𝑏 ↔ 𝑧 < 𝑦))
20	19	rexbidv 2531	. . . . . . . 8 ⊢ (𝑏 = 𝑦 → (∃𝑧 ∈ 𝐴 𝑧 < 𝑏 ↔ ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))
21	18, 20	imbi12d 234	. . . . . . 7 ⊢ (𝑏 = 𝑦 → ((𝑎 < 𝑏 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑏) ↔ (𝑎 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))
22	21	cbvralv 2765	. . . . . 6 ⊢ (∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑏) ↔ ∀𝑦 ∈ ℝ (𝑎 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))
23	17, 22	bitri 184	. . . . 5 ⊢ (∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏) ↔ ∀𝑦 ∈ ℝ (𝑎 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))
24	13, 23	anbi12i 460	. . . 4 ⊢ ((∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ↔ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑎 ∧ ∀𝑦 ∈ ℝ (𝑎 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))
25	24	rexbii 2537	. . 3 ⊢ (∃𝑎 ∈ ℝ (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ↔ ∃𝑎 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑎 ∧ ∀𝑦 ∈ ℝ (𝑎 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))
26	10, 25	sylibr 134	. 2 ⊢ (𝜑 → ∃𝑎 ∈ ℝ (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)))
27		renegcl 8430	. . . . . 6 ⊢ (𝑎 ∈ ℝ → -𝑎 ∈ ℝ)
28	27	ad2antlr 489	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏))) → -𝑎 ∈ ℝ)
29		simplr 528	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏))) → 𝑎 ∈ ℝ)
30		simprl 529	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏))) → ∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎)
31		elrabi 2957	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} → 𝑦 ∈ ℝ)
32		negeq 8362	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑦 → -𝑤 = -𝑦)
33	32	eleq1d 2298	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑦 → (-𝑤 ∈ 𝐴 ↔ -𝑦 ∈ 𝐴))
34	33	elrab3 2961	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℝ → (𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ↔ -𝑦 ∈ 𝐴))
35	34	biimpd 144	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℝ → (𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} → -𝑦 ∈ 𝐴))
36	31, 35	mpcom 36	. . . . . . . . . . 11 ⊢ (𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} → -𝑦 ∈ 𝐴)
37		breq1 4089	. . . . . . . . . . . . 13 ⊢ (𝑏 = -𝑦 → (𝑏 < 𝑎 ↔ -𝑦 < 𝑎))
38	37	notbid 671	. . . . . . . . . . . 12 ⊢ (𝑏 = -𝑦 → (¬ 𝑏 < 𝑎 ↔ ¬ -𝑦 < 𝑎))
39	38	rspcv 2904	. . . . . . . . . . 11 ⊢ (-𝑦 ∈ 𝐴 → (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 → ¬ -𝑦 < 𝑎))
40	36, 39	syl 14	. . . . . . . . . 10 ⊢ (𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} → (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 → ¬ -𝑦 < 𝑎))
41	40	adantr 276	. . . . . . . . 9 ⊢ ((𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ∧ 𝑎 ∈ ℝ) → (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 → ¬ -𝑦 < 𝑎))
42		ltnegcon1 8633	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (-𝑎 < 𝑦 ↔ -𝑦 < 𝑎))
43	42	ancoms 268	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℝ ∧ 𝑎 ∈ ℝ) → (-𝑎 < 𝑦 ↔ -𝑦 < 𝑎))
44	43	notbid 671	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℝ ∧ 𝑎 ∈ ℝ) → (¬ -𝑎 < 𝑦 ↔ ¬ -𝑦 < 𝑎))
45	31, 44	sylan 283	. . . . . . . . 9 ⊢ ((𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ∧ 𝑎 ∈ ℝ) → (¬ -𝑎 < 𝑦 ↔ ¬ -𝑦 < 𝑎))
46	41, 45	sylibrd 169	. . . . . . . 8 ⊢ ((𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ∧ 𝑎 ∈ ℝ) → (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 → ¬ -𝑎 < 𝑦))
47	46	ancoms 268	. . . . . . 7 ⊢ ((𝑎 ∈ ℝ ∧ 𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}) → (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 → ¬ -𝑎 < 𝑦))
48	47	ralrimdva 2610	. . . . . 6 ⊢ (𝑎 ∈ ℝ → (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 → ∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ -𝑎 < 𝑦))
49	29, 30, 48	sylc 62	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏))) → ∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ -𝑎 < 𝑦)
50		nfv 1574	. . . . . . . . . . . 12 ⊢ Ⅎ𝑐(𝜑 ∧ 𝑎 ∈ ℝ)
51		nfcv 2372	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑐ℝ
52		nfv 1574	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑐 𝑎 < 𝑏
53		nfre1 2573	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑐∃𝑐 ∈ 𝐴 𝑐 < 𝑏
54	52, 53	nfim 1618	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑐(𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)
55	51, 54	nfralya 2570	. . . . . . . . . . . 12 ⊢ Ⅎ𝑐∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)
56	50, 55	nfan 1611	. . . . . . . . . . 11 ⊢ Ⅎ𝑐((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏))
57		nfv 1574	. . . . . . . . . . 11 ⊢ Ⅎ𝑐 𝑦 ∈ ℝ
58	56, 57	nfan 1611	. . . . . . . . . 10 ⊢ Ⅎ𝑐(((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ)
59		nfv 1574	. . . . . . . . . 10 ⊢ Ⅎ𝑐 𝑦 < -𝑎
60	58, 59	nfan 1611	. . . . . . . . 9 ⊢ Ⅎ𝑐((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎)
61		simplr 528	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎) ∧ 𝑐 ∈ 𝐴) ∧ 𝑐 < -𝑦) → 𝑐 ∈ 𝐴)
62		infsupneg.ss	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ⊆ ℝ)
63	62	sseld 3224	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑐 ∈ 𝐴 → 𝑐 ∈ ℝ))
64	63	ad6antr 498	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎) ∧ 𝑐 ∈ 𝐴) ∧ 𝑐 < -𝑦) → (𝑐 ∈ 𝐴 → 𝑐 ∈ ℝ))
65	61, 64	mpd 13	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎) ∧ 𝑐 ∈ 𝐴) ∧ 𝑐 < -𝑦) → 𝑐 ∈ ℝ)
66	65	renegcld 8549	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎) ∧ 𝑐 ∈ 𝐴) ∧ 𝑐 < -𝑦) → -𝑐 ∈ ℝ)
67	65	recnd 8198	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎) ∧ 𝑐 ∈ 𝐴) ∧ 𝑐 < -𝑦) → 𝑐 ∈ ℂ)
68	67	negnegd 8471	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎) ∧ 𝑐 ∈ 𝐴) ∧ 𝑐 < -𝑦) → --𝑐 = 𝑐)
69	68, 61	eqeltrd 2306	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎) ∧ 𝑐 ∈ 𝐴) ∧ 𝑐 < -𝑦) → --𝑐 ∈ 𝐴)
70		negeq 8362	. . . . . . . . . . . . 13 ⊢ (𝑤 = -𝑐 → -𝑤 = --𝑐)
71	70	eleq1d 2298	. . . . . . . . . . . 12 ⊢ (𝑤 = -𝑐 → (-𝑤 ∈ 𝐴 ↔ --𝑐 ∈ 𝐴))
72	71	elrab 2960	. . . . . . . . . . 11 ⊢ (-𝑐 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ↔ (-𝑐 ∈ ℝ ∧ --𝑐 ∈ 𝐴))
73	66, 69, 72	sylanbrc 417	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎) ∧ 𝑐 ∈ 𝐴) ∧ 𝑐 < -𝑦) → -𝑐 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴})
74		simp-4r 542	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎) ∧ 𝑐 ∈ 𝐴) ∧ 𝑐 < -𝑦) → 𝑦 ∈ ℝ)
75		simpr 110	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎) ∧ 𝑐 ∈ 𝐴) ∧ 𝑐 < -𝑦) → 𝑐 < -𝑦)
76	65, 74, 75	ltnegcon2d 8696	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎) ∧ 𝑐 ∈ 𝐴) ∧ 𝑐 < -𝑦) → 𝑦 < -𝑐)
77		breq2 4090	. . . . . . . . . . 11 ⊢ (𝑧 = -𝑐 → (𝑦 < 𝑧 ↔ 𝑦 < -𝑐))
78	77	rspcev 2908	. . . . . . . . . 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 8634	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ ℝ ∧ 𝑎 ∈ ℝ) → (𝑦 < -𝑎 ↔ 𝑎 < -𝑦))
85	84	ancoms 268	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑦 < -𝑎 ↔ 𝑎 < -𝑦))
86	85	adantr 276	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) → (𝑦 < -𝑎 ↔ 𝑎 < -𝑦))
87		renegcl 8430	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℝ → -𝑦 ∈ ℝ)
88		breq2 4090	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = -𝑦 → (𝑎 < 𝑏 ↔ 𝑎 < -𝑦))
89		breq2 4090	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = -𝑦 → (𝑐 < 𝑏 ↔ 𝑐 < -𝑦))
90	89	rexbidv 2531	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = -𝑦 → (∃𝑐 ∈ 𝐴 𝑐 < 𝑏 ↔ ∃𝑐 ∈ 𝐴 𝑐 < -𝑦))
91	88, 90	imbi12d 234	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = -𝑦 → ((𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏) ↔ (𝑎 < -𝑦 → ∃𝑐 ∈ 𝐴 𝑐 < -𝑦)))
92	91	rspcv 2904	. . . . . . . . . . . . . . 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 2672	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎) → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧)
100	99	ex 115	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) → (𝑦 < -𝑎 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧))
101	100	ralrimiva 2603	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) → ∀𝑦 ∈ ℝ (𝑦 < -𝑎 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧))
102	101	adantrl 478	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏))) → ∀𝑦 ∈ ℝ (𝑦 < -𝑎 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧))
103		breq1 4089	. . . . . . . . 9 ⊢ (𝑥 = -𝑎 → (𝑥 < 𝑦 ↔ -𝑎 < 𝑦))
104	103	notbid 671	. . . . . . . 8 ⊢ (𝑥 = -𝑎 → (¬ 𝑥 < 𝑦 ↔ ¬ -𝑎 < 𝑦))
105	104	ralbidv 2530	. . . . . . 7 ⊢ (𝑥 = -𝑎 → (∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑥 < 𝑦 ↔ ∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ -𝑎 < 𝑦))
106		breq2 4090	. . . . . . . . 9 ⊢ (𝑥 = -𝑎 → (𝑦 < 𝑥 ↔ 𝑦 < -𝑎))
107	106	imbi1d 231	. . . . . . . 8 ⊢ (𝑥 = -𝑎 → ((𝑦 < 𝑥 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧) ↔ (𝑦 < -𝑎 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧)))
108	107	ralbidv 2530	. . . . . . 7 ⊢ (𝑥 = -𝑎 → (∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧) ↔ ∀𝑦 ∈ ℝ (𝑦 < -𝑎 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧)))
109	105, 108	anbi12d 473	. . . . . 6 ⊢ (𝑥 = -𝑎 → ((∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧)) ↔ (∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ -𝑎 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < -𝑎 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧))))
110	109	rspcev 2908	. . . . 5 ⊢ ((-𝑎 ∈ ℝ ∧ (∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ -𝑎 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < -𝑎 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧))) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧)))
111	28, 49, 102, 110	syl12anc 1269	. . . 4 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏))) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧)))
112	111	ex 115	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → ((∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧))))
113	112	rexlimdva 2648	. 2 ⊢ (𝜑 → (∃𝑎 ∈ ℝ (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧))))
114	26, 113	mpd 13	1 ⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1395   ∈ wcel 2200  ∀wral 2508  ∃wrex 2509  {crab 2512   ⊆ wss 3198   class class class wbr 4086  ℝcr 8021   < clt 8204  -cneg 8341

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 617  ax-in2 618  ax-io 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-13 2202  ax-14 2203  ax-ext 2211  ax-sep 4205  ax-pow 4262  ax-pr 4297  ax-un 4528  ax-setind 4633  ax-cnex 8113  ax-resscn 8114  ax-1cn 8115  ax-1re 8116  ax-icn 8117  ax-addcl 8118  ax-addrcl 8119  ax-mulcl 8120  ax-addcom 8122  ax-addass 8124  ax-distr 8126  ax-i2m1 8127  ax-0id 8130  ax-rnegex 8131  ax-cnre 8133  ax-pre-ltadd 8138

This theorem depends on definitions:  df-bi 117  df-3an 1004  df-tru 1398  df-fal 1401  df-nf 1507  df-sb 1809  df-eu 2080  df-mo 2081  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ne 2401  df-nel 2496  df-ral 2513  df-rex 2514  df-reu 2515  df-rab 2517  df-v 2802  df-sbc 3030  df-dif 3200  df-un 3202  df-in 3204  df-ss 3211  df-pw 3652  df-sn 3673  df-pr 3674  df-op 3676  df-uni 3892  df-br 4087  df-opab 4149  df-id 4388  df-xp 4729  df-rel 4730  df-cnv 4731  df-co 4732  df-dm 4733  df-iota 5284  df-fun 5326  df-fv 5332  df-riota 5966  df-ov 6016  df-oprab 6017  df-mpo 6018  df-pnf 8206  df-mnf 8207  df-ltxr 8209  df-sub 8342  df-neg 8343

This theorem is referenced by:  infssuzcldc  10485