Theorem infrenegsup

Description: The infimum of a set of reals A is the negative of the supremum of the negatives of its elements. The antecedent ensures that A is nonempty and has a lower bound. (Contributed by NM, 14-Jun-2005) (Revised by AV, 4-Sep-2020)

	Ref	Expression
Assertion	infrenegsup	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → inf ( 𝐴 , ℝ , < ) = - sup ( { 𝑧 ∈ ℝ ∣ - 𝑧 ∈ 𝐴 } , ℝ , < ) )

Proof

Step	Hyp	Ref	Expression
1		infrecl	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → inf ( 𝐴 , ℝ , < ) ∈ ℝ )
2	1	recnd	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → inf ( 𝐴 , ℝ , < ) ∈ ℂ )
3	2	negnegd	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → - - inf ( 𝐴 , ℝ , < ) = inf ( 𝐴 , ℝ , < ) )
4		negeq	⊢ ( 𝑤 = 𝑧 → - 𝑤 = - 𝑧 )
5	4	cbvmptv	⊢ ( 𝑤 ∈ ℝ ↦ - 𝑤 ) = ( 𝑧 ∈ ℝ ↦ - 𝑧 )
6	5	mptpreima	⊢ ( ◡ ( 𝑤 ∈ ℝ ↦ - 𝑤 ) “ 𝐴 ) = { 𝑧 ∈ ℝ ∣ - 𝑧 ∈ 𝐴 }
7		eqid	⊢ ( 𝑤 ∈ ℝ ↦ - 𝑤 ) = ( 𝑤 ∈ ℝ ↦ - 𝑤 )
8	7	negiso	⊢ ( ( 𝑤 ∈ ℝ ↦ - 𝑤 ) Isom < , ◡ < ( ℝ , ℝ ) ∧ ◡ ( 𝑤 ∈ ℝ ↦ - 𝑤 ) = ( 𝑤 ∈ ℝ ↦ - 𝑤 ) )
9	8	simpri	⊢ ◡ ( 𝑤 ∈ ℝ ↦ - 𝑤 ) = ( 𝑤 ∈ ℝ ↦ - 𝑤 )
10	9	imaeq1i	⊢ ( ◡ ( 𝑤 ∈ ℝ ↦ - 𝑤 ) “ 𝐴 ) = ( ( 𝑤 ∈ ℝ ↦ - 𝑤 ) “ 𝐴 )
11	6 10	eqtr3i	⊢ { 𝑧 ∈ ℝ ∣ - 𝑧 ∈ 𝐴 } = ( ( 𝑤 ∈ ℝ ↦ - 𝑤 ) “ 𝐴 )
12	11	supeq1i	⊢ sup ( { 𝑧 ∈ ℝ ∣ - 𝑧 ∈ 𝐴 } , ℝ , < ) = sup ( ( ( 𝑤 ∈ ℝ ↦ - 𝑤 ) “ 𝐴 ) , ℝ , < )
13	8	simpli	⊢ ( 𝑤 ∈ ℝ ↦ - 𝑤 ) Isom < , ◡ < ( ℝ , ℝ )
14		isocnv	⊢ ( ( 𝑤 ∈ ℝ ↦ - 𝑤 ) Isom < , ◡ < ( ℝ , ℝ ) → ◡ ( 𝑤 ∈ ℝ ↦ - 𝑤 ) Isom ◡ < , < ( ℝ , ℝ ) )
15	13 14	ax-mp	⊢ ◡ ( 𝑤 ∈ ℝ ↦ - 𝑤 ) Isom ◡ < , < ( ℝ , ℝ )
16		isoeq1	⊢ ( ◡ ( 𝑤 ∈ ℝ ↦ - 𝑤 ) = ( 𝑤 ∈ ℝ ↦ - 𝑤 ) → ( ◡ ( 𝑤 ∈ ℝ ↦ - 𝑤 ) Isom ◡ < , < ( ℝ , ℝ ) ↔ ( 𝑤 ∈ ℝ ↦ - 𝑤 ) Isom ◡ < , < ( ℝ , ℝ ) ) )
17	9 16	ax-mp	⊢ ( ◡ ( 𝑤 ∈ ℝ ↦ - 𝑤 ) Isom ◡ < , < ( ℝ , ℝ ) ↔ ( 𝑤 ∈ ℝ ↦ - 𝑤 ) Isom ◡ < , < ( ℝ , ℝ ) )
18	15 17	mpbi	⊢ ( 𝑤 ∈ ℝ ↦ - 𝑤 ) Isom ◡ < , < ( ℝ , ℝ )
19	18	a1i	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → ( 𝑤 ∈ ℝ ↦ - 𝑤 ) Isom ◡ < , < ( ℝ , ℝ ) )
20		simp1	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → 𝐴 ⊆ ℝ )
21		infm3	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → ∃ 𝑥 ∈ ℝ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) )
22		vex	⊢ 𝑥 ∈ V
23		vex	⊢ 𝑦 ∈ V
24	22 23	brcnv	⊢ ( 𝑥 ◡ < 𝑦 ↔ 𝑦 < 𝑥 )
25	24	notbii	⊢ ( ¬ 𝑥 ◡ < 𝑦 ↔ ¬ 𝑦 < 𝑥 )
26	25	ralbii	⊢ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ◡ < 𝑦 ↔ ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 )
27	23 22	brcnv	⊢ ( 𝑦 ◡ < 𝑥 ↔ 𝑥 < 𝑦 )
28		vex	⊢ 𝑧 ∈ V
29	23 28	brcnv	⊢ ( 𝑦 ◡ < 𝑧 ↔ 𝑧 < 𝑦 )
30	29	rexbii	⊢ ( ∃ 𝑧 ∈ 𝐴 𝑦 ◡ < 𝑧 ↔ ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 )
31	27 30	imbi12i	⊢ ( ( 𝑦 ◡ < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 ◡ < 𝑧 ) ↔ ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) )
32	31	ralbii	⊢ ( ∀ 𝑦 ∈ ℝ ( 𝑦 ◡ < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 ◡ < 𝑧 ) ↔ ∀ 𝑦 ∈ ℝ ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) )
33	26 32	anbi12i	⊢ ( ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ◡ < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 ◡ < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 ◡ < 𝑧 ) ) ↔ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) )
34	33	rexbii	⊢ ( ∃ 𝑥 ∈ ℝ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ◡ < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 ◡ < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 ◡ < 𝑧 ) ) ↔ ∃ 𝑥 ∈ ℝ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑦 < 𝑥 ∧ ∀ 𝑦 ∈ ℝ ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) )
35	21 34	sylibr	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → ∃ 𝑥 ∈ ℝ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ◡ < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 ◡ < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 ◡ < 𝑧 ) ) )
36		gtso	⊢ ◡ < Or ℝ
37	36	a1i	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → ◡ < Or ℝ )
38	19 20 35 37	supiso	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → sup ( ( ( 𝑤 ∈ ℝ ↦ - 𝑤 ) “ 𝐴 ) , ℝ , < ) = ( ( 𝑤 ∈ ℝ ↦ - 𝑤 ) ‘ sup ( 𝐴 , ℝ , ◡ < ) ) )
39	12 38	syl5eq	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → sup ( { 𝑧 ∈ ℝ ∣ - 𝑧 ∈ 𝐴 } , ℝ , < ) = ( ( 𝑤 ∈ ℝ ↦ - 𝑤 ) ‘ sup ( 𝐴 , ℝ , ◡ < ) ) )
40		df-inf	⊢ inf ( 𝐴 , ℝ , < ) = sup ( 𝐴 , ℝ , ◡ < )
41	40	eqcomi	⊢ sup ( 𝐴 , ℝ , ◡ < ) = inf ( 𝐴 , ℝ , < )
42	41	fveq2i	⊢ ( ( 𝑤 ∈ ℝ ↦ - 𝑤 ) ‘ sup ( 𝐴 , ℝ , ◡ < ) ) = ( ( 𝑤 ∈ ℝ ↦ - 𝑤 ) ‘ inf ( 𝐴 , ℝ , < ) )
43		negeq	⊢ ( 𝑤 = inf ( 𝐴 , ℝ , < ) → - 𝑤 = - inf ( 𝐴 , ℝ , < ) )
44		negex	⊢ - inf ( 𝐴 , ℝ , < ) ∈ V
45	43 7 44	fvmpt	⊢ ( inf ( 𝐴 , ℝ , < ) ∈ ℝ → ( ( 𝑤 ∈ ℝ ↦ - 𝑤 ) ‘ inf ( 𝐴 , ℝ , < ) ) = - inf ( 𝐴 , ℝ , < ) )
46	42 45	syl5eq	⊢ ( inf ( 𝐴 , ℝ , < ) ∈ ℝ → ( ( 𝑤 ∈ ℝ ↦ - 𝑤 ) ‘ sup ( 𝐴 , ℝ , ◡ < ) ) = - inf ( 𝐴 , ℝ , < ) )
47	1 46	syl	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → ( ( 𝑤 ∈ ℝ ↦ - 𝑤 ) ‘ sup ( 𝐴 , ℝ , ◡ < ) ) = - inf ( 𝐴 , ℝ , < ) )
48	39 47	eqtr2d	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → - inf ( 𝐴 , ℝ , < ) = sup ( { 𝑧 ∈ ℝ ∣ - 𝑧 ∈ 𝐴 } , ℝ , < ) )
49	48	negeqd	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → - - inf ( 𝐴 , ℝ , < ) = - sup ( { 𝑧 ∈ ℝ ∣ - 𝑧 ∈ 𝐴 } , ℝ , < ) )
50	3 49	eqtr3d	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) → inf ( 𝐴 , ℝ , < ) = - sup ( { 𝑧 ∈ ℝ ∣ - 𝑧 ∈ 𝐴 } , ℝ , < ) )