rlimdm

Description: Two ways to express that a function has a limit. (The expression ( ~>rF ) is sometimes useful as a shorthand for "the unique limit of the function F "). (Contributed by Mario Carneiro, 8-May-2016)

	Ref	Expression
Hypotheses	rlimuni.1	$⊢ φ \to F : A ⟶ ℂ$
	rlimuni.2	$⊢ φ \to sup (A ℝ^{*} <) = +∞$
Assertion	rlimdm	$⊢ φ \to (F \in dom \underset{ℝ}{⇝} \leftrightarrow F \underset{ℝ}{⇝} \underset{ℝ}{⇝} (F))$

Proof

Step	Hyp	Ref	Expression
1		rlimuni.1	$⊢ φ \to F : A ⟶ ℂ$
2		rlimuni.2	$⊢ φ \to sup (A ℝ^{*} <) = +∞$
3		eldmg	$⊢ F \in dom \underset{ℝ}{⇝} \to (F \in dom \underset{ℝ}{⇝} \leftrightarrow \exists x F \underset{ℝ}{⇝} x)$
4	3	ibi	$⊢ F \in dom \underset{ℝ}{⇝} \to \exists x F \underset{ℝ}{⇝} x$
5		simpr	$⊢ (φ \land F \underset{ℝ}{⇝} x) \to F \underset{ℝ}{⇝} x$
6		df-fv	$⊢ \underset{ℝ}{⇝} (F) = (ι y \| F \underset{ℝ}{⇝} y)$
7	1	adantr	$⊢ (φ \land (F \underset{ℝ}{⇝} x \land F \underset{ℝ}{⇝} y)) \to F : A ⟶ ℂ$
8	2	adantr	$⊢ (φ \land (F \underset{ℝ}{⇝} x \land F \underset{ℝ}{⇝} y)) \to sup (A ℝ^{*} <) = +∞$
9		simprr	$⊢ (φ \land (F \underset{ℝ}{⇝} x \land F \underset{ℝ}{⇝} y)) \to F \underset{ℝ}{⇝} y$
10		simprl	$⊢ (φ \land (F \underset{ℝ}{⇝} x \land F \underset{ℝ}{⇝} y)) \to F \underset{ℝ}{⇝} x$
11	7 8 9 10	rlimuni	$⊢ (φ \land (F \underset{ℝ}{⇝} x \land F \underset{ℝ}{⇝} y)) \to y = x$
12	11	expr	$⊢ (φ \land F \underset{ℝ}{⇝} x) \to (F \underset{ℝ}{⇝} y \to y = x)$
13		breq2	$⊢ y = x \to (F \underset{ℝ}{⇝} y \leftrightarrow F \underset{ℝ}{⇝} x)$
14	5 13	syl5ibrcom	$⊢ (φ \land F \underset{ℝ}{⇝} x) \to (y = x \to F \underset{ℝ}{⇝} y)$
15	12 14	impbid	$⊢ (φ \land F \underset{ℝ}{⇝} x) \to (F \underset{ℝ}{⇝} y \leftrightarrow y = x)$
16	15	adantr	$⊢ ((φ \land F \underset{ℝ}{⇝} x) \land x \in V) \to (F \underset{ℝ}{⇝} y \leftrightarrow y = x)$
17	16	iota5	$⊢ ((φ \land F \underset{ℝ}{⇝} x) \land x \in V) \to (ι y \| F \underset{ℝ}{⇝} y) = x$
18	17	elvd	$⊢ (φ \land F \underset{ℝ}{⇝} x) \to (ι y \| F \underset{ℝ}{⇝} y) = x$
19	6 18	syl5eq	$⊢ (φ \land F \underset{ℝ}{⇝} x) \to \underset{ℝ}{⇝} (F) = x$
20	5 19	breqtrrd	$⊢ (φ \land F \underset{ℝ}{⇝} x) \to F \underset{ℝ}{⇝} \underset{ℝ}{⇝} (F)$
21	20	ex	$⊢ φ \to (F \underset{ℝ}{⇝} x \to F \underset{ℝ}{⇝} \underset{ℝ}{⇝} (F))$
22	21	exlimdv	$⊢ φ \to (\exists x F \underset{ℝ}{⇝} x \to F \underset{ℝ}{⇝} \underset{ℝ}{⇝} (F))$
23	4 22	syl5	$⊢ φ \to (F \in dom \underset{ℝ}{⇝} \to F \underset{ℝ}{⇝} \underset{ℝ}{⇝} (F))$
24		rlimrel	$⊢ Rel \underset{ℝ}{⇝}$
25	24	releldmi	$⊢ F \underset{ℝ}{⇝} \underset{ℝ}{⇝} (F) \to F \in dom \underset{ℝ}{⇝}$
26	23 25	impbid1	$⊢ φ \to (F \in dom \underset{ℝ}{⇝} \leftrightarrow F \underset{ℝ}{⇝} \underset{ℝ}{⇝} (F))$

Metamath Proof Explorer

Theorem rlimdm

Proof