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

Metamath Proof Explorer

Theorem itg2splitlem

Description: Lemma for itg2split . (Contributed by Mario Carneiro, 11-Aug-2014)

Ref Expression
Hypotheses itg2split.a 
|- ( ph -> A e. dom vol )
itg2split.b 
|- ( ph -> B e. dom vol )
itg2split.i 
|- ( ph -> ( vol* ` ( A i^i B ) ) = 0 )
itg2split.u 
|- ( ph -> U = ( A u. B ) )
itg2split.c 
|- ( ( ph /\ x e. U ) -> C e. ( 0 [,] +oo ) )
itg2split.f 
|- F = ( x e. RR |-> if ( x e. A , C , 0 ) )
itg2split.g 
|- G = ( x e. RR |-> if ( x e. B , C , 0 ) )
itg2split.h 
|- H = ( x e. RR |-> if ( x e. U , C , 0 ) )
itg2split.sf 
|- ( ph -> ( S.2 ` F ) e. RR )
itg2split.sg 
|- ( ph -> ( S.2 ` G ) e. RR )
Assertion itg2splitlem 
|- ( ph -> ( S.2 ` H ) <_ ( ( S.2 ` F ) + ( S.2 ` G ) ) )

Proof

Step Hyp Ref Expression
1 itg2split.a 
 |-  ( ph -> A e. dom vol )
2 itg2split.b 
 |-  ( ph -> B e. dom vol )
3 itg2split.i 
 |-  ( ph -> ( vol* ` ( A i^i B ) ) = 0 )
4 itg2split.u 
 |-  ( ph -> U = ( A u. B ) )
5 itg2split.c 
 |-  ( ( ph /\ x e. U ) -> C e. ( 0 [,] +oo ) )
6 itg2split.f 
 |-  F = ( x e. RR |-> if ( x e. A , C , 0 ) )
7 itg2split.g 
 |-  G = ( x e. RR |-> if ( x e. B , C , 0 ) )
8 itg2split.h 
 |-  H = ( x e. RR |-> if ( x e. U , C , 0 ) )
9 itg2split.sf 
 |-  ( ph -> ( S.2 ` F ) e. RR )
10 itg2split.sg 
 |-  ( ph -> ( S.2 ` G ) e. RR )
11 simprl 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) -> f e. dom S.1 )
12 itg1cl 
 |-  ( f e. dom S.1 -> ( S.1 ` f ) e. RR )
13 11 12 syl 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) -> ( S.1 ` f ) e. RR )
14 1 adantr 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) -> A e. dom vol )
15 eqid 
 |-  ( x e. RR |-> if ( x e. A , ( f ` x ) , 0 ) ) = ( x e. RR |-> if ( x e. A , ( f ` x ) , 0 ) )
16 15 i1fres 
 |-  ( ( f e. dom S.1 /\ A e. dom vol ) -> ( x e. RR |-> if ( x e. A , ( f ` x ) , 0 ) ) e. dom S.1 )
17 11 14 16 syl2anc 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) -> ( x e. RR |-> if ( x e. A , ( f ` x ) , 0 ) ) e. dom S.1 )
18 itg1cl 
 |-  ( ( x e. RR |-> if ( x e. A , ( f ` x ) , 0 ) ) e. dom S.1 -> ( S.1 ` ( x e. RR |-> if ( x e. A , ( f ` x ) , 0 ) ) ) e. RR )
19 17 18 syl 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) -> ( S.1 ` ( x e. RR |-> if ( x e. A , ( f ` x ) , 0 ) ) ) e. RR )
20 2 adantr 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) -> B e. dom vol )
21 eqid 
 |-  ( x e. RR |-> if ( x e. B , ( f ` x ) , 0 ) ) = ( x e. RR |-> if ( x e. B , ( f ` x ) , 0 ) )
22 21 i1fres 
 |-  ( ( f e. dom S.1 /\ B e. dom vol ) -> ( x e. RR |-> if ( x e. B , ( f ` x ) , 0 ) ) e. dom S.1 )
23 11 20 22 syl2anc 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) -> ( x e. RR |-> if ( x e. B , ( f ` x ) , 0 ) ) e. dom S.1 )
24 itg1cl 
 |-  ( ( x e. RR |-> if ( x e. B , ( f ` x ) , 0 ) ) e. dom S.1 -> ( S.1 ` ( x e. RR |-> if ( x e. B , ( f ` x ) , 0 ) ) ) e. RR )
25 23 24 syl 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) -> ( S.1 ` ( x e. RR |-> if ( x e. B , ( f ` x ) , 0 ) ) ) e. RR )
26 19 25 readdcld 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) -> ( ( S.1 ` ( x e. RR |-> if ( x e. A , ( f ` x ) , 0 ) ) ) + ( S.1 ` ( x e. RR |-> if ( x e. B , ( f ` x ) , 0 ) ) ) ) e. RR )
27 9 10 readdcld 
 |-  ( ph -> ( ( S.2 ` F ) + ( S.2 ` G ) ) e. RR )
28 27 adantr 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) -> ( ( S.2 ` F ) + ( S.2 ` G ) ) e. RR )
29 inss1 
 |-  ( A i^i B ) C_ A
30 mblss 
 |-  ( A e. dom vol -> A C_ RR )
31 1 30 syl 
 |-  ( ph -> A C_ RR )
32 29 31 sstrid 
 |-  ( ph -> ( A i^i B ) C_ RR )
33 32 adantr 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) -> ( A i^i B ) C_ RR )
34 3 adantr 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) -> ( vol* ` ( A i^i B ) ) = 0 )
35 reex 
 |-  RR e. _V
36 35 a1i 
 |-  ( ph -> RR e. _V )
37 fvex 
 |-  ( f ` x ) e. _V
38 c0ex 
 |-  0 e. _V
39 37 38 ifex 
 |-  if ( x e. A , ( f ` x ) , 0 ) e. _V
40 39 a1i 
 |-  ( ( ph /\ x e. RR ) -> if ( x e. A , ( f ` x ) , 0 ) e. _V )
41 37 38 ifex 
 |-  if ( x e. B , ( f ` x ) , 0 ) e. _V
42 41 a1i 
 |-  ( ( ph /\ x e. RR ) -> if ( x e. B , ( f ` x ) , 0 ) e. _V )
43 eqidd 
 |-  ( ph -> ( x e. RR |-> if ( x e. A , ( f ` x ) , 0 ) ) = ( x e. RR |-> if ( x e. A , ( f ` x ) , 0 ) ) )
44 eqidd 
 |-  ( ph -> ( x e. RR |-> if ( x e. B , ( f ` x ) , 0 ) ) = ( x e. RR |-> if ( x e. B , ( f ` x ) , 0 ) ) )
45 36 40 42 43 44 offval2 
 |-  ( ph -> ( ( x e. RR |-> if ( x e. A , ( f ` x ) , 0 ) ) oF + ( x e. RR |-> if ( x e. B , ( f ` x ) , 0 ) ) ) = ( x e. RR |-> ( if ( x e. A , ( f ` x ) , 0 ) + if ( x e. B , ( f ` x ) , 0 ) ) ) )
46 45 adantr 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) -> ( ( x e. RR |-> if ( x e. A , ( f ` x ) , 0 ) ) oF + ( x e. RR |-> if ( x e. B , ( f ` x ) , 0 ) ) ) = ( x e. RR |-> ( if ( x e. A , ( f ` x ) , 0 ) + if ( x e. B , ( f ` x ) , 0 ) ) ) )
47 17 23 i1fadd 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) -> ( ( x e. RR |-> if ( x e. A , ( f ` x ) , 0 ) ) oF + ( x e. RR |-> if ( x e. B , ( f ` x ) , 0 ) ) ) e. dom S.1 )
48 46 47 eqeltrrd 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) -> ( x e. RR |-> ( if ( x e. A , ( f ` x ) , 0 ) + if ( x e. B , ( f ` x ) , 0 ) ) ) e. dom S.1 )
49 i1ff 
 |-  ( f e. dom S.1 -> f : RR --> RR )
50 11 49 syl 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) -> f : RR --> RR )
51 eldifi 
 |-  ( y e. ( RR \ ( A i^i B ) ) -> y e. RR )
52 ffvelcdm 
 |-  ( ( f : RR --> RR /\ y e. RR ) -> ( f ` y ) e. RR )
53 50 51 52 syl2an 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ y e. ( RR \ ( A i^i B ) ) ) -> ( f ` y ) e. RR )
54 53 leidd 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ y e. ( RR \ ( A i^i B ) ) ) -> ( f ` y ) <_ ( f ` y ) )
55 54 adantr 
 |-  ( ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ y e. ( RR \ ( A i^i B ) ) ) /\ y e. A ) -> ( f ` y ) <_ ( f ` y ) )
56 iftrue 
 |-  ( y e. A -> if ( y e. A , ( f ` y ) , 0 ) = ( f ` y ) )
57 56 adantl 
 |-  ( ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ y e. ( RR \ ( A i^i B ) ) ) /\ y e. A ) -> if ( y e. A , ( f ` y ) , 0 ) = ( f ` y ) )
58 eldifn 
 |-  ( y e. ( RR \ ( A i^i B ) ) -> -. y e. ( A i^i B ) )
59 58 adantl 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ y e. ( RR \ ( A i^i B ) ) ) -> -. y e. ( A i^i B ) )
60 elin 
 |-  ( y e. ( A i^i B ) <-> ( y e. A /\ y e. B ) )
61 59 60 sylnib 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ y e. ( RR \ ( A i^i B ) ) ) -> -. ( y e. A /\ y e. B ) )
62 imnan 
 |-  ( ( y e. A -> -. y e. B ) <-> -. ( y e. A /\ y e. B ) )
63 61 62 sylibr 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ y e. ( RR \ ( A i^i B ) ) ) -> ( y e. A -> -. y e. B ) )
64 63 imp 
 |-  ( ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ y e. ( RR \ ( A i^i B ) ) ) /\ y e. A ) -> -. y e. B )
65 iffalse 
 |-  ( -. y e. B -> if ( y e. B , ( f ` y ) , 0 ) = 0 )
66 64 65 syl 
 |-  ( ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ y e. ( RR \ ( A i^i B ) ) ) /\ y e. A ) -> if ( y e. B , ( f ` y ) , 0 ) = 0 )
67 57 66 oveq12d 
 |-  ( ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ y e. ( RR \ ( A i^i B ) ) ) /\ y e. A ) -> ( if ( y e. A , ( f ` y ) , 0 ) + if ( y e. B , ( f ` y ) , 0 ) ) = ( ( f ` y ) + 0 ) )
68 53 recnd 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ y e. ( RR \ ( A i^i B ) ) ) -> ( f ` y ) e. CC )
69 68 adantr 
 |-  ( ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ y e. ( RR \ ( A i^i B ) ) ) /\ y e. A ) -> ( f ` y ) e. CC )
70 69 addridd 
 |-  ( ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ y e. ( RR \ ( A i^i B ) ) ) /\ y e. A ) -> ( ( f ` y ) + 0 ) = ( f ` y ) )
71 67 70 eqtrd 
 |-  ( ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ y e. ( RR \ ( A i^i B ) ) ) /\ y e. A ) -> ( if ( y e. A , ( f ` y ) , 0 ) + if ( y e. B , ( f ` y ) , 0 ) ) = ( f ` y ) )
72 55 71 breqtrrd 
 |-  ( ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ y e. ( RR \ ( A i^i B ) ) ) /\ y e. A ) -> ( f ` y ) <_ ( if ( y e. A , ( f ` y ) , 0 ) + if ( y e. B , ( f ` y ) , 0 ) ) )
73 54 ad2antrr 
 |-  ( ( ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ y e. ( RR \ ( A i^i B ) ) ) /\ -. y e. A ) /\ y e. B ) -> ( f ` y ) <_ ( f ` y ) )
74 iftrue 
 |-  ( y e. B -> if ( y e. B , ( f ` y ) , 0 ) = ( f ` y ) )
75 74 adantl 
 |-  ( ( ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ y e. ( RR \ ( A i^i B ) ) ) /\ -. y e. A ) /\ y e. B ) -> if ( y e. B , ( f ` y ) , 0 ) = ( f ` y ) )
76 73 75 breqtrrd 
 |-  ( ( ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ y e. ( RR \ ( A i^i B ) ) ) /\ -. y e. A ) /\ y e. B ) -> ( f ` y ) <_ if ( y e. B , ( f ` y ) , 0 ) )
77 4 ad2antrr 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ y e. ( RR \ ( A i^i B ) ) ) -> U = ( A u. B ) )
78 77 eleq2d 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ y e. ( RR \ ( A i^i B ) ) ) -> ( y e. U <-> y e. ( A u. B ) ) )
79 elun 
 |-  ( y e. ( A u. B ) <-> ( y e. A \/ y e. B ) )
80 78 79 bitrdi 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ y e. ( RR \ ( A i^i B ) ) ) -> ( y e. U <-> ( y e. A \/ y e. B ) ) )
81 80 notbid 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ y e. ( RR \ ( A i^i B ) ) ) -> ( -. y e. U <-> -. ( y e. A \/ y e. B ) ) )
82 ioran 
 |-  ( -. ( y e. A \/ y e. B ) <-> ( -. y e. A /\ -. y e. B ) )
83 81 82 bitrdi 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ y e. ( RR \ ( A i^i B ) ) ) -> ( -. y e. U <-> ( -. y e. A /\ -. y e. B ) ) )
84 83 biimpar 
 |-  ( ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ y e. ( RR \ ( A i^i B ) ) ) /\ ( -. y e. A /\ -. y e. B ) ) -> -. y e. U )
85 simprr 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) -> f oR <_ H )
86 50 ffnd 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) -> f Fn RR )
87 5 adantlr 
 |-  ( ( ( ph /\ x e. RR ) /\ x e. U ) -> C e. ( 0 [,] +oo ) )
88 0e0iccpnf 
 |-  0 e. ( 0 [,] +oo )
89 88 a1i 
 |-  ( ( ( ph /\ x e. RR ) /\ -. x e. U ) -> 0 e. ( 0 [,] +oo ) )
90 87 89 ifclda 
 |-  ( ( ph /\ x e. RR ) -> if ( x e. U , C , 0 ) e. ( 0 [,] +oo ) )
91 90 8 fmptd 
 |-  ( ph -> H : RR --> ( 0 [,] +oo ) )
92 91 ffnd 
 |-  ( ph -> H Fn RR )
93 92 adantr 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) -> H Fn RR )
94 35 a1i 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) -> RR e. _V )
95 inidm 
 |-  ( RR i^i RR ) = RR
96 eqidd 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ y e. RR ) -> ( f ` y ) = ( f ` y ) )
97 eqidd 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ y e. RR ) -> ( H ` y ) = ( H ` y ) )
98 86 93 94 94 95 96 97 ofrfval 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) -> ( f oR <_ H <-> A. y e. RR ( f ` y ) <_ ( H ` y ) ) )
99 85 98 mpbid 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) -> A. y e. RR ( f ` y ) <_ ( H ` y ) )
100 99 r19.21bi 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ y e. RR ) -> ( f ` y ) <_ ( H ` y ) )
101 51 100 sylan2 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ y e. ( RR \ ( A i^i B ) ) ) -> ( f ` y ) <_ ( H ` y ) )
102 101 adantr 
 |-  ( ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ y e. ( RR \ ( A i^i B ) ) ) /\ -. y e. U ) -> ( f ` y ) <_ ( H ` y ) )
103 51 adantl 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ y e. ( RR \ ( A i^i B ) ) ) -> y e. RR )
104 eldif 
 |-  ( y e. ( RR \ U ) <-> ( y e. RR /\ -. y e. U ) )
105 nfcv 
 |-  F/_ x y
106 nfmpt1 
 |-  F/_ x ( x e. RR |-> if ( x e. U , C , 0 ) )
107 8 106 nfcxfr 
 |-  F/_ x H
108 107 105 nffv 
 |-  F/_ x ( H ` y )
109 108 nfeq1 
 |-  F/ x ( H ` y ) = 0
110 fveqeq2 
 |-  ( x = y -> ( ( H ` x ) = 0 <-> ( H ` y ) = 0 ) )
111 eldif 
 |-  ( x e. ( RR \ U ) <-> ( x e. RR /\ -. x e. U ) )
112 8 fvmpt2i 
 |-  ( x e. RR -> ( H ` x ) = ( _I ` if ( x e. U , C , 0 ) ) )
113 iffalse 
 |-  ( -. x e. U -> if ( x e. U , C , 0 ) = 0 )
114 113 fveq2d 
 |-  ( -. x e. U -> ( _I ` if ( x e. U , C , 0 ) ) = ( _I ` 0 ) )
115 0cn 
 |-  0 e. CC
116 fvi 
 |-  ( 0 e. CC -> ( _I ` 0 ) = 0 )
117 115 116 ax-mp 
 |-  ( _I ` 0 ) = 0
118 114 117 eqtrdi 
 |-  ( -. x e. U -> ( _I ` if ( x e. U , C , 0 ) ) = 0 )
119 112 118 sylan9eq 
 |-  ( ( x e. RR /\ -. x e. U ) -> ( H ` x ) = 0 )
120 111 119 sylbi 
 |-  ( x e. ( RR \ U ) -> ( H ` x ) = 0 )
121 105 109 110 120 vtoclgaf 
 |-  ( y e. ( RR \ U ) -> ( H ` y ) = 0 )
122 104 121 sylbir 
 |-  ( ( y e. RR /\ -. y e. U ) -> ( H ` y ) = 0 )
123 103 122 sylan 
 |-  ( ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ y e. ( RR \ ( A i^i B ) ) ) /\ -. y e. U ) -> ( H ` y ) = 0 )
124 102 123 breqtrd 
 |-  ( ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ y e. ( RR \ ( A i^i B ) ) ) /\ -. y e. U ) -> ( f ` y ) <_ 0 )
125 84 124 syldan 
 |-  ( ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ y e. ( RR \ ( A i^i B ) ) ) /\ ( -. y e. A /\ -. y e. B ) ) -> ( f ` y ) <_ 0 )
126 125 anassrs 
 |-  ( ( ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ y e. ( RR \ ( A i^i B ) ) ) /\ -. y e. A ) /\ -. y e. B ) -> ( f ` y ) <_ 0 )
127 65 adantl 
 |-  ( ( ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ y e. ( RR \ ( A i^i B ) ) ) /\ -. y e. A ) /\ -. y e. B ) -> if ( y e. B , ( f ` y ) , 0 ) = 0 )
128 126 127 breqtrrd 
 |-  ( ( ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ y e. ( RR \ ( A i^i B ) ) ) /\ -. y e. A ) /\ -. y e. B ) -> ( f ` y ) <_ if ( y e. B , ( f ` y ) , 0 ) )
129 76 128 pm2.61dan 
 |-  ( ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ y e. ( RR \ ( A i^i B ) ) ) /\ -. y e. A ) -> ( f ` y ) <_ if ( y e. B , ( f ` y ) , 0 ) )
130 iffalse 
 |-  ( -. y e. A -> if ( y e. A , ( f ` y ) , 0 ) = 0 )
131 130 adantl 
 |-  ( ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ y e. ( RR \ ( A i^i B ) ) ) /\ -. y e. A ) -> if ( y e. A , ( f ` y ) , 0 ) = 0 )
132 131 oveq1d 
 |-  ( ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ y e. ( RR \ ( A i^i B ) ) ) /\ -. y e. A ) -> ( if ( y e. A , ( f ` y ) , 0 ) + if ( y e. B , ( f ` y ) , 0 ) ) = ( 0 + if ( y e. B , ( f ` y ) , 0 ) ) )
133 0re 
 |-  0 e. RR
134 ifcl 
 |-  ( ( ( f ` y ) e. RR /\ 0 e. RR ) -> if ( y e. B , ( f ` y ) , 0 ) e. RR )
135 53 133 134 sylancl 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ y e. ( RR \ ( A i^i B ) ) ) -> if ( y e. B , ( f ` y ) , 0 ) e. RR )
136 135 recnd 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ y e. ( RR \ ( A i^i B ) ) ) -> if ( y e. B , ( f ` y ) , 0 ) e. CC )
137 136 adantr 
 |-  ( ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ y e. ( RR \ ( A i^i B ) ) ) /\ -. y e. A ) -> if ( y e. B , ( f ` y ) , 0 ) e. CC )
138 137 addlidd 
 |-  ( ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ y e. ( RR \ ( A i^i B ) ) ) /\ -. y e. A ) -> ( 0 + if ( y e. B , ( f ` y ) , 0 ) ) = if ( y e. B , ( f ` y ) , 0 ) )
139 132 138 eqtrd 
 |-  ( ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ y e. ( RR \ ( A i^i B ) ) ) /\ -. y e. A ) -> ( if ( y e. A , ( f ` y ) , 0 ) + if ( y e. B , ( f ` y ) , 0 ) ) = if ( y e. B , ( f ` y ) , 0 ) )
140 129 139 breqtrrd 
 |-  ( ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ y e. ( RR \ ( A i^i B ) ) ) /\ -. y e. A ) -> ( f ` y ) <_ ( if ( y e. A , ( f ` y ) , 0 ) + if ( y e. B , ( f ` y ) , 0 ) ) )
141 72 140 pm2.61dan 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ y e. ( RR \ ( A i^i B ) ) ) -> ( f ` y ) <_ ( if ( y e. A , ( f ` y ) , 0 ) + if ( y e. B , ( f ` y ) , 0 ) ) )
142 eleq1w 
 |-  ( x = y -> ( x e. A <-> y e. A ) )
143 fveq2 
 |-  ( x = y -> ( f ` x ) = ( f ` y ) )
144 142 143 ifbieq1d 
 |-  ( x = y -> if ( x e. A , ( f ` x ) , 0 ) = if ( y e. A , ( f ` y ) , 0 ) )
145 eleq1w 
 |-  ( x = y -> ( x e. B <-> y e. B ) )
146 145 143 ifbieq1d 
 |-  ( x = y -> if ( x e. B , ( f ` x ) , 0 ) = if ( y e. B , ( f ` y ) , 0 ) )
147 144 146 oveq12d 
 |-  ( x = y -> ( if ( x e. A , ( f ` x ) , 0 ) + if ( x e. B , ( f ` x ) , 0 ) ) = ( if ( y e. A , ( f ` y ) , 0 ) + if ( y e. B , ( f ` y ) , 0 ) ) )
148 eqid 
 |-  ( x e. RR |-> ( if ( x e. A , ( f ` x ) , 0 ) + if ( x e. B , ( f ` x ) , 0 ) ) ) = ( x e. RR |-> ( if ( x e. A , ( f ` x ) , 0 ) + if ( x e. B , ( f ` x ) , 0 ) ) )
149 ovex 
 |-  ( if ( y e. A , ( f ` y ) , 0 ) + if ( y e. B , ( f ` y ) , 0 ) ) e. _V
150 147 148 149 fvmpt 
 |-  ( y e. RR -> ( ( x e. RR |-> ( if ( x e. A , ( f ` x ) , 0 ) + if ( x e. B , ( f ` x ) , 0 ) ) ) ` y ) = ( if ( y e. A , ( f ` y ) , 0 ) + if ( y e. B , ( f ` y ) , 0 ) ) )
151 103 150 syl 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ y e. ( RR \ ( A i^i B ) ) ) -> ( ( x e. RR |-> ( if ( x e. A , ( f ` x ) , 0 ) + if ( x e. B , ( f ` x ) , 0 ) ) ) ` y ) = ( if ( y e. A , ( f ` y ) , 0 ) + if ( y e. B , ( f ` y ) , 0 ) ) )
152 141 151 breqtrrd 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ y e. ( RR \ ( A i^i B ) ) ) -> ( f ` y ) <_ ( ( x e. RR |-> ( if ( x e. A , ( f ` x ) , 0 ) + if ( x e. B , ( f ` x ) , 0 ) ) ) ` y ) )
153 11 33 34 48 152 itg1lea 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) -> ( S.1 ` f ) <_ ( S.1 ` ( x e. RR |-> ( if ( x e. A , ( f ` x ) , 0 ) + if ( x e. B , ( f ` x ) , 0 ) ) ) ) )
154 46 fveq2d 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) -> ( S.1 ` ( ( x e. RR |-> if ( x e. A , ( f ` x ) , 0 ) ) oF + ( x e. RR |-> if ( x e. B , ( f ` x ) , 0 ) ) ) ) = ( S.1 ` ( x e. RR |-> ( if ( x e. A , ( f ` x ) , 0 ) + if ( x e. B , ( f ` x ) , 0 ) ) ) ) )
155 17 23 itg1add 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) -> ( S.1 ` ( ( x e. RR |-> if ( x e. A , ( f ` x ) , 0 ) ) oF + ( x e. RR |-> if ( x e. B , ( f ` x ) , 0 ) ) ) ) = ( ( S.1 ` ( x e. RR |-> if ( x e. A , ( f ` x ) , 0 ) ) ) + ( S.1 ` ( x e. RR |-> if ( x e. B , ( f ` x ) , 0 ) ) ) ) )
156 154 155 eqtr3d 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) -> ( S.1 ` ( x e. RR |-> ( if ( x e. A , ( f ` x ) , 0 ) + if ( x e. B , ( f ` x ) , 0 ) ) ) ) = ( ( S.1 ` ( x e. RR |-> if ( x e. A , ( f ` x ) , 0 ) ) ) + ( S.1 ` ( x e. RR |-> if ( x e. B , ( f ` x ) , 0 ) ) ) ) )
157 153 156 breqtrd 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) -> ( S.1 ` f ) <_ ( ( S.1 ` ( x e. RR |-> if ( x e. A , ( f ` x ) , 0 ) ) ) + ( S.1 ` ( x e. RR |-> if ( x e. B , ( f ` x ) , 0 ) ) ) ) )
158 9 adantr 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) -> ( S.2 ` F ) e. RR )
159 10 adantr 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) -> ( S.2 ` G ) e. RR )
160 ssun1 
 |-  A C_ ( A u. B )
161 160 4 sseqtrrid 
 |-  ( ph -> A C_ U )
162 161 sselda 
 |-  ( ( ph /\ x e. A ) -> x e. U )
163 162 adantlr 
 |-  ( ( ( ph /\ x e. RR ) /\ x e. A ) -> x e. U )
164 163 87 syldan 
 |-  ( ( ( ph /\ x e. RR ) /\ x e. A ) -> C e. ( 0 [,] +oo ) )
165 88 a1i 
 |-  ( ( ( ph /\ x e. RR ) /\ -. x e. A ) -> 0 e. ( 0 [,] +oo ) )
166 164 165 ifclda 
 |-  ( ( ph /\ x e. RR ) -> if ( x e. A , C , 0 ) e. ( 0 [,] +oo ) )
167 166 6 fmptd 
 |-  ( ph -> F : RR --> ( 0 [,] +oo ) )
168 167 adantr 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) -> F : RR --> ( 0 [,] +oo ) )
169 nfv 
 |-  F/ x ph
170 nfv 
 |-  F/ x f e. dom S.1
171 nfcv 
 |-  F/_ x f
172 nfcv 
 |-  F/_ x oR <_
173 171 172 107 nfbr 
 |-  F/ x f oR <_ H
174 170 173 nfan 
 |-  F/ x ( f e. dom S.1 /\ f oR <_ H )
175 169 174 nfan 
 |-  F/ x ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) )
176 14 30 syl 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) -> A C_ RR )
177 176 sselda 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ x e. A ) -> x e. RR )
178 35 a1i 
 |-  ( ( ph /\ f e. dom S.1 ) -> RR e. _V )
179 37 a1i 
 |-  ( ( ( ph /\ f e. dom S.1 ) /\ x e. RR ) -> ( f ` x ) e. _V )
180 90 adantlr 
 |-  ( ( ( ph /\ f e. dom S.1 ) /\ x e. RR ) -> if ( x e. U , C , 0 ) e. ( 0 [,] +oo ) )
181 49 adantl 
 |-  ( ( ph /\ f e. dom S.1 ) -> f : RR --> RR )
182 181 feqmptd 
 |-  ( ( ph /\ f e. dom S.1 ) -> f = ( x e. RR |-> ( f ` x ) ) )
183 8 a1i 
 |-  ( ( ph /\ f e. dom S.1 ) -> H = ( x e. RR |-> if ( x e. U , C , 0 ) ) )
184 178 179 180 182 183 ofrfval2 
 |-  ( ( ph /\ f e. dom S.1 ) -> ( f oR <_ H <-> A. x e. RR ( f ` x ) <_ if ( x e. U , C , 0 ) ) )
185 184 biimpd 
 |-  ( ( ph /\ f e. dom S.1 ) -> ( f oR <_ H -> A. x e. RR ( f ` x ) <_ if ( x e. U , C , 0 ) ) )
186 185 impr 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) -> A. x e. RR ( f ` x ) <_ if ( x e. U , C , 0 ) )
187 186 r19.21bi 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ x e. RR ) -> ( f ` x ) <_ if ( x e. U , C , 0 ) )
188 177 187 syldan 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ x e. A ) -> ( f ` x ) <_ if ( x e. U , C , 0 ) )
189 162 adantlr 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ x e. A ) -> x e. U )
190 189 iftrued 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ x e. A ) -> if ( x e. U , C , 0 ) = C )
191 188 190 breqtrd 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ x e. A ) -> ( f ` x ) <_ C )
192 iftrue 
 |-  ( x e. A -> if ( x e. A , ( f ` x ) , 0 ) = ( f ` x ) )
193 192 adantl 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ x e. A ) -> if ( x e. A , ( f ` x ) , 0 ) = ( f ` x ) )
194 iftrue 
 |-  ( x e. A -> if ( x e. A , C , 0 ) = C )
195 194 adantl 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ x e. A ) -> if ( x e. A , C , 0 ) = C )
196 191 193 195 3brtr4d 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ x e. A ) -> if ( x e. A , ( f ` x ) , 0 ) <_ if ( x e. A , C , 0 ) )
197 0le0 
 |-  0 <_ 0
198 197 a1i 
 |-  ( -. x e. A -> 0 <_ 0 )
199 iffalse 
 |-  ( -. x e. A -> if ( x e. A , ( f ` x ) , 0 ) = 0 )
200 iffalse 
 |-  ( -. x e. A -> if ( x e. A , C , 0 ) = 0 )
201 198 199 200 3brtr4d 
 |-  ( -. x e. A -> if ( x e. A , ( f ` x ) , 0 ) <_ if ( x e. A , C , 0 ) )
202 201 adantl 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ -. x e. A ) -> if ( x e. A , ( f ` x ) , 0 ) <_ if ( x e. A , C , 0 ) )
203 196 202 pm2.61dan 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) -> if ( x e. A , ( f ` x ) , 0 ) <_ if ( x e. A , C , 0 ) )
204 203 a1d 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) -> ( x e. RR -> if ( x e. A , ( f ` x ) , 0 ) <_ if ( x e. A , C , 0 ) ) )
205 175 204 ralrimi 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) -> A. x e. RR if ( x e. A , ( f ` x ) , 0 ) <_ if ( x e. A , C , 0 ) )
206 6 a1i 
 |-  ( ph -> F = ( x e. RR |-> if ( x e. A , C , 0 ) ) )
207 36 40 166 43 206 ofrfval2 
 |-  ( ph -> ( ( x e. RR |-> if ( x e. A , ( f ` x ) , 0 ) ) oR <_ F <-> A. x e. RR if ( x e. A , ( f ` x ) , 0 ) <_ if ( x e. A , C , 0 ) ) )
208 207 adantr 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) -> ( ( x e. RR |-> if ( x e. A , ( f ` x ) , 0 ) ) oR <_ F <-> A. x e. RR if ( x e. A , ( f ` x ) , 0 ) <_ if ( x e. A , C , 0 ) ) )
209 205 208 mpbird 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) -> ( x e. RR |-> if ( x e. A , ( f ` x ) , 0 ) ) oR <_ F )
210 itg2ub 
 |-  ( ( F : RR --> ( 0 [,] +oo ) /\ ( x e. RR |-> if ( x e. A , ( f ` x ) , 0 ) ) e. dom S.1 /\ ( x e. RR |-> if ( x e. A , ( f ` x ) , 0 ) ) oR <_ F ) -> ( S.1 ` ( x e. RR |-> if ( x e. A , ( f ` x ) , 0 ) ) ) <_ ( S.2 ` F ) )
211 168 17 209 210 syl3anc 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) -> ( S.1 ` ( x e. RR |-> if ( x e. A , ( f ` x ) , 0 ) ) ) <_ ( S.2 ` F ) )
212 ssun2 
 |-  B C_ ( A u. B )
213 212 4 sseqtrrid 
 |-  ( ph -> B C_ U )
214 213 sselda 
 |-  ( ( ph /\ x e. B ) -> x e. U )
215 214 adantlr 
 |-  ( ( ( ph /\ x e. RR ) /\ x e. B ) -> x e. U )
216 215 87 syldan 
 |-  ( ( ( ph /\ x e. RR ) /\ x e. B ) -> C e. ( 0 [,] +oo ) )
217 88 a1i 
 |-  ( ( ( ph /\ x e. RR ) /\ -. x e. B ) -> 0 e. ( 0 [,] +oo ) )
218 216 217 ifclda 
 |-  ( ( ph /\ x e. RR ) -> if ( x e. B , C , 0 ) e. ( 0 [,] +oo ) )
219 218 7 fmptd 
 |-  ( ph -> G : RR --> ( 0 [,] +oo ) )
220 219 adantr 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) -> G : RR --> ( 0 [,] +oo ) )
221 mblss 
 |-  ( B e. dom vol -> B C_ RR )
222 20 221 syl 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) -> B C_ RR )
223 222 sselda 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ x e. B ) -> x e. RR )
224 223 187 syldan 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ x e. B ) -> ( f ` x ) <_ if ( x e. U , C , 0 ) )
225 214 adantlr 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ x e. B ) -> x e. U )
226 225 iftrued 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ x e. B ) -> if ( x e. U , C , 0 ) = C )
227 224 226 breqtrd 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ x e. B ) -> ( f ` x ) <_ C )
228 iftrue 
 |-  ( x e. B -> if ( x e. B , ( f ` x ) , 0 ) = ( f ` x ) )
229 228 adantl 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ x e. B ) -> if ( x e. B , ( f ` x ) , 0 ) = ( f ` x ) )
230 iftrue 
 |-  ( x e. B -> if ( x e. B , C , 0 ) = C )
231 230 adantl 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ x e. B ) -> if ( x e. B , C , 0 ) = C )
232 227 229 231 3brtr4d 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ x e. B ) -> if ( x e. B , ( f ` x ) , 0 ) <_ if ( x e. B , C , 0 ) )
233 197 a1i 
 |-  ( -. x e. B -> 0 <_ 0 )
234 iffalse 
 |-  ( -. x e. B -> if ( x e. B , ( f ` x ) , 0 ) = 0 )
235 iffalse 
 |-  ( -. x e. B -> if ( x e. B , C , 0 ) = 0 )
236 233 234 235 3brtr4d 
 |-  ( -. x e. B -> if ( x e. B , ( f ` x ) , 0 ) <_ if ( x e. B , C , 0 ) )
237 236 adantl 
 |-  ( ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) /\ -. x e. B ) -> if ( x e. B , ( f ` x ) , 0 ) <_ if ( x e. B , C , 0 ) )
238 232 237 pm2.61dan 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) -> if ( x e. B , ( f ` x ) , 0 ) <_ if ( x e. B , C , 0 ) )
239 238 a1d 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) -> ( x e. RR -> if ( x e. B , ( f ` x ) , 0 ) <_ if ( x e. B , C , 0 ) ) )
240 175 239 ralrimi 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) -> A. x e. RR if ( x e. B , ( f ` x ) , 0 ) <_ if ( x e. B , C , 0 ) )
241 7 a1i 
 |-  ( ph -> G = ( x e. RR |-> if ( x e. B , C , 0 ) ) )
242 36 42 218 44 241 ofrfval2 
 |-  ( ph -> ( ( x e. RR |-> if ( x e. B , ( f ` x ) , 0 ) ) oR <_ G <-> A. x e. RR if ( x e. B , ( f ` x ) , 0 ) <_ if ( x e. B , C , 0 ) ) )
243 242 adantr 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) -> ( ( x e. RR |-> if ( x e. B , ( f ` x ) , 0 ) ) oR <_ G <-> A. x e. RR if ( x e. B , ( f ` x ) , 0 ) <_ if ( x e. B , C , 0 ) ) )
244 240 243 mpbird 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) -> ( x e. RR |-> if ( x e. B , ( f ` x ) , 0 ) ) oR <_ G )
245 itg2ub 
 |-  ( ( G : RR --> ( 0 [,] +oo ) /\ ( x e. RR |-> if ( x e. B , ( f ` x ) , 0 ) ) e. dom S.1 /\ ( x e. RR |-> if ( x e. B , ( f ` x ) , 0 ) ) oR <_ G ) -> ( S.1 ` ( x e. RR |-> if ( x e. B , ( f ` x ) , 0 ) ) ) <_ ( S.2 ` G ) )
246 220 23 244 245 syl3anc 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) -> ( S.1 ` ( x e. RR |-> if ( x e. B , ( f ` x ) , 0 ) ) ) <_ ( S.2 ` G ) )
247 19 25 158 159 211 246 le2addd 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) -> ( ( S.1 ` ( x e. RR |-> if ( x e. A , ( f ` x ) , 0 ) ) ) + ( S.1 ` ( x e. RR |-> if ( x e. B , ( f ` x ) , 0 ) ) ) ) <_ ( ( S.2 ` F ) + ( S.2 ` G ) ) )
248 13 26 28 157 247 letrd 
 |-  ( ( ph /\ ( f e. dom S.1 /\ f oR <_ H ) ) -> ( S.1 ` f ) <_ ( ( S.2 ` F ) + ( S.2 ` G ) ) )
249 248 expr 
 |-  ( ( ph /\ f e. dom S.1 ) -> ( f oR <_ H -> ( S.1 ` f ) <_ ( ( S.2 ` F ) + ( S.2 ` G ) ) ) )
250 249 ralrimiva 
 |-  ( ph -> A. f e. dom S.1 ( f oR <_ H -> ( S.1 ` f ) <_ ( ( S.2 ` F ) + ( S.2 ` G ) ) ) )
251 27 rexrd 
 |-  ( ph -> ( ( S.2 ` F ) + ( S.2 ` G ) ) e. RR* )
252 itg2leub 
 |-  ( ( H : RR --> ( 0 [,] +oo ) /\ ( ( S.2 ` F ) + ( S.2 ` G ) ) e. RR* ) -> ( ( S.2 ` H ) <_ ( ( S.2 ` F ) + ( S.2 ` G ) ) <-> A. f e. dom S.1 ( f oR <_ H -> ( S.1 ` f ) <_ ( ( S.2 ` F ) + ( S.2 ` G ) ) ) ) )
253 91 251 252 syl2anc 
 |-  ( ph -> ( ( S.2 ` H ) <_ ( ( S.2 ` F ) + ( S.2 ` G ) ) <-> A. f e. dom S.1 ( f oR <_ H -> ( S.1 ` f ) <_ ( ( S.2 ` F ) + ( S.2 ` G ) ) ) ) )
254 250 253 mpbird 
 |-  ( ph -> ( S.2 ` H ) <_ ( ( S.2 ` F ) + ( S.2 ` G ) ) )