Metamath Proof Explorer

Theorem lmfval

Description: The relation "sequence f converges to point y " in a metric space. (Contributed by NM, 7-Sep-2006) (Revised by Mario Carneiro, 21-Aug-2015)

Ref Expression
Assertion lmfval ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( ⇝𝑡 ‘ 𝐽 ) = { ⟨ 𝑓 , 𝑥 ⟩ ∣ ( 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) } )

Proof

Step Hyp Ref Expression
1 df-lm ⊢ ⇝𝑡 = ( 𝑗 ∈ Top ↦ { ⟨ 𝑓 , 𝑥 ⟩ ∣ ( 𝑓 ∈ ( ∪ 𝑗 ↑pm ℂ ) ∧ 𝑥 ∈ ∪ 𝑗 ∧ ∀ 𝑢 ∈ 𝑗 ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) } )
2 simpr ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑗 = 𝐽 ) → 𝑗 = 𝐽 )
3 2 unieqd ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑗 = 𝐽 ) → ∪ 𝑗 = ∪ 𝐽 )
4 toponuni ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 = ∪ 𝐽 )
5 4 adantr ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑗 = 𝐽 ) → 𝑋 = ∪ 𝐽 )
6 3 5 eqtr4d ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑗 = 𝐽 ) → ∪ 𝑗 = 𝑋 )
7 6 oveq1d ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑗 = 𝐽 ) → ( ∪ 𝑗 ↑pm ℂ ) = ( 𝑋 ↑pm ℂ ) )
8 7 eleq2d ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑗 = 𝐽 ) → ( 𝑓 ∈ ( ∪ 𝑗 ↑pm ℂ ) ↔ 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ) )
9 6 eleq2d ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑗 = 𝐽 ) → ( 𝑥 ∈ ∪ 𝑗 ↔ 𝑥 ∈ 𝑋 ) )
10 2 raleqdv ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑗 = 𝐽 ) → ( ∀ 𝑢 ∈ 𝑗 ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ↔ ∀ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) )
11 8 9 10 3anbi123d ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑗 = 𝐽 ) → ( ( 𝑓 ∈ ( ∪ 𝑗 ↑pm ℂ ) ∧ 𝑥 ∈ ∪ 𝑗 ∧ ∀ 𝑢 ∈ 𝑗 ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) ↔ ( 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) ) )
12 11 opabbidv ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑗 = 𝐽 ) → { ⟨ 𝑓 , 𝑥 ⟩ ∣ ( 𝑓 ∈ ( ∪ 𝑗 ↑pm ℂ ) ∧ 𝑥 ∈ ∪ 𝑗 ∧ ∀ 𝑢 ∈ 𝑗 ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) } = { ⟨ 𝑓 , 𝑥 ⟩ ∣ ( 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) } )
13 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
14 df-3an ⊢ ( ( 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) ↔ ( ( 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) )
15 14 opabbii ⊢ { ⟨ 𝑓 , 𝑥 ⟩ ∣ ( 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) } = { ⟨ 𝑓 , 𝑥 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) }
16 opabssxp ⊢ { ⟨ 𝑓 , 𝑥 ⟩ ∣ ( ( 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑥 ∈ 𝑋 ) ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) } ⊆ ( ( 𝑋 ↑pm ℂ ) × 𝑋 )
17 15 16 eqsstri ⊢ { ⟨ 𝑓 , 𝑥 ⟩ ∣ ( 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) } ⊆ ( ( 𝑋 ↑pm ℂ ) × 𝑋 )
18 ovex ⊢ ( 𝑋 ↑pm ℂ ) ∈ V
19 toponmax ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 ∈ 𝐽 )
20 xpexg ⊢ ( ( ( 𝑋 ↑pm ℂ ) ∈ V ∧ 𝑋 ∈ 𝐽 ) → ( ( 𝑋 ↑pm ℂ ) × 𝑋 ) ∈ V )
21 18 19 20 sylancr ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( ( 𝑋 ↑pm ℂ ) × 𝑋 ) ∈ V )
22 ssexg ⊢ ( ( { ⟨ 𝑓 , 𝑥 ⟩ ∣ ( 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) } ⊆ ( ( 𝑋 ↑pm ℂ ) × 𝑋 ) ∧ ( ( 𝑋 ↑pm ℂ ) × 𝑋 ) ∈ V ) → { ⟨ 𝑓 , 𝑥 ⟩ ∣ ( 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) } ∈ V )
23 17 21 22 sylancr ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → { ⟨ 𝑓 , 𝑥 ⟩ ∣ ( 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) } ∈ V )
24 1 12 13 23 fvmptd2 ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → ( ⇝𝑡 ‘ 𝐽 ) = { ⟨ 𝑓 , 𝑥 ⟩ ∣ ( 𝑓 ∈ ( 𝑋 ↑pm ℂ ) ∧ 𝑥 ∈ 𝑋 ∧ ∀ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) } )