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 us 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 ℤ ( 𝐹𝑦 ) : 𝑦𝑢 ) ) ) )