Metamath Proof Explorer


Theorem cfslb

Description: Any cofinal subset of A is at least as large as ( cfA ) . (Contributed by Mario Carneiro, 24-Jun-2013)

Ref Expression
Hypothesis cfslb.1 𝐴 ∈ V
Assertion cfslb ( ( Lim 𝐴𝐵𝐴 𝐵 = 𝐴 ) → ( cf ‘ 𝐴 ) ≼ 𝐵 )

Proof

Step Hyp Ref Expression
1 cfslb.1 𝐴 ∈ V
2 fvex ( card ‘ 𝐵 ) ∈ V
3 ssid ( card ‘ 𝐵 ) ⊆ ( card ‘ 𝐵 )
4 1 ssex ( 𝐵𝐴𝐵 ∈ V )
5 4 ad2antrr ( ( ( 𝐵𝐴 𝐵 = 𝐴 ) ∧ ( card ‘ 𝐵 ) ⊆ ( card ‘ 𝐵 ) ) → 𝐵 ∈ V )
6 velpw ( 𝑥 ∈ 𝒫 𝐴𝑥𝐴 )
7 sseq1 ( 𝑥 = 𝐵 → ( 𝑥𝐴𝐵𝐴 ) )
8 6 7 syl5bb ( 𝑥 = 𝐵 → ( 𝑥 ∈ 𝒫 𝐴𝐵𝐴 ) )
9 unieq ( 𝑥 = 𝐵 𝑥 = 𝐵 )
10 9 eqeq1d ( 𝑥 = 𝐵 → ( 𝑥 = 𝐴 𝐵 = 𝐴 ) )
11 8 10 anbi12d ( 𝑥 = 𝐵 → ( ( 𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴 ) ↔ ( 𝐵𝐴 𝐵 = 𝐴 ) ) )
12 fveq2 ( 𝑥 = 𝐵 → ( card ‘ 𝑥 ) = ( card ‘ 𝐵 ) )
13 12 sseq1d ( 𝑥 = 𝐵 → ( ( card ‘ 𝑥 ) ⊆ ( card ‘ 𝐵 ) ↔ ( card ‘ 𝐵 ) ⊆ ( card ‘ 𝐵 ) ) )
14 11 13 anbi12d ( 𝑥 = 𝐵 → ( ( ( 𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴 ) ∧ ( card ‘ 𝑥 ) ⊆ ( card ‘ 𝐵 ) ) ↔ ( ( 𝐵𝐴 𝐵 = 𝐴 ) ∧ ( card ‘ 𝐵 ) ⊆ ( card ‘ 𝐵 ) ) ) )
15 14 spcegv ( 𝐵 ∈ V → ( ( ( 𝐵𝐴 𝐵 = 𝐴 ) ∧ ( card ‘ 𝐵 ) ⊆ ( card ‘ 𝐵 ) ) → ∃ 𝑥 ( ( 𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴 ) ∧ ( card ‘ 𝑥 ) ⊆ ( card ‘ 𝐵 ) ) ) )
16 5 15 mpcom ( ( ( 𝐵𝐴 𝐵 = 𝐴 ) ∧ ( card ‘ 𝐵 ) ⊆ ( card ‘ 𝐵 ) ) → ∃ 𝑥 ( ( 𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴 ) ∧ ( card ‘ 𝑥 ) ⊆ ( card ‘ 𝐵 ) ) )
17 df-rex ( ∃ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴 } ( card ‘ 𝑥 ) ⊆ ( card ‘ 𝐵 ) ↔ ∃ 𝑥 ( 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴 } ∧ ( card ‘ 𝑥 ) ⊆ ( card ‘ 𝐵 ) ) )
18 rabid ( 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴 } ↔ ( 𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴 ) )
19 18 anbi1i ( ( 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴 } ∧ ( card ‘ 𝑥 ) ⊆ ( card ‘ 𝐵 ) ) ↔ ( ( 𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴 ) ∧ ( card ‘ 𝑥 ) ⊆ ( card ‘ 𝐵 ) ) )
20 19 exbii ( ∃ 𝑥 ( 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴 } ∧ ( card ‘ 𝑥 ) ⊆ ( card ‘ 𝐵 ) ) ↔ ∃ 𝑥 ( ( 𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴 ) ∧ ( card ‘ 𝑥 ) ⊆ ( card ‘ 𝐵 ) ) )
21 17 20 bitri ( ∃ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴 } ( card ‘ 𝑥 ) ⊆ ( card ‘ 𝐵 ) ↔ ∃ 𝑥 ( ( 𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴 ) ∧ ( card ‘ 𝑥 ) ⊆ ( card ‘ 𝐵 ) ) )
22 16 21 sylibr ( ( ( 𝐵𝐴 𝐵 = 𝐴 ) ∧ ( card ‘ 𝐵 ) ⊆ ( card ‘ 𝐵 ) ) → ∃ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴 } ( card ‘ 𝑥 ) ⊆ ( card ‘ 𝐵 ) )
23 3 22 mpan2 ( ( 𝐵𝐴 𝐵 = 𝐴 ) → ∃ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴 } ( card ‘ 𝑥 ) ⊆ ( card ‘ 𝐵 ) )
24 iinss ( ∃ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴 } ( card ‘ 𝑥 ) ⊆ ( card ‘ 𝐵 ) → 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴 } ( card ‘ 𝑥 ) ⊆ ( card ‘ 𝐵 ) )
25 23 24 syl ( ( 𝐵𝐴 𝐵 = 𝐴 ) → 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴 } ( card ‘ 𝑥 ) ⊆ ( card ‘ 𝐵 ) )
26 1 cflim3 ( Lim 𝐴 → ( cf ‘ 𝐴 ) = 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴 } ( card ‘ 𝑥 ) )
27 26 sseq1d ( Lim 𝐴 → ( ( cf ‘ 𝐴 ) ⊆ ( card ‘ 𝐵 ) ↔ 𝑥 ∈ { 𝑥 ∈ 𝒫 𝐴 𝑥 = 𝐴 } ( card ‘ 𝑥 ) ⊆ ( card ‘ 𝐵 ) ) )
28 25 27 syl5ibr ( Lim 𝐴 → ( ( 𝐵𝐴 𝐵 = 𝐴 ) → ( cf ‘ 𝐴 ) ⊆ ( card ‘ 𝐵 ) ) )
29 28 3impib ( ( Lim 𝐴𝐵𝐴 𝐵 = 𝐴 ) → ( cf ‘ 𝐴 ) ⊆ ( card ‘ 𝐵 ) )
30 ssdomg ( ( card ‘ 𝐵 ) ∈ V → ( ( cf ‘ 𝐴 ) ⊆ ( card ‘ 𝐵 ) → ( cf ‘ 𝐴 ) ≼ ( card ‘ 𝐵 ) ) )
31 2 29 30 mpsyl ( ( Lim 𝐴𝐵𝐴 𝐵 = 𝐴 ) → ( cf ‘ 𝐴 ) ≼ ( card ‘ 𝐵 ) )
32 limord ( Lim 𝐴 → Ord 𝐴 )
33 ordsson ( Ord 𝐴𝐴 ⊆ On )
34 32 33 syl ( Lim 𝐴𝐴 ⊆ On )
35 sstr2 ( 𝐵𝐴 → ( 𝐴 ⊆ On → 𝐵 ⊆ On ) )
36 34 35 mpan9 ( ( Lim 𝐴𝐵𝐴 ) → 𝐵 ⊆ On )
37 onssnum ( ( 𝐵 ∈ V ∧ 𝐵 ⊆ On ) → 𝐵 ∈ dom card )
38 4 36 37 syl2an2 ( ( Lim 𝐴𝐵𝐴 ) → 𝐵 ∈ dom card )
39 cardid2 ( 𝐵 ∈ dom card → ( card ‘ 𝐵 ) ≈ 𝐵 )
40 38 39 syl ( ( Lim 𝐴𝐵𝐴 ) → ( card ‘ 𝐵 ) ≈ 𝐵 )
41 40 3adant3 ( ( Lim 𝐴𝐵𝐴 𝐵 = 𝐴 ) → ( card ‘ 𝐵 ) ≈ 𝐵 )
42 domentr ( ( ( cf ‘ 𝐴 ) ≼ ( card ‘ 𝐵 ) ∧ ( card ‘ 𝐵 ) ≈ 𝐵 ) → ( cf ‘ 𝐴 ) ≼ 𝐵 )
43 31 41 42 syl2anc ( ( Lim 𝐴𝐵𝐴 𝐵 = 𝐴 ) → ( cf ‘ 𝐴 ) ≼ 𝐵 )