Theorem infsupneg 9891

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 9890. (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 4097	. . . . . . . 8 ⊢ (𝑎 = 𝑥 → (𝑦 < 𝑎 ↔ 𝑦 < 𝑥))
3	2	notbid 673	. . . . . . 7 ⊢ (𝑎 = 𝑥 → (¬ 𝑦 < 𝑎 ↔ ¬ 𝑦 < 𝑥))
4	3	ralbidv 2533	. . . . . 6 ⊢ (𝑎 = 𝑥 → (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑎 ↔ ∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥))
5		breq1 4096	. . . . . . . 8 ⊢ (𝑎 = 𝑥 → (𝑎 < 𝑦 ↔ 𝑥 < 𝑦))
6	5	imbi1d 231	. . . . . . 7 ⊢ (𝑎 = 𝑥 → ((𝑎 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦) ↔ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))
7	6	ralbidv 2533	. . . . . 6 ⊢ (𝑎 = 𝑥 → (∀𝑦 ∈ ℝ (𝑎 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦) ↔ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))
8	4, 7	anbi12d 473	. . . . 5 ⊢ (𝑎 = 𝑥 → ((∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑎 ∧ ∀𝑦 ∈ ℝ (𝑎 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)) ↔ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))))
9	8	cbvrexv 2769	. . . 4 ⊢ (∃𝑎 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑎 ∧ ∀𝑦 ∈ ℝ (𝑎 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)) ↔ ∃𝑥 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀𝑦 ∈ ℝ (𝑥 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))
10	1, 9	sylibr 134	. . 3 ⊢ (𝜑 → ∃𝑎 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑎 ∧ ∀𝑦 ∈ ℝ (𝑎 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))
11		breq1 4096	. . . . . . 7 ⊢ (𝑏 = 𝑦 → (𝑏 < 𝑎 ↔ 𝑦 < 𝑎))
12	11	notbid 673	. . . . . 6 ⊢ (𝑏 = 𝑦 → (¬ 𝑏 < 𝑎 ↔ ¬ 𝑦 < 𝑎))
13	12	cbvralv 2768	. . . . 5 ⊢ (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 ↔ ∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑎)
14		breq1 4096	. . . . . . . . 9 ⊢ (𝑐 = 𝑧 → (𝑐 < 𝑏 ↔ 𝑧 < 𝑏))
15	14	cbvrexv 2769	. . . . . . . 8 ⊢ (∃𝑐 ∈ 𝐴 𝑐 < 𝑏 ↔ ∃𝑧 ∈ 𝐴 𝑧 < 𝑏)
16	15	imbi2i 226	. . . . . . 7 ⊢ ((𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏) ↔ (𝑎 < 𝑏 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑏))
17	16	ralbii 2539	. . . . . 6 ⊢ (∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏) ↔ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑏))
18		breq2 4097	. . . . . . . 8 ⊢ (𝑏 = 𝑦 → (𝑎 < 𝑏 ↔ 𝑎 < 𝑦))
19		breq2 4097	. . . . . . . . 9 ⊢ (𝑏 = 𝑦 → (𝑧 < 𝑏 ↔ 𝑧 < 𝑦))
20	19	rexbidv 2534	. . . . . . . 8 ⊢ (𝑏 = 𝑦 → (∃𝑧 ∈ 𝐴 𝑧 < 𝑏 ↔ ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))
21	18, 20	imbi12d 234	. . . . . . 7 ⊢ (𝑏 = 𝑦 → ((𝑎 < 𝑏 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑏) ↔ (𝑎 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))
22	21	cbvralv 2768	. . . . . 6 ⊢ (∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑏) ↔ ∀𝑦 ∈ ℝ (𝑎 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))
23	17, 22	bitri 184	. . . . 5 ⊢ (∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏) ↔ ∀𝑦 ∈ ℝ (𝑎 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦))
24	13, 23	anbi12i 460	. . . 4 ⊢ ((∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ↔ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑎 ∧ ∀𝑦 ∈ ℝ (𝑎 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))
25	24	rexbii 2540	. . 3 ⊢ (∃𝑎 ∈ ℝ (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ↔ ∃𝑎 ∈ ℝ (∀𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑎 ∧ ∀𝑦 ∈ ℝ (𝑎 < 𝑦 → ∃𝑧 ∈ 𝐴 𝑧 < 𝑦)))
26	10, 25	sylibr 134	. 2 ⊢ (𝜑 → ∃𝑎 ∈ ℝ (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)))
27		renegcl 8499	. . . . . 6 ⊢ (𝑎 ∈ ℝ → -𝑎 ∈ ℝ)
28	27	ad2antlr 489	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏))) → -𝑎 ∈ ℝ)
29		simplr 529	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏))) → 𝑎 ∈ ℝ)
30		simprl 531	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏))) → ∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎)
31		elrabi 2960	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} → 𝑦 ∈ ℝ)
32		negeq 8431	. . . . . . . . . . . . . . 15 ⊢ (𝑤 = 𝑦 → -𝑤 = -𝑦)
33	32	eleq1d 2300	. . . . . . . . . . . . . 14 ⊢ (𝑤 = 𝑦 → (-𝑤 ∈ 𝐴 ↔ -𝑦 ∈ 𝐴))
34	33	elrab3 2964	. . . . . . . . . . . . 13 ⊢ (𝑦 ∈ ℝ → (𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ↔ -𝑦 ∈ 𝐴))
35	34	biimpd 144	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℝ → (𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} → -𝑦 ∈ 𝐴))
36	31, 35	mpcom 36	. . . . . . . . . . 11 ⊢ (𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} → -𝑦 ∈ 𝐴)
37		breq1 4096	. . . . . . . . . . . . 13 ⊢ (𝑏 = -𝑦 → (𝑏 < 𝑎 ↔ -𝑦 < 𝑎))
38	37	notbid 673	. . . . . . . . . . . 12 ⊢ (𝑏 = -𝑦 → (¬ 𝑏 < 𝑎 ↔ ¬ -𝑦 < 𝑎))
39	38	rspcv 2907	. . . . . . . . . . 11 ⊢ (-𝑦 ∈ 𝐴 → (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 → ¬ -𝑦 < 𝑎))
40	36, 39	syl 14	. . . . . . . . . 10 ⊢ (𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} → (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 → ¬ -𝑦 < 𝑎))
41	40	adantr 276	. . . . . . . . 9 ⊢ ((𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ∧ 𝑎 ∈ ℝ) → (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 → ¬ -𝑦 < 𝑎))
42		ltnegcon1 8702	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (-𝑎 < 𝑦 ↔ -𝑦 < 𝑎))
43	42	ancoms 268	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℝ ∧ 𝑎 ∈ ℝ) → (-𝑎 < 𝑦 ↔ -𝑦 < 𝑎))
44	43	notbid 673	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℝ ∧ 𝑎 ∈ ℝ) → (¬ -𝑎 < 𝑦 ↔ ¬ -𝑦 < 𝑎))
45	31, 44	sylan 283	. . . . . . . . 9 ⊢ ((𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ∧ 𝑎 ∈ ℝ) → (¬ -𝑎 < 𝑦 ↔ ¬ -𝑦 < 𝑎))
46	41, 45	sylibrd 169	. . . . . . . 8 ⊢ ((𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ∧ 𝑎 ∈ ℝ) → (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 → ¬ -𝑎 < 𝑦))
47	46	ancoms 268	. . . . . . 7 ⊢ ((𝑎 ∈ ℝ ∧ 𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}) → (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 → ¬ -𝑎 < 𝑦))
48	47	ralrimdva 2613	. . . . . 6 ⊢ (𝑎 ∈ ℝ → (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 → ∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ -𝑎 < 𝑦))
49	29, 30, 48	sylc 62	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏))) → ∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ -𝑎 < 𝑦)
50		nfv 1577	. . . . . . . . . . . 12 ⊢ Ⅎ𝑐(𝜑 ∧ 𝑎 ∈ ℝ)
51		nfcv 2375	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑐ℝ
52		nfv 1577	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑐 𝑎 < 𝑏
53		nfre1 2576	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑐∃𝑐 ∈ 𝐴 𝑐 < 𝑏
54	52, 53	nfim 1621	. . . . . . . . . . . . 13 ⊢ Ⅎ𝑐(𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)
55	51, 54	nfralya 2573	. . . . . . . . . . . 12 ⊢ Ⅎ𝑐∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)
56	50, 55	nfan 1614	. . . . . . . . . . 11 ⊢ Ⅎ𝑐((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏))
57		nfv 1577	. . . . . . . . . . 11 ⊢ Ⅎ𝑐 𝑦 ∈ ℝ
58	56, 57	nfan 1614	. . . . . . . . . 10 ⊢ Ⅎ𝑐(((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ)
59		nfv 1577	. . . . . . . . . 10 ⊢ Ⅎ𝑐 𝑦 < -𝑎
60	58, 59	nfan 1614	. . . . . . . . 9 ⊢ Ⅎ𝑐((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎)
61		simplr 529	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎) ∧ 𝑐 ∈ 𝐴) ∧ 𝑐 < -𝑦) → 𝑐 ∈ 𝐴)
62		infsupneg.ss	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 ⊆ ℝ)
63	62	sseld 3227	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (𝑐 ∈ 𝐴 → 𝑐 ∈ ℝ))
64	63	ad6antr 498	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎) ∧ 𝑐 ∈ 𝐴) ∧ 𝑐 < -𝑦) → (𝑐 ∈ 𝐴 → 𝑐 ∈ ℝ))
65	61, 64	mpd 13	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎) ∧ 𝑐 ∈ 𝐴) ∧ 𝑐 < -𝑦) → 𝑐 ∈ ℝ)
66	65	renegcld 8618	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎) ∧ 𝑐 ∈ 𝐴) ∧ 𝑐 < -𝑦) → -𝑐 ∈ ℝ)
67	65	recnd 8267	. . . . . . . . . . . . 13 ⊢ (((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎) ∧ 𝑐 ∈ 𝐴) ∧ 𝑐 < -𝑦) → 𝑐 ∈ ℂ)
68	67	negnegd 8540	. . . . . . . . . . . 12 ⊢ (((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎) ∧ 𝑐 ∈ 𝐴) ∧ 𝑐 < -𝑦) → --𝑐 = 𝑐)
69	68, 61	eqeltrd 2308	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎) ∧ 𝑐 ∈ 𝐴) ∧ 𝑐 < -𝑦) → --𝑐 ∈ 𝐴)
70		negeq 8431	. . . . . . . . . . . . 13 ⊢ (𝑤 = -𝑐 → -𝑤 = --𝑐)
71	70	eleq1d 2300	. . . . . . . . . . . 12 ⊢ (𝑤 = -𝑐 → (-𝑤 ∈ 𝐴 ↔ --𝑐 ∈ 𝐴))
72	71	elrab 2963	. . . . . . . . . . 11 ⊢ (-𝑐 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ↔ (-𝑐 ∈ ℝ ∧ --𝑐 ∈ 𝐴))
73	66, 69, 72	sylanbrc 417	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎) ∧ 𝑐 ∈ 𝐴) ∧ 𝑐 < -𝑦) → -𝑐 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴})
74		simp-4r 544	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎) ∧ 𝑐 ∈ 𝐴) ∧ 𝑐 < -𝑦) → 𝑦 ∈ ℝ)
75		simpr 110	. . . . . . . . . . 11 ⊢ (((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎) ∧ 𝑐 ∈ 𝐴) ∧ 𝑐 < -𝑦) → 𝑐 < -𝑦)
76	65, 74, 75	ltnegcon2d 8765	. . . . . . . . . 10 ⊢ (((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎) ∧ 𝑐 ∈ 𝐴) ∧ 𝑐 < -𝑦) → 𝑦 < -𝑐)
77		breq2 4097	. . . . . . . . . . 11 ⊢ (𝑧 = -𝑐 → (𝑦 < 𝑧 ↔ 𝑦 < -𝑐))
78	77	rspcev 2911	. . . . . . . . . 10 ⊢ ((-𝑐 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ∧ 𝑦 < -𝑐) → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧)
79	73, 76, 78	syl2anc 411	. . . . . . . . 9 ⊢ (((((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎) ∧ 𝑐 ∈ 𝐴) ∧ 𝑐 < -𝑦) → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧)
80		simpllr 536	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) → 𝑎 ∈ ℝ)
81		simpr 110	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) → 𝑦 ∈ ℝ)
82		simplr 529	. . . . . . . . . . 11 ⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) → ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏))
83	80, 81, 82	jca31 309	. . . . . . . . . 10 ⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) → ((𝑎 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)))
84		ltnegcon2 8703	. . . . . . . . . . . . . 14 ⊢ ((𝑦 ∈ ℝ ∧ 𝑎 ∈ ℝ) → (𝑦 < -𝑎 ↔ 𝑎 < -𝑦))
85	84	ancoms 268	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑦 < -𝑎 ↔ 𝑎 < -𝑦))
86	85	adantr 276	. . . . . . . . . . . 12 ⊢ (((𝑎 ∈ ℝ ∧ 𝑦 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) → (𝑦 < -𝑎 ↔ 𝑎 < -𝑦))
87		renegcl 8499	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℝ → -𝑦 ∈ ℝ)
88		breq2 4097	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = -𝑦 → (𝑎 < 𝑏 ↔ 𝑎 < -𝑦))
89		breq2 4097	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑏 = -𝑦 → (𝑐 < 𝑏 ↔ 𝑐 < -𝑦))
90	89	rexbidv 2534	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = -𝑦 → (∃𝑐 ∈ 𝐴 𝑐 < 𝑏 ↔ ∃𝑐 ∈ 𝐴 𝑐 < -𝑦))
91	88, 90	imbi12d 234	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 = -𝑦 → ((𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏) ↔ (𝑎 < -𝑦 → ∃𝑐 ∈ 𝐴 𝑐 < -𝑦)))
92	91	rspcv 2907	. . . . . . . . . . . . . . 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 2675	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) ∧ 𝑦 < -𝑎) → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧)
100	99	ex 115	. . . . . . 7 ⊢ ((((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) ∧ 𝑦 ∈ ℝ) → (𝑦 < -𝑎 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧))
101	100	ralrimiva 2606	. . . . . 6 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) → ∀𝑦 ∈ ℝ (𝑦 < -𝑎 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧))
102	101	adantrl 478	. . . . 5 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏))) → ∀𝑦 ∈ ℝ (𝑦 < -𝑎 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧))
103		breq1 4096	. . . . . . . . 9 ⊢ (𝑥 = -𝑎 → (𝑥 < 𝑦 ↔ -𝑎 < 𝑦))
104	103	notbid 673	. . . . . . . 8 ⊢ (𝑥 = -𝑎 → (¬ 𝑥 < 𝑦 ↔ ¬ -𝑎 < 𝑦))
105	104	ralbidv 2533	. . . . . . 7 ⊢ (𝑥 = -𝑎 → (∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑥 < 𝑦 ↔ ∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ -𝑎 < 𝑦))
106		breq2 4097	. . . . . . . . 9 ⊢ (𝑥 = -𝑎 → (𝑦 < 𝑥 ↔ 𝑦 < -𝑎))
107	106	imbi1d 231	. . . . . . . 8 ⊢ (𝑥 = -𝑎 → ((𝑦 < 𝑥 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧) ↔ (𝑦 < -𝑎 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧)))
108	107	ralbidv 2533	. . . . . . 7 ⊢ (𝑥 = -𝑎 → (∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧) ↔ ∀𝑦 ∈ ℝ (𝑦 < -𝑎 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧)))
109	105, 108	anbi12d 473	. . . . . 6 ⊢ (𝑥 = -𝑎 → ((∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧)) ↔ (∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ -𝑎 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < -𝑎 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧))))
110	109	rspcev 2911	. . . . 5 ⊢ ((-𝑎 ∈ ℝ ∧ (∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ -𝑎 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < -𝑎 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧))) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧)))
111	28, 49, 102, 110	syl12anc 1272	. . . 4 ⊢ (((𝜑 ∧ 𝑎 ∈ ℝ) ∧ (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏))) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧)))
112	111	ex 115	. . 3 ⊢ ((𝜑 ∧ 𝑎 ∈ ℝ) → ((∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧))))
113	112	rexlimdva 2651	. 2 ⊢ (𝜑 → (∃𝑎 ∈ ℝ (∀𝑏 ∈ 𝐴 ¬ 𝑏 < 𝑎 ∧ ∀𝑏 ∈ ℝ (𝑎 < 𝑏 → ∃𝑐 ∈ 𝐴 𝑐 < 𝑏)) → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧))))
114	26, 113	mpd 13	1 ⊢ (𝜑 → ∃𝑥 ∈ ℝ (∀𝑦 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴} ¬ 𝑥 < 𝑦 ∧ ∀𝑦 ∈ ℝ (𝑦 < 𝑥 → ∃𝑧 ∈ {𝑤 ∈ ℝ ∣ -𝑤 ∈ 𝐴}𝑦 < 𝑧)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 104   ↔ wb 105   = wceq 1398   ∈ wcel 2202  ∀wral 2511  ∃wrex 2512  {crab 2515   ⊆ wss 3201   class class class wbr 4093  ℝcr 8091   < clt 8273  -cneg 8410

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 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2204  ax-14 2205  ax-ext 2213  ax-sep 4212  ax-pow 4270  ax-pr 4305  ax-un 4536  ax-setind 4641  ax-cnex 8183  ax-resscn 8184  ax-1cn 8185  ax-1re 8186  ax-icn 8187  ax-addcl 8188  ax-addrcl 8189  ax-mulcl 8190  ax-addcom 8192  ax-addass 8194  ax-distr 8196  ax-i2m1 8197  ax-0id 8200  ax-rnegex 8201  ax-cnre 8203  ax-pre-ltadd 8208

This theorem depends on definitions:  df-bi 117  df-3an 1007  df-tru 1401  df-fal 1404  df-nf 1510  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ne 2404  df-nel 2499  df-ral 2516  df-rex 2517  df-reu 2518  df-rab 2520  df-v 2805  df-sbc 3033  df-dif 3203  df-un 3205  df-in 3207  df-ss 3214  df-pw 3658  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-br 4094  df-opab 4156  df-id 4396  df-xp 4737  df-rel 4738  df-cnv 4739  df-co 4740  df-dm 4741  df-iota 5293  df-fun 5335  df-fv 5341  df-riota 5981  df-ov 6031  df-oprab 6032  df-mpo 6033  df-pnf 8275  df-mnf 8276  df-ltxr 8278  df-sub 8411  df-neg 8412

This theorem is referenced by:  infssuzcldc  10558