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 ( 𝐴 ∈ 𝐵 → ( 𝐴 ≼ ω ↔ ( fi ‘ 𝐴 ) ≼ ω ) )

Proof

Step Hyp Ref Expression
1 brdomi ⊢ ( 𝐴 ≼ ω → ∃ 𝑓 𝑓 : 𝐴 –1-1→ ω )
2 1 adantl ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐴 ≼ ω ) → ∃ 𝑓 𝑓 : 𝐴 –1-1→ ω )
3 reldom ⊢ Rel ≼
4 3 brrelex2i ⊢ ( 𝐴 ≼ ω → ω ∈ V )
5 omelon2 ⊢ ( ω ∈ V → ω ∈ On )
6 5 ad2antlr ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ ω ∈ V ) ∧ 𝑓 : 𝐴 –1-1→ ω ) → ω ∈ On )
7 pwexg ⊢ ( 𝐴 ∈ 𝐵 → 𝒫 𝐴 ∈ V )
8 7 ad2antrr ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ ω ∈ V ) ∧ 𝑓 : 𝐴 –1-1→ ω ) → 𝒫 𝐴 ∈ V )
9 inex1g ⊢ ( 𝒫 𝐴 ∈ V → ( 𝒫 𝐴 ∩ Fin ) ∈ V )
10 8 9 syl ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ ω ∈ V ) ∧ 𝑓 : 𝐴 –1-1→ ω ) → ( 𝒫 𝐴 ∩ Fin ) ∈ V )
11 difss ⊢ ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ⊆ ( 𝒫 𝐴 ∩ Fin )
12 ssdomg ⊢ ( ( 𝒫 𝐴 ∩ Fin ) ∈ V → ( ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ⊆ ( 𝒫 𝐴 ∩ Fin ) → ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ≼ ( 𝒫 𝐴 ∩ Fin ) ) )
13 10 11 12 mpisyl ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ ω ∈ V ) ∧ 𝑓 : 𝐴 –1-1→ ω ) → ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ≼ ( 𝒫 𝐴 ∩ Fin ) )
14 f1f1orn ⊢ ( 𝑓 : 𝐴 –1-1→ ω → 𝑓 : 𝐴 –1-1-onto→ ran 𝑓 )
15 14 adantl ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ ω ∈ V ) ∧ 𝑓 : 𝐴 –1-1→ ω ) → 𝑓 : 𝐴 –1-1-onto→ ran 𝑓 )
16 f1opwfi ⊢ ( 𝑓 : 𝐴 –1-1-onto→ ran 𝑓 → ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝑓 “ 𝑥 ) ) : ( 𝒫 𝐴 ∩ Fin ) –1-1-onto→ ( 𝒫 ran 𝑓 ∩ Fin ) )
17 15 16 syl ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ ω ∈ V ) ∧ 𝑓 : 𝐴 –1-1→ ω ) → ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝑓 “ 𝑥 ) ) : ( 𝒫 𝐴 ∩ Fin ) –1-1-onto→ ( 𝒫 ran 𝑓 ∩ Fin ) )
18 f1oeng ⊢ ( ( ( 𝒫 𝐴 ∩ Fin ) ∈ V ∧ ( 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ↦ ( 𝑓 “ 𝑥 ) ) : ( 𝒫 𝐴 ∩ Fin ) –1-1-onto→ ( 𝒫 ran 𝑓 ∩ Fin ) ) → ( 𝒫 𝐴 ∩ Fin ) ≈ ( 𝒫 ran 𝑓 ∩ Fin ) )
19 10 17 18 syl2anc ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ ω ∈ V ) ∧ 𝑓 : 𝐴 –1-1→ ω ) → ( 𝒫 𝐴 ∩ Fin ) ≈ ( 𝒫 ran 𝑓 ∩ Fin ) )
20 pwexg ⊢ ( ω ∈ V → 𝒫 ω ∈ V )
21 20 ad2antlr ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ ω ∈ V ) ∧ 𝑓 : 𝐴 –1-1→ ω ) → 𝒫 ω ∈ V )
22 inex1g ⊢ ( 𝒫 ω ∈ V → ( 𝒫 ω ∩ Fin ) ∈ V )
23 21 22 syl ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ ω ∈ V ) ∧ 𝑓 : 𝐴 –1-1→ ω ) → ( 𝒫 ω ∩ Fin ) ∈ V )
24 f1f ⊢ ( 𝑓 : 𝐴 –1-1→ ω → 𝑓 : 𝐴 ⟶ ω )
25 24 adantl ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ ω ∈ V ) ∧ 𝑓 : 𝐴 –1-1→ ω ) → 𝑓 : 𝐴 ⟶ ω )
26 25 frnd ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ ω ∈ V ) ∧ 𝑓 : 𝐴 –1-1→ ω ) → ran 𝑓 ⊆ ω )
27 sspwb ⊢ ( ran 𝑓 ⊆ ω ↔ 𝒫 ran 𝑓 ⊆ 𝒫 ω )
28 26 27 sylib ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ ω ∈ V ) ∧ 𝑓 : 𝐴 –1-1→ ω ) → 𝒫 ran 𝑓 ⊆ 𝒫 ω )
29 28 ssrind ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ ω ∈ V ) ∧ 𝑓 : 𝐴 –1-1→ ω ) → ( 𝒫 ran 𝑓 ∩ Fin ) ⊆ ( 𝒫 ω ∩ Fin ) )
30 ssdomg ⊢ ( ( 𝒫 ω ∩ Fin ) ∈ V → ( ( 𝒫 ran 𝑓 ∩ Fin ) ⊆ ( 𝒫 ω ∩ Fin ) → ( 𝒫 ran 𝑓 ∩ Fin ) ≼ ( 𝒫 ω ∩ Fin ) ) )
31 23 29 30 sylc ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ ω ∈ V ) ∧ 𝑓 : 𝐴 –1-1→ ω ) → ( 𝒫 ran 𝑓 ∩ Fin ) ≼ ( 𝒫 ω ∩ Fin ) )
32 sneq ⊢ ( 𝑓 = 𝑧 → { 𝑓 } = { 𝑧 } )
33 pweq ⊢ ( 𝑓 = 𝑧 → 𝒫 𝑓 = 𝒫 𝑧 )
34 32 33 xpeq12d ⊢ ( 𝑓 = 𝑧 → ( { 𝑓 } × 𝒫 𝑓 ) = ( { 𝑧 } × 𝒫 𝑧 ) )
35 34 cbviunv ⊢ ∪ 𝑓 ∈ 𝑥 ( { 𝑓 } × 𝒫 𝑓 ) = ∪ 𝑧 ∈ 𝑥 ( { 𝑧 } × 𝒫 𝑧 )
36 iuneq1 ⊢ ( 𝑥 = 𝑦 → ∪ 𝑧 ∈ 𝑥 ( { 𝑧 } × 𝒫 𝑧 ) = ∪ 𝑧 ∈ 𝑦 ( { 𝑧 } × 𝒫 𝑧 ) )
37 35 36 syl5eq ⊢ ( 𝑥 = 𝑦 → ∪ 𝑓 ∈ 𝑥 ( { 𝑓 } × 𝒫 𝑓 ) = ∪ 𝑧 ∈ 𝑦 ( { 𝑧 } × 𝒫 𝑧 ) )
38 37 fveq2d ⊢ ( 𝑥 = 𝑦 → ( card ‘ ∪ 𝑓 ∈ 𝑥 ( { 𝑓 } × 𝒫 𝑓 ) ) = ( card ‘ ∪ 𝑧 ∈ 𝑦 ( { 𝑧 } × 𝒫 𝑧 ) ) )
39 38 cbvmptv ⊢ ( 𝑥 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑥 ( { 𝑓 } × 𝒫 𝑓 ) ) ) = ( 𝑦 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑧 ∈ 𝑦 ( { 𝑧 } × 𝒫 𝑧 ) ) )
40 39 ackbij1 ⊢ ( 𝑥 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑥 ( { 𝑓 } × 𝒫 𝑓 ) ) ) : ( 𝒫 ω ∩ Fin ) –1-1-onto→ ω
41 f1oeng ⊢ ( ( ( 𝒫 ω ∩ Fin ) ∈ V ∧ ( 𝑥 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑥 ( { 𝑓 } × 𝒫 𝑓 ) ) ) : ( 𝒫 ω ∩ Fin ) –1-1-onto→ ω ) → ( 𝒫 ω ∩ Fin ) ≈ ω )
42 23 40 41 sylancl ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ ω ∈ V ) ∧ 𝑓 : 𝐴 –1-1→ ω ) → ( 𝒫 ω ∩ Fin ) ≈ ω )
43 domentr ⊢ ( ( ( 𝒫 ran 𝑓 ∩ Fin ) ≼ ( 𝒫 ω ∩ Fin ) ∧ ( 𝒫 ω ∩ Fin ) ≈ ω ) → ( 𝒫 ran 𝑓 ∩ Fin ) ≼ ω )
44 31 42 43 syl2anc ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ ω ∈ V ) ∧ 𝑓 : 𝐴 –1-1→ ω ) → ( 𝒫 ran 𝑓 ∩ Fin ) ≼ ω )
45 endomtr ⊢ ( ( ( 𝒫 𝐴 ∩ Fin ) ≈ ( 𝒫 ran 𝑓 ∩ Fin ) ∧ ( 𝒫 ran 𝑓 ∩ Fin ) ≼ ω ) → ( 𝒫 𝐴 ∩ Fin ) ≼ ω )
46 19 44 45 syl2anc ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ ω ∈ V ) ∧ 𝑓 : 𝐴 –1-1→ ω ) → ( 𝒫 𝐴 ∩ Fin ) ≼ ω )
47 domtr ⊢ ( ( ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ≼ ( 𝒫 𝐴 ∩ Fin ) ∧ ( 𝒫 𝐴 ∩ Fin ) ≼ ω ) → ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ≼ ω )
48 13 46 47 syl2anc ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ ω ∈ V ) ∧ 𝑓 : 𝐴 –1-1→ ω ) → ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ≼ ω )
49 ondomen ⊢ ( ( ω ∈ On ∧ ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ≼ ω ) → ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ∈ dom card )
50 6 48 49 syl2anc ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ ω ∈ V ) ∧ 𝑓 : 𝐴 –1-1→ ω ) → ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ∈ dom card )
51 eqid ⊢ ( 𝑦 ∈ ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ↦ ∩ 𝑦 ) = ( 𝑦 ∈ ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ↦ ∩ 𝑦 )
52 51 fifo ⊢ ( 𝐴 ∈ 𝐵 → ( 𝑦 ∈ ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ↦ ∩ 𝑦 ) : ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) –onto→ ( fi ‘ 𝐴 ) )
53 52 ad2antrr ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ ω ∈ V ) ∧ 𝑓 : 𝐴 –1-1→ ω ) → ( 𝑦 ∈ ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ↦ ∩ 𝑦 ) : ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) –onto→ ( fi ‘ 𝐴 ) )
54 fodomnum ⊢ ( ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ∈ dom card → ( ( 𝑦 ∈ ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ↦ ∩ 𝑦 ) : ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) –onto→ ( fi ‘ 𝐴 ) → ( fi ‘ 𝐴 ) ≼ ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ) )
55 50 53 54 sylc ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ ω ∈ V ) ∧ 𝑓 : 𝐴 –1-1→ ω ) → ( fi ‘ 𝐴 ) ≼ ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) )
56 domtr ⊢ ( ( ( fi ‘ 𝐴 ) ≼ ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ∧ ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ≼ ω ) → ( fi ‘ 𝐴 ) ≼ ω )
57 55 48 56 syl2anc ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ ω ∈ V ) ∧ 𝑓 : 𝐴 –1-1→ ω ) → ( fi ‘ 𝐴 ) ≼ ω )
58 57 ex ⊢ ( ( 𝐴 ∈ 𝐵 ∧ ω ∈ V ) → ( 𝑓 : 𝐴 –1-1→ ω → ( fi ‘ 𝐴 ) ≼ ω ) )
59 58 exlimdv ⊢ ( ( 𝐴 ∈ 𝐵 ∧ ω ∈ V ) → ( ∃ 𝑓 𝑓 : 𝐴 –1-1→ ω → ( fi ‘ 𝐴 ) ≼ ω ) )
60 4 59 sylan2 ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐴 ≼ ω ) → ( ∃ 𝑓 𝑓 : 𝐴 –1-1→ ω → ( fi ‘ 𝐴 ) ≼ ω ) )
61 2 60 mpd ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐴 ≼ ω ) → ( fi ‘ 𝐴 ) ≼ ω )
62 61 ex ⊢ ( 𝐴 ∈ 𝐵 → ( 𝐴 ≼ ω → ( fi ‘ 𝐴 ) ≼ ω ) )
63 fvex ⊢ ( fi ‘ 𝐴 ) ∈ V
64 ssfii ⊢ ( 𝐴 ∈ 𝐵 → 𝐴 ⊆ ( fi ‘ 𝐴 ) )
65 ssdomg ⊢ ( ( fi ‘ 𝐴 ) ∈ V → ( 𝐴 ⊆ ( fi ‘ 𝐴 ) → 𝐴 ≼ ( fi ‘ 𝐴 ) ) )
66 63 64 65 mpsyl ⊢ ( 𝐴 ∈ 𝐵 → 𝐴 ≼ ( fi ‘ 𝐴 ) )
67 domtr ⊢ ( ( 𝐴 ≼ ( fi ‘ 𝐴 ) ∧ ( fi ‘ 𝐴 ) ≼ ω ) → 𝐴 ≼ ω )
68 67 ex ⊢ ( 𝐴 ≼ ( fi ‘ 𝐴 ) → ( ( fi ‘ 𝐴 ) ≼ ω → 𝐴 ≼ ω ) )
69 66 68 syl ⊢ ( 𝐴 ∈ 𝐵 → ( ( fi ‘ 𝐴 ) ≼ ω → 𝐴 ≼ ω ) )
70 62 69 impbid ⊢ ( 𝐴 ∈ 𝐵 → ( 𝐴 ≼ ω ↔ ( fi ‘ 𝐴 ) ≼ ω ) )