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 syl5bi ( ( 𝐴 ∈ 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 ‘ 𝑦 ) ∧ ( 𝑦𝐴𝐴 𝑦 ) ) }