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 )