Metamath Proof Explorer

Theorem smfid

Description: The identity function is Borel sigma-measurable. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses smfid.j 
|- J = ( topGen ` ran (,) )
smfid.b 
|- B = ( SalGen ` J )
smfid.a 
|- ( ph -> A C_ RR )
Assertion smfid 
|- ( ph -> ( x e. A |-> x ) e. ( SMblFn ` B ) )

Proof

Step Hyp Ref Expression
1 smfid.j 
 |-  J = ( topGen ` ran (,) )
2 smfid.b 
 |-  B = ( SalGen ` J )
3 smfid.a 
 |-  ( ph -> A C_ RR )
4 3 adantr 
 |-  ( ( ph /\ x e. A ) -> A C_ RR )
5 simpr 
 |-  ( ( ph /\ x e. A ) -> x e. A )
6 4 5 sseldd 
 |-  ( ( ph /\ x e. A ) -> x e. RR )
7 6 fmpttd 
 |-  ( ph -> ( x e. A |-> x ) : A --> RR )
8 simpr 
 |-  ( ( ( ( ph /\ y e. A ) /\ z e. A ) /\ y <_ z ) -> y <_ z )
9 eqid 
 |-  ( x e. A |-> x ) = ( x e. A |-> x )
10 9 a1i 
 |-  ( ( ph /\ y e. A ) -> ( x e. A |-> x ) = ( x e. A |-> x ) )
11 simpr 
 |-  ( ( ( ph /\ y e. A ) /\ x = y ) -> x = y )
12 simpr 
 |-  ( ( ph /\ y e. A ) -> y e. A )
13 10 11 12 12 fvmptd 
 |-  ( ( ph /\ y e. A ) -> ( ( x e. A |-> x ) ` y ) = y )
14 13 ad2antrr 
 |-  ( ( ( ( ph /\ y e. A ) /\ z e. A ) /\ y <_ z ) -> ( ( x e. A |-> x ) ` y ) = y )
15 9 a1i 
 |-  ( ( ph /\ z e. A ) -> ( x e. A |-> x ) = ( x e. A |-> x ) )
16 simpr 
 |-  ( ( ( ph /\ z e. A ) /\ x = z ) -> x = z )
17 simpr 
 |-  ( ( ph /\ z e. A ) -> z e. A )
18 15 16 17 17 fvmptd 
 |-  ( ( ph /\ z e. A ) -> ( ( x e. A |-> x ) ` z ) = z )
19 18 ad4ant13 
 |-  ( ( ( ( ph /\ y e. A ) /\ z e. A ) /\ y <_ z ) -> ( ( x e. A |-> x ) ` z ) = z )
20 14 19 breq12d 
 |-  ( ( ( ( ph /\ y e. A ) /\ z e. A ) /\ y <_ z ) -> ( ( ( x e. A |-> x ) ` y ) <_ ( ( x e. A |-> x ) ` z ) <-> y <_ z ) )
21 8 20 mpbird 
 |-  ( ( ( ( ph /\ y e. A ) /\ z e. A ) /\ y <_ z ) -> ( ( x e. A |-> x ) ` y ) <_ ( ( x e. A |-> x ) ` z ) )
22 21 ex 
 |-  ( ( ( ph /\ y e. A ) /\ z e. A ) -> ( y <_ z -> ( ( x e. A |-> x ) ` y ) <_ ( ( x e. A |-> x ) ` z ) ) )
23 22 ralrimiva 
 |-  ( ( ph /\ y e. A ) -> A. z e. A ( y <_ z -> ( ( x e. A |-> x ) ` y ) <_ ( ( x e. A |-> x ) ` z ) ) )
24 23 ralrimiva 
 |-  ( ph -> A. y e. A A. z e. A ( y <_ z -> ( ( x e. A |-> x ) ` y ) <_ ( ( x e. A |-> x ) ` z ) ) )
25 3 7 24 1 2 incsmf 
 |-  ( ph -> ( x e. A |-> x ) e. ( SMblFn ` B ) )