liminfvalxrmpt

Description: Alternate definition of liminf when F is an extended real-valued function. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	liminfvalxrmpt.1	$⊢ Ⅎ x φ$
	liminfvalxrmpt.2	$⊢ φ \to A \in V$
	liminfvalxrmpt.3	$⊢ (φ \land x \in A) \to B \in ℝ^{*}$
Assertion	liminfvalxrmpt	$⊢ φ \to lim inf ((x \in A ⟼ B)) = - lim sup ((x \in A ⟼ - B))$

Step	Hyp	Ref	Expression
1		liminfvalxrmpt.1	$⊢ Ⅎ x φ$
2		liminfvalxrmpt.2	$⊢ φ \to A \in V$
3		liminfvalxrmpt.3	$⊢ (φ \land x \in A) \to B \in ℝ^{*}$
4		nfmpt1	$⊢ \underline{Ⅎ} x (x \in A ⟼ B)$
5	1 3	fmptd2f	$⊢ φ \to (x \in A ⟼ B) : A ⟶ ℝ^{*}$
6	4 2 5	liminfvalxr	$⊢ φ \to lim inf ((x \in A ⟼ B)) = - lim sup ((x \in A ⟼ - (x \in A ⟼ B) (x)))$
7		eqidd	$⊢ φ \to (x \in A ⟼ B) = (x \in A ⟼ B)$
8	7 3	fvmpt2d	$⊢ (φ \land x \in A) \to (x \in A ⟼ B) (x) = B$
9	8	xnegeqd	$⊢ (φ \land x \in A) \to - (x \in A ⟼ B) (x) = - B$
10	1 9	mpteq2da	$⊢ φ \to (x \in A ⟼ - (x \in A ⟼ B) (x)) = (x \in A ⟼ - B)$
11	10	fveq2d	$⊢ φ \to lim sup ((x \in A ⟼ - (x \in A ⟼ B) (x))) = lim sup ((x \in A ⟼ - B))$
12	11	xnegeqd	$⊢ φ \to - lim sup ((x \in A ⟼ - (x \in A ⟼ B) (x))) = - lim sup ((x \in A ⟼ - B))$
13	6 12	eqtrd	$⊢ φ \to lim inf ((x \in A ⟼ B)) = - lim sup ((x \in A ⟼ - B))$

Metamath Proof Explorer