This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem climfv

Description: The limit of a convergent sequence, expressed as the function value of the convergence relation. (Contributed by Glauco Siliprandi, 23-Oct-2021)

		Ref	Expression
	Assertion	climfv	$⊢ F ⇝ A \to A = ⇝ (F)$

Proof

Step	Hyp	Ref	Expression
1		id	$⊢ F ⇝ A \to F ⇝ A$
2		climrel	$⊢ Rel ⇝$
3	2	a1i	$⊢ F ⇝ A \to Rel ⇝$
4		brrelex1	$⊢ (Rel ⇝ \land F ⇝ A) \to F \in V$
5	3 1 4	syl2anc	$⊢ F ⇝ A \to F \in V$
6		brrelex2	$⊢ (Rel ⇝ \land F ⇝ A) \to A \in V$
7	3 1 6	syl2anc	$⊢ F ⇝ A \to A \in V$
8		breldmg	$⊢ (F \in V \land A \in V \land F ⇝ A) \to F \in dom ⇝$
9	5 7 1 8	syl3anc	$⊢ F ⇝ A \to F \in dom ⇝$
10		climdm	$⊢ F \in dom ⇝ \leftrightarrow F ⇝ ⇝ (F)$
11	9 10	sylib	$⊢ F ⇝ A \to F ⇝ ⇝ (F)$
12		climuni	$⊢ (F ⇝ A \land F ⇝ ⇝ (F)) \to A = ⇝ (F)$
13	1 11 12	syl2anc	$⊢ F ⇝ A \to A = ⇝ (F)$