This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cfub

Description: An upper bound on cofinality. (Contributed by NM, 25-Apr-2004) (Revised by Mario Carneiro, 15-Sep-2013)

Ref Expression
Assertion cfub ( cf ‘ 𝐴 ) ⊆ ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ ∪ 𝑦 ) ) }

Proof

Step Hyp Ref Expression
1 cfval ⊢ ( 𝐴 ∈ On → ( cf ‘ 𝐴 ) = ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } )
2 dfss3 ⊢ ( 𝐴 ⊆ ∪ 𝑦 ↔ ∀ 𝑧 ∈ 𝐴 𝑧 ∈ ∪ 𝑦 )
3 ssel ⊢ ( 𝑦 ⊆ 𝐴 → ( 𝑤 ∈ 𝑦 → 𝑤 ∈ 𝐴 ) )
4 onelon ⊢ ( ( 𝐴 ∈ On ∧ 𝑤 ∈ 𝐴 ) → 𝑤 ∈ On )
5 4 ex ⊢ ( 𝐴 ∈ On → ( 𝑤 ∈ 𝐴 → 𝑤 ∈ On ) )
6 3 5 sylan9r ⊢ ( ( 𝐴 ∈ On ∧ 𝑦 ⊆ 𝐴 ) → ( 𝑤 ∈ 𝑦 → 𝑤 ∈ On ) )
7 onelss ⊢ ( 𝑤 ∈ On → ( 𝑧 ∈ 𝑤 → 𝑧 ⊆ 𝑤 ) )
8 6 7 syl6 ⊢ ( ( 𝐴 ∈ On ∧ 𝑦 ⊆ 𝐴 ) → ( 𝑤 ∈ 𝑦 → ( 𝑧 ∈ 𝑤 → 𝑧 ⊆ 𝑤 ) ) )
9 8 imdistand ⊢ ( ( 𝐴 ∈ On ∧ 𝑦 ⊆ 𝐴 ) → ( ( 𝑤 ∈ 𝑦 ∧ 𝑧 ∈ 𝑤 ) → ( 𝑤 ∈ 𝑦 ∧ 𝑧 ⊆ 𝑤 ) ) )
10 9 ancomsd ⊢ ( ( 𝐴 ∈ On ∧ 𝑦 ⊆ 𝐴 ) → ( ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦 ) → ( 𝑤 ∈ 𝑦 ∧ 𝑧 ⊆ 𝑤 ) ) )
11 10 eximdv ⊢ ( ( 𝐴 ∈ On ∧ 𝑦 ⊆ 𝐴 ) → ( ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦 ) → ∃ 𝑤 ( 𝑤 ∈ 𝑦 ∧ 𝑧 ⊆ 𝑤 ) ) )
12 eluni ⊢ ( 𝑧 ∈ ∪ 𝑦 ↔ ∃ 𝑤 ( 𝑧 ∈ 𝑤 ∧ 𝑤 ∈ 𝑦 ) )
13 df-rex ⊢ ( ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ↔ ∃ 𝑤 ( 𝑤 ∈ 𝑦 ∧ 𝑧 ⊆ 𝑤 ) )
14 11 12 13 3imtr4g ⊢ ( ( 𝐴 ∈ On ∧ 𝑦 ⊆ 𝐴 ) → ( 𝑧 ∈ ∪ 𝑦 → ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) )
15 14 ralimdv ⊢ ( ( 𝐴 ∈ On ∧ 𝑦 ⊆ 𝐴 ) → ( ∀ 𝑧 ∈ 𝐴 𝑧 ∈ ∪ 𝑦 → ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) )
16 2 15 biimtrid ⊢ ( ( 𝐴 ∈ On ∧ 𝑦 ⊆ 𝐴 ) → ( 𝐴 ⊆ ∪ 𝑦 → ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) )
17 16 imdistanda ⊢ ( 𝐴 ∈ On → ( ( 𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ ∪ 𝑦 ) → ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) )
18 17 anim2d ⊢ ( 𝐴 ∈ On → ( ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ ∪ 𝑦 ) ) → ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) ) )
19 18 eximdv ⊢ ( 𝐴 ∈ On → ( ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ ∪ 𝑦 ) ) → ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) ) )
20 19 ss2abdv ⊢ ( 𝐴 ∈ On → { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ ∪ 𝑦 ) ) } ⊆ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } )
21 intss ⊢ ( { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ ∪ 𝑦 ) ) } ⊆ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } → ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } ⊆ ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ ∪ 𝑦 ) ) } )
22 20 21 syl ⊢ ( 𝐴 ∈ On → ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } ⊆ ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ ∪ 𝑦 ) ) } )
23 1 22 eqsstrd ⊢ ( 𝐴 ∈ On → ( cf ‘ 𝐴 ) ⊆ ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ ∪ 𝑦 ) ) } )
24 cff ⊢ cf : On ⟶ On
25 24 fdmi ⊢ dom cf = On
26 25 eleq2i ⊢ ( 𝐴 ∈ dom cf ↔ 𝐴 ∈ On )
27 ndmfv ⊢ ( ¬ 𝐴 ∈ dom cf → ( cf ‘ 𝐴 ) = ∅ )
28 26 27 sylnbir ⊢ ( ¬ 𝐴 ∈ On → ( cf ‘ 𝐴 ) = ∅ )
29 0ss ⊢ ∅ ⊆ ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ ∪ 𝑦 ) ) }
30 28 29 eqsstrdi ⊢ ( ¬ 𝐴 ∈ On → ( cf ‘ 𝐴 ) ⊆ ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ ∪ 𝑦 ) ) } )
31 23 30 pm2.61i ⊢ ( cf ‘ 𝐴 ) ⊆ ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ ∪ 𝑦 ) ) }