Metamath Proof Explorer

Theorem inelcarsg

Description: The Caratheodory measurable sets are closed under intersection. (Contributed by Thierry Arnoux, 18-May-2020)

Ref Expression
Hypotheses carsgval.1 
|- ( ph -> O e. V )
carsgval.2 
|- ( ph -> M : ~P O --> ( 0 [,] +oo ) )
difelcarsg.1 
|- ( ph -> A e. ( toCaraSiga ` M ) )
inelcarsg.1 
|- ( ( ph /\ a e. ~P O /\ b e. ~P O ) -> ( M ` ( a u. b ) ) <_ ( ( M ` a ) +e ( M ` b ) ) )
inelcarsg.2 
|- ( ph -> B e. ( toCaraSiga ` M ) )
Assertion inelcarsg 
|- ( ph -> ( A i^i B ) e. ( toCaraSiga ` M ) )

Proof

Step Hyp Ref Expression
1 carsgval.1 
 |-  ( ph -> O e. V )
2 carsgval.2 
 |-  ( ph -> M : ~P O --> ( 0 [,] +oo ) )
3 difelcarsg.1 
 |-  ( ph -> A e. ( toCaraSiga ` M ) )
4 inelcarsg.1 
 |-  ( ( ph /\ a e. ~P O /\ b e. ~P O ) -> ( M ` ( a u. b ) ) <_ ( ( M ` a ) +e ( M ` b ) ) )
5 inelcarsg.2 
 |-  ( ph -> B e. ( toCaraSiga ` M ) )
6 1 2 elcarsg 
 |-  ( ph -> ( A e. ( toCaraSiga ` M ) <-> ( A C_ O /\ A. e e. ~P O ( ( M ` ( e i^i A ) ) +e ( M ` ( e \ A ) ) ) = ( M ` e ) ) ) )
7 3 6 mpbid 
 |-  ( ph -> ( A C_ O /\ A. e e. ~P O ( ( M ` ( e i^i A ) ) +e ( M ` ( e \ A ) ) ) = ( M ` e ) ) )
8 7 simpld 
 |-  ( ph -> A C_ O )
9 ssinss1 
 |-  ( A C_ O -> ( A i^i B ) C_ O )
10 8 9 syl 
 |-  ( ph -> ( A i^i B ) C_ O )
11 iccssxr 
 |-  ( 0 [,] +oo ) C_ RR*
12 2 adantr 
 |-  ( ( ph /\ e e. ~P O ) -> M : ~P O --> ( 0 [,] +oo ) )
13 simpr 
 |-  ( ( ph /\ e e. ~P O ) -> e e. ~P O )
14 13 elpwdifcl 
 |-  ( ( ph /\ e e. ~P O ) -> ( e \ ( A i^i B ) ) e. ~P O )
15 12 14 ffvelrnd 
 |-  ( ( ph /\ e e. ~P O ) -> ( M ` ( e \ ( A i^i B ) ) ) e. ( 0 [,] +oo ) )
16 11 15 sselid 
 |-  ( ( ph /\ e e. ~P O ) -> ( M ` ( e \ ( A i^i B ) ) ) e. RR* )
17 13 elpwincl1 
 |-  ( ( ph /\ e e. ~P O ) -> ( e i^i A ) e. ~P O )
18 17 elpwdifcl 
 |-  ( ( ph /\ e e. ~P O ) -> ( ( e i^i A ) \ B ) e. ~P O )
19 12 18 ffvelrnd 
 |-  ( ( ph /\ e e. ~P O ) -> ( M ` ( ( e i^i A ) \ B ) ) e. ( 0 [,] +oo ) )
20 11 19 sselid 
 |-  ( ( ph /\ e e. ~P O ) -> ( M ` ( ( e i^i A ) \ B ) ) e. RR* )
21 13 elpwdifcl 
 |-  ( ( ph /\ e e. ~P O ) -> ( e \ A ) e. ~P O )
22 12 21 ffvelrnd 
 |-  ( ( ph /\ e e. ~P O ) -> ( M ` ( e \ A ) ) e. ( 0 [,] +oo ) )
23 11 22 sselid 
 |-  ( ( ph /\ e e. ~P O ) -> ( M ` ( e \ A ) ) e. RR* )
24 20 23 xaddcld 
 |-  ( ( ph /\ e e. ~P O ) -> ( ( M ` ( ( e i^i A ) \ B ) ) +e ( M ` ( e \ A ) ) ) e. RR* )
25 13 elpwincl1 
 |-  ( ( ph /\ e e. ~P O ) -> ( e i^i ( A i^i B ) ) e. ~P O )
26 12 25 ffvelrnd 
 |-  ( ( ph /\ e e. ~P O ) -> ( M ` ( e i^i ( A i^i B ) ) ) e. ( 0 [,] +oo ) )
27 11 26 sselid 
 |-  ( ( ph /\ e e. ~P O ) -> ( M ` ( e i^i ( A i^i B ) ) ) e. RR* )
28 indifundif 
 |-  ( ( ( e i^i A ) \ B ) u. ( e \ A ) ) = ( e \ ( A i^i B ) )
29 28 fveq2i 
 |-  ( M ` ( ( ( e i^i A ) \ B ) u. ( e \ A ) ) ) = ( M ` ( e \ ( A i^i B ) ) )
30 4 3expb 
 |-  ( ( ph /\ ( a e. ~P O /\ b e. ~P O ) ) -> ( M ` ( a u. b ) ) <_ ( ( M ` a ) +e ( M ` b ) ) )
31 30 ralrimivva 
 |-  ( ph -> A. a e. ~P O A. b e. ~P O ( M ` ( a u. b ) ) <_ ( ( M ` a ) +e ( M ` b ) ) )
32 31 adantr 
 |-  ( ( ph /\ e e. ~P O ) -> A. a e. ~P O A. b e. ~P O ( M ` ( a u. b ) ) <_ ( ( M ` a ) +e ( M ` b ) ) )
33 uneq1 
 |-  ( a = ( ( e i^i A ) \ B ) -> ( a u. b ) = ( ( ( e i^i A ) \ B ) u. b ) )
34 33 fveq2d 
 |-  ( a = ( ( e i^i A ) \ B ) -> ( M ` ( a u. b ) ) = ( M ` ( ( ( e i^i A ) \ B ) u. b ) ) )
35 fveq2 
 |-  ( a = ( ( e i^i A ) \ B ) -> ( M ` a ) = ( M ` ( ( e i^i A ) \ B ) ) )
36 35 oveq1d 
 |-  ( a = ( ( e i^i A ) \ B ) -> ( ( M ` a ) +e ( M ` b ) ) = ( ( M ` ( ( e i^i A ) \ B ) ) +e ( M ` b ) ) )
37 34 36 breq12d 
 |-  ( a = ( ( e i^i A ) \ B ) -> ( ( M ` ( a u. b ) ) <_ ( ( M ` a ) +e ( M ` b ) ) <-> ( M ` ( ( ( e i^i A ) \ B ) u. b ) ) <_ ( ( M ` ( ( e i^i A ) \ B ) ) +e ( M ` b ) ) ) )
38 uneq2 
 |-  ( b = ( e \ A ) -> ( ( ( e i^i A ) \ B ) u. b ) = ( ( ( e i^i A ) \ B ) u. ( e \ A ) ) )
39 38 fveq2d 
 |-  ( b = ( e \ A ) -> ( M ` ( ( ( e i^i A ) \ B ) u. b ) ) = ( M ` ( ( ( e i^i A ) \ B ) u. ( e \ A ) ) ) )
40 fveq2 
 |-  ( b = ( e \ A ) -> ( M ` b ) = ( M ` ( e \ A ) ) )
41 40 oveq2d 
 |-  ( b = ( e \ A ) -> ( ( M ` ( ( e i^i A ) \ B ) ) +e ( M ` b ) ) = ( ( M ` ( ( e i^i A ) \ B ) ) +e ( M ` ( e \ A ) ) ) )
42 39 41 breq12d 
 |-  ( b = ( e \ A ) -> ( ( M ` ( ( ( e i^i A ) \ B ) u. b ) ) <_ ( ( M ` ( ( e i^i A ) \ B ) ) +e ( M ` b ) ) <-> ( M ` ( ( ( e i^i A ) \ B ) u. ( e \ A ) ) ) <_ ( ( M ` ( ( e i^i A ) \ B ) ) +e ( M ` ( e \ A ) ) ) ) )
43 37 42 rspc2v 
 |-  ( ( ( ( e i^i A ) \ B ) e. ~P O /\ ( e \ A ) e. ~P O ) -> ( A. a e. ~P O A. b e. ~P O ( M ` ( a u. b ) ) <_ ( ( M ` a ) +e ( M ` b ) ) -> ( M ` ( ( ( e i^i A ) \ B ) u. ( e \ A ) ) ) <_ ( ( M ` ( ( e i^i A ) \ B ) ) +e ( M ` ( e \ A ) ) ) ) )
44 43 imp 
 |-  ( ( ( ( ( e i^i A ) \ B ) e. ~P O /\ ( e \ A ) e. ~P O ) /\ A. a e. ~P O A. b e. ~P O ( M ` ( a u. b ) ) <_ ( ( M ` a ) +e ( M ` b ) ) ) -> ( M ` ( ( ( e i^i A ) \ B ) u. ( e \ A ) ) ) <_ ( ( M ` ( ( e i^i A ) \ B ) ) +e ( M ` ( e \ A ) ) ) )
45 18 21 32 44 syl21anc 
 |-  ( ( ph /\ e e. ~P O ) -> ( M ` ( ( ( e i^i A ) \ B ) u. ( e \ A ) ) ) <_ ( ( M ` ( ( e i^i A ) \ B ) ) +e ( M ` ( e \ A ) ) ) )
46 29 45 eqbrtrrid 
 |-  ( ( ph /\ e e. ~P O ) -> ( M ` ( e \ ( A i^i B ) ) ) <_ ( ( M ` ( ( e i^i A ) \ B ) ) +e ( M ` ( e \ A ) ) ) )
47 xleadd2a 
 |-  ( ( ( ( M ` ( e \ ( A i^i B ) ) ) e. RR* /\ ( ( M ` ( ( e i^i A ) \ B ) ) +e ( M ` ( e \ A ) ) ) e. RR* /\ ( M ` ( e i^i ( A i^i B ) ) ) e. RR* ) /\ ( M ` ( e \ ( A i^i B ) ) ) <_ ( ( M ` ( ( e i^i A ) \ B ) ) +e ( M ` ( e \ A ) ) ) ) -> ( ( M ` ( e i^i ( A i^i B ) ) ) +e ( M ` ( e \ ( A i^i B ) ) ) ) <_ ( ( M ` ( e i^i ( A i^i B ) ) ) +e ( ( M ` ( ( e i^i A ) \ B ) ) +e ( M ` ( e \ A ) ) ) ) )
48 16 24 27 46 47 syl31anc 
 |-  ( ( ph /\ e e. ~P O ) -> ( ( M ` ( e i^i ( A i^i B ) ) ) +e ( M ` ( e \ ( A i^i B ) ) ) ) <_ ( ( M ` ( e i^i ( A i^i B ) ) ) +e ( ( M ` ( ( e i^i A ) \ B ) ) +e ( M ` ( e \ A ) ) ) ) )
49 1 2 elcarsg 
 |-  ( ph -> ( B e. ( toCaraSiga ` M ) <-> ( B C_ O /\ A. f e. ~P O ( ( M ` ( f i^i B ) ) +e ( M ` ( f \ B ) ) ) = ( M ` f ) ) ) )
50 5 49 mpbid 
 |-  ( ph -> ( B C_ O /\ A. f e. ~P O ( ( M ` ( f i^i B ) ) +e ( M ` ( f \ B ) ) ) = ( M ` f ) ) )
51 50 simprd 
 |-  ( ph -> A. f e. ~P O ( ( M ` ( f i^i B ) ) +e ( M ` ( f \ B ) ) ) = ( M ` f ) )
52 51 adantr 
 |-  ( ( ph /\ e e. ~P O ) -> A. f e. ~P O ( ( M ` ( f i^i B ) ) +e ( M ` ( f \ B ) ) ) = ( M ` f ) )
53 ineq1 
 |-  ( f = ( e i^i A ) -> ( f i^i B ) = ( ( e i^i A ) i^i B ) )
54 53 fveq2d 
 |-  ( f = ( e i^i A ) -> ( M ` ( f i^i B ) ) = ( M ` ( ( e i^i A ) i^i B ) ) )
55 difeq1 
 |-  ( f = ( e i^i A ) -> ( f \ B ) = ( ( e i^i A ) \ B ) )
56 55 fveq2d 
 |-  ( f = ( e i^i A ) -> ( M ` ( f \ B ) ) = ( M ` ( ( e i^i A ) \ B ) ) )
57 54 56 oveq12d 
 |-  ( f = ( e i^i A ) -> ( ( M ` ( f i^i B ) ) +e ( M ` ( f \ B ) ) ) = ( ( M ` ( ( e i^i A ) i^i B ) ) +e ( M ` ( ( e i^i A ) \ B ) ) ) )
58 fveq2 
 |-  ( f = ( e i^i A ) -> ( M ` f ) = ( M ` ( e i^i A ) ) )
59 57 58 eqeq12d 
 |-  ( f = ( e i^i A ) -> ( ( ( M ` ( f i^i B ) ) +e ( M ` ( f \ B ) ) ) = ( M ` f ) <-> ( ( M ` ( ( e i^i A ) i^i B ) ) +e ( M ` ( ( e i^i A ) \ B ) ) ) = ( M ` ( e i^i A ) ) ) )
60 59 adantl 
 |-  ( ( ( ph /\ e e. ~P O ) /\ f = ( e i^i A ) ) -> ( ( ( M ` ( f i^i B ) ) +e ( M ` ( f \ B ) ) ) = ( M ` f ) <-> ( ( M ` ( ( e i^i A ) i^i B ) ) +e ( M ` ( ( e i^i A ) \ B ) ) ) = ( M ` ( e i^i A ) ) ) )
61 17 60 rspcdv 
 |-  ( ( ph /\ e e. ~P O ) -> ( A. f e. ~P O ( ( M ` ( f i^i B ) ) +e ( M ` ( f \ B ) ) ) = ( M ` f ) -> ( ( M ` ( ( e i^i A ) i^i B ) ) +e ( M ` ( ( e i^i A ) \ B ) ) ) = ( M ` ( e i^i A ) ) ) )
62 52 61 mpd 
 |-  ( ( ph /\ e e. ~P O ) -> ( ( M ` ( ( e i^i A ) i^i B ) ) +e ( M ` ( ( e i^i A ) \ B ) ) ) = ( M ` ( e i^i A ) ) )
63 62 oveq1d 
 |-  ( ( ph /\ e e. ~P O ) -> ( ( ( M ` ( ( e i^i A ) i^i B ) ) +e ( M ` ( ( e i^i A ) \ B ) ) ) +e ( M ` ( e \ A ) ) ) = ( ( M ` ( e i^i A ) ) +e ( M ` ( e \ A ) ) ) )
64 17 elpwincl1 
 |-  ( ( ph /\ e e. ~P O ) -> ( ( e i^i A ) i^i B ) e. ~P O )
65 12 64 ffvelrnd 
 |-  ( ( ph /\ e e. ~P O ) -> ( M ` ( ( e i^i A ) i^i B ) ) e. ( 0 [,] +oo ) )
66 xrge0addass 
 |-  ( ( ( M ` ( ( e i^i A ) i^i B ) ) e. ( 0 [,] +oo ) /\ ( M ` ( ( e i^i A ) \ B ) ) e. ( 0 [,] +oo ) /\ ( M ` ( e \ A ) ) e. ( 0 [,] +oo ) ) -> ( ( ( M ` ( ( e i^i A ) i^i B ) ) +e ( M ` ( ( e i^i A ) \ B ) ) ) +e ( M ` ( e \ A ) ) ) = ( ( M ` ( ( e i^i A ) i^i B ) ) +e ( ( M ` ( ( e i^i A ) \ B ) ) +e ( M ` ( e \ A ) ) ) ) )
67 65 19 22 66 syl3anc 
 |-  ( ( ph /\ e e. ~P O ) -> ( ( ( M ` ( ( e i^i A ) i^i B ) ) +e ( M ` ( ( e i^i A ) \ B ) ) ) +e ( M ` ( e \ A ) ) ) = ( ( M ` ( ( e i^i A ) i^i B ) ) +e ( ( M ` ( ( e i^i A ) \ B ) ) +e ( M ` ( e \ A ) ) ) ) )
68 inass 
 |-  ( ( e i^i A ) i^i B ) = ( e i^i ( A i^i B ) )
69 68 fveq2i 
 |-  ( M ` ( ( e i^i A ) i^i B ) ) = ( M ` ( e i^i ( A i^i B ) ) )
70 69 oveq1i 
 |-  ( ( M ` ( ( e i^i A ) i^i B ) ) +e ( ( M ` ( ( e i^i A ) \ B ) ) +e ( M ` ( e \ A ) ) ) ) = ( ( M ` ( e i^i ( A i^i B ) ) ) +e ( ( M ` ( ( e i^i A ) \ B ) ) +e ( M ` ( e \ A ) ) ) )
71 67 70 eqtrdi 
 |-  ( ( ph /\ e e. ~P O ) -> ( ( ( M ` ( ( e i^i A ) i^i B ) ) +e ( M ` ( ( e i^i A ) \ B ) ) ) +e ( M ` ( e \ A ) ) ) = ( ( M ` ( e i^i ( A i^i B ) ) ) +e ( ( M ` ( ( e i^i A ) \ B ) ) +e ( M ` ( e \ A ) ) ) ) )
72 7 simprd 
 |-  ( ph -> A. e e. ~P O ( ( M ` ( e i^i A ) ) +e ( M ` ( e \ A ) ) ) = ( M ` e ) )
73 72 r19.21bi 
 |-  ( ( ph /\ e e. ~P O ) -> ( ( M ` ( e i^i A ) ) +e ( M ` ( e \ A ) ) ) = ( M ` e ) )
74 63 71 73 3eqtr3d 
 |-  ( ( ph /\ e e. ~P O ) -> ( ( M ` ( e i^i ( A i^i B ) ) ) +e ( ( M ` ( ( e i^i A ) \ B ) ) +e ( M ` ( e \ A ) ) ) ) = ( M ` e ) )
75 48 74 breqtrd 
 |-  ( ( ph /\ e e. ~P O ) -> ( ( M ` ( e i^i ( A i^i B ) ) ) +e ( M ` ( e \ ( A i^i B ) ) ) ) <_ ( M ` e ) )
76 inundif 
 |-  ( ( e i^i ( A i^i B ) ) u. ( e \ ( A i^i B ) ) ) = e
77 76 fveq2i 
 |-  ( M ` ( ( e i^i ( A i^i B ) ) u. ( e \ ( A i^i B ) ) ) ) = ( M ` e )
78 uneq1 
 |-  ( a = ( e i^i ( A i^i B ) ) -> ( a u. b ) = ( ( e i^i ( A i^i B ) ) u. b ) )
79 78 fveq2d 
 |-  ( a = ( e i^i ( A i^i B ) ) -> ( M ` ( a u. b ) ) = ( M ` ( ( e i^i ( A i^i B ) ) u. b ) ) )
80 fveq2 
 |-  ( a = ( e i^i ( A i^i B ) ) -> ( M ` a ) = ( M ` ( e i^i ( A i^i B ) ) ) )
81 80 oveq1d 
 |-  ( a = ( e i^i ( A i^i B ) ) -> ( ( M ` a ) +e ( M ` b ) ) = ( ( M ` ( e i^i ( A i^i B ) ) ) +e ( M ` b ) ) )
82 79 81 breq12d 
 |-  ( a = ( e i^i ( A i^i B ) ) -> ( ( M ` ( a u. b ) ) <_ ( ( M ` a ) +e ( M ` b ) ) <-> ( M ` ( ( e i^i ( A i^i B ) ) u. b ) ) <_ ( ( M ` ( e i^i ( A i^i B ) ) ) +e ( M ` b ) ) ) )
83 uneq2 
 |-  ( b = ( e \ ( A i^i B ) ) -> ( ( e i^i ( A i^i B ) ) u. b ) = ( ( e i^i ( A i^i B ) ) u. ( e \ ( A i^i B ) ) ) )
84 83 fveq2d 
 |-  ( b = ( e \ ( A i^i B ) ) -> ( M ` ( ( e i^i ( A i^i B ) ) u. b ) ) = ( M ` ( ( e i^i ( A i^i B ) ) u. ( e \ ( A i^i B ) ) ) ) )
85 fveq2 
 |-  ( b = ( e \ ( A i^i B ) ) -> ( M ` b ) = ( M ` ( e \ ( A i^i B ) ) ) )
86 85 oveq2d 
 |-  ( b = ( e \ ( A i^i B ) ) -> ( ( M ` ( e i^i ( A i^i B ) ) ) +e ( M ` b ) ) = ( ( M ` ( e i^i ( A i^i B ) ) ) +e ( M ` ( e \ ( A i^i B ) ) ) ) )
87 84 86 breq12d 
 |-  ( b = ( e \ ( A i^i B ) ) -> ( ( M ` ( ( e i^i ( A i^i B ) ) u. b ) ) <_ ( ( M ` ( e i^i ( A i^i B ) ) ) +e ( M ` b ) ) <-> ( M ` ( ( e i^i ( A i^i B ) ) u. ( e \ ( A i^i B ) ) ) ) <_ ( ( M ` ( e i^i ( A i^i B ) ) ) +e ( M ` ( e \ ( A i^i B ) ) ) ) ) )
88 82 87 rspc2v 
 |-  ( ( ( e i^i ( A i^i B ) ) e. ~P O /\ ( e \ ( A i^i B ) ) e. ~P O ) -> ( A. a e. ~P O A. b e. ~P O ( M ` ( a u. b ) ) <_ ( ( M ` a ) +e ( M ` b ) ) -> ( M ` ( ( e i^i ( A i^i B ) ) u. ( e \ ( A i^i B ) ) ) ) <_ ( ( M ` ( e i^i ( A i^i B ) ) ) +e ( M ` ( e \ ( A i^i B ) ) ) ) ) )
89 88 imp 
 |-  ( ( ( ( e i^i ( A i^i B ) ) e. ~P O /\ ( e \ ( A i^i B ) ) e. ~P O ) /\ A. a e. ~P O A. b e. ~P O ( M ` ( a u. b ) ) <_ ( ( M ` a ) +e ( M ` b ) ) ) -> ( M ` ( ( e i^i ( A i^i B ) ) u. ( e \ ( A i^i B ) ) ) ) <_ ( ( M ` ( e i^i ( A i^i B ) ) ) +e ( M ` ( e \ ( A i^i B ) ) ) ) )
90 25 14 32 89 syl21anc 
 |-  ( ( ph /\ e e. ~P O ) -> ( M ` ( ( e i^i ( A i^i B ) ) u. ( e \ ( A i^i B ) ) ) ) <_ ( ( M ` ( e i^i ( A i^i B ) ) ) +e ( M ` ( e \ ( A i^i B ) ) ) ) )
91 77 90 eqbrtrrid 
 |-  ( ( ph /\ e e. ~P O ) -> ( M ` e ) <_ ( ( M ` ( e i^i ( A i^i B ) ) ) +e ( M ` ( e \ ( A i^i B ) ) ) ) )
92 75 91 jca 
 |-  ( ( ph /\ e e. ~P O ) -> ( ( ( M ` ( e i^i ( A i^i B ) ) ) +e ( M ` ( e \ ( A i^i B ) ) ) ) <_ ( M ` e ) /\ ( M ` e ) <_ ( ( M ` ( e i^i ( A i^i B ) ) ) +e ( M ` ( e \ ( A i^i B ) ) ) ) ) )
93 27 16 xaddcld 
 |-  ( ( ph /\ e e. ~P O ) -> ( ( M ` ( e i^i ( A i^i B ) ) ) +e ( M ` ( e \ ( A i^i B ) ) ) ) e. RR* )
94 2 ffvelrnda 
 |-  ( ( ph /\ e e. ~P O ) -> ( M ` e ) e. ( 0 [,] +oo ) )
95 11 94 sselid 
 |-  ( ( ph /\ e e. ~P O ) -> ( M ` e ) e. RR* )
96 xrletri3 
 |-  ( ( ( ( M ` ( e i^i ( A i^i B ) ) ) +e ( M ` ( e \ ( A i^i B ) ) ) ) e. RR* /\ ( M ` e ) e. RR* ) -> ( ( ( M ` ( e i^i ( A i^i B ) ) ) +e ( M ` ( e \ ( A i^i B ) ) ) ) = ( M ` e ) <-> ( ( ( M ` ( e i^i ( A i^i B ) ) ) +e ( M ` ( e \ ( A i^i B ) ) ) ) <_ ( M ` e ) /\ ( M ` e ) <_ ( ( M ` ( e i^i ( A i^i B ) ) ) +e ( M ` ( e \ ( A i^i B ) ) ) ) ) ) )
97 93 95 96 syl2anc 
 |-  ( ( ph /\ e e. ~P O ) -> ( ( ( M ` ( e i^i ( A i^i B ) ) ) +e ( M ` ( e \ ( A i^i B ) ) ) ) = ( M ` e ) <-> ( ( ( M ` ( e i^i ( A i^i B ) ) ) +e ( M ` ( e \ ( A i^i B ) ) ) ) <_ ( M ` e ) /\ ( M ` e ) <_ ( ( M ` ( e i^i ( A i^i B ) ) ) +e ( M ` ( e \ ( A i^i B ) ) ) ) ) ) )
98 92 97 mpbird 
 |-  ( ( ph /\ e e. ~P O ) -> ( ( M ` ( e i^i ( A i^i B ) ) ) +e ( M ` ( e \ ( A i^i B ) ) ) ) = ( M ` e ) )
99 98 ralrimiva 
 |-  ( ph -> A. e e. ~P O ( ( M ` ( e i^i ( A i^i B ) ) ) +e ( M ` ( e \ ( A i^i B ) ) ) ) = ( M ` e ) )
100 10 99 jca 
 |-  ( ph -> ( ( A i^i B ) C_ O /\ A. e e. ~P O ( ( M ` ( e i^i ( A i^i B ) ) ) +e ( M ` ( e \ ( A i^i B ) ) ) ) = ( M ` e ) ) )
101 1 2 elcarsg 
 |-  ( ph -> ( ( A i^i B ) e. ( toCaraSiga ` M ) <-> ( ( A i^i B ) C_ O /\ A. e e. ~P O ( ( M ` ( e i^i ( A i^i B ) ) ) +e ( M ` ( e \ ( A i^i B ) ) ) ) = ( M ` e ) ) ) )
102 100 101 mpbird 
 |-  ( ph -> ( A i^i B ) e. ( toCaraSiga ` M ) )