Metamath Proof Explorer

Theorem rn1st

Description: The range of a function with a first-countable domain is itself first-countable. This is a variation of 1stcrestlem , with a not-free hypothesis replacing a disjoint variable constraint. (Contributed by Glauco Siliprandi, 24-Jan-2025)

Ref Expression
Hypothesis rn1st.1 ⊢Ⅎ_xB
Assertion rn1st ⊢B≼ω→ran⁡x∈B⟼C≼ω

Proof

Step Hyp Ref Expression
1 rn1st.1 ⊢Ⅎ_xB
2 ordom ⊢Ord⁡ω
3 reldom ⊢Rel⁡≼
4 3 brrelex2i ⊢B≼ω→ω∈V
5 elong ⊢ω∈V→ω∈On↔Ord⁡ω
6 4 5 syl ⊢B≼ω→ω∈On↔Ord⁡ω
7 2 6 mpbiri ⊢B≼ω→ω∈On
8 ondomen ⊢ω∈On∧B≼ω→B∈dom⁡card
9 7 8 mpancom ⊢B≼ω→B∈dom⁡card
10 eqid ⊢x∈B⟼C=x∈B⟼C
11 1 10 dmmptssf ⊢dom⁡x∈B⟼C⊆B
12 ssnum ⊢B∈dom⁡card∧dom⁡x∈B⟼C⊆B→dom⁡x∈B⟼C∈dom⁡card
13 9 11 12 sylancl ⊢B≼ω→dom⁡x∈B⟼C∈dom⁡card
14 funmpt ⊢Fun⁡x∈B⟼C
15 funforn ⊢Fun⁡x∈B⟼C↔x∈B⟼C:dom⁡x∈B⟼C⟶ontoran⁡x∈B⟼C
16 14 15 mpbi ⊢x∈B⟼C:dom⁡x∈B⟼C⟶ontoran⁡x∈B⟼C
17 fodomnum ⊢dom⁡x∈B⟼C∈dom⁡card→x∈B⟼C:dom⁡x∈B⟼C⟶ontoran⁡x∈B⟼C→ran⁡x∈B⟼C≼dom⁡x∈B⟼C
18 13 16 17 mpisyl ⊢B≼ω→ran⁡x∈B⟼C≼dom⁡x∈B⟼C
19 ctex ⊢B≼ω→B∈V
20 ssdomg ⊢B∈V→dom⁡x∈B⟼C⊆B→dom⁡x∈B⟼C≼B
21 19 11 20 mpisyl ⊢B≼ω→dom⁡x∈B⟼C≼B
22 domtr ⊢dom⁡x∈B⟼C≼B∧B≼ω→dom⁡x∈B⟼C≼ω
23 21 22 mpancom ⊢B≼ω→dom⁡x∈B⟼C≼ω
24 domtr ⊢ran⁡x∈B⟼C≼dom⁡x∈B⟼C∧dom⁡x∈B⟼C≼ω→ran⁡x∈B⟼C≼ω
25 18 23 24 syl2anc ⊢B≼ω→ran⁡x∈B⟼C≼ω