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 ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ ∪ 𝑦 ) ) }