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 
|- F/_ x B
Assertion rn1st 
|- ( B ~<_ _om -> ran ( x e. B |-> C ) ~<_ _om )

Proof

Step Hyp Ref Expression
1 rn1st.1 
 |-  F/_ x B
2 ordom 
 |-  Ord _om
3 reldom 
 |-  Rel ~<_
4 3 brrelex2i 
 |-  ( B ~<_ _om -> _om e. _V )
5 elong 
 |-  ( _om e. _V -> ( _om e. On <-> Ord _om ) )
6 4 5 syl 
 |-  ( B ~<_ _om -> ( _om e. On <-> Ord _om ) )
7 2 6 mpbiri 
 |-  ( B ~<_ _om -> _om e. On )
8 ondomen 
 |-  ( ( _om e. On /\ B ~<_ _om ) -> B e. dom card )
9 7 8 mpancom 
 |-  ( B ~<_ _om -> B e. dom card )
10 eqid 
 |-  ( x e. B |-> C ) = ( x e. B |-> C )
11 1 10 dmmptssf 
 |-  dom ( x e. B |-> C ) C_ B
12 ssnum 
 |-  ( ( B e. dom card /\ dom ( x e. B |-> C ) C_ B ) -> dom ( x e. B |-> C ) e. dom card )
13 9 11 12 sylancl 
 |-  ( B ~<_ _om -> dom ( x e. B |-> C ) e. dom card )
14 funmpt 
 |-  Fun ( x e. B |-> C )
15 funforn 
 |-  ( Fun ( x e. B |-> C ) <-> ( x e. B |-> C ) : dom ( x e. B |-> C ) -onto-> ran ( x e. B |-> C ) )
16 14 15 mpbi 
 |-  ( x e. B |-> C ) : dom ( x e. B |-> C ) -onto-> ran ( x e. B |-> C )
17 fodomnum 
 |-  ( dom ( x e. B |-> C ) e. dom card -> ( ( x e. B |-> C ) : dom ( x e. B |-> C ) -onto-> ran ( x e. B |-> C ) -> ran ( x e. B |-> C ) ~<_ dom ( x e. B |-> C ) ) )
18 13 16 17 mpisyl 
 |-  ( B ~<_ _om -> ran ( x e. B |-> C ) ~<_ dom ( x e. B |-> C ) )
19 ctex 
 |-  ( B ~<_ _om -> B e. _V )
20 ssdomg 
 |-  ( B e. _V -> ( dom ( x e. B |-> C ) C_ B -> dom ( x e. B |-> C ) ~<_ B ) )
21 19 11 20 mpisyl 
 |-  ( B ~<_ _om -> dom ( x e. B |-> C ) ~<_ B )
22 domtr 
 |-  ( ( dom ( x e. B |-> C ) ~<_ B /\ B ~<_ _om ) -> dom ( x e. B |-> C ) ~<_ _om )
23 21 22 mpancom 
 |-  ( B ~<_ _om -> dom ( x e. B |-> C ) ~<_ _om )
24 domtr 
 |-  ( ( ran ( x e. B |-> C ) ~<_ dom ( x e. B |-> C ) /\ dom ( x e. B |-> C ) ~<_ _om ) -> ran ( x e. B |-> C ) ~<_ _om )
25 18 23 24 syl2anc 
 |-  ( B ~<_ _om -> ran ( x e. B |-> C ) ~<_ _om )