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	⊢ ( 𝐹 ⇝ 𝐴 → 𝐴 = ( ⇝ ‘ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		id	⊢ ( 𝐹 ⇝ 𝐴 → 𝐹 ⇝ 𝐴 )
2		climrel	⊢ Rel ⇝
3	2	a1i	⊢ ( 𝐹 ⇝ 𝐴 → Rel ⇝ )
4		brrelex1	⊢ ( ( Rel ⇝ ∧ 𝐹 ⇝ 𝐴 ) → 𝐹 ∈ V )
5	3 1 4	syl2anc	⊢ ( 𝐹 ⇝ 𝐴 → 𝐹 ∈ V )
6		brrelex2	⊢ ( ( Rel ⇝ ∧ 𝐹 ⇝ 𝐴 ) → 𝐴 ∈ V )
7	3 1 6	syl2anc	⊢ ( 𝐹 ⇝ 𝐴 → 𝐴 ∈ V )
8		breldmg	⊢ ( ( 𝐹 ∈ V ∧ 𝐴 ∈ V ∧ 𝐹 ⇝ 𝐴 ) → 𝐹 ∈ dom ⇝ )
9	5 7 1 8	syl3anc	⊢ ( 𝐹 ⇝ 𝐴 → 𝐹 ∈ dom ⇝ )
10		climdm	⊢ ( 𝐹 ∈ dom ⇝ ↔ 𝐹 ⇝ ( ⇝ ‘ 𝐹 ) )
11	9 10	sylib	⊢ ( 𝐹 ⇝ 𝐴 → 𝐹 ⇝ ( ⇝ ‘ 𝐹 ) )
12		climuni	⊢ ( ( 𝐹 ⇝ 𝐴 ∧ 𝐹 ⇝ ( ⇝ ‘ 𝐹 ) ) → 𝐴 = ( ⇝ ‘ 𝐹 ) )
13	1 11 12	syl2anc	⊢ ( 𝐹 ⇝ 𝐴 → 𝐴 = ( ⇝ ‘ 𝐹 ) )