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

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 ⊢ Ⅎ 𝑥 𝐵
Assertion rn1st ( 𝐵 ≼ ω → ran ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ≼ ω )

Proof

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