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 ( 𝑥 ∈ 𝐵 ↦ 𝐶 ) ≼ ω )