Metamath Proof Explorer

Theorem omessle

Description: The outer measure of a set is greater than or equal to the measure of a subset, Definition 113A (ii) of Fremlin1 p. 19. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses omessle.o 
|- ( ph -> O e. OutMeas )
omessle.x 
|- X = U. dom O
omessle.b 
|- ( ph -> B C_ X )
omessle.a 
|- ( ph -> A C_ B )
Assertion omessle 
|- ( ph -> ( O ` A ) <_ ( O ` B ) )

Proof

Step Hyp Ref Expression
1 omessle.o 
 |-  ( ph -> O e. OutMeas )
2 omessle.x 
 |-  X = U. dom O
3 omessle.b 
 |-  ( ph -> B C_ X )
4 omessle.a 
 |-  ( ph -> A C_ B )
5 1 2 unidmex 
 |-  ( ph -> X e. _V )
6 5 3 ssexd 
 |-  ( ph -> B e. _V )
7 6 4 ssexd 
 |-  ( ph -> A e. _V )
8 elpwg 
 |-  ( A e. _V -> ( A e. ~P B <-> A C_ B ) )
9 7 8 syl 
 |-  ( ph -> ( A e. ~P B <-> A C_ B ) )
10 4 9 mpbird 
 |-  ( ph -> A e. ~P B )
11 3 2 sseqtrdi 
 |-  ( ph -> B C_ U. dom O )
12 elpwg 
 |-  ( B e. _V -> ( B e. ~P U. dom O <-> B C_ U. dom O ) )
13 6 12 syl 
 |-  ( ph -> ( B e. ~P U. dom O <-> B C_ U. dom O ) )
14 11 13 mpbird 
 |-  ( ph -> B e. ~P U. dom O )
15 isome 
 |-  ( O e. OutMeas -> ( O e. OutMeas <-> ( ( ( ( O : dom O --> ( 0 [,] +oo ) /\ dom O = ~P U. dom O ) /\ ( O ` (/) ) = 0 ) /\ A. y e. ~P U. dom O A. z e. ~P y ( O ` z ) <_ ( O ` y ) ) /\ A. y e. ~P dom O ( y ~<_ _om -> ( O ` U. y ) <_ ( sum^ ` ( O |` y ) ) ) ) ) )
16 1 15 syl 
 |-  ( ph -> ( O e. OutMeas <-> ( ( ( ( O : dom O --> ( 0 [,] +oo ) /\ dom O = ~P U. dom O ) /\ ( O ` (/) ) = 0 ) /\ A. y e. ~P U. dom O A. z e. ~P y ( O ` z ) <_ ( O ` y ) ) /\ A. y e. ~P dom O ( y ~<_ _om -> ( O ` U. y ) <_ ( sum^ ` ( O |` y ) ) ) ) ) )
17 1 16 mpbid 
 |-  ( ph -> ( ( ( ( O : dom O --> ( 0 [,] +oo ) /\ dom O = ~P U. dom O ) /\ ( O ` (/) ) = 0 ) /\ A. y e. ~P U. dom O A. z e. ~P y ( O ` z ) <_ ( O ` y ) ) /\ A. y e. ~P dom O ( y ~<_ _om -> ( O ` U. y ) <_ ( sum^ ` ( O |` y ) ) ) ) )
18 17 simplrd 
 |-  ( ph -> A. y e. ~P U. dom O A. z e. ~P y ( O ` z ) <_ ( O ` y ) )
19 pweq 
 |-  ( y = B -> ~P y = ~P B )
20 19 raleqdv 
 |-  ( y = B -> ( A. z e. ~P y ( O ` z ) <_ ( O ` y ) <-> A. z e. ~P B ( O ` z ) <_ ( O ` y ) ) )
21 fveq2 
 |-  ( y = B -> ( O ` y ) = ( O ` B ) )
22 21 breq2d 
 |-  ( y = B -> ( ( O ` z ) <_ ( O ` y ) <-> ( O ` z ) <_ ( O ` B ) ) )
23 22 ralbidv 
 |-  ( y = B -> ( A. z e. ~P B ( O ` z ) <_ ( O ` y ) <-> A. z e. ~P B ( O ` z ) <_ ( O ` B ) ) )
24 20 23 bitrd 
 |-  ( y = B -> ( A. z e. ~P y ( O ` z ) <_ ( O ` y ) <-> A. z e. ~P B ( O ` z ) <_ ( O ` B ) ) )
25 24 rspcva 
 |-  ( ( B e. ~P U. dom O /\ A. y e. ~P U. dom O A. z e. ~P y ( O ` z ) <_ ( O ` y ) ) -> A. z e. ~P B ( O ` z ) <_ ( O ` B ) )
26 14 18 25 syl2anc 
 |-  ( ph -> A. z e. ~P B ( O ` z ) <_ ( O ` B ) )
27 fveq2 
 |-  ( z = A -> ( O ` z ) = ( O ` A ) )
28 27 breq1d 
 |-  ( z = A -> ( ( O ` z ) <_ ( O ` B ) <-> ( O ` A ) <_ ( O ` B ) ) )
29 28 rspcva 
 |-  ( ( A e. ~P B /\ A. z e. ~P B ( O ` z ) <_ ( O ` B ) ) -> ( O ` A ) <_ ( O ` B ) )
30 10 26 29 syl2anc 
 |-  ( ph -> ( O ` A ) <_ ( O ` B ) )