Theorem lmbr

Description: Express the binary relation "sequence F converges to point P " in a topological space. Definition 1.4-1 of Kreyszig p. 25. The condition F C_ ( CC X. X ) allows to use objects more general than sequences when convenient; see the comment in df-lm . (Contributed by Mario Carneiro, 14-Nov-2013)

	Ref	Expression
Hypothesis	lmbr.2	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
Assertion	lmbr	⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ↔ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		lmbr.2	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
2		lmfval	⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( ⇝𝑡 ‘ 𝐽 ) = { ⟨ 𝑓 , 𝑥 ⟩ ∣ ( 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) } )
3	1 2	syl	⊢ ( 𝜑 → ( ⇝𝑡 ‘ 𝐽 ) = { ⟨ 𝑓 , 𝑥 ⟩ ∣ ( 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) } )
4	3	breqd	⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ↔ 𝐹 { ⟨ 𝑓 , 𝑥 ⟩ ∣ ( 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) } 𝑃 ) )
5		reseq1	⊢ ( 𝑓 = 𝐹 → ( 𝑓 ↾ 𝑦 ) = ( 𝐹 ↾ 𝑦 ) )
6	5	feq1d	⊢ ( 𝑓 = 𝐹 → ( ( 𝑓 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ↔ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) )
7	6	rexbidv	⊢ ( 𝑓 = 𝐹 → ( ∃ 𝑦 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ↔ ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) )
8	7	imbi2d	⊢ ( 𝑓 = 𝐹 → ( ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ↔ ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) )
9	8	ralbidv	⊢ ( 𝑓 = 𝐹 → ( ∀ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ↔ ∀ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) )
10		eleq1	⊢ ( 𝑥 = 𝑃 → ( 𝑥 ∈ 𝑢 ↔ 𝑃 ∈ 𝑢 ) )
11	10	imbi1d	⊢ ( 𝑥 = 𝑃 → ( ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ↔ ( 𝑃 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) )
12	11	ralbidv	⊢ ( 𝑥 = 𝑃 → ( ∀ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ↔ ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) )
13	9 12	sylan9bb	⊢ ( ( 𝑓 = 𝐹 ∧ 𝑥 = 𝑃 ) → ( ∀ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ↔ ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) )
14		df-3an	⊢ ( ( 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) ↔ ( ( 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) )
15	14	opabbii	⊢ { ⟨ 𝑓 , 𝑥 ⟩ ∣ ( 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) } = { ⟨ 𝑓 , 𝑥 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) }
16	13 15	brab2a	⊢ ( 𝐹 { ⟨ 𝑓 , 𝑥 ⟩ ∣ ( 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) } 𝑃 ↔ ( ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ) ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) )
17		df-3an	⊢ ( ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) ↔ ( ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ) ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) )
18	16 17	bitr4i	⊢ ( 𝐹 { ⟨ 𝑓 , 𝑥 ⟩ ∣ ( 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) } 𝑃 ↔ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) )
19	4 18	bitrdi	⊢ ( 𝜑 → ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ↔ ( 𝐹 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑃 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑃 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) ) )