rlimdmafv

Description: Two ways to express that a function has a limit, analogous to rlimdm . (Contributed by Alexander van der Vekens, 27-Nov-2017)

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

Proof

Step	Hyp	Ref	Expression
1		rlimdmafv.1	$⊢ φ \to F : A ⟶ ℂ$
2		rlimdmafv.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		rlimrel	$⊢ Rel \underset{ℝ}{⇝}$
7	6	brrelex1i	$⊢ F \underset{ℝ}{⇝} x \to F \in V$
8	7	adantl	$⊢ (φ \land F \underset{ℝ}{⇝} x) \to F \in V$
9		vex	$⊢ x \in V$
10	9	a1i	$⊢ (φ \land F \underset{ℝ}{⇝} x) \to x \in V$
11		breldmg	$⊢ (F \in V \land x \in V \land F \underset{ℝ}{⇝} x) \to F \in dom \underset{ℝ}{⇝}$
12	8 10 5 11	syl3anc	$⊢ (φ \land F \underset{ℝ}{⇝} x) \to F \in dom \underset{ℝ}{⇝}$
13		breq2	$⊢ y = x \to (F \underset{ℝ}{⇝} y \leftrightarrow F \underset{ℝ}{⇝} x)$
14	13	biimprd	$⊢ y = x \to (F \underset{ℝ}{⇝} x \to F \underset{ℝ}{⇝} y)$
15	14	spimevw	$⊢ F \underset{ℝ}{⇝} x \to \exists y F \underset{ℝ}{⇝} y$
16	15	adantl	$⊢ (φ \land F \underset{ℝ}{⇝} x) \to \exists y F \underset{ℝ}{⇝} y$
17	1	adantr	$⊢ (φ \land F \underset{ℝ}{⇝} x) \to F : A ⟶ ℂ$
18	17	adantr	$⊢ ((φ \land F \underset{ℝ}{⇝} x) \land (F \underset{ℝ}{⇝} y \land F \underset{ℝ}{⇝} z)) \to F : A ⟶ ℂ$
19	2	adantr	$⊢ (φ \land F \underset{ℝ}{⇝} x) \to sup (A ℝ^{*} <) = +∞$
20	19	adantr	$⊢ ((φ \land F \underset{ℝ}{⇝} x) \land (F \underset{ℝ}{⇝} y \land F \underset{ℝ}{⇝} z)) \to sup (A ℝ^{*} <) = +∞$
21		simprl	$⊢ ((φ \land F \underset{ℝ}{⇝} x) \land (F \underset{ℝ}{⇝} y \land F \underset{ℝ}{⇝} z)) \to F \underset{ℝ}{⇝} y$
22		simprr	$⊢ ((φ \land F \underset{ℝ}{⇝} x) \land (F \underset{ℝ}{⇝} y \land F \underset{ℝ}{⇝} z)) \to F \underset{ℝ}{⇝} z$
23	18 20 21 22	rlimuni	$⊢ ((φ \land F \underset{ℝ}{⇝} x) \land (F \underset{ℝ}{⇝} y \land F \underset{ℝ}{⇝} z)) \to y = z$
24	23	ex	$⊢ (φ \land F \underset{ℝ}{⇝} x) \to ((F \underset{ℝ}{⇝} y \land F \underset{ℝ}{⇝} z) \to y = z)$
25	24	alrimivv	$⊢ (φ \land F \underset{ℝ}{⇝} x) \to \forall y \forall z ((F \underset{ℝ}{⇝} y \land F \underset{ℝ}{⇝} z) \to y = z)$
26		breq2	$⊢ y = z \to (F \underset{ℝ}{⇝} y \leftrightarrow F \underset{ℝ}{⇝} z)$
27	26	eu4	$⊢ \exists! y F \underset{ℝ}{⇝} y \leftrightarrow (\exists y F \underset{ℝ}{⇝} y \land \forall y \forall z ((F \underset{ℝ}{⇝} y \land F \underset{ℝ}{⇝} z) \to y = z))$
28	16 25 27	sylanbrc	$⊢ (φ \land F \underset{ℝ}{⇝} x) \to \exists! y F \underset{ℝ}{⇝} y$
29		dfdfat2	$⊢ \underset{ℝ}{⇝} defAt F \leftrightarrow (F \in dom \underset{ℝ}{⇝} \land \exists! y F \underset{ℝ}{⇝} y)$
30	12 28 29	sylanbrc	$⊢ (φ \land F \underset{ℝ}{⇝} x) \to \underset{ℝ}{⇝} defAt F$
31		afvfundmfveq	$⊢ \underset{ℝ}{⇝} defAt F \to (\underset{ℝ}{⇝}''' F) = \underset{ℝ}{⇝} (F)$
32	30 31	syl	$⊢ (φ \land F \underset{ℝ}{⇝} x) \to (\underset{ℝ}{⇝}''' F) = \underset{ℝ}{⇝} (F)$
33		df-fv	$⊢ \underset{ℝ}{⇝} (F) = (ι w \| F \underset{ℝ}{⇝} w)$
34	1	adantr	$⊢ (φ \land (F \underset{ℝ}{⇝} x \land F \underset{ℝ}{⇝} w)) \to F : A ⟶ ℂ$
35	2	adantr	$⊢ (φ \land (F \underset{ℝ}{⇝} x \land F \underset{ℝ}{⇝} w)) \to sup (A ℝ^{*} <) = +∞$
36		simprr	$⊢ (φ \land (F \underset{ℝ}{⇝} x \land F \underset{ℝ}{⇝} w)) \to F \underset{ℝ}{⇝} w$
37		simprl	$⊢ (φ \land (F \underset{ℝ}{⇝} x \land F \underset{ℝ}{⇝} w)) \to F \underset{ℝ}{⇝} x$
38	34 35 36 37	rlimuni	$⊢ (φ \land (F \underset{ℝ}{⇝} x \land F \underset{ℝ}{⇝} w)) \to w = x$
39	38	expr	$⊢ (φ \land F \underset{ℝ}{⇝} x) \to (F \underset{ℝ}{⇝} w \to w = x)$
40		breq2	$⊢ w = x \to (F \underset{ℝ}{⇝} w \leftrightarrow F \underset{ℝ}{⇝} x)$
41	5 40	syl5ibrcom	$⊢ (φ \land F \underset{ℝ}{⇝} x) \to (w = x \to F \underset{ℝ}{⇝} w)$
42	39 41	impbid	$⊢ (φ \land F \underset{ℝ}{⇝} x) \to (F \underset{ℝ}{⇝} w \leftrightarrow w = x)$
43	42	adantr	$⊢ ((φ \land F \underset{ℝ}{⇝} x) \land x \in V) \to (F \underset{ℝ}{⇝} w \leftrightarrow w = x)$
44	43	iota5	$⊢ ((φ \land F \underset{ℝ}{⇝} x) \land x \in V) \to (ι w \| F \underset{ℝ}{⇝} w) = x$
45	44	elvd	$⊢ (φ \land F \underset{ℝ}{⇝} x) \to (ι w \| F \underset{ℝ}{⇝} w) = x$
46	33 45	syl5eq	$⊢ (φ \land F \underset{ℝ}{⇝} x) \to \underset{ℝ}{⇝} (F) = x$
47	32 46	eqtrd	$⊢ (φ \land F \underset{ℝ}{⇝} x) \to (\underset{ℝ}{⇝}''' F) = x$
48	5 47	breqtrrd	$⊢ (φ \land F \underset{ℝ}{⇝} x) \to F \underset{ℝ}{⇝} (\underset{ℝ}{⇝}''' F)$
49	48	ex	$⊢ φ \to (F \underset{ℝ}{⇝} x \to F \underset{ℝ}{⇝} (\underset{ℝ}{⇝}''' F))$
50	49	exlimdv	$⊢ φ \to (\exists x F \underset{ℝ}{⇝} x \to F \underset{ℝ}{⇝} (\underset{ℝ}{⇝}''' F))$
51	4 50	syl5	$⊢ φ \to (F \in dom \underset{ℝ}{⇝} \to F \underset{ℝ}{⇝} (\underset{ℝ}{⇝}''' F))$
52	6	releldmi	$⊢ F \underset{ℝ}{⇝} (\underset{ℝ}{⇝}''' F) \to F \in dom \underset{ℝ}{⇝}$
53	51 52	impbid1	$⊢ φ \to (F \in dom \underset{ℝ}{⇝} \leftrightarrow F \underset{ℝ}{⇝} (\underset{ℝ}{⇝}''' F))$

Metamath Proof Explorer

Theorem rlimdmafv

Proof