Metamath Proof Explorer

Theorem i1fposd

Description: Deduction form of i1fposd . (Contributed by Mario Carneiro, 6-Aug-2014)

Ref Expression
Hypothesis i1fposd.1 
|- ( ph -> ( x e. RR |-> A ) e. dom S.1 )
Assertion i1fposd 
|- ( ph -> ( x e. RR |-> if ( 0 <_ A , A , 0 ) ) e. dom S.1 )

Proof

Step Hyp Ref Expression
1 i1fposd.1 
 |-  ( ph -> ( x e. RR |-> A ) e. dom S.1 )
2 nfcv 
 |-  F/_ x 0
3 nfcv 
 |-  F/_ x <_
4 nffvmpt1 
 |-  F/_ x ( ( x e. RR |-> A ) ` y )
5 2 3 4 nfbr 
 |-  F/ x 0 <_ ( ( x e. RR |-> A ) ` y )
6 5 4 2 nfif 
 |-  F/_ x if ( 0 <_ ( ( x e. RR |-> A ) ` y ) , ( ( x e. RR |-> A ) ` y ) , 0 )
7 nfcv 
 |-  F/_ y if ( 0 <_ ( ( x e. RR |-> A ) ` x ) , ( ( x e. RR |-> A ) ` x ) , 0 )
8 fveq2 
 |-  ( y = x -> ( ( x e. RR |-> A ) ` y ) = ( ( x e. RR |-> A ) ` x ) )
9 8 breq2d 
 |-  ( y = x -> ( 0 <_ ( ( x e. RR |-> A ) ` y ) <-> 0 <_ ( ( x e. RR |-> A ) ` x ) ) )
10 9 8 ifbieq1d 
 |-  ( y = x -> if ( 0 <_ ( ( x e. RR |-> A ) ` y ) , ( ( x e. RR |-> A ) ` y ) , 0 ) = if ( 0 <_ ( ( x e. RR |-> A ) ` x ) , ( ( x e. RR |-> A ) ` x ) , 0 ) )
11 6 7 10 cbvmpt 
 |-  ( y e. RR |-> if ( 0 <_ ( ( x e. RR |-> A ) ` y ) , ( ( x e. RR |-> A ) ` y ) , 0 ) ) = ( x e. RR |-> if ( 0 <_ ( ( x e. RR |-> A ) ` x ) , ( ( x e. RR |-> A ) ` x ) , 0 ) )
12 simpr 
 |-  ( ( ph /\ x e. RR ) -> x e. RR )
13 i1ff 
 |-  ( ( x e. RR |-> A ) e. dom S.1 -> ( x e. RR |-> A ) : RR --> RR )
14 1 13 syl 
 |-  ( ph -> ( x e. RR |-> A ) : RR --> RR )
15 14 fvmptelrn 
 |-  ( ( ph /\ x e. RR ) -> A e. RR )
16 eqid 
 |-  ( x e. RR |-> A ) = ( x e. RR |-> A )
17 16 fvmpt2 
 |-  ( ( x e. RR /\ A e. RR ) -> ( ( x e. RR |-> A ) ` x ) = A )
18 12 15 17 syl2anc 
 |-  ( ( ph /\ x e. RR ) -> ( ( x e. RR |-> A ) ` x ) = A )
19 18 breq2d 
 |-  ( ( ph /\ x e. RR ) -> ( 0 <_ ( ( x e. RR |-> A ) ` x ) <-> 0 <_ A ) )
20 19 18 ifbieq1d 
 |-  ( ( ph /\ x e. RR ) -> if ( 0 <_ ( ( x e. RR |-> A ) ` x ) , ( ( x e. RR |-> A ) ` x ) , 0 ) = if ( 0 <_ A , A , 0 ) )
21 20 mpteq2dva 
 |-  ( ph -> ( x e. RR |-> if ( 0 <_ ( ( x e. RR |-> A ) ` x ) , ( ( x e. RR |-> A ) ` x ) , 0 ) ) = ( x e. RR |-> if ( 0 <_ A , A , 0 ) ) )
22 11 21 syl5eq 
 |-  ( ph -> ( y e. RR |-> if ( 0 <_ ( ( x e. RR |-> A ) ` y ) , ( ( x e. RR |-> A ) ` y ) , 0 ) ) = ( x e. RR |-> if ( 0 <_ A , A , 0 ) ) )
23 eqid 
 |-  ( y e. RR |-> if ( 0 <_ ( ( x e. RR |-> A ) ` y ) , ( ( x e. RR |-> A ) ` y ) , 0 ) ) = ( y e. RR |-> if ( 0 <_ ( ( x e. RR |-> A ) ` y ) , ( ( x e. RR |-> A ) ` y ) , 0 ) )
24 23 i1fpos 
 |-  ( ( x e. RR |-> A ) e. dom S.1 -> ( y e. RR |-> if ( 0 <_ ( ( x e. RR |-> A ) ` y ) , ( ( x e. RR |-> A ) ` y ) , 0 ) ) e. dom S.1 )
25 1 24 syl 
 |-  ( ph -> ( y e. RR |-> if ( 0 <_ ( ( x e. RR |-> A ) ` y ) , ( ( x e. RR |-> A ) ` y ) , 0 ) ) e. dom S.1 )
26 22 25 eqeltrrd 
 |-  ( ph -> ( x e. RR |-> if ( 0 <_ A , A , 0 ) ) e. dom S.1 )