Metamath Proof Explorer

Theorem itg2cnlem1

Description: Lemma for itgcn . (Contributed by Mario Carneiro, 30-Aug-2014)

Ref Expression
Hypotheses itg2cn.1 
|- ( ph -> F : RR --> ( 0 [,) +oo ) )
itg2cn.2 
|- ( ph -> F e. MblFn )
itg2cn.3 
|- ( ph -> ( S.2 ` F ) e. RR )
Assertion itg2cnlem1 
|- ( ph -> sup ( ran ( n e. NN |-> ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ) , RR* , < ) = ( S.2 ` F ) )

Proof

Step Hyp Ref Expression
1 itg2cn.1 
 |-  ( ph -> F : RR --> ( 0 [,) +oo ) )
2 itg2cn.2 
 |-  ( ph -> F e. MblFn )
3 itg2cn.3 
 |-  ( ph -> ( S.2 ` F ) e. RR )
4 fvex 
 |-  ( F ` x ) e. _V
5 c0ex 
 |-  0 e. _V
6 4 5 ifex 
 |-  if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) e. _V
7 eqid 
 |-  ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) = ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) )
8 7 fvmpt2 
 |-  ( ( x e. RR /\ if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) e. _V ) -> ( ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ` x ) = if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) )
9 6 8 mpan2 
 |-  ( x e. RR -> ( ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ` x ) = if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) )
10 9 mpteq2dv 
 |-  ( x e. RR -> ( n e. NN |-> ( ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ` x ) ) = ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) )
11 10 rneqd 
 |-  ( x e. RR -> ran ( n e. NN |-> ( ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ` x ) ) = ran ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) )
12 11 supeq1d 
 |-  ( x e. RR -> sup ( ran ( n e. NN |-> ( ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ` x ) ) , RR , < ) = sup ( ran ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) , RR , < ) )
13 12 mpteq2ia 
 |-  ( x e. RR |-> sup ( ran ( n e. NN |-> ( ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ` x ) ) , RR , < ) ) = ( x e. RR |-> sup ( ran ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) , RR , < ) )
14 nfcv 
 |-  F/_ y sup ( ran ( n e. NN |-> ( ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ` x ) ) , RR , < )
15 nfcv 
 |-  F/_ x NN
16 nfmpt1 
 |-  F/_ x ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) )
17 15 16 nfmpt 
 |-  F/_ x ( n e. NN |-> ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) )
18 nfcv 
 |-  F/_ x m
19 17 18 nffv 
 |-  F/_ x ( ( n e. NN |-> ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ` m )
20 nfcv 
 |-  F/_ x y
21 19 20 nffv 
 |-  F/_ x ( ( ( n e. NN |-> ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ` m ) ` y )
22 15 21 nfmpt 
 |-  F/_ x ( m e. NN |-> ( ( ( n e. NN |-> ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ` m ) ` y ) )
23 22 nfrn 
 |-  F/_ x ran ( m e. NN |-> ( ( ( n e. NN |-> ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ` m ) ` y ) )
24 nfcv 
 |-  F/_ x RR
25 nfcv 
 |-  F/_ x <
26 23 24 25 nfsup 
 |-  F/_ x sup ( ran ( m e. NN |-> ( ( ( n e. NN |-> ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ` m ) ` y ) ) , RR , < )
27 fveq2 
 |-  ( x = y -> ( ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ` x ) = ( ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ` y ) )
28 27 mpteq2dv 
 |-  ( x = y -> ( n e. NN |-> ( ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ` x ) ) = ( n e. NN |-> ( ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ` y ) ) )
29 breq2 
 |-  ( n = m -> ( ( F ` x ) <_ n <-> ( F ` x ) <_ m ) )
30 29 ifbid 
 |-  ( n = m -> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) = if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) )
31 30 mpteq2dv 
 |-  ( n = m -> ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) = ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) )
32 31 fveq1d 
 |-  ( n = m -> ( ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ` y ) = ( ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) ` y ) )
33 32 cbvmptv 
 |-  ( n e. NN |-> ( ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ` y ) ) = ( m e. NN |-> ( ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) ` y ) )
34 eqid 
 |-  ( n e. NN |-> ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) = ( n e. NN |-> ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) )
35 reex 
 |-  RR e. _V
36 35 mptex 
 |-  ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) e. _V
37 31 34 36 fvmpt 
 |-  ( m e. NN -> ( ( n e. NN |-> ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ` m ) = ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) )
38 37 fveq1d 
 |-  ( m e. NN -> ( ( ( n e. NN |-> ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ` m ) ` y ) = ( ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) ` y ) )
39 38 mpteq2ia 
 |-  ( m e. NN |-> ( ( ( n e. NN |-> ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ` m ) ` y ) ) = ( m e. NN |-> ( ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) ` y ) )
40 33 39 eqtr4i 
 |-  ( n e. NN |-> ( ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ` y ) ) = ( m e. NN |-> ( ( ( n e. NN |-> ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ` m ) ` y ) )
41 28 40 eqtrdi 
 |-  ( x = y -> ( n e. NN |-> ( ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ` x ) ) = ( m e. NN |-> ( ( ( n e. NN |-> ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ` m ) ` y ) ) )
42 41 rneqd 
 |-  ( x = y -> ran ( n e. NN |-> ( ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ` x ) ) = ran ( m e. NN |-> ( ( ( n e. NN |-> ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ` m ) ` y ) ) )
43 42 supeq1d 
 |-  ( x = y -> sup ( ran ( n e. NN |-> ( ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ` x ) ) , RR , < ) = sup ( ran ( m e. NN |-> ( ( ( n e. NN |-> ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ` m ) ` y ) ) , RR , < ) )
44 14 26 43 cbvmpt 
 |-  ( x e. RR |-> sup ( ran ( n e. NN |-> ( ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ` x ) ) , RR , < ) ) = ( y e. RR |-> sup ( ran ( m e. NN |-> ( ( ( n e. NN |-> ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ` m ) ` y ) ) , RR , < ) )
45 13 44 eqtr3i 
 |-  ( x e. RR |-> sup ( ran ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) , RR , < ) ) = ( y e. RR |-> sup ( ran ( m e. NN |-> ( ( ( n e. NN |-> ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ` m ) ` y ) ) , RR , < ) )
46 fveq2 
 |-  ( x = y -> ( F ` x ) = ( F ` y ) )
47 46 breq1d 
 |-  ( x = y -> ( ( F ` x ) <_ m <-> ( F ` y ) <_ m ) )
48 47 46 ifbieq1d 
 |-  ( x = y -> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) = if ( ( F ` y ) <_ m , ( F ` y ) , 0 ) )
49 48 cbvmptv 
 |-  ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) = ( y e. RR |-> if ( ( F ` y ) <_ m , ( F ` y ) , 0 ) )
50 37 adantl 
 |-  ( ( ph /\ m e. NN ) -> ( ( n e. NN |-> ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ` m ) = ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) )
51 nnre 
 |-  ( m e. NN -> m e. RR )
52 51 ad2antlr 
 |-  ( ( ( ph /\ m e. NN ) /\ y e. RR ) -> m e. RR )
53 52 rexrd 
 |-  ( ( ( ph /\ m e. NN ) /\ y e. RR ) -> m e. RR* )
54 elioopnf 
 |-  ( m e. RR* -> ( ( F ` y ) e. ( m (,) +oo ) <-> ( ( F ` y ) e. RR /\ m < ( F ` y ) ) ) )
55 53 54 syl 
 |-  ( ( ( ph /\ m e. NN ) /\ y e. RR ) -> ( ( F ` y ) e. ( m (,) +oo ) <-> ( ( F ` y ) e. RR /\ m < ( F ` y ) ) ) )
56 simpr 
 |-  ( ( ( ph /\ m e. NN ) /\ y e. RR ) -> y e. RR )
57 1 ffnd 
 |-  ( ph -> F Fn RR )
58 57 ad2antrr 
 |-  ( ( ( ph /\ m e. NN ) /\ y e. RR ) -> F Fn RR )
59 elpreima 
 |-  ( F Fn RR -> ( y e. ( `' F " ( m (,) +oo ) ) <-> ( y e. RR /\ ( F ` y ) e. ( m (,) +oo ) ) ) )
60 58 59 syl 
 |-  ( ( ( ph /\ m e. NN ) /\ y e. RR ) -> ( y e. ( `' F " ( m (,) +oo ) ) <-> ( y e. RR /\ ( F ` y ) e. ( m (,) +oo ) ) ) )
61 56 60 mpbirand 
 |-  ( ( ( ph /\ m e. NN ) /\ y e. RR ) -> ( y e. ( `' F " ( m (,) +oo ) ) <-> ( F ` y ) e. ( m (,) +oo ) ) )
62 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
63 fss 
 |-  ( ( F : RR --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ RR ) -> F : RR --> RR )
64 1 62 63 sylancl 
 |-  ( ph -> F : RR --> RR )
65 64 adantr 
 |-  ( ( ph /\ m e. NN ) -> F : RR --> RR )
66 65 ffvelcdmda 
 |-  ( ( ( ph /\ m e. NN ) /\ y e. RR ) -> ( F ` y ) e. RR )
67 66 biantrurd 
 |-  ( ( ( ph /\ m e. NN ) /\ y e. RR ) -> ( m < ( F ` y ) <-> ( ( F ` y ) e. RR /\ m < ( F ` y ) ) ) )
68 55 61 67 3bitr4d 
 |-  ( ( ( ph /\ m e. NN ) /\ y e. RR ) -> ( y e. ( `' F " ( m (,) +oo ) ) <-> m < ( F ` y ) ) )
69 68 notbid 
 |-  ( ( ( ph /\ m e. NN ) /\ y e. RR ) -> ( -. y e. ( `' F " ( m (,) +oo ) ) <-> -. m < ( F ` y ) ) )
70 eldif 
 |-  ( y e. ( RR \ ( `' F " ( m (,) +oo ) ) ) <-> ( y e. RR /\ -. y e. ( `' F " ( m (,) +oo ) ) ) )
71 70 baib 
 |-  ( y e. RR -> ( y e. ( RR \ ( `' F " ( m (,) +oo ) ) ) <-> -. y e. ( `' F " ( m (,) +oo ) ) ) )
72 71 adantl 
 |-  ( ( ( ph /\ m e. NN ) /\ y e. RR ) -> ( y e. ( RR \ ( `' F " ( m (,) +oo ) ) ) <-> -. y e. ( `' F " ( m (,) +oo ) ) ) )
73 66 52 lenltd 
 |-  ( ( ( ph /\ m e. NN ) /\ y e. RR ) -> ( ( F ` y ) <_ m <-> -. m < ( F ` y ) ) )
74 69 72 73 3bitr4d 
 |-  ( ( ( ph /\ m e. NN ) /\ y e. RR ) -> ( y e. ( RR \ ( `' F " ( m (,) +oo ) ) ) <-> ( F ` y ) <_ m ) )
75 74 ifbid 
 |-  ( ( ( ph /\ m e. NN ) /\ y e. RR ) -> if ( y e. ( RR \ ( `' F " ( m (,) +oo ) ) ) , ( F ` y ) , 0 ) = if ( ( F ` y ) <_ m , ( F ` y ) , 0 ) )
76 75 mpteq2dva 
 |-  ( ( ph /\ m e. NN ) -> ( y e. RR |-> if ( y e. ( RR \ ( `' F " ( m (,) +oo ) ) ) , ( F ` y ) , 0 ) ) = ( y e. RR |-> if ( ( F ` y ) <_ m , ( F ` y ) , 0 ) ) )
77 49 50 76 3eqtr4a 
 |-  ( ( ph /\ m e. NN ) -> ( ( n e. NN |-> ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ` m ) = ( y e. RR |-> if ( y e. ( RR \ ( `' F " ( m (,) +oo ) ) ) , ( F ` y ) , 0 ) ) )
78 difss 
 |-  ( RR \ ( `' F " ( m (,) +oo ) ) ) C_ RR
79 78 a1i 
 |-  ( ( ph /\ m e. NN ) -> ( RR \ ( `' F " ( m (,) +oo ) ) ) C_ RR )
80 rembl 
 |-  RR e. dom vol
81 80 a1i 
 |-  ( ( ph /\ m e. NN ) -> RR e. dom vol )
82 fvex 
 |-  ( F ` y ) e. _V
83 82 5 ifex 
 |-  if ( y e. ( RR \ ( `' F " ( m (,) +oo ) ) ) , ( F ` y ) , 0 ) e. _V
84 83 a1i 
 |-  ( ( ( ph /\ m e. NN ) /\ y e. ( RR \ ( `' F " ( m (,) +oo ) ) ) ) -> if ( y e. ( RR \ ( `' F " ( m (,) +oo ) ) ) , ( F ` y ) , 0 ) e. _V )
85 eldifn 
 |-  ( y e. ( RR \ ( RR \ ( `' F " ( m (,) +oo ) ) ) ) -> -. y e. ( RR \ ( `' F " ( m (,) +oo ) ) ) )
86 85 adantl 
 |-  ( ( ( ph /\ m e. NN ) /\ y e. ( RR \ ( RR \ ( `' F " ( m (,) +oo ) ) ) ) ) -> -. y e. ( RR \ ( `' F " ( m (,) +oo ) ) ) )
87 86 iffalsed 
 |-  ( ( ( ph /\ m e. NN ) /\ y e. ( RR \ ( RR \ ( `' F " ( m (,) +oo ) ) ) ) ) -> if ( y e. ( RR \ ( `' F " ( m (,) +oo ) ) ) , ( F ` y ) , 0 ) = 0 )
88 iftrue 
 |-  ( y e. ( RR \ ( `' F " ( m (,) +oo ) ) ) -> if ( y e. ( RR \ ( `' F " ( m (,) +oo ) ) ) , ( F ` y ) , 0 ) = ( F ` y ) )
89 88 mpteq2ia 
 |-  ( y e. ( RR \ ( `' F " ( m (,) +oo ) ) ) |-> if ( y e. ( RR \ ( `' F " ( m (,) +oo ) ) ) , ( F ` y ) , 0 ) ) = ( y e. ( RR \ ( `' F " ( m (,) +oo ) ) ) |-> ( F ` y ) )
90 resmpt 
 |-  ( ( RR \ ( `' F " ( m (,) +oo ) ) ) C_ RR -> ( ( y e. RR |-> ( F ` y ) ) |` ( RR \ ( `' F " ( m (,) +oo ) ) ) ) = ( y e. ( RR \ ( `' F " ( m (,) +oo ) ) ) |-> ( F ` y ) ) )
91 78 90 ax-mp 
 |-  ( ( y e. RR |-> ( F ` y ) ) |` ( RR \ ( `' F " ( m (,) +oo ) ) ) ) = ( y e. ( RR \ ( `' F " ( m (,) +oo ) ) ) |-> ( F ` y ) )
92 89 91 eqtr4i 
 |-  ( y e. ( RR \ ( `' F " ( m (,) +oo ) ) ) |-> if ( y e. ( RR \ ( `' F " ( m (,) +oo ) ) ) , ( F ` y ) , 0 ) ) = ( ( y e. RR |-> ( F ` y ) ) |` ( RR \ ( `' F " ( m (,) +oo ) ) ) )
93 1 feqmptd 
 |-  ( ph -> F = ( y e. RR |-> ( F ` y ) ) )
94 93 2 eqeltrrd 
 |-  ( ph -> ( y e. RR |-> ( F ` y ) ) e. MblFn )
95 mbfima 
 |-  ( ( F e. MblFn /\ F : RR --> RR ) -> ( `' F " ( m (,) +oo ) ) e. dom vol )
96 2 64 95 syl2anc 
 |-  ( ph -> ( `' F " ( m (,) +oo ) ) e. dom vol )
97 cmmbl 
 |-  ( ( `' F " ( m (,) +oo ) ) e. dom vol -> ( RR \ ( `' F " ( m (,) +oo ) ) ) e. dom vol )
98 96 97 syl 
 |-  ( ph -> ( RR \ ( `' F " ( m (,) +oo ) ) ) e. dom vol )
99 mbfres 
 |-  ( ( ( y e. RR |-> ( F ` y ) ) e. MblFn /\ ( RR \ ( `' F " ( m (,) +oo ) ) ) e. dom vol ) -> ( ( y e. RR |-> ( F ` y ) ) |` ( RR \ ( `' F " ( m (,) +oo ) ) ) ) e. MblFn )
100 94 98 99 syl2anc 
 |-  ( ph -> ( ( y e. RR |-> ( F ` y ) ) |` ( RR \ ( `' F " ( m (,) +oo ) ) ) ) e. MblFn )
101 92 100 eqeltrid 
 |-  ( ph -> ( y e. ( RR \ ( `' F " ( m (,) +oo ) ) ) |-> if ( y e. ( RR \ ( `' F " ( m (,) +oo ) ) ) , ( F ` y ) , 0 ) ) e. MblFn )
102 101 adantr 
 |-  ( ( ph /\ m e. NN ) -> ( y e. ( RR \ ( `' F " ( m (,) +oo ) ) ) |-> if ( y e. ( RR \ ( `' F " ( m (,) +oo ) ) ) , ( F ` y ) , 0 ) ) e. MblFn )
103 79 81 84 87 102 mbfss 
 |-  ( ( ph /\ m e. NN ) -> ( y e. RR |-> if ( y e. ( RR \ ( `' F " ( m (,) +oo ) ) ) , ( F ` y ) , 0 ) ) e. MblFn )
104 77 103 eqeltrd 
 |-  ( ( ph /\ m e. NN ) -> ( ( n e. NN |-> ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ` m ) e. MblFn )
105 1 ffvelcdmda 
 |-  ( ( ph /\ x e. RR ) -> ( F ` x ) e. ( 0 [,) +oo ) )
106 0e0icopnf 
 |-  0 e. ( 0 [,) +oo )
107 ifcl 
 |-  ( ( ( F ` x ) e. ( 0 [,) +oo ) /\ 0 e. ( 0 [,) +oo ) ) -> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) e. ( 0 [,) +oo ) )
108 105 106 107 sylancl 
 |-  ( ( ph /\ x e. RR ) -> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) e. ( 0 [,) +oo ) )
109 108 adantlr 
 |-  ( ( ( ph /\ m e. NN ) /\ x e. RR ) -> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) e. ( 0 [,) +oo ) )
110 50 109 fmpt3d 
 |-  ( ( ph /\ m e. NN ) -> ( ( n e. NN |-> ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ` m ) : RR --> ( 0 [,) +oo ) )
111 elrege0 
 |-  ( ( F ` x ) e. ( 0 [,) +oo ) <-> ( ( F ` x ) e. RR /\ 0 <_ ( F ` x ) ) )
112 105 111 sylib 
 |-  ( ( ph /\ x e. RR ) -> ( ( F ` x ) e. RR /\ 0 <_ ( F ` x ) ) )
113 112 simpld 
 |-  ( ( ph /\ x e. RR ) -> ( F ` x ) e. RR )
114 113 adantlr 
 |-  ( ( ( ph /\ m e. NN ) /\ x e. RR ) -> ( F ` x ) e. RR )
115 114 adantr 
 |-  ( ( ( ( ph /\ m e. NN ) /\ x e. RR ) /\ ( F ` x ) <_ m ) -> ( F ` x ) e. RR )
116 115 leidd 
 |-  ( ( ( ( ph /\ m e. NN ) /\ x e. RR ) /\ ( F ` x ) <_ m ) -> ( F ` x ) <_ ( F ` x ) )
117 iftrue 
 |-  ( ( F ` x ) <_ m -> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) = ( F ` x ) )
118 117 adantl 
 |-  ( ( ( ( ph /\ m e. NN ) /\ x e. RR ) /\ ( F ` x ) <_ m ) -> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) = ( F ` x ) )
119 51 ad3antlr 
 |-  ( ( ( ( ph /\ m e. NN ) /\ x e. RR ) /\ ( F ` x ) <_ m ) -> m e. RR )
120 peano2re 
 |-  ( m e. RR -> ( m + 1 ) e. RR )
121 119 120 syl 
 |-  ( ( ( ( ph /\ m e. NN ) /\ x e. RR ) /\ ( F ` x ) <_ m ) -> ( m + 1 ) e. RR )
122 simpr 
 |-  ( ( ( ( ph /\ m e. NN ) /\ x e. RR ) /\ ( F ` x ) <_ m ) -> ( F ` x ) <_ m )
123 119 lep1d 
 |-  ( ( ( ( ph /\ m e. NN ) /\ x e. RR ) /\ ( F ` x ) <_ m ) -> m <_ ( m + 1 ) )
124 115 119 121 122 123 letrd 
 |-  ( ( ( ( ph /\ m e. NN ) /\ x e. RR ) /\ ( F ` x ) <_ m ) -> ( F ` x ) <_ ( m + 1 ) )
125 124 iftrued 
 |-  ( ( ( ( ph /\ m e. NN ) /\ x e. RR ) /\ ( F ` x ) <_ m ) -> if ( ( F ` x ) <_ ( m + 1 ) , ( F ` x ) , 0 ) = ( F ` x ) )
126 116 118 125 3brtr4d 
 |-  ( ( ( ( ph /\ m e. NN ) /\ x e. RR ) /\ ( F ` x ) <_ m ) -> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) <_ if ( ( F ` x ) <_ ( m + 1 ) , ( F ` x ) , 0 ) )
127 iffalse 
 |-  ( -. ( F ` x ) <_ m -> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) = 0 )
128 127 adantl 
 |-  ( ( ( ( ph /\ m e. NN ) /\ x e. RR ) /\ -. ( F ` x ) <_ m ) -> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) = 0 )
129 112 simprd 
 |-  ( ( ph /\ x e. RR ) -> 0 <_ ( F ` x ) )
130 0le0 
 |-  0 <_ 0
131 breq2 
 |-  ( ( F ` x ) = if ( ( F ` x ) <_ ( m + 1 ) , ( F ` x ) , 0 ) -> ( 0 <_ ( F ` x ) <-> 0 <_ if ( ( F ` x ) <_ ( m + 1 ) , ( F ` x ) , 0 ) ) )
132 breq2 
 |-  ( 0 = if ( ( F ` x ) <_ ( m + 1 ) , ( F ` x ) , 0 ) -> ( 0 <_ 0 <-> 0 <_ if ( ( F ` x ) <_ ( m + 1 ) , ( F ` x ) , 0 ) ) )
133 131 132 ifboth 
 |-  ( ( 0 <_ ( F ` x ) /\ 0 <_ 0 ) -> 0 <_ if ( ( F ` x ) <_ ( m + 1 ) , ( F ` x ) , 0 ) )
134 129 130 133 sylancl 
 |-  ( ( ph /\ x e. RR ) -> 0 <_ if ( ( F ` x ) <_ ( m + 1 ) , ( F ` x ) , 0 ) )
135 134 adantlr 
 |-  ( ( ( ph /\ m e. NN ) /\ x e. RR ) -> 0 <_ if ( ( F ` x ) <_ ( m + 1 ) , ( F ` x ) , 0 ) )
136 135 adantr 
 |-  ( ( ( ( ph /\ m e. NN ) /\ x e. RR ) /\ -. ( F ` x ) <_ m ) -> 0 <_ if ( ( F ` x ) <_ ( m + 1 ) , ( F ` x ) , 0 ) )
137 128 136 eqbrtrd 
 |-  ( ( ( ( ph /\ m e. NN ) /\ x e. RR ) /\ -. ( F ` x ) <_ m ) -> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) <_ if ( ( F ` x ) <_ ( m + 1 ) , ( F ` x ) , 0 ) )
138 126 137 pm2.61dan 
 |-  ( ( ( ph /\ m e. NN ) /\ x e. RR ) -> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) <_ if ( ( F ` x ) <_ ( m + 1 ) , ( F ` x ) , 0 ) )
139 138 ralrimiva 
 |-  ( ( ph /\ m e. NN ) -> A. x e. RR if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) <_ if ( ( F ` x ) <_ ( m + 1 ) , ( F ` x ) , 0 ) )
140 4 5 ifex 
 |-  if ( ( F ` x ) <_ ( m + 1 ) , ( F ` x ) , 0 ) e. _V
141 140 a1i 
 |-  ( ( ( ph /\ m e. NN ) /\ x e. RR ) -> if ( ( F ` x ) <_ ( m + 1 ) , ( F ` x ) , 0 ) e. _V )
142 eqidd 
 |-  ( ( ph /\ m e. NN ) -> ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) = ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) )
143 eqidd 
 |-  ( ( ph /\ m e. NN ) -> ( x e. RR |-> if ( ( F ` x ) <_ ( m + 1 ) , ( F ` x ) , 0 ) ) = ( x e. RR |-> if ( ( F ` x ) <_ ( m + 1 ) , ( F ` x ) , 0 ) ) )
144 81 109 141 142 143 ofrfval2 
 |-  ( ( ph /\ m e. NN ) -> ( ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) oR <_ ( x e. RR |-> if ( ( F ` x ) <_ ( m + 1 ) , ( F ` x ) , 0 ) ) <-> A. x e. RR if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) <_ if ( ( F ` x ) <_ ( m + 1 ) , ( F ` x ) , 0 ) ) )
145 139 144 mpbird 
 |-  ( ( ph /\ m e. NN ) -> ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) oR <_ ( x e. RR |-> if ( ( F ` x ) <_ ( m + 1 ) , ( F ` x ) , 0 ) ) )
146 peano2nn 
 |-  ( m e. NN -> ( m + 1 ) e. NN )
147 146 adantl 
 |-  ( ( ph /\ m e. NN ) -> ( m + 1 ) e. NN )
148 breq2 
 |-  ( n = ( m + 1 ) -> ( ( F ` x ) <_ n <-> ( F ` x ) <_ ( m + 1 ) ) )
149 148 ifbid 
 |-  ( n = ( m + 1 ) -> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) = if ( ( F ` x ) <_ ( m + 1 ) , ( F ` x ) , 0 ) )
150 149 mpteq2dv 
 |-  ( n = ( m + 1 ) -> ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) = ( x e. RR |-> if ( ( F ` x ) <_ ( m + 1 ) , ( F ` x ) , 0 ) ) )
151 35 mptex 
 |-  ( x e. RR |-> if ( ( F ` x ) <_ ( m + 1 ) , ( F ` x ) , 0 ) ) e. _V
152 150 34 151 fvmpt 
 |-  ( ( m + 1 ) e. NN -> ( ( n e. NN |-> ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ` ( m + 1 ) ) = ( x e. RR |-> if ( ( F ` x ) <_ ( m + 1 ) , ( F ` x ) , 0 ) ) )
153 147 152 syl 
 |-  ( ( ph /\ m e. NN ) -> ( ( n e. NN |-> ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ` ( m + 1 ) ) = ( x e. RR |-> if ( ( F ` x ) <_ ( m + 1 ) , ( F ` x ) , 0 ) ) )
154 145 50 153 3brtr4d 
 |-  ( ( ph /\ m e. NN ) -> ( ( n e. NN |-> ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ` m ) oR <_ ( ( n e. NN |-> ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ` ( m + 1 ) ) )
155 64 ffvelcdmda 
 |-  ( ( ph /\ y e. RR ) -> ( F ` y ) e. RR )
156 37 adantl 
 |-  ( ( ( ph /\ y e. RR ) /\ m e. NN ) -> ( ( n e. NN |-> ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ` m ) = ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) )
157 156 fveq1d 
 |-  ( ( ( ph /\ y e. RR ) /\ m e. NN ) -> ( ( ( n e. NN |-> ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ` m ) ` y ) = ( ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) ` y ) )
158 113 leidd 
 |-  ( ( ph /\ x e. RR ) -> ( F ` x ) <_ ( F ` x ) )
159 breq1 
 |-  ( ( F ` x ) = if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) -> ( ( F ` x ) <_ ( F ` x ) <-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) <_ ( F ` x ) ) )
160 breq1 
 |-  ( 0 = if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) -> ( 0 <_ ( F ` x ) <-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) <_ ( F ` x ) ) )
161 159 160 ifboth 
 |-  ( ( ( F ` x ) <_ ( F ` x ) /\ 0 <_ ( F ` x ) ) -> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) <_ ( F ` x ) )
162 158 129 161 syl2anc 
 |-  ( ( ph /\ x e. RR ) -> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) <_ ( F ` x ) )
163 162 adantlr 
 |-  ( ( ( ph /\ m e. NN ) /\ x e. RR ) -> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) <_ ( F ` x ) )
164 163 ralrimiva 
 |-  ( ( ph /\ m e. NN ) -> A. x e. RR if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) <_ ( F ` x ) )
165 35 a1i 
 |-  ( ( ph /\ m e. NN ) -> RR e. _V )
166 4 5 ifex 
 |-  if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) e. _V
167 166 a1i 
 |-  ( ( ( ph /\ m e. NN ) /\ x e. RR ) -> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) e. _V )
168 1 feqmptd 
 |-  ( ph -> F = ( x e. RR |-> ( F ` x ) ) )
169 168 adantr 
 |-  ( ( ph /\ m e. NN ) -> F = ( x e. RR |-> ( F ` x ) ) )
170 165 167 114 142 169 ofrfval2 
 |-  ( ( ph /\ m e. NN ) -> ( ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) oR <_ F <-> A. x e. RR if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) <_ ( F ` x ) ) )
171 164 170 mpbird 
 |-  ( ( ph /\ m e. NN ) -> ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) oR <_ F )
172 167 fmpttd 
 |-  ( ( ph /\ m e. NN ) -> ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) : RR --> _V )
173 172 ffnd 
 |-  ( ( ph /\ m e. NN ) -> ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) Fn RR )
174 57 adantr 
 |-  ( ( ph /\ m e. NN ) -> F Fn RR )
175 inidm 
 |-  ( RR i^i RR ) = RR
176 eqidd 
 |-  ( ( ( ph /\ m e. NN ) /\ y e. RR ) -> ( ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) ` y ) = ( ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) ` y ) )
177 eqidd 
 |-  ( ( ( ph /\ m e. NN ) /\ y e. RR ) -> ( F ` y ) = ( F ` y ) )
178 173 174 165 165 175 176 177 ofrfval 
 |-  ( ( ph /\ m e. NN ) -> ( ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) oR <_ F <-> A. y e. RR ( ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) ` y ) <_ ( F ` y ) ) )
179 171 178 mpbid 
 |-  ( ( ph /\ m e. NN ) -> A. y e. RR ( ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) ` y ) <_ ( F ` y ) )
180 179 r19.21bi 
 |-  ( ( ( ph /\ m e. NN ) /\ y e. RR ) -> ( ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) ` y ) <_ ( F ` y ) )
181 180 an32s 
 |-  ( ( ( ph /\ y e. RR ) /\ m e. NN ) -> ( ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) ` y ) <_ ( F ` y ) )
182 157 181 eqbrtrd 
 |-  ( ( ( ph /\ y e. RR ) /\ m e. NN ) -> ( ( ( n e. NN |-> ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ` m ) ` y ) <_ ( F ` y ) )
183 182 ralrimiva 
 |-  ( ( ph /\ y e. RR ) -> A. m e. NN ( ( ( n e. NN |-> ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ` m ) ` y ) <_ ( F ` y ) )
184 brralrspcev 
 |-  ( ( ( F ` y ) e. RR /\ A. m e. NN ( ( ( n e. NN |-> ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ` m ) ` y ) <_ ( F ` y ) ) -> E. z e. RR A. m e. NN ( ( ( n e. NN |-> ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ` m ) ` y ) <_ z )
185 155 183 184 syl2anc 
 |-  ( ( ph /\ y e. RR ) -> E. z e. RR A. m e. NN ( ( ( n e. NN |-> ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ` m ) ` y ) <_ z )
186 31 fveq2d 
 |-  ( n = m -> ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) ) )
187 186 cbvmptv 
 |-  ( n e. NN |-> ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ) = ( m e. NN |-> ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) ) )
188 37 fveq2d 
 |-  ( m e. NN -> ( S.2 ` ( ( n e. NN |-> ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ` m ) ) = ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) ) )
189 188 mpteq2ia 
 |-  ( m e. NN |-> ( S.2 ` ( ( n e. NN |-> ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ` m ) ) ) = ( m e. NN |-> ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) ) ) )
190 187 189 eqtr4i 
 |-  ( n e. NN |-> ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ) = ( m e. NN |-> ( S.2 ` ( ( n e. NN |-> ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ` m ) ) )
191 190 rneqi 
 |-  ran ( n e. NN |-> ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ) = ran ( m e. NN |-> ( S.2 ` ( ( n e. NN |-> ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ` m ) ) )
192 191 supeq1i 
 |-  sup ( ran ( n e. NN |-> ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ) , RR* , < ) = sup ( ran ( m e. NN |-> ( S.2 ` ( ( n e. NN |-> ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ` m ) ) ) , RR* , < )
193 45 104 110 154 185 192 itg2mono 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> sup ( ran ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) , RR , < ) ) ) = sup ( ran ( n e. NN |-> ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ) , RR* , < ) )
194 eqid 
 |-  ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) = ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) )
195 30 194 166 fvmpt 
 |-  ( m e. NN -> ( ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ` m ) = if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) )
196 195 adantl 
 |-  ( ( ( ph /\ x e. RR ) /\ m e. NN ) -> ( ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ` m ) = if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) )
197 162 adantr 
 |-  ( ( ( ph /\ x e. RR ) /\ m e. NN ) -> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) <_ ( F ` x ) )
198 196 197 eqbrtrd 
 |-  ( ( ( ph /\ x e. RR ) /\ m e. NN ) -> ( ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ` m ) <_ ( F ` x ) )
199 198 ralrimiva 
 |-  ( ( ph /\ x e. RR ) -> A. m e. NN ( ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ` m ) <_ ( F ` x ) )
200 6 a1i 
 |-  ( ( ( ph /\ x e. RR ) /\ n e. NN ) -> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) e. _V )
201 200 fmpttd 
 |-  ( ( ph /\ x e. RR ) -> ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) : NN --> _V )
202 201 ffnd 
 |-  ( ( ph /\ x e. RR ) -> ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) Fn NN )
203 breq1 
 |-  ( w = ( ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ` m ) -> ( w <_ ( F ` x ) <-> ( ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ` m ) <_ ( F ` x ) ) )
204 203 ralrn 
 |-  ( ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) Fn NN -> ( A. w e. ran ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) w <_ ( F ` x ) <-> A. m e. NN ( ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ` m ) <_ ( F ` x ) ) )
205 202 204 syl 
 |-  ( ( ph /\ x e. RR ) -> ( A. w e. ran ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) w <_ ( F ` x ) <-> A. m e. NN ( ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ` m ) <_ ( F ` x ) ) )
206 199 205 mpbird 
 |-  ( ( ph /\ x e. RR ) -> A. w e. ran ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) w <_ ( F ` x ) )
207 113 adantr 
 |-  ( ( ( ph /\ x e. RR ) /\ n e. NN ) -> ( F ` x ) e. RR )
208 0re 
 |-  0 e. RR
209 ifcl 
 |-  ( ( ( F ` x ) e. RR /\ 0 e. RR ) -> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) e. RR )
210 207 208 209 sylancl 
 |-  ( ( ( ph /\ x e. RR ) /\ n e. NN ) -> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) e. RR )
211 210 fmpttd 
 |-  ( ( ph /\ x e. RR ) -> ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) : NN --> RR )
212 211 frnd 
 |-  ( ( ph /\ x e. RR ) -> ran ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) C_ RR )
213 1nn 
 |-  1 e. NN
214 194 210 dmmptd 
 |-  ( ( ph /\ x e. RR ) -> dom ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) = NN )
215 213 214 eleqtrrid 
 |-  ( ( ph /\ x e. RR ) -> 1 e. dom ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) )
216 n0i 
 |-  ( 1 e. dom ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) -> -. dom ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) = (/) )
217 dm0rn0 
 |-  ( dom ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) = (/) <-> ran ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) = (/) )
218 217 necon3bbii 
 |-  ( -. dom ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) = (/) <-> ran ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) =/= (/) )
219 216 218 sylib 
 |-  ( 1 e. dom ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) -> ran ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) =/= (/) )
220 215 219 syl 
 |-  ( ( ph /\ x e. RR ) -> ran ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) =/= (/) )
221 brralrspcev 
 |-  ( ( ( F ` x ) e. RR /\ A. w e. ran ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) w <_ ( F ` x ) ) -> E. z e. RR A. w e. ran ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) w <_ z )
222 113 206 221 syl2anc 
 |-  ( ( ph /\ x e. RR ) -> E. z e. RR A. w e. ran ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) w <_ z )
223 suprleub 
 |-  ( ( ( ran ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) C_ RR /\ ran ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) =/= (/) /\ E. z e. RR A. w e. ran ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) w <_ z ) /\ ( F ` x ) e. RR ) -> ( sup ( ran ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) , RR , < ) <_ ( F ` x ) <-> A. w e. ran ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) w <_ ( F ` x ) ) )
224 212 220 222 113 223 syl31anc 
 |-  ( ( ph /\ x e. RR ) -> ( sup ( ran ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) , RR , < ) <_ ( F ` x ) <-> A. w e. ran ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) w <_ ( F ` x ) ) )
225 206 224 mpbird 
 |-  ( ( ph /\ x e. RR ) -> sup ( ran ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) , RR , < ) <_ ( F ` x ) )
226 arch 
 |-  ( ( F ` x ) e. RR -> E. m e. NN ( F ` x ) < m )
227 113 226 syl 
 |-  ( ( ph /\ x e. RR ) -> E. m e. NN ( F ` x ) < m )
228 195 ad2antrl 
 |-  ( ( ( ph /\ x e. RR ) /\ ( m e. NN /\ ( F ` x ) < m ) ) -> ( ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ` m ) = if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) )
229 ltle 
 |-  ( ( ( F ` x ) e. RR /\ m e. RR ) -> ( ( F ` x ) < m -> ( F ` x ) <_ m ) )
230 113 51 229 syl2an 
 |-  ( ( ( ph /\ x e. RR ) /\ m e. NN ) -> ( ( F ` x ) < m -> ( F ` x ) <_ m ) )
231 230 impr 
 |-  ( ( ( ph /\ x e. RR ) /\ ( m e. NN /\ ( F ` x ) < m ) ) -> ( F ` x ) <_ m )
232 231 iftrued 
 |-  ( ( ( ph /\ x e. RR ) /\ ( m e. NN /\ ( F ` x ) < m ) ) -> if ( ( F ` x ) <_ m , ( F ` x ) , 0 ) = ( F ` x ) )
233 228 232 eqtrd 
 |-  ( ( ( ph /\ x e. RR ) /\ ( m e. NN /\ ( F ` x ) < m ) ) -> ( ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ` m ) = ( F ` x ) )
234 202 adantr 
 |-  ( ( ( ph /\ x e. RR ) /\ ( m e. NN /\ ( F ` x ) < m ) ) -> ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) Fn NN )
235 simprl 
 |-  ( ( ( ph /\ x e. RR ) /\ ( m e. NN /\ ( F ` x ) < m ) ) -> m e. NN )
236 fnfvelrn 
 |-  ( ( ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) Fn NN /\ m e. NN ) -> ( ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ` m ) e. ran ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) )
237 234 235 236 syl2anc 
 |-  ( ( ( ph /\ x e. RR ) /\ ( m e. NN /\ ( F ` x ) < m ) ) -> ( ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ` m ) e. ran ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) )
238 233 237 eqeltrrd 
 |-  ( ( ( ph /\ x e. RR ) /\ ( m e. NN /\ ( F ` x ) < m ) ) -> ( F ` x ) e. ran ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) )
239 227 238 rexlimddv 
 |-  ( ( ph /\ x e. RR ) -> ( F ` x ) e. ran ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) )
240 212 220 222 239 suprubd 
 |-  ( ( ph /\ x e. RR ) -> ( F ` x ) <_ sup ( ran ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) , RR , < ) )
241 212 220 222 suprcld 
 |-  ( ( ph /\ x e. RR ) -> sup ( ran ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) , RR , < ) e. RR )
242 241 113 letri3d 
 |-  ( ( ph /\ x e. RR ) -> ( sup ( ran ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) , RR , < ) = ( F ` x ) <-> ( sup ( ran ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) , RR , < ) <_ ( F ` x ) /\ ( F ` x ) <_ sup ( ran ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) , RR , < ) ) ) )
243 225 240 242 mpbir2and 
 |-  ( ( ph /\ x e. RR ) -> sup ( ran ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) , RR , < ) = ( F ` x ) )
244 243 mpteq2dva 
 |-  ( ph -> ( x e. RR |-> sup ( ran ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) , RR , < ) ) = ( x e. RR |-> ( F ` x ) ) )
245 244 168 eqtr4d 
 |-  ( ph -> ( x e. RR |-> sup ( ran ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) , RR , < ) ) = F )
246 245 fveq2d 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> sup ( ran ( n e. NN |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) , RR , < ) ) ) = ( S.2 ` F ) )
247 193 246 eqtr3d 
 |-  ( ph -> sup ( ran ( n e. NN |-> ( S.2 ` ( x e. RR |-> if ( ( F ` x ) <_ n , ( F ` x ) , 0 ) ) ) ) , RR* , < ) = ( S.2 ` F ) )