Theorem lmrcl

Description: Reverse closure for the convergence relation. (Contributed by Mario Carneiro, 7-Sep-2015)

	Ref	Expression
Assertion	lmrcl	⊢ ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 → 𝐽 ∈ Top )

Proof

Step	Hyp	Ref	Expression
1		df-lm	⊢ ⇝𝑡 = ( 𝑗 ∈ Top ↦ { ⟨ 𝑓 , 𝑥 ⟩ ∣ ( 𝑓 ∈ ( ∪ 𝑗 ↑pm ℂ ) ∧ 𝑥 ∈ ∪ 𝑗 ∧ ∀ 𝑢 ∈ 𝑗 ( 𝑥 ∈ 𝑢 → ∃ 𝑦 ∈ ran ℤ≥ ( 𝑓 ↾ 𝑦 ) : 𝑦 ⟶ 𝑢 ) ) } )
2	1	dmmptss	⊢ dom ⇝𝑡 ⊆ Top
3		df-br	⊢ ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 ↔ ⟨ 𝐹 , 𝑃 ⟩ ∈ ( ⇝𝑡 ‘ 𝐽 ) )
4		elfvdm	⊢ ( ⟨ 𝐹 , 𝑃 ⟩ ∈ ( ⇝𝑡 ‘ 𝐽 ) → 𝐽 ∈ dom ⇝𝑡 )
5	3 4	sylbi	⊢ ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 → 𝐽 ∈ dom ⇝𝑡 )
6	2 5	sseldi	⊢ ( 𝐹 ( ⇝𝑡 ‘ 𝐽 ) 𝑃 → 𝐽 ∈ Top )