Metamath Proof Explorer

Theorem fictb

Description: A set is countable iff its collection of finite intersections is countable. (Contributed by Jeff Hankins, 24-Aug-2009) (Proof shortened by Mario Carneiro, 17-May-2015)

Ref Expression
Assertion fictb 
|- ( A e. B -> ( A ~<_ _om <-> ( fi ` A ) ~<_ _om ) )

Proof

Step Hyp Ref Expression
1 brdomi 
 |-  ( A ~<_ _om -> E. f f : A -1-1-> _om )
2 1 adantl 
 |-  ( ( A e. B /\ A ~<_ _om ) -> E. f f : A -1-1-> _om )
3 reldom 
 |-  Rel ~<_
4 3 brrelex2i 
 |-  ( A ~<_ _om -> _om e. _V )
5 omelon2 
 |-  ( _om e. _V -> _om e. On )
6 5 ad2antlr 
 |-  ( ( ( A e. B /\ _om e. _V ) /\ f : A -1-1-> _om ) -> _om e. On )
7 pwexg 
 |-  ( A e. B -> ~P A e. _V )
8 7 ad2antrr 
 |-  ( ( ( A e. B /\ _om e. _V ) /\ f : A -1-1-> _om ) -> ~P A e. _V )
9 inex1g 
 |-  ( ~P A e. _V -> ( ~P A i^i Fin ) e. _V )
10 8 9 syl 
 |-  ( ( ( A e. B /\ _om e. _V ) /\ f : A -1-1-> _om ) -> ( ~P A i^i Fin ) e. _V )
11 difss 
 |-  ( ( ~P A i^i Fin ) \ { (/) } ) C_ ( ~P A i^i Fin )
12 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 ) ) )
13 10 11 12 mpisyl 
 |-  ( ( ( A e. B /\ _om e. _V ) /\ f : A -1-1-> _om ) -> ( ( ~P A i^i Fin ) \ { (/) } ) ~<_ ( ~P A i^i Fin ) )
14 f1f1orn 
 |-  ( f : A -1-1-> _om -> f : A -1-1-onto-> ran f )
15 14 adantl 
 |-  ( ( ( A e. B /\ _om e. _V ) /\ f : A -1-1-> _om ) -> f : A -1-1-onto-> ran f )
16 f1opwfi 
 |-  ( f : A -1-1-onto-> ran f -> ( x e. ( ~P A i^i Fin ) |-> ( f " x ) ) : ( ~P A i^i Fin ) -1-1-onto-> ( ~P ran f i^i Fin ) )
17 15 16 syl 
 |-  ( ( ( A e. B /\ _om e. _V ) /\ f : A -1-1-> _om ) -> ( x e. ( ~P A i^i Fin ) |-> ( f " x ) ) : ( ~P A i^i Fin ) -1-1-onto-> ( ~P ran f i^i Fin ) )
18 f1oeng 
 |-  ( ( ( ~P A i^i Fin ) e. _V /\ ( x e. ( ~P A i^i Fin ) |-> ( f " x ) ) : ( ~P A i^i Fin ) -1-1-onto-> ( ~P ran f i^i Fin ) ) -> ( ~P A i^i Fin ) ~~ ( ~P ran f i^i Fin ) )
19 10 17 18 syl2anc 
 |-  ( ( ( A e. B /\ _om e. _V ) /\ f : A -1-1-> _om ) -> ( ~P A i^i Fin ) ~~ ( ~P ran f i^i Fin ) )
20 pwexg 
 |-  ( _om e. _V -> ~P _om e. _V )
21 20 ad2antlr 
 |-  ( ( ( A e. B /\ _om e. _V ) /\ f : A -1-1-> _om ) -> ~P _om e. _V )
22 inex1g 
 |-  ( ~P _om e. _V -> ( ~P _om i^i Fin ) e. _V )
23 21 22 syl 
 |-  ( ( ( A e. B /\ _om e. _V ) /\ f : A -1-1-> _om ) -> ( ~P _om i^i Fin ) e. _V )
24 f1f 
 |-  ( f : A -1-1-> _om -> f : A --> _om )
25 24 frnd 
 |-  ( f : A -1-1-> _om -> ran f C_ _om )
26 25 adantl 
 |-  ( ( ( A e. B /\ _om e. _V ) /\ f : A -1-1-> _om ) -> ran f C_ _om )
27 26 sspwd 
 |-  ( ( ( A e. B /\ _om e. _V ) /\ f : A -1-1-> _om ) -> ~P ran f C_ ~P _om )
28 27 ssrind 
 |-  ( ( ( A e. B /\ _om e. _V ) /\ f : A -1-1-> _om ) -> ( ~P ran f i^i Fin ) C_ ( ~P _om i^i Fin ) )
29 ssdomg 
 |-  ( ( ~P _om i^i Fin ) e. _V -> ( ( ~P ran f i^i Fin ) C_ ( ~P _om i^i Fin ) -> ( ~P ran f i^i Fin ) ~<_ ( ~P _om i^i Fin ) ) )
30 23 28 29 sylc 
 |-  ( ( ( A e. B /\ _om e. _V ) /\ f : A -1-1-> _om ) -> ( ~P ran f i^i Fin ) ~<_ ( ~P _om i^i Fin ) )
31 sneq 
 |-  ( f = z -> { f } = { z } )
32 pweq 
 |-  ( f = z -> ~P f = ~P z )
33 31 32 xpeq12d 
 |-  ( f = z -> ( { f } X. ~P f ) = ( { z } X. ~P z ) )
34 33 cbviunv 
 |-  U_ f e. x ( { f } X. ~P f ) = U_ z e. x ( { z } X. ~P z )
35 iuneq1 
 |-  ( x = y -> U_ z e. x ( { z } X. ~P z ) = U_ z e. y ( { z } X. ~P z ) )
36 34 35 syl5eq 
 |-  ( x = y -> U_ f e. x ( { f } X. ~P f ) = U_ z e. y ( { z } X. ~P z ) )
37 36 fveq2d 
 |-  ( x = y -> ( card ` U_ f e. x ( { f } X. ~P f ) ) = ( card ` U_ z e. y ( { z } X. ~P z ) ) )
38 37 cbvmptv 
 |-  ( x e. ( ~P _om i^i Fin ) |-> ( card ` U_ f e. x ( { f } X. ~P f ) ) ) = ( y e. ( ~P _om i^i Fin ) |-> ( card ` U_ z e. y ( { z } X. ~P z ) ) )
39 38 ackbij1 
 |-  ( x e. ( ~P _om i^i Fin ) |-> ( card ` U_ f e. x ( { f } X. ~P f ) ) ) : ( ~P _om i^i Fin ) -1-1-onto-> _om
40 f1oeng 
 |-  ( ( ( ~P _om i^i Fin ) e. _V /\ ( x e. ( ~P _om i^i Fin ) |-> ( card ` U_ f e. x ( { f } X. ~P f ) ) ) : ( ~P _om i^i Fin ) -1-1-onto-> _om ) -> ( ~P _om i^i Fin ) ~~ _om )
41 23 39 40 sylancl 
 |-  ( ( ( A e. B /\ _om e. _V ) /\ f : A -1-1-> _om ) -> ( ~P _om i^i Fin ) ~~ _om )
42 domentr 
 |-  ( ( ( ~P ran f i^i Fin ) ~<_ ( ~P _om i^i Fin ) /\ ( ~P _om i^i Fin ) ~~ _om ) -> ( ~P ran f i^i Fin ) ~<_ _om )
43 30 41 42 syl2anc 
 |-  ( ( ( A e. B /\ _om e. _V ) /\ f : A -1-1-> _om ) -> ( ~P ran f i^i Fin ) ~<_ _om )
44 endomtr 
 |-  ( ( ( ~P A i^i Fin ) ~~ ( ~P ran f i^i Fin ) /\ ( ~P ran f i^i Fin ) ~<_ _om ) -> ( ~P A i^i Fin ) ~<_ _om )
45 19 43 44 syl2anc 
 |-  ( ( ( A e. B /\ _om e. _V ) /\ f : A -1-1-> _om ) -> ( ~P A i^i Fin ) ~<_ _om )
46 domtr 
 |-  ( ( ( ( ~P A i^i Fin ) \ { (/) } ) ~<_ ( ~P A i^i Fin ) /\ ( ~P A i^i Fin ) ~<_ _om ) -> ( ( ~P A i^i Fin ) \ { (/) } ) ~<_ _om )
47 13 45 46 syl2anc 
 |-  ( ( ( A e. B /\ _om e. _V ) /\ f : A -1-1-> _om ) -> ( ( ~P A i^i Fin ) \ { (/) } ) ~<_ _om )
48 ondomen 
 |-  ( ( _om e. On /\ ( ( ~P A i^i Fin ) \ { (/) } ) ~<_ _om ) -> ( ( ~P A i^i Fin ) \ { (/) } ) e. dom card )
49 6 47 48 syl2anc 
 |-  ( ( ( A e. B /\ _om e. _V ) /\ f : A -1-1-> _om ) -> ( ( ~P A i^i Fin ) \ { (/) } ) e. dom card )
50 eqid 
 |-  ( y e. ( ( ~P A i^i Fin ) \ { (/) } ) |-> |^| y ) = ( y e. ( ( ~P A i^i Fin ) \ { (/) } ) |-> |^| y )
51 50 fifo 
 |-  ( A e. B -> ( y e. ( ( ~P A i^i Fin ) \ { (/) } ) |-> |^| y ) : ( ( ~P A i^i Fin ) \ { (/) } ) -onto-> ( fi ` A ) )
52 51 ad2antrr 
 |-  ( ( ( A e. B /\ _om e. _V ) /\ f : A -1-1-> _om ) -> ( y e. ( ( ~P A i^i Fin ) \ { (/) } ) |-> |^| y ) : ( ( ~P A i^i Fin ) \ { (/) } ) -onto-> ( fi ` A ) )
53 fodomnum 
 |-  ( ( ( ~P A i^i Fin ) \ { (/) } ) e. dom card -> ( ( y e. ( ( ~P A i^i Fin ) \ { (/) } ) |-> |^| y ) : ( ( ~P A i^i Fin ) \ { (/) } ) -onto-> ( fi ` A ) -> ( fi ` A ) ~<_ ( ( ~P A i^i Fin ) \ { (/) } ) ) )
54 49 52 53 sylc 
 |-  ( ( ( A e. B /\ _om e. _V ) /\ f : A -1-1-> _om ) -> ( fi ` A ) ~<_ ( ( ~P A i^i Fin ) \ { (/) } ) )
55 domtr 
 |-  ( ( ( fi ` A ) ~<_ ( ( ~P A i^i Fin ) \ { (/) } ) /\ ( ( ~P A i^i Fin ) \ { (/) } ) ~<_ _om ) -> ( fi ` A ) ~<_ _om )
56 54 47 55 syl2anc 
 |-  ( ( ( A e. B /\ _om e. _V ) /\ f : A -1-1-> _om ) -> ( fi ` A ) ~<_ _om )
57 56 ex 
 |-  ( ( A e. B /\ _om e. _V ) -> ( f : A -1-1-> _om -> ( fi ` A ) ~<_ _om ) )
58 57 exlimdv 
 |-  ( ( A e. B /\ _om e. _V ) -> ( E. f f : A -1-1-> _om -> ( fi ` A ) ~<_ _om ) )
59 4 58 sylan2 
 |-  ( ( A e. B /\ A ~<_ _om ) -> ( E. f f : A -1-1-> _om -> ( fi ` A ) ~<_ _om ) )
60 2 59 mpd 
 |-  ( ( A e. B /\ A ~<_ _om ) -> ( fi ` A ) ~<_ _om )
61 60 ex 
 |-  ( A e. B -> ( A ~<_ _om -> ( fi ` A ) ~<_ _om ) )
62 fvex 
 |-  ( fi ` A ) e. _V
63 ssfii 
 |-  ( A e. B -> A C_ ( fi ` A ) )
64 ssdomg 
 |-  ( ( fi ` A ) e. _V -> ( A C_ ( fi ` A ) -> A ~<_ ( fi ` A ) ) )
65 62 63 64 mpsyl 
 |-  ( A e. B -> A ~<_ ( fi ` A ) )
66 domtr 
 |-  ( ( A ~<_ ( fi ` A ) /\ ( fi ` A ) ~<_ _om ) -> A ~<_ _om )
67 66 ex 
 |-  ( A ~<_ ( fi ` A ) -> ( ( fi ` A ) ~<_ _om -> A ~<_ _om ) )
68 65 67 syl 
 |-  ( A e. B -> ( ( fi ` A ) ~<_ _om -> A ~<_ _om ) )
69 61 68 impbid 
 |-  ( A e. B -> ( A ~<_ _om <-> ( fi ` A ) ~<_ _om ) )