infcvgaux1i

Description: Auxiliary theorem for applications of supcvg . Hypothesis for several supremum theorems. (Contributed by NM, 8-Feb-2008)

	Ref	Expression
Hypotheses	infcvg.1	⊢ 𝑅 = { 𝑥 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = - 𝐴 }
	infcvg.2	⊢ ( 𝑦 ∈ 𝑋 → 𝐴 ∈ ℝ )
	infcvg.3	⊢ 𝑍 ∈ 𝑋
	infcvg.4	⊢ ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑤 ≤ 𝑧
Assertion	infcvgaux1i	⊢ ( 𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑤 ≤ 𝑧 )

Proof

Step	Hyp	Ref	Expression
1		infcvg.1	⊢ 𝑅 = { 𝑥 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = - 𝐴 }
2		infcvg.2	⊢ ( 𝑦 ∈ 𝑋 → 𝐴 ∈ ℝ )
3		infcvg.3	⊢ 𝑍 ∈ 𝑋
4		infcvg.4	⊢ ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑤 ≤ 𝑧
5	2	renegcld	⊢ ( 𝑦 ∈ 𝑋 → - 𝐴 ∈ ℝ )
6		eleq1	⊢ ( 𝑥 = - 𝐴 → ( 𝑥 ∈ ℝ ↔ - 𝐴 ∈ ℝ ) )
7	5 6	syl5ibrcom	⊢ ( 𝑦 ∈ 𝑋 → ( 𝑥 = - 𝐴 → 𝑥 ∈ ℝ ) )
8	7	rexlimiv	⊢ ( ∃ 𝑦 ∈ 𝑋 𝑥 = - 𝐴 → 𝑥 ∈ ℝ )
9	8	abssi	⊢ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = - 𝐴 } ⊆ ℝ
10	1 9	eqsstri	⊢ 𝑅 ⊆ ℝ
11		eqid	⊢ - ⦋ 𝑍 / 𝑦 ⦌ 𝐴 = - ⦋ 𝑍 / 𝑦 ⦌ 𝐴
12	11	nfth	⊢ Ⅎ 𝑦 - ⦋ 𝑍 / 𝑦 ⦌ 𝐴 = - ⦋ 𝑍 / 𝑦 ⦌ 𝐴
13		csbeq1a	⊢ ( 𝑦 = 𝑍 → 𝐴 = ⦋ 𝑍 / 𝑦 ⦌ 𝐴 )
14	13	negeqd	⊢ ( 𝑦 = 𝑍 → - 𝐴 = - ⦋ 𝑍 / 𝑦 ⦌ 𝐴 )
15	14	eqeq2d	⊢ ( 𝑦 = 𝑍 → ( - ⦋ 𝑍 / 𝑦 ⦌ 𝐴 = - 𝐴 ↔ - ⦋ 𝑍 / 𝑦 ⦌ 𝐴 = - ⦋ 𝑍 / 𝑦 ⦌ 𝐴 ) )
16	12 15	rspce	⊢ ( ( 𝑍 ∈ 𝑋 ∧ - ⦋ 𝑍 / 𝑦 ⦌ 𝐴 = - ⦋ 𝑍 / 𝑦 ⦌ 𝐴 ) → ∃ 𝑦 ∈ 𝑋 - ⦋ 𝑍 / 𝑦 ⦌ 𝐴 = - 𝐴 )
17	3 11 16	mp2an	⊢ ∃ 𝑦 ∈ 𝑋 - ⦋ 𝑍 / 𝑦 ⦌ 𝐴 = - 𝐴
18		negex	⊢ - ⦋ 𝑍 / 𝑦 ⦌ 𝐴 ∈ V
19		nfcsb1v	⊢ Ⅎ 𝑦 ⦋ 𝑍 / 𝑦 ⦌ 𝐴
20	19	nfneg	⊢ Ⅎ 𝑦 - ⦋ 𝑍 / 𝑦 ⦌ 𝐴
21	20	nfeq2	⊢ Ⅎ 𝑦 𝑥 = - ⦋ 𝑍 / 𝑦 ⦌ 𝐴
22		eqeq1	⊢ ( 𝑥 = - ⦋ 𝑍 / 𝑦 ⦌ 𝐴 → ( 𝑥 = - 𝐴 ↔ - ⦋ 𝑍 / 𝑦 ⦌ 𝐴 = - 𝐴 ) )
23	21 22	rexbid	⊢ ( 𝑥 = - ⦋ 𝑍 / 𝑦 ⦌ 𝐴 → ( ∃ 𝑦 ∈ 𝑋 𝑥 = - 𝐴 ↔ ∃ 𝑦 ∈ 𝑋 - ⦋ 𝑍 / 𝑦 ⦌ 𝐴 = - 𝐴 ) )
24	18 23	elab	⊢ ( - ⦋ 𝑍 / 𝑦 ⦌ 𝐴 ∈ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = - 𝐴 } ↔ ∃ 𝑦 ∈ 𝑋 - ⦋ 𝑍 / 𝑦 ⦌ 𝐴 = - 𝐴 )
25	17 24	mpbir	⊢ - ⦋ 𝑍 / 𝑦 ⦌ 𝐴 ∈ { 𝑥 ∣ ∃ 𝑦 ∈ 𝑋 𝑥 = - 𝐴 }
26	25 1	eleqtrri	⊢ - ⦋ 𝑍 / 𝑦 ⦌ 𝐴 ∈ 𝑅
27	26	ne0ii	⊢ 𝑅 ≠ ∅
28	10 27 4	3pm3.2i	⊢ ( 𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∃ 𝑧 ∈ ℝ ∀ 𝑤 ∈ 𝑅 𝑤 ≤ 𝑧 )

Metamath Proof Explorer

Theorem infcvgaux1i

Proof