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