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

Metamath Proof Explorer

Theorem supxrrernmpt

Description: The real and extended real indexed suprema match when the indexed real supremum exists. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses supxrrernmpt.x 
|- F/ x ph
supxrrernmpt.a 
|- ( ph -> A =/= (/) )
supxrrernmpt.b 
|- ( ( ph /\ x e. A ) -> B e. RR )
supxrrernmpt.y 
|- ( ph -> E. y e. RR A. x e. A B <_ y )
Assertion supxrrernmpt 
|- ( ph -> sup ( ran ( x e. A |-> B ) , RR* , < ) = sup ( ran ( x e. A |-> B ) , RR , < ) )

Proof

Step Hyp Ref Expression
1 supxrrernmpt.x 
 |-  F/ x ph
2 supxrrernmpt.a 
 |-  ( ph -> A =/= (/) )
3 supxrrernmpt.b 
 |-  ( ( ph /\ x e. A ) -> B e. RR )
4 supxrrernmpt.y 
 |-  ( ph -> E. y e. RR A. x e. A B <_ y )
5 eqid 
 |-  ( x e. A |-> B ) = ( x e. A |-> B )
6 1 5 3 rnmptssd 
 |-  ( ph -> ran ( x e. A |-> B ) C_ RR )
7 1 3 5 2 rnmptn0 
 |-  ( ph -> ran ( x e. A |-> B ) =/= (/) )
8 1 4 rnmptbdd 
 |-  ( ph -> E. y e. RR A. z e. ran ( x e. A |-> B ) z <_ y )
9 supxrre 
 |-  ( ( ran ( x e. A |-> B ) C_ RR /\ ran ( x e. A |-> B ) =/= (/) /\ E. y e. RR A. z e. ran ( x e. A |-> B ) z <_ y ) -> sup ( ran ( x e. A |-> B ) , RR* , < ) = sup ( ran ( x e. A |-> B ) , RR , < ) )
10 6 7 8 9 syl3anc 
 |-  ( ph -> sup ( ran ( x e. A |-> B ) , RR* , < ) = sup ( ran ( x e. A |-> B ) , RR , < ) )