Metamath Proof Explorer


Theorem inffien

Description: The set of finite intersections of an infinite well-orderable set is equinumerous to the set itself. (Contributed by Mario Carneiro, 18-May-2015)

Ref Expression
Assertion inffien
|- ( ( A e. dom card /\ _om ~<_ A ) -> ( fi ` A ) ~~ A )

Proof

Step Hyp Ref Expression
1 infpwfien
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> ( ~P A i^i Fin ) ~~ A )
2 relen
 |-  Rel ~~
3 2 brrelex1i
 |-  ( ( ~P A i^i Fin ) ~~ A -> ( ~P A i^i Fin ) e. _V )
4 1 3 syl
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> ( ~P A i^i Fin ) e. _V )
5 difss
 |-  ( ( ~P A i^i Fin ) \ { (/) } ) C_ ( ~P A i^i Fin )
6 ssdomg
 |-  ( ( ~P A i^i Fin ) e. _V -> ( ( ( ~P A i^i Fin ) \ { (/) } ) C_ ( ~P A i^i Fin ) -> ( ( ~P A i^i Fin ) \ { (/) } ) ~<_ ( ~P A i^i Fin ) ) )
7 4 5 6 mpisyl
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> ( ( ~P A i^i Fin ) \ { (/) } ) ~<_ ( ~P A i^i Fin ) )
8 domentr
 |-  ( ( ( ( ~P A i^i Fin ) \ { (/) } ) ~<_ ( ~P A i^i Fin ) /\ ( ~P A i^i Fin ) ~~ A ) -> ( ( ~P A i^i Fin ) \ { (/) } ) ~<_ A )
9 7 1 8 syl2anc
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> ( ( ~P A i^i Fin ) \ { (/) } ) ~<_ A )
10 numdom
 |-  ( ( A e. dom card /\ ( ( ~P A i^i Fin ) \ { (/) } ) ~<_ A ) -> ( ( ~P A i^i Fin ) \ { (/) } ) e. dom card )
11 9 10 syldan
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> ( ( ~P A i^i Fin ) \ { (/) } ) e. dom card )
12 eqid
 |-  ( x e. ( ( ~P A i^i Fin ) \ { (/) } ) |-> |^| x ) = ( x e. ( ( ~P A i^i Fin ) \ { (/) } ) |-> |^| x )
13 12 fifo
 |-  ( A e. dom card -> ( x e. ( ( ~P A i^i Fin ) \ { (/) } ) |-> |^| x ) : ( ( ~P A i^i Fin ) \ { (/) } ) -onto-> ( fi ` A ) )
14 13 adantr
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> ( x e. ( ( ~P A i^i Fin ) \ { (/) } ) |-> |^| x ) : ( ( ~P A i^i Fin ) \ { (/) } ) -onto-> ( fi ` A ) )
15 fodomnum
 |-  ( ( ( ~P A i^i Fin ) \ { (/) } ) e. dom card -> ( ( x e. ( ( ~P A i^i Fin ) \ { (/) } ) |-> |^| x ) : ( ( ~P A i^i Fin ) \ { (/) } ) -onto-> ( fi ` A ) -> ( fi ` A ) ~<_ ( ( ~P A i^i Fin ) \ { (/) } ) ) )
16 11 14 15 sylc
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> ( fi ` A ) ~<_ ( ( ~P A i^i Fin ) \ { (/) } ) )
17 domtr
 |-  ( ( ( fi ` A ) ~<_ ( ( ~P A i^i Fin ) \ { (/) } ) /\ ( ( ~P A i^i Fin ) \ { (/) } ) ~<_ A ) -> ( fi ` A ) ~<_ A )
18 16 9 17 syl2anc
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> ( fi ` A ) ~<_ A )
19 fvex
 |-  ( fi ` A ) e. _V
20 ssfii
 |-  ( A e. dom card -> A C_ ( fi ` A ) )
21 20 adantr
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> A C_ ( fi ` A ) )
22 ssdomg
 |-  ( ( fi ` A ) e. _V -> ( A C_ ( fi ` A ) -> A ~<_ ( fi ` A ) ) )
23 19 21 22 mpsyl
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> A ~<_ ( fi ` A ) )
24 sbth
 |-  ( ( ( fi ` A ) ~<_ A /\ A ~<_ ( fi ` A ) ) -> ( fi ` A ) ~~ A )
25 18 23 24 syl2anc
 |-  ( ( A e. dom card /\ _om ~<_ A ) -> ( fi ` A ) ~~ A )