Metamath Proof Explorer

Theorem caragenel

Description: Membership in the Caratheodory's construction. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypotheses caragenel.o 
|- ( ph -> O e. OutMeas )
caragenel.s 
|- S = ( CaraGen ` O )
Assertion caragenel 
|- ( ph -> ( E e. S <-> ( E e. ~P U. dom O /\ A. a e. ~P U. dom O ( ( O ` ( a i^i E ) ) +e ( O ` ( a \ E ) ) ) = ( O ` a ) ) ) )

Proof

Step Hyp Ref Expression
1 caragenel.o 
 |-  ( ph -> O e. OutMeas )
2 caragenel.s 
 |-  S = ( CaraGen ` O )
3 caragenval 
 |-  ( O e. OutMeas -> ( CaraGen ` O ) = { e e. ~P U. dom O | A. a e. ~P U. dom O ( ( O ` ( a i^i e ) ) +e ( O ` ( a \ e ) ) ) = ( O ` a ) } )
4 1 3 syl 
 |-  ( ph -> ( CaraGen ` O ) = { e e. ~P U. dom O | A. a e. ~P U. dom O ( ( O ` ( a i^i e ) ) +e ( O ` ( a \ e ) ) ) = ( O ` a ) } )
5 2 4 syl5eq 
 |-  ( ph -> S = { e e. ~P U. dom O | A. a e. ~P U. dom O ( ( O ` ( a i^i e ) ) +e ( O ` ( a \ e ) ) ) = ( O ` a ) } )
6 5 eleq2d 
 |-  ( ph -> ( E e. S <-> E e. { e e. ~P U. dom O | A. a e. ~P U. dom O ( ( O ` ( a i^i e ) ) +e ( O ` ( a \ e ) ) ) = ( O ` a ) } ) )
7 ineq2 
 |-  ( e = E -> ( a i^i e ) = ( a i^i E ) )
8 7 fveq2d 
 |-  ( e = E -> ( O ` ( a i^i e ) ) = ( O ` ( a i^i E ) ) )
9 difeq2 
 |-  ( e = E -> ( a \ e ) = ( a \ E ) )
10 9 fveq2d 
 |-  ( e = E -> ( O ` ( a \ e ) ) = ( O ` ( a \ E ) ) )
11 8 10 oveq12d 
 |-  ( e = E -> ( ( O ` ( a i^i e ) ) +e ( O ` ( a \ e ) ) ) = ( ( O ` ( a i^i E ) ) +e ( O ` ( a \ E ) ) ) )
12 11 eqeq1d 
 |-  ( e = E -> ( ( ( O ` ( a i^i e ) ) +e ( O ` ( a \ e ) ) ) = ( O ` a ) <-> ( ( O ` ( a i^i E ) ) +e ( O ` ( a \ E ) ) ) = ( O ` a ) ) )
13 12 ralbidv 
 |-  ( e = E -> ( A. a e. ~P U. dom O ( ( O ` ( a i^i e ) ) +e ( O ` ( a \ e ) ) ) = ( O ` a ) <-> A. a e. ~P U. dom O ( ( O ` ( a i^i E ) ) +e ( O ` ( a \ E ) ) ) = ( O ` a ) ) )
14 13 elrab 
 |-  ( E e. { e e. ~P U. dom O | A. a e. ~P U. dom O ( ( O ` ( a i^i e ) ) +e ( O ` ( a \ e ) ) ) = ( O ` a ) } <-> ( E e. ~P U. dom O /\ A. a e. ~P U. dom O ( ( O ` ( a i^i E ) ) +e ( O ` ( a \ E ) ) ) = ( O ` a ) ) )
15 14 a1i 
 |-  ( ph -> ( E e. { e e. ~P U. dom O | A. a e. ~P U. dom O ( ( O ` ( a i^i e ) ) +e ( O ` ( a \ e ) ) ) = ( O ` a ) } <-> ( E e. ~P U. dom O /\ A. a e. ~P U. dom O ( ( O ` ( a i^i E ) ) +e ( O ` ( a \ E ) ) ) = ( O ` a ) ) ) )
16 6 15 bitrd 
 |-  ( ph -> ( E e. S <-> ( E e. ~P U. dom O /\ A. a e. ~P U. dom O ( ( O ` ( a i^i E ) ) +e ( O ` ( a \ E ) ) ) = ( O ` a ) ) ) )