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 bitrid ⊢ ( 𝑥 = 𝐵 → ( 𝑥 ∈ 𝒫 𝐴 ↔ 𝐵 ⊆ 𝐴 ) )
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 imbitrrid ⊢ ( 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 ‘ 𝐴 ) ≼ 𝐵 )