Metamath Proof Explorer

Theorem isome

Description: Express the predicate " O is an outer measure." Definition 113A of Fremlin1 p. 19. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Assertion isome 
|- ( O e. V -> ( 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 ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( x = O -> x = O )
2 dmeq 
 |-  ( x = O -> dom x = dom O )
3 1 2 feq12d 
 |-  ( x = O -> ( x : dom x --> ( 0 [,] +oo ) <-> O : dom O --> ( 0 [,] +oo ) ) )
4 2 unieqd 
 |-  ( x = O -> U. dom x = U. dom O )
5 4 pweqd 
 |-  ( x = O -> ~P U. dom x = ~P U. dom O )
6 2 5 eqeq12d 
 |-  ( x = O -> ( dom x = ~P U. dom x <-> dom O = ~P U. dom O ) )
7 3 6 anbi12d 
 |-  ( x = O -> ( ( x : dom x --> ( 0 [,] +oo ) /\ dom x = ~P U. dom x ) <-> ( O : dom O --> ( 0 [,] +oo ) /\ dom O = ~P U. dom O ) ) )
8 fveq1 
 |-  ( x = O -> ( x ` (/) ) = ( O ` (/) ) )
9 8 eqeq1d 
 |-  ( x = O -> ( ( x ` (/) ) = 0 <-> ( O ` (/) ) = 0 ) )
10 7 9 anbi12d 
 |-  ( x = O -> ( ( ( x : dom x --> ( 0 [,] +oo ) /\ dom x = ~P U. dom x ) /\ ( x ` (/) ) = 0 ) <-> ( ( O : dom O --> ( 0 [,] +oo ) /\ dom O = ~P U. dom O ) /\ ( O ` (/) ) = 0 ) ) )
11 fveq1 
 |-  ( x = O -> ( x ` z ) = ( O ` z ) )
12 fveq1 
 |-  ( x = O -> ( x ` y ) = ( O ` y ) )
13 11 12 breq12d 
 |-  ( x = O -> ( ( x ` z ) <_ ( x ` y ) <-> ( O ` z ) <_ ( O ` y ) ) )
14 13 ralbidv 
 |-  ( x = O -> ( A. z e. ~P y ( x ` z ) <_ ( x ` y ) <-> A. z e. ~P y ( O ` z ) <_ ( O ` y ) ) )
15 5 14 raleqbidv 
 |-  ( x = O -> ( A. y e. ~P U. dom x A. z e. ~P y ( x ` z ) <_ ( x ` y ) <-> A. y e. ~P U. dom O A. z e. ~P y ( O ` z ) <_ ( O ` y ) ) )
16 10 15 anbi12d 
 |-  ( x = O -> ( ( ( ( x : dom x --> ( 0 [,] +oo ) /\ dom x = ~P U. dom x ) /\ ( x ` (/) ) = 0 ) /\ A. y e. ~P U. dom x A. z e. ~P y ( x ` z ) <_ ( x ` y ) ) <-> ( ( ( 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 ) ) ) )
17 2 pweqd 
 |-  ( x = O -> ~P dom x = ~P dom O )
18 fveq1 
 |-  ( x = O -> ( x ` U. y ) = ( O ` U. y ) )
19 reseq1 
 |-  ( x = O -> ( x |` y ) = ( O |` y ) )
20 19 fveq2d 
 |-  ( x = O -> ( sum^ ` ( x |` y ) ) = ( sum^ ` ( O |` y ) ) )
21 18 20 breq12d 
 |-  ( x = O -> ( ( x ` U. y ) <_ ( sum^ ` ( x |` y ) ) <-> ( O ` U. y ) <_ ( sum^ ` ( O |` y ) ) ) )
22 21 imbi2d 
 |-  ( x = O -> ( ( y ~<_ _om -> ( x ` U. y ) <_ ( sum^ ` ( x |` y ) ) ) <-> ( y ~<_ _om -> ( O ` U. y ) <_ ( sum^ ` ( O |` y ) ) ) ) )
23 17 22 raleqbidv 
 |-  ( x = O -> ( A. y e. ~P dom x ( y ~<_ _om -> ( x ` U. y ) <_ ( sum^ ` ( x |` y ) ) ) <-> A. y e. ~P dom O ( y ~<_ _om -> ( O ` U. y ) <_ ( sum^ ` ( O |` y ) ) ) ) )
24 16 23 anbi12d 
 |-  ( x = O -> ( ( ( ( ( x : dom x --> ( 0 [,] +oo ) /\ dom x = ~P U. dom x ) /\ ( x ` (/) ) = 0 ) /\ A. y e. ~P U. dom x A. z e. ~P y ( x ` z ) <_ ( x ` y ) ) /\ A. y e. ~P dom x ( y ~<_ _om -> ( x ` U. y ) <_ ( sum^ ` ( x |` y ) ) ) ) <-> ( ( ( ( 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 ) ) ) ) ) )
25 df-ome 
 |-  OutMeas = { x | ( ( ( ( x : dom x --> ( 0 [,] +oo ) /\ dom x = ~P U. dom x ) /\ ( x ` (/) ) = 0 ) /\ A. y e. ~P U. dom x A. z e. ~P y ( x ` z ) <_ ( x ` y ) ) /\ A. y e. ~P dom x ( y ~<_ _om -> ( x ` U. y ) <_ ( sum^ ` ( x |` y ) ) ) ) }
26 24 25 elab2g 
 |-  ( O e. V -> ( 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 ) ) ) ) ) )