rlimdmafv2

Description: Two ways to express that a function has a limit, analogous to rlimdm . (Contributed by AV, 5-Sep-2022)

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

Proof

Step	Hyp	Ref	Expression
1		rlimdmafv2.1	$⊢ φ \to F : A ⟶ ℂ$
2		rlimdmafv2.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		dfatafv2iota	$⊢ \underset{ℝ}{⇝} defAt F \to (\underset{ℝ}{⇝}'''' F) = (ι w \| F \underset{ℝ}{⇝} w)$
32	30 31	syl	$⊢ (φ \land F \underset{ℝ}{⇝} x) \to (\underset{ℝ}{⇝}'''' F) = (ι w \| F \underset{ℝ}{⇝} w)$
33	1	adantr	$⊢ (φ \land (F \underset{ℝ}{⇝} x \land F \underset{ℝ}{⇝} w)) \to F : A ⟶ ℂ$
34	2	adantr	$⊢ (φ \land (F \underset{ℝ}{⇝} x \land F \underset{ℝ}{⇝} w)) \to sup (A ℝ^{*} <) = +∞$
35		simprr	$⊢ (φ \land (F \underset{ℝ}{⇝} x \land F \underset{ℝ}{⇝} w)) \to F \underset{ℝ}{⇝} w$
36		simprl	$⊢ (φ \land (F \underset{ℝ}{⇝} x \land F \underset{ℝ}{⇝} w)) \to F \underset{ℝ}{⇝} x$
37	33 34 35 36	rlimuni	$⊢ (φ \land (F \underset{ℝ}{⇝} x \land F \underset{ℝ}{⇝} w)) \to w = x$
38	37	expr	$⊢ (φ \land F \underset{ℝ}{⇝} x) \to (F \underset{ℝ}{⇝} w \to w = x)$
39		breq2	$⊢ w = x \to (F \underset{ℝ}{⇝} w \leftrightarrow F \underset{ℝ}{⇝} x)$
40	5 39	syl5ibrcom	$⊢ (φ \land F \underset{ℝ}{⇝} x) \to (w = x \to F \underset{ℝ}{⇝} w)$
41	38 40	impbid	$⊢ (φ \land F \underset{ℝ}{⇝} x) \to (F \underset{ℝ}{⇝} w \leftrightarrow w = x)$
42	41	adantr	$⊢ ((φ \land F \underset{ℝ}{⇝} x) \land x \in V) \to (F \underset{ℝ}{⇝} w \leftrightarrow w = x)$
43	42	iota5	$⊢ ((φ \land F \underset{ℝ}{⇝} x) \land x \in V) \to (ι w \| F \underset{ℝ}{⇝} w) = x$
44	43	elvd	$⊢ (φ \land F \underset{ℝ}{⇝} x) \to (ι w \| F \underset{ℝ}{⇝} w) = x$
45	32 44	eqtrd	$⊢ (φ \land F \underset{ℝ}{⇝} x) \to (\underset{ℝ}{⇝}'''' F) = x$
46	5 45	breqtrrd	$⊢ (φ \land F \underset{ℝ}{⇝} x) \to F \underset{ℝ}{⇝} (\underset{ℝ}{⇝}'''' F)$
47	46	ex	$⊢ φ \to (F \underset{ℝ}{⇝} x \to F \underset{ℝ}{⇝} (\underset{ℝ}{⇝}'''' F))$
48	47	exlimdv	$⊢ φ \to (\exists x F \underset{ℝ}{⇝} x \to F \underset{ℝ}{⇝} (\underset{ℝ}{⇝}'''' F))$
49	4 48	syl5	$⊢ φ \to (F \in dom \underset{ℝ}{⇝} \to F \underset{ℝ}{⇝} (\underset{ℝ}{⇝}'''' F))$
50	6	releldmi	$⊢ F \underset{ℝ}{⇝} (\underset{ℝ}{⇝}'''' F) \to F \in dom \underset{ℝ}{⇝}$
51	49 50	impbid1	$⊢ φ \to (F \in dom \underset{ℝ}{⇝} \leftrightarrow F \underset{ℝ}{⇝} (\underset{ℝ}{⇝}'''' F))$

Metamath Proof Explorer

Theorem rlimdmafv2

Proof