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

Metamath Proof Explorer

Theorem limcmptdm

Description: The domain of a maps-to function with a limit. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses limcmptdm.f ⊢ F = x ∈ A ⟼ B
limcmptdm.b ⊢ φ ∧ x ∈ A → B ∈ ℂ
limcmptdm.c ⊢ φ → C ∈ F lim ℂ D
Assertion limcmptdm ⊢ φ → A ⊆ ℂ

Proof

Step Hyp Ref Expression
1 limcmptdm.f ⊢ F = x ∈ A ⟼ B
2 limcmptdm.b ⊢ φ ∧ x ∈ A → B ∈ ℂ
3 limcmptdm.c ⊢ φ → C ∈ F lim ℂ D
4 1 2 dmmptd ⊢ φ → dom ⁡ F = A
5 limcrcl ⊢ C ∈ F lim ℂ D → F : dom ⁡ F ⟶ ℂ ∧ dom ⁡ F ⊆ ℂ ∧ D ∈ ℂ
6 3 5 syl ⊢ φ → F : dom ⁡ F ⟶ ℂ ∧ dom ⁡ F ⊆ ℂ ∧ D ∈ ℂ
7 6 simp2d ⊢ φ → dom ⁡ F ⊆ ℂ
8 4 7 eqsstrrd ⊢ φ → A ⊆ ℂ