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

Metamath Proof Explorer

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 ℤ≥ ( 𝐹 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) ) )