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 frnd ⊢ ( 𝑓 : 𝐴 –1-1→ ω → ran 𝑓 ⊆ ω )
26 25 adantl ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ ω ∈ V ) ∧ 𝑓 : 𝐴 –1-1→ ω ) → ran 𝑓 ⊆ ω )
27 26 sspwd ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ ω ∈ V ) ∧ 𝑓 : 𝐴 –1-1→ ω ) → 𝒫 ran 𝑓 ⊆ 𝒫 ω )
28 27 ssrind ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ ω ∈ V ) ∧ 𝑓 : 𝐴 –1-1→ ω ) → ( 𝒫 ran 𝑓 ∩ Fin ) ⊆ ( 𝒫 ω ∩ Fin ) )
29 ssdomg ⊢ ( ( 𝒫 ω ∩ Fin ) ∈ V → ( ( 𝒫 ran 𝑓 ∩ Fin ) ⊆ ( 𝒫 ω ∩ Fin ) → ( 𝒫 ran 𝑓 ∩ Fin ) ≼ ( 𝒫 ω ∩ Fin ) ) )
30 23 28 29 sylc ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ ω ∈ V ) ∧ 𝑓 : 𝐴 –1-1→ ω ) → ( 𝒫 ran 𝑓 ∩ Fin ) ≼ ( 𝒫 ω ∩ Fin ) )
31 sneq ⊢ ( 𝑓 = 𝑧 → { 𝑓 } = { 𝑧 } )
32 pweq ⊢ ( 𝑓 = 𝑧 → 𝒫 𝑓 = 𝒫 𝑧 )
33 31 32 xpeq12d ⊢ ( 𝑓 = 𝑧 → ( { 𝑓 } × 𝒫 𝑓 ) = ( { 𝑧 } × 𝒫 𝑧 ) )
34 33 cbviunv ⊢ ∪ 𝑓 ∈ 𝑥 ( { 𝑓 } × 𝒫 𝑓 ) = ∪ 𝑧 ∈ 𝑥 ( { 𝑧 } × 𝒫 𝑧 )
35 iuneq1 ⊢ ( 𝑥 = 𝑦 → ∪ 𝑧 ∈ 𝑥 ( { 𝑧 } × 𝒫 𝑧 ) = ∪ 𝑧 ∈ 𝑦 ( { 𝑧 } × 𝒫 𝑧 ) )
36 34 35 syl5eq ⊢ ( 𝑥 = 𝑦 → ∪ 𝑓 ∈ 𝑥 ( { 𝑓 } × 𝒫 𝑓 ) = ∪ 𝑧 ∈ 𝑦 ( { 𝑧 } × 𝒫 𝑧 ) )
37 36 fveq2d ⊢ ( 𝑥 = 𝑦 → ( card ‘ ∪ 𝑓 ∈ 𝑥 ( { 𝑓 } × 𝒫 𝑓 ) ) = ( card ‘ ∪ 𝑧 ∈ 𝑦 ( { 𝑧 } × 𝒫 𝑧 ) ) )
38 37 cbvmptv ⊢ ( 𝑥 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑥 ( { 𝑓 } × 𝒫 𝑓 ) ) ) = ( 𝑦 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑧 ∈ 𝑦 ( { 𝑧 } × 𝒫 𝑧 ) ) )
39 38 ackbij1 ⊢ ( 𝑥 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑥 ( { 𝑓 } × 𝒫 𝑓 ) ) ) : ( 𝒫 ω ∩ Fin ) –1-1-onto→ ω
40 f1oeng ⊢ ( ( ( 𝒫 ω ∩ Fin ) ∈ V ∧ ( 𝑥 ∈ ( 𝒫 ω ∩ Fin ) ↦ ( card ‘ ∪ 𝑓 ∈ 𝑥 ( { 𝑓 } × 𝒫 𝑓 ) ) ) : ( 𝒫 ω ∩ Fin ) –1-1-onto→ ω ) → ( 𝒫 ω ∩ Fin ) ≈ ω )
41 23 39 40 sylancl ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ ω ∈ V ) ∧ 𝑓 : 𝐴 –1-1→ ω ) → ( 𝒫 ω ∩ Fin ) ≈ ω )
42 domentr ⊢ ( ( ( 𝒫 ran 𝑓 ∩ Fin ) ≼ ( 𝒫 ω ∩ Fin ) ∧ ( 𝒫 ω ∩ Fin ) ≈ ω ) → ( 𝒫 ran 𝑓 ∩ Fin ) ≼ ω )
43 30 41 42 syl2anc ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ ω ∈ V ) ∧ 𝑓 : 𝐴 –1-1→ ω ) → ( 𝒫 ran 𝑓 ∩ Fin ) ≼ ω )
44 endomtr ⊢ ( ( ( 𝒫 𝐴 ∩ Fin ) ≈ ( 𝒫 ran 𝑓 ∩ Fin ) ∧ ( 𝒫 ran 𝑓 ∩ Fin ) ≼ ω ) → ( 𝒫 𝐴 ∩ Fin ) ≼ ω )
45 19 43 44 syl2anc ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ ω ∈ V ) ∧ 𝑓 : 𝐴 –1-1→ ω ) → ( 𝒫 𝐴 ∩ Fin ) ≼ ω )
46 domtr ⊢ ( ( ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ≼ ( 𝒫 𝐴 ∩ Fin ) ∧ ( 𝒫 𝐴 ∩ Fin ) ≼ ω ) → ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ≼ ω )
47 13 45 46 syl2anc ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ ω ∈ V ) ∧ 𝑓 : 𝐴 –1-1→ ω ) → ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ≼ ω )
48 ondomen ⊢ ( ( ω ∈ On ∧ ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ≼ ω ) → ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ∈ dom card )
49 6 47 48 syl2anc ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ ω ∈ V ) ∧ 𝑓 : 𝐴 –1-1→ ω ) → ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ∈ dom card )
50 eqid ⊢ ( 𝑦 ∈ ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ↦ ∩ 𝑦 ) = ( 𝑦 ∈ ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ↦ ∩ 𝑦 )
51 50 fifo ⊢ ( 𝐴 ∈ 𝐵 → ( 𝑦 ∈ ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ↦ ∩ 𝑦 ) : ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) –onto→ ( fi ‘ 𝐴 ) )
52 51 ad2antrr ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ ω ∈ V ) ∧ 𝑓 : 𝐴 –1-1→ ω ) → ( 𝑦 ∈ ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ↦ ∩ 𝑦 ) : ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) –onto→ ( fi ‘ 𝐴 ) )
53 fodomnum ⊢ ( ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ∈ dom card → ( ( 𝑦 ∈ ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ↦ ∩ 𝑦 ) : ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) –onto→ ( fi ‘ 𝐴 ) → ( fi ‘ 𝐴 ) ≼ ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ) )
54 49 52 53 sylc ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ ω ∈ V ) ∧ 𝑓 : 𝐴 –1-1→ ω ) → ( fi ‘ 𝐴 ) ≼ ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) )
55 domtr ⊢ ( ( ( fi ‘ 𝐴 ) ≼ ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ∧ ( ( 𝒫 𝐴 ∩ Fin ) ∖ { ∅ } ) ≼ ω ) → ( fi ‘ 𝐴 ) ≼ ω )
56 54 47 55 syl2anc ⊢ ( ( ( 𝐴 ∈ 𝐵 ∧ ω ∈ V ) ∧ 𝑓 : 𝐴 –1-1→ ω ) → ( fi ‘ 𝐴 ) ≼ ω )
57 56 ex ⊢ ( ( 𝐴 ∈ 𝐵 ∧ ω ∈ V ) → ( 𝑓 : 𝐴 –1-1→ ω → ( fi ‘ 𝐴 ) ≼ ω ) )
58 57 exlimdv ⊢ ( ( 𝐴 ∈ 𝐵 ∧ ω ∈ V ) → ( ∃ 𝑓 𝑓 : 𝐴 –1-1→ ω → ( fi ‘ 𝐴 ) ≼ ω ) )
59 4 58 sylan2 ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐴 ≼ ω ) → ( ∃ 𝑓 𝑓 : 𝐴 –1-1→ ω → ( fi ‘ 𝐴 ) ≼ ω ) )
60 2 59 mpd ⊢ ( ( 𝐴 ∈ 𝐵 ∧ 𝐴 ≼ ω ) → ( fi ‘ 𝐴 ) ≼ ω )
61 60 ex ⊢ ( 𝐴 ∈ 𝐵 → ( 𝐴 ≼ ω → ( fi ‘ 𝐴 ) ≼ ω ) )
62 fvex ⊢ ( fi ‘ 𝐴 ) ∈ V
63 ssfii ⊢ ( 𝐴 ∈ 𝐵 → 𝐴 ⊆ ( fi ‘ 𝐴 ) )
64 ssdomg ⊢ ( ( fi ‘ 𝐴 ) ∈ V → ( 𝐴 ⊆ ( fi ‘ 𝐴 ) → 𝐴 ≼ ( fi ‘ 𝐴 ) ) )
65 62 63 64 mpsyl ⊢ ( 𝐴 ∈ 𝐵 → 𝐴 ≼ ( fi ‘ 𝐴 ) )
66 domtr ⊢ ( ( 𝐴 ≼ ( fi ‘ 𝐴 ) ∧ ( fi ‘ 𝐴 ) ≼ ω ) → 𝐴 ≼ ω )
67 66 ex ⊢ ( 𝐴 ≼ ( fi ‘ 𝐴 ) → ( ( fi ‘ 𝐴 ) ≼ ω → 𝐴 ≼ ω ) )
68 65 67 syl ⊢ ( 𝐴 ∈ 𝐵 → ( ( fi ‘ 𝐴 ) ≼ ω → 𝐴 ≼ ω ) )
69 61 68 impbid ⊢ ( 𝐴 ∈ 𝐵 → ( 𝐴 ≼ ω ↔ ( fi ‘ 𝐴 ) ≼ ω ) )