Theorem dfinfre

Description: The infimum of a set of reals A . (Contributed by NM, 9-Oct-2005) (Revised by AV, 4-Sep-2020)

	Ref	Expression
Assertion	dfinfre	⊢ ( 𝐴 ⊆ ℝ → inf ( 𝐴 , ℝ , < ) = ∪ { 𝑥 ∈ ℝ ∣ ( ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) } )

Proof

Step	Hyp	Ref	Expression
1		df-inf	⊢ inf ( 𝐴 , ℝ , < ) = sup ( 𝐴 , ℝ , ◡ < )
2		df-sup	⊢ sup ( 𝐴 , ℝ , ◡ < ) = ∪ { 𝑥 ∈ ℝ ∣ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ◡ < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 ◡ < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 ◡ < 𝑧 ) ) }
3		ssel2	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ ℝ )
4		vex	⊢ 𝑥 ∈ V
5		vex	⊢ 𝑦 ∈ V
6	4 5	brcnv	⊢ ( 𝑥 ◡ < 𝑦 ↔ 𝑦 < 𝑥 )
7	6	notbii	⊢ ( ¬ 𝑥 ◡ < 𝑦 ↔ ¬ 𝑦 < 𝑥 )
8		lenlt	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 ≤ 𝑦 ↔ ¬ 𝑦 < 𝑥 ) )
9	7 8	bitr4id	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ¬ 𝑥 ◡ < 𝑦 ↔ 𝑥 ≤ 𝑦 ) )
10	3 9	sylan2	⊢ ( ( 𝑥 ∈ ℝ ∧ ( 𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴 ) ) → ( ¬ 𝑥 ◡ < 𝑦 ↔ 𝑥 ≤ 𝑦 ) )
11	10	ancoms	⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑥 ∈ ℝ ) → ( ¬ 𝑥 ◡ < 𝑦 ↔ 𝑥 ≤ 𝑦 ) )
12	11	an32s	⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ ) ∧ 𝑦 ∈ 𝐴 ) → ( ¬ 𝑥 ◡ < 𝑦 ↔ 𝑥 ≤ 𝑦 ) )
13	12	ralbidva	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ◡ < 𝑦 ↔ ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ) )
14	5 4	brcnv	⊢ ( 𝑦 ◡ < 𝑥 ↔ 𝑥 < 𝑦 )
15		vex	⊢ 𝑧 ∈ V
16	5 15	brcnv	⊢ ( 𝑦 ◡ < 𝑧 ↔ 𝑧 < 𝑦 )
17	16	rexbii	⊢ ( ∃ 𝑧 ∈ 𝐴 𝑦 ◡ < 𝑧 ↔ ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 )
18	14 17	imbi12i	⊢ ( ( 𝑦 ◡ < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 ◡ < 𝑧 ) ↔ ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) )
19	18	ralbii	⊢ ( ∀ 𝑦 ∈ ℝ ( 𝑦 ◡ < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 ◡ < 𝑧 ) ↔ ∀ 𝑦 ∈ ℝ ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) )
20	19	a1i	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ ) → ( ∀ 𝑦 ∈ ℝ ( 𝑦 ◡ < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 ◡ < 𝑧 ) ↔ ∀ 𝑦 ∈ ℝ ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) )
21	13 20	anbi12d	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝑥 ∈ ℝ ) → ( ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ◡ < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 ◡ < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 ◡ < 𝑧 ) ) ↔ ( ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) ) )
22	21	rabbidva	⊢ ( 𝐴 ⊆ ℝ → { 𝑥 ∈ ℝ ∣ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ◡ < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 ◡ < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 ◡ < 𝑧 ) ) } = { 𝑥 ∈ ℝ ∣ ( ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) } )
23	22	unieqd	⊢ ( 𝐴 ⊆ ℝ → ∪ { 𝑥 ∈ ℝ ∣ ( ∀ 𝑦 ∈ 𝐴 ¬ 𝑥 ◡ < 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑦 ◡ < 𝑥 → ∃ 𝑧 ∈ 𝐴 𝑦 ◡ < 𝑧 ) ) } = ∪ { 𝑥 ∈ ℝ ∣ ( ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) } )
24	2 23	syl5eq	⊢ ( 𝐴 ⊆ ℝ → sup ( 𝐴 , ℝ , ◡ < ) = ∪ { 𝑥 ∈ ℝ ∣ ( ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) } )
25	1 24	syl5eq	⊢ ( 𝐴 ⊆ ℝ → inf ( 𝐴 , ℝ , < ) = ∪ { 𝑥 ∈ ℝ ∣ ( ∀ 𝑦 ∈ 𝐴 𝑥 ≤ 𝑦 ∧ ∀ 𝑦 ∈ ℝ ( 𝑥 < 𝑦 → ∃ 𝑧 ∈ 𝐴 𝑧 < 𝑦 ) ) } )