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 ⊢ Ⅎ _ x B
Assertion rn1st ⊢ B ≼ ω → ran ⁡ x ∈ B ⟼ C ≼ ω

Proof

Step Hyp Ref Expression
1 rn1st.1 ⊢ Ⅎ _ x B
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 ⟶ onto ran ⁡ x ∈ B ⟼ C
16 14 15 mpbi ⊢ x ∈ B ⟼ C : dom ⁡ x ∈ B ⟼ C ⟶ onto ran ⁡ x ∈ B ⟼ C
17 fodomnum ⊢ dom ⁡ x ∈ B ⟼ C ∈ dom ⁡ card → x ∈ B ⟼ C : dom ⁡ x ∈ B ⟼ C ⟶ onto ran ⁡ 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 ≼ ω