HomePage RecentChanges

mmj2bug

    $( <MM> <PROOF_ASST> THEOREM=fcfrl  LOC_AFTER=?
    $d x y z A n u
    $d n B
    $d n C
    $d x B
    $d x C
    $d n D
    *** A -- A \ U. B is finite  ((( E. n e. om ( A \ U. B ) ~~ n )))
    * si A est fini et B (_ A alors B est fini.
    1::ssfi            |- ( ( E. x e. om A ~~ x /\ B (_ A ) -> E. x e. om B ~~ x ) 
    * Si A e. B alors |^| B (_ A.
    2::intss1          |- ( A e. B -> |^| B (_ A )
    * Le complement de l'union = l'intersection des complement.
    3::iindif2         |- ( -. A = (/) -> |^|_ x e. A ( B \ C ) = ( B \ U_ x e. A C ) ) 
    * Relationship betwwen U_ and U. |^| and |^|_ .
    4::uniiun          |- U. A = U_ x e. A x 
    5::intiin          |- |^| A = |^|_ x e. A x 
    * Union indexee incluse dans
    * iinss  |- ( E. x e. A B (_ C ->  |^|_ x e. A B (_ C ) $=
    * ( x = U. u /\ ( x (_ A /\ ( E. n e. om ( A \ x ) ~~ n \/ x = (/) ) ) )
    * E. x ( x = U. u /\ ( x (_ A /\ ( E. n e. om ( A \ x ) ~~ n \/ x = (/) ) ) )
    * 10:: ( -. u = (/) -> |^|_ x e. u ( A \ x ) = ( A \ U_ x e. u x ) )
    * iinss  |- ( E. x e. u ( A \ x ) (_ ( A \ x ) ->  |^|_ x e. u ( A \ x ) (_ ( A \ x ) ) $=
    * 1::ssfi            |- ( ( E. n e. om ( A \ x ) ~~ n /\ |^|_ x e. u ( A \ x ) (_ ( A \ x ) -> E. n e. om |^|_ x e. u ( A \ x ) ~~ n ) 
    * 10:: ( -. u = (/) -> |^|_ x e. u ( A \ x ) = ( A \ U_ x e. u x ) )
    * 10:: ( -. u = (/) -> E. n e. om |^|_ x e. u ( A \ x ) = E. n e. om ( A \ U_ x e. u x ) )
    * 4::uniiun          |- U. u = U_ x e. u x
    * 10:: ( -. u = (/) -> E. n e. om |^|_ x e. u ( A \ x ) = E. n e. om ( A \ U. u ) )
    * 10:: ( -. u = (/) -> E. n e. om ( A \ U. u ) ~~ n )
    6:?:    |- ( ( x e. u -> ( x (_ A /\ ( E. n e. om ( A \ x ) ~~ n \/ x = (/) ) ) ) -> U. u (_ A )
    7:?:    |- ( ( x e. u -> ( x (_ A /\ ( E. n e. om ( A \ x ) ~~ n \/ x = (/) ) ) ) -> ( E. n e. om ( A \ U. u ) ~~ n \/ U. u = (/) ) )
    *|- ( ( x e. u -> ( x (_ A /\ ( E. n e. om ( A \ x ) ~~ n \/ x = (/) ) ) ) -> ( U. u (_ A /\ ( E. n e. om ( A \ U. u ) ~~ n \/ U. u = (/) ) ) )
    **** B -- A \ x i^i y is finite.
    **** C -- The end of the proof
    * On supprime le quantificateur
    8::clelab   |- ( 
                  U. u e. { x | ( x (_ A /\ ( E. n e. om ( A \ x ) ~~ n \/ x = (/) ) ) } 
                <-> 
                  E. x ( x = U. u /\ ( x (_ A /\ ( E. n e. om ( A \ x ) ~~ n \/ x = (/) ) ) )
                )
    * On remplace e. Top par sa definition
    9:?:   |- { x | ( x (_ A /\ ( E. n e. om ( A \ x ) ~~ n \/ x = (/) ) ) } e. V
    * On remplace e. Top par sa definition
    10::istopg   |- ( { x | ( x (_ A /\ ( E. n e. om ( A \ x ) ~~ n \/ x = (/) ) ) } e. V -> 
                 ( { x | ( x (_ A /\ ( E. n e. om ( A \ x ) ~~ n \/ x = (/) ) ) } e. Top <-> 
                 ( A. u ( u (_ { x | ( x (_ A /\ ( E. n e. om ( A \ x ) ~~ n \/ x = (/) ) ) } -> 
                 U. u e. { x | ( x (_ A /\ ( E. n e. om ( A \ x ) ~~ n \/ x = (/) ) ) } ) 
                 /\ A. u e. { x | ( x (_ A /\ ( E. n e. om ( A \ x ) ~~ n \/ x = (/) ) ) } 
                 A. z e. { x | ( x (_ A /\ ( E. n e. om ( A \ x ) ~~ n \/ x = (/) ) ) } 
                ( u i^i z ) e. { x | ( x (_ A /\ ( E. n e. om ( A \ x ) ~~ n \/ x = (/) ) ) } ) ) )
    * On remplace e. Top par sa definition
    11:9,10:ax-mp    |- ( { x | ( x (_ A /\ ( E. n e. om ( A \ x ) ~~ n \/ x = (/) ) ) } e. Top <-> 
                     ( A. u ( u (_ { x | ( x (_ A /\ ( E. n e. om ( A \ x ) ~~ n \/ x = (/) ) ) } -> 
                     U. u e. { x | ( x (_ A /\ ( E. n e. om ( A \ x ) ~~ n \/ x = (/) ) ) } ) /\ 
                     A. u e. { x | ( x (_ A /\ ( E. n e. om ( A \ x ) ~~ n \/ x = (/) ) ) } 
                     A. z e. { x | ( x (_ A /\ ( E. n e. om ( A \ x ) ~~ n \/ x = (/) ) ) } 
                     ( u i^i z ) e. { x | ( x (_ A /\ ( E. n e. om ( A \ x ) ~~ n \/ x = (/) ) ) } ) )
    * On se debarasse de la seconde classe
    12::ax-17        |- ( y e. u -> A. x y e. u ) 
    * On se debarasse de la seconde classe
    13::hbab1         |- ( y e. { x | ( x (_ A /\ ( E. n e. om ( A \ x ) ~~ n \/ 
                          x = (/) ) ) } -> A. x y e. { x | ( x (_ A /\ ( E. n e. om
                          ( A \ x ) ~~ n \/ x = (/) ) ) } ) 
    * On se debarasse de la seconde classe
    14:12,13:dfss2f     |- (
                           u (_ { x | ( x (_ A /\ ( E. n e. om ( A \ x ) ~~ n \/ x = (/) ) ) }
                           <->
                           A. x ( x e. u -> x e. { x | ( x (_ A /\ ( E. n e. om ( A \ x ) ~~ n \/ x = (/) ) ) } )
                           )
    * On se debarasse de la classe nouvellement apparue.
    15::abid  |- (
     x e. { x | ( x (_ A /\ ( E. n e. om ( A \ x ) ~~ n \/ x = (/) ) ) }
     <->
     ( x (_ A /\ ( E. n e. om ( A \ x ) ~~ n \/ x = (/) ) )
     )
    * On se debarasse de la classe nouvellement apparue.
    16:15:imbi2i |- (
      ( x e. u -> x e. { x | ( x (_ A /\ ( E. n e. om ( A \ x ) ~~ n \/ x = (/) ) ) } )
      <->
      ( x e. u -> ( x (_ A /\ ( E. n e. om ( A \ x ) ~~ n \/ x = (/) ) ) )
      )
    * On se debarasse de la classe nouvellement apparue.
    17:16:albii  |- (
      A. x ( x e. u -> x e. { x | ( x (_ A /\ ( E. n e. om ( A \ x ) ~~ n \/ x = (/) ) ) } )
      <->
      A. x ( x e. u -> ( x (_ A /\ ( E. n e. om ( A \ x ) ~~ n \/ x = (/) ) ) )
      )
    * On substitue x par U. u.
    18::sseq1 |- ( x = U. u -> ( x (_ A <-> U. u (_ A ) )
    * On substitue x par U. u.
    19::difeq2 |- ( x = U. u -> ( A \ x ) = ( A \ U. u ) )
    * On substitue x par U. u.
    20:19:breq1d |- ( x = U. u -> ( ( A \ x ) ~~ n <-> ( A \ U. u ) ~~ n ) )
    * On substitue x par U. u.
    21:20:rexbidv |- ( x = U. u -> ( E. n e. om ( A \ x ) ~~ n <-> E. n e. om ( A \ U. u ) ~~ n ) )
    * On substitue x par U. u.
    22::eqeq1 |- ( x = U. u -> ( x = (/) <-> U. u = (/) ) )
    * On substitue x par U. u.
    23:21,22:orbi12d |- ( x = U. u -> 
                              ( 
                                 ( E. n e. om ( A \ x ) ~~ n \/ x = (/) ) 
                              <-> 
                                 ( E. n e. om ( A \ U. u ) ~~ n \/ U. u = (/) ) 
                               ) 
                   )
    * On substitue x par U. u.
    24:18,23:anbi12d |- ( x = U. u -> 
                              ( 
                                 ( x (_ A /\ ( E. n e. om ( A \ x ) ~~ n \/ x = (/) ) )
                              <-> 
                                 ( U. u (_ A /\ ( E. n e. om ( A \ U. u ) ~~ n \/ U. u = (/) ) )
                               ) 
                   )
    * On substitue x par U. u.
    25:24:bicomd |- ( x = U. u -> 
                              ( 
                                 ( U. u (_ A /\ ( E. n e. om ( A \ U. u ) ~~ n \/ U. u = (/) ) )
                              <-> 
                                 ( x (_ A /\ ( E. n e. om ( A \ x ) ~~ n \/ x = (/) ) )
                               ) 
                   )
    * On substitue x par U. u. Suppression du x = U. u surnumeraire
    26:25:biimpd        |- ( x = U. u -> ( ( U. u (_ A /\ ( E. n e. om ( A \
                          U. u ) ~~ n \/ U. u = (/) ) ) -> ( x (_ A /\ 
                          ( E. n e. om ( A \ x ) ~~ n \/ x = (/) ) ) ) )
    * On substitue x par U. u.
    27::anc2l              |- ( ( x = U. u -> ( ( U. u (_ A /\ ( E. n e. om ( A \
                          U. u ) ~~ n \/ U. u = (/) ) ) -> ( x (_ A /\ 
                          ( E. n e. om ( A \ x ) ~~ n \/ x = (/) ) ) ) )
                           -> ( x = U. u -> ( ( U. u (_ A /\ ( E. n e. om ( A \
                          U. u ) ~~ n \/ U. u = (/) ) ) -> ( x = U. u /\ ( x (_ A /\ 
                          ( E. n e. om ( A \ x ) ~~ n \/ x = (/) ) ) ) ) ) )
    * On substitue x par U. u. Suppression du E. ( etrange et fascinant a4w )
    28:26,27:ax-mp   |- ( x = U. u -> ( ( U. u (_ A /\ ( E. n e. om ( A \ U. u ) ~~
                          n \/ U. u = (/) ) ) -> ( x = U. u /\ ( x (_ A /\ ( E. n e.
                          om ( A \ x ) ~~ n \/ x = (/) ) ) ) ) )
    * On substitue x par U. u
    29:?:             |- ( x = U. u -> ( ( U. u (_ A /\ ( E. n e. om ( A \ U. u ) ~~
                          n \/ U. u = (/) ) ) -> ( x = U. u /\ ( x (_ A /\ ( E. n e.
                          om ( A \ x ) ~~ n \/ x = (/) ) ) ) ) )
    * On se debarasse de la classe nouvellement apparue.
    30:29:a4w |- ( ( U. u (_ A /\ ( E. n e. om ( A \ U. u ) ~~ n \/ U. u = (/) ) ) -> 
            E. x ( x = U. u /\ ( x (_ A /\ ( E. n e. om ( A \ x ) ~~ n \/ x = (/) ) ) ) )
    * On se debarasse de la classe nouvellement apparue
    31:30:a4s   |- (  A. x ( x e. u -> ( x (_ A /\ ( E. n e. om ( A \ x ) ~~ n \/ x = (/) ) ) ) -> 
                ( U. u (_ A /\ ( E. n e. om ( A \ U. u ) ~~ n \/ U. u = (/) ) ) )
    * On se debarasse de la classe nouvellement apparue
    32:31,30:syl                 |- (  A. x ( x e. u -> ( x (_ A /\ ( E. n e. om ( A \ x ) ~~ n \/ x = (/) ) ) ) -> 
                            E. x ( x = U. u /\ ( x (_ A /\ ( E. n e. om ( A \ x ) ~~ n \/ x = (/) ) ) ) )
    * On se debarasse de la premiere classe. Mais une nouvelle classe est apparue
    * x est un element de la topologie
    33:17,32:sylbi           |- ( A. x ( x e. u -> x e. { x | ( x (_ A /\ ( E. n e. om ( A \ x ) ~~ n \/ x = (/) ) ) } ) -> 
                            E. x ( x = U. u /\ ( x (_ A /\ ( E. n e. om ( A \ x ) ~~ n \/ x = (/) ) ) ) )
    * On se debarasse de la seconde classe
    34:14,33:sylbi       |- ( u (_ { x | ( x (_ A /\ ( E. n e. om ( A \ x ) ~~ n \/ x
                          = (/) ) ) } -> E. x ( x = U. u /\ ( x (_ A /\ ( E. n e. om
                          ( A \ x ) ~~ n \/ x = (/) ) ) ) )
    * On supprime le quantificateur
    35:34,8:sylibr              |- ( u (_ { x | ( x (_ A /\ ( E. n e. om ( A \ x ) ~~ n \/ x
                          = (/) ) ) } -> U. u e. { x | ( x (_ A /\ ( E. n e. om ( A 
                          \ x ) ~~ n \/ x = (/) ) ) } )
    * On split 26 en les deux termes de la definition
    36:35:ax-gen           |- A. u ( u (_ { x | ( x (_ A /\ ( E. n e. om ( A \ x ) ~~ n
                          \/ x = (/) ) ) } -> U. u e. { x | ( x (_ A /\ ( E. n e. om 
                          ( A \ x ) ~~ n \/ x = (/) ) ) } ) 
    * On split 26 en les deux termes de la definition
    37:?:              |- A. u e. { x | ( x (_ A /\ ( E. n e. om ( A \ x ) ~~ n \/ 
                          x = (/) ) ) } A. z e. { x | ( x (_ A /\ ( E. n e. om ( A \
                          x ) ~~ n \/ x = (/) ) ) } ( u i^i z ) e. { x | ( x (_ A /\
                          ( E. n e. om ( A \ x ) ~~ n \/ x = (/) ) ) } 
    * On remplace e. Top par sa definition
    38:36,37:pm3.2i     |- ( A. u ( u (_ { x | ( x (_ A /\ ( E. n e. om ( A \ x ) ~~ n \/ x = (/) ) ) } -> 
                        U. u e. { x | ( x (_ A /\ ( E. n e. om ( A \ x ) ~~ n \/ x = (/) ) ) } ) 
                        /\ A. u e. { x | ( x (_ A /\ ( E. n e. om ( A \ x ) ~~ n \/ x = (/) ) ) } 
                        A. z e. { x | ( x (_ A /\ ( E. n e. om ( A \ x ) ~~ n \/ x = (/) ) ) } 
                        ( u i^i z ) e. { x | ( x (_ A /\ ( E. n e. om ( A \ x ) ~~ n \/ x = (/) ) ) } )
    qed:11,38:mpbir  |- { x | ( x (_ A /\ ( E. n e. om ( A \ x ) ~~ n \/ x = (/) ) ) } e. Top
    $)