Metamath Proof Explorer

Theorem cfss

Description: There is a cofinal subset of A of cardinality ( cfA ) . (Contributed by Mario Carneiro, 24-Jun-2013)

Ref Expression
Hypothesis cfss.1 ⊢ 𝐴 ∈ V
Assertion cfss ( Lim 𝐴 → ∃ 𝑥 ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ( cf ‘ 𝐴 ) ∧ ∪ 𝑥 = 𝐴 ) )

Proof

Step Hyp Ref Expression
1 cfss.1 ⊢ 𝐴 ∈ V
2 1 cflim3 ⊢ ( Lim 𝐴 → ( cf ‘ 𝐴 ) = ∩ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } ( card ‘ 𝑥 ) )
3 fvex ⊢ ( card ‘ 𝑥 ) ∈ V
4 3 dfiin2 ⊢ ∩ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } ( card ‘ 𝑥 ) = ∩ { 𝑦 ∣ ∃ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } 𝑦 = ( card ‘ 𝑥 ) }
5 cardon ⊢ ( card ‘ 𝑥 ) ∈ On
6 eleq1 ⊢ ( 𝑦 = ( card ‘ 𝑥 ) → ( 𝑦 ∈ On ↔ ( card ‘ 𝑥 ) ∈ On ) )
7 5 6 mpbiri ⊢ ( 𝑦 = ( card ‘ 𝑥 ) → 𝑦 ∈ On )
8 7 rexlimivw ⊢ ( ∃ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } 𝑦 = ( card ‘ 𝑥 ) → 𝑦 ∈ On )
9 8 abssi ⊢ { 𝑦 ∣ ∃ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } 𝑦 = ( card ‘ 𝑥 ) } ⊆ On
10 limuni ⊢ ( Lim 𝐴 → 𝐴 = ∪ 𝐴 )
11 10 eqcomd ⊢ ( Lim 𝐴 → ∪ 𝐴 = 𝐴 )
12 fveq2 ⊢ ( 𝑥 = 𝐴 → ( card ‘ 𝑥 ) = ( card ‘ 𝐴 ) )
13 12 eqcomd ⊢ ( 𝑥 = 𝐴 → ( card ‘ 𝐴 ) = ( card ‘ 𝑥 ) )
14 13 biantrud ⊢ ( 𝑥 = 𝐴 → ( ∪ 𝐴 = 𝐴 ↔ ( ∪ 𝐴 = 𝐴 ∧ ( card ‘ 𝐴 ) = ( card ‘ 𝑥 ) ) ) )
15 unieq ⊢ ( 𝑥 = 𝐴 → ∪ 𝑥 = ∪ 𝐴 )
16 15 eqeq1d ⊢ ( 𝑥 = 𝐴 → ( ∪ 𝑥 = 𝐴 ↔ ∪ 𝐴 = 𝐴 ) )
17 1 pwid ⊢ 𝐴 ∈ 𝒫 𝐴
18 eleq1 ⊢ ( 𝑥 = 𝐴 → ( 𝑥 ∈ 𝒫 𝐴 ↔ 𝐴 ∈ 𝒫 𝐴 ) )
19 17 18 mpbiri ⊢ ( 𝑥 = 𝐴 → 𝑥 ∈ 𝒫 𝐴 )
20 19 biantrurd ⊢ ( 𝑥 = 𝐴 → ( ∪ 𝑥 = 𝐴 ↔ ( 𝑥 ∈ 𝒫 𝐴 ∧ ∪ 𝑥 = 𝐴 ) ) )
21 16 20 bitr3d ⊢ ( 𝑥 = 𝐴 → ( ∪ 𝐴 = 𝐴 ↔ ( 𝑥 ∈ 𝒫 𝐴 ∧ ∪ 𝑥 = 𝐴 ) ) )
22 21 anbi1d ⊢ ( 𝑥 = 𝐴 → ( ( ∪ 𝐴 = 𝐴 ∧ ( card ‘ 𝐴 ) = ( card ‘ 𝑥 ) ) ↔ ( ( 𝑥 ∈ 𝒫 𝐴 ∧ ∪ 𝑥 = 𝐴 ) ∧ ( card ‘ 𝐴 ) = ( card ‘ 𝑥 ) ) ) )
23 14 22 bitr2d ⊢ ( 𝑥 = 𝐴 → ( ( ( 𝑥 ∈ 𝒫 𝐴 ∧ ∪ 𝑥 = 𝐴 ) ∧ ( card ‘ 𝐴 ) = ( card ‘ 𝑥 ) ) ↔ ∪ 𝐴 = 𝐴 ) )
24 1 23 spcev ⊢ ( ∪ 𝐴 = 𝐴 → ∃ 𝑥 ( ( 𝑥 ∈ 𝒫 𝐴 ∧ ∪ 𝑥 = 𝐴 ) ∧ ( card ‘ 𝐴 ) = ( card ‘ 𝑥 ) ) )
25 11 24 syl ⊢ ( Lim 𝐴 → ∃ 𝑥 ( ( 𝑥 ∈ 𝒫 𝐴 ∧ ∪ 𝑥 = 𝐴 ) ∧ ( card ‘ 𝐴 ) = ( card ‘ 𝑥 ) ) )
26 df-rex ⊢ ( ∃ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } ( card ‘ 𝐴 ) = ( card ‘ 𝑥 ) ↔ ∃ 𝑥 ( 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } ∧ ( card ‘ 𝐴 ) = ( card ‘ 𝑥 ) ) )
27 rabid ⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } ↔ ( 𝑥 ∈ 𝒫 𝐴 ∧ ∪ 𝑥 = 𝐴 ) )
28 27 anbi1i ⊢ ( ( 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } ∧ ( card ‘ 𝐴 ) = ( card ‘ 𝑥 ) ) ↔ ( ( 𝑥 ∈ 𝒫 𝐴 ∧ ∪ 𝑥 = 𝐴 ) ∧ ( card ‘ 𝐴 ) = ( card ‘ 𝑥 ) ) )
29 28 exbii ⊢ ( ∃ 𝑥 ( 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } ∧ ( card ‘ 𝐴 ) = ( card ‘ 𝑥 ) ) ↔ ∃ 𝑥 ( ( 𝑥 ∈ 𝒫 𝐴 ∧ ∪ 𝑥 = 𝐴 ) ∧ ( card ‘ 𝐴 ) = ( card ‘ 𝑥 ) ) )
30 26 29 bitri ⊢ ( ∃ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } ( card ‘ 𝐴 ) = ( card ‘ 𝑥 ) ↔ ∃ 𝑥 ( ( 𝑥 ∈ 𝒫 𝐴 ∧ ∪ 𝑥 = 𝐴 ) ∧ ( card ‘ 𝐴 ) = ( card ‘ 𝑥 ) ) )
31 25 30 sylibr ⊢ ( Lim 𝐴 → ∃ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } ( card ‘ 𝐴 ) = ( card ‘ 𝑥 ) )
32 fvex ⊢ ( card ‘ 𝐴 ) ∈ V
33 eqeq1 ⊢ ( 𝑦 = ( card ‘ 𝐴 ) → ( 𝑦 = ( card ‘ 𝑥 ) ↔ ( card ‘ 𝐴 ) = ( card ‘ 𝑥 ) ) )
34 33 rexbidv ⊢ ( 𝑦 = ( card ‘ 𝐴 ) → ( ∃ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } 𝑦 = ( card ‘ 𝑥 ) ↔ ∃ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } ( card ‘ 𝐴 ) = ( card ‘ 𝑥 ) ) )
35 32 34 spcev ⊢ ( ∃ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } ( card ‘ 𝐴 ) = ( card ‘ 𝑥 ) → ∃ 𝑦 ∃ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } 𝑦 = ( card ‘ 𝑥 ) )
36 31 35 syl ⊢ ( Lim 𝐴 → ∃ 𝑦 ∃ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } 𝑦 = ( card ‘ 𝑥 ) )
37 abn0 ⊢ ( { 𝑦 ∣ ∃ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } 𝑦 = ( card ‘ 𝑥 ) } ≠ ∅ ↔ ∃ 𝑦 ∃ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } 𝑦 = ( card ‘ 𝑥 ) )
38 36 37 sylibr ⊢ ( Lim 𝐴 → { 𝑦 ∣ ∃ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } 𝑦 = ( card ‘ 𝑥 ) } ≠ ∅ )
39 onint ⊢ ( ( { 𝑦 ∣ ∃ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } 𝑦 = ( card ‘ 𝑥 ) } ⊆ On ∧ { 𝑦 ∣ ∃ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } 𝑦 = ( card ‘ 𝑥 ) } ≠ ∅ ) → ∩ { 𝑦 ∣ ∃ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } 𝑦 = ( card ‘ 𝑥 ) } ∈ { 𝑦 ∣ ∃ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } 𝑦 = ( card ‘ 𝑥 ) } )
40 9 38 39 sylancr ⊢ ( Lim 𝐴 → ∩ { 𝑦 ∣ ∃ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } 𝑦 = ( card ‘ 𝑥 ) } ∈ { 𝑦 ∣ ∃ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } 𝑦 = ( card ‘ 𝑥 ) } )
41 4 40 eqeltrid ⊢ ( Lim 𝐴 → ∩ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } ( card ‘ 𝑥 ) ∈ { 𝑦 ∣ ∃ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } 𝑦 = ( card ‘ 𝑥 ) } )
42 2 41 eqeltrd ⊢ ( Lim 𝐴 → ( cf ‘ 𝐴 ) ∈ { 𝑦 ∣ ∃ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } 𝑦 = ( card ‘ 𝑥 ) } )
43 fvex ⊢ ( cf ‘ 𝐴 ) ∈ V
44 eqeq1 ⊢ ( 𝑦 = ( cf ‘ 𝐴 ) → ( 𝑦 = ( card ‘ 𝑥 ) ↔ ( cf ‘ 𝐴 ) = ( card ‘ 𝑥 ) ) )
45 44 rexbidv ⊢ ( 𝑦 = ( cf ‘ 𝐴 ) → ( ∃ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } 𝑦 = ( card ‘ 𝑥 ) ↔ ∃ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } ( cf ‘ 𝐴 ) = ( card ‘ 𝑥 ) ) )
46 43 45 elab ⊢ ( ( cf ‘ 𝐴 ) ∈ { 𝑦 ∣ ∃ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } 𝑦 = ( card ‘ 𝑥 ) } ↔ ∃ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } ( cf ‘ 𝐴 ) = ( card ‘ 𝑥 ) )
47 42 46 sylib ⊢ ( Lim 𝐴 → ∃ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } ( cf ‘ 𝐴 ) = ( card ‘ 𝑥 ) )
48 df-rex ⊢ ( ∃ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } ( cf ‘ 𝐴 ) = ( card ‘ 𝑥 ) ↔ ∃ 𝑥 ( 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } ∧ ( cf ‘ 𝐴 ) = ( card ‘ 𝑥 ) ) )
49 47 48 sylib ⊢ ( Lim 𝐴 → ∃ 𝑥 ( 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } ∧ ( cf ‘ 𝐴 ) = ( card ‘ 𝑥 ) ) )
50 simprl ⊢ ( ( Lim 𝐴 ∧ ( 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } ∧ ( cf ‘ 𝐴 ) = ( card ‘ 𝑥 ) ) ) → 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } )
51 50 27 sylib ⊢ ( ( Lim 𝐴 ∧ ( 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } ∧ ( cf ‘ 𝐴 ) = ( card ‘ 𝑥 ) ) ) → ( 𝑥 ∈ 𝒫 𝐴 ∧ ∪ 𝑥 = 𝐴 ) )
52 51 simpld ⊢ ( ( Lim 𝐴 ∧ ( 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } ∧ ( cf ‘ 𝐴 ) = ( card ‘ 𝑥 ) ) ) → 𝑥 ∈ 𝒫 𝐴 )
53 52 elpwid ⊢ ( ( Lim 𝐴 ∧ ( 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } ∧ ( cf ‘ 𝐴 ) = ( card ‘ 𝑥 ) ) ) → 𝑥 ⊆ 𝐴 )
54 simpl ⊢ ( ( Lim 𝐴 ∧ ( 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } ∧ ( cf ‘ 𝐴 ) = ( card ‘ 𝑥 ) ) ) → Lim 𝐴 )
55 vex ⊢ 𝑥 ∈ V
56 limord ⊢ ( Lim 𝐴 → Ord 𝐴 )
57 ordsson ⊢ ( Ord 𝐴 → 𝐴 ⊆ On )
58 56 57 syl ⊢ ( Lim 𝐴 → 𝐴 ⊆ On )
59 sstr ⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝐴 ⊆ On ) → 𝑥 ⊆ On )
60 58 59 sylan2 ⊢ ( ( 𝑥 ⊆ 𝐴 ∧ Lim 𝐴 ) → 𝑥 ⊆ On )
61 onssnum ⊢ ( ( 𝑥 ∈ V ∧ 𝑥 ⊆ On ) → 𝑥 ∈ dom card )
62 55 60 61 sylancr ⊢ ( ( 𝑥 ⊆ 𝐴 ∧ Lim 𝐴 ) → 𝑥 ∈ dom card )
63 cardid2 ⊢ ( 𝑥 ∈ dom card → ( card ‘ 𝑥 ) ≈ 𝑥 )
64 62 63 syl ⊢ ( ( 𝑥 ⊆ 𝐴 ∧ Lim 𝐴 ) → ( card ‘ 𝑥 ) ≈ 𝑥 )
65 64 ensymd ⊢ ( ( 𝑥 ⊆ 𝐴 ∧ Lim 𝐴 ) → 𝑥 ≈ ( card ‘ 𝑥 ) )
66 53 54 65 syl2anc ⊢ ( ( Lim 𝐴 ∧ ( 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } ∧ ( cf ‘ 𝐴 ) = ( card ‘ 𝑥 ) ) ) → 𝑥 ≈ ( card ‘ 𝑥 ) )
67 simprr ⊢ ( ( Lim 𝐴 ∧ ( 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } ∧ ( cf ‘ 𝐴 ) = ( card ‘ 𝑥 ) ) ) → ( cf ‘ 𝐴 ) = ( card ‘ 𝑥 ) )
68 66 67 breqtrrd ⊢ ( ( Lim 𝐴 ∧ ( 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } ∧ ( cf ‘ 𝐴 ) = ( card ‘ 𝑥 ) ) ) → 𝑥 ≈ ( cf ‘ 𝐴 ) )
69 51 simprd ⊢ ( ( Lim 𝐴 ∧ ( 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } ∧ ( cf ‘ 𝐴 ) = ( card ‘ 𝑥 ) ) ) → ∪ 𝑥 = 𝐴 )
70 53 68 69 3jca ⊢ ( ( Lim 𝐴 ∧ ( 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } ∧ ( cf ‘ 𝐴 ) = ( card ‘ 𝑥 ) ) ) → ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ( cf ‘ 𝐴 ) ∧ ∪ 𝑥 = 𝐴 ) )
71 70 ex ⊢ ( Lim 𝐴 → ( ( 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } ∧ ( cf ‘ 𝐴 ) = ( card ‘ 𝑥 ) ) → ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ( cf ‘ 𝐴 ) ∧ ∪ 𝑥 = 𝐴 ) ) )
72 71 eximdv ⊢ ( Lim 𝐴 → ( ∃ 𝑥 ( 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 ∣ ∪ 𝑥 = 𝐴 } ∧ ( cf ‘ 𝐴 ) = ( card ‘ 𝑥 ) ) → ∃ 𝑥 ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ( cf ‘ 𝐴 ) ∧ ∪ 𝑥 = 𝐴 ) ) )
73 49 72 mpd ⊢ ( Lim 𝐴 → ∃ 𝑥 ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ( cf ‘ 𝐴 ) ∧ ∪ 𝑥 = 𝐴 ) )