$( <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
$)