Metamath Proof Explorer

Theorem cfcof

Description: If there is a cofinal map from A to B , then they have the same cofinality. This was used as Definition 11.1 of TakeutiZaring p. 100, who defines an equivalence relation cof ( A , B ) and defines our cf ( B ) as the minimum B such that cof ( A , B ) . (Contributed by Mario Carneiro, 20-Mar-2013)

Ref Expression
Assertion cfcof ⊢ A ∈ On ∧ B ∈ On → ∃ f f : B ⟶ A ∧ Smo ⁡ f ∧ ∀ z ∈ A ∃ w ∈ B z ⊆ f ⁡ w → cf ⁡ A = cf ⁡ B

Proof

Step Hyp Ref Expression
1 cfcoflem ⊢ A ∈ On ∧ B ∈ On → ∃ f f : B ⟶ A ∧ Smo ⁡ f ∧ ∀ z ∈ A ∃ w ∈ B z ⊆ f ⁡ w → cf ⁡ A ⊆ cf ⁡ B
2 1 imp ⊢ A ∈ On ∧ B ∈ On ∧ ∃ f f : B ⟶ A ∧ Smo ⁡ f ∧ ∀ z ∈ A ∃ w ∈ B z ⊆ f ⁡ w → cf ⁡ A ⊆ cf ⁡ B
3 cff1 ⊢ A ∈ On → ∃ g g : cf ⁡ A ⟶ 1-1 A ∧ ∀ s ∈ A ∃ t ∈ cf ⁡ A s ⊆ g ⁡ t
4 f1f ⊢ g : cf ⁡ A ⟶ 1-1 A → g : cf ⁡ A ⟶ A
5 4 anim1i ⊢ g : cf ⁡ A ⟶ 1-1 A ∧ ∀ s ∈ A ∃ t ∈ cf ⁡ A s ⊆ g ⁡ t → g : cf ⁡ A ⟶ A ∧ ∀ s ∈ A ∃ t ∈ cf ⁡ A s ⊆ g ⁡ t
6 5 eximi ⊢ ∃ g g : cf ⁡ A ⟶ 1-1 A ∧ ∀ s ∈ A ∃ t ∈ cf ⁡ A s ⊆ g ⁡ t → ∃ g g : cf ⁡ A ⟶ A ∧ ∀ s ∈ A ∃ t ∈ cf ⁡ A s ⊆ g ⁡ t
7 3 6 syl ⊢ A ∈ On → ∃ g g : cf ⁡ A ⟶ A ∧ ∀ s ∈ A ∃ t ∈ cf ⁡ A s ⊆ g ⁡ t
8 eqid ⊢ y ∈ cf ⁡ A ⟼ ⋂ v ∈ B | g ⁡ y ⊆ f ⁡ v = y ∈ cf ⁡ A ⟼ ⋂ v ∈ B | g ⁡ y ⊆ f ⁡ v
9 8 coftr ⊢ ∃ f f : B ⟶ A ∧ Smo ⁡ f ∧ ∀ z ∈ A ∃ w ∈ B z ⊆ f ⁡ w → ∃ g g : cf ⁡ A ⟶ A ∧ ∀ s ∈ A ∃ t ∈ cf ⁡ A s ⊆ g ⁡ t → ∃ h h : cf ⁡ A ⟶ B ∧ ∀ r ∈ B ∃ t ∈ cf ⁡ A r ⊆ h ⁡ t
10 7 9 syl5com ⊢ A ∈ On → ∃ f f : B ⟶ A ∧ Smo ⁡ f ∧ ∀ z ∈ A ∃ w ∈ B z ⊆ f ⁡ w → ∃ h h : cf ⁡ A ⟶ B ∧ ∀ r ∈ B ∃ t ∈ cf ⁡ A r ⊆ h ⁡ t
11 eloni ⊢ B ∈ On → Ord ⁡ B
12 cfon ⊢ cf ⁡ A ∈ On
13 eqid ⊢ x ∈ cf ⁡ A | ∀ t ∈ x h ⁡ t ∈ h ⁡ x = x ∈ cf ⁡ A | ∀ t ∈ x h ⁡ t ∈ h ⁡ x
14 eqid ⊢ ⋂ c ∈ cf ⁡ A | r ⊆ h ⁡ c = ⋂ c ∈ cf ⁡ A | r ⊆ h ⁡ c
15 eqid ⊢ OrdIso E x ∈ cf ⁡ A | ∀ t ∈ x h ⁡ t ∈ h ⁡ x = OrdIso E x ∈ cf ⁡ A | ∀ t ∈ x h ⁡ t ∈ h ⁡ x
16 13 14 15 cofsmo ⊢ Ord ⁡ B ∧ cf ⁡ A ∈ On → ∃ h h : cf ⁡ A ⟶ B ∧ ∀ r ∈ B ∃ t ∈ cf ⁡ A r ⊆ h ⁡ t → ∃ c ∈ suc ⁡ cf ⁡ A ∃ k k : c ⟶ B ∧ Smo ⁡ k ∧ ∀ r ∈ B ∃ s ∈ c r ⊆ k ⁡ s
17 11 12 16 sylancl ⊢ B ∈ On → ∃ h h : cf ⁡ A ⟶ B ∧ ∀ r ∈ B ∃ t ∈ cf ⁡ A r ⊆ h ⁡ t → ∃ c ∈ suc ⁡ cf ⁡ A ∃ k k : c ⟶ B ∧ Smo ⁡ k ∧ ∀ r ∈ B ∃ s ∈ c r ⊆ k ⁡ s
18 12 onsuci ⊢ suc ⁡ cf ⁡ A ∈ On
19 18 oneli ⊢ c ∈ suc ⁡ cf ⁡ A → c ∈ On
20 cfflb ⊢ B ∈ On ∧ c ∈ On → ∃ k k : c ⟶ B ∧ ∀ r ∈ B ∃ s ∈ c r ⊆ k ⁡ s → cf ⁡ B ⊆ c
21 19 20 sylan2 ⊢ B ∈ On ∧ c ∈ suc ⁡ cf ⁡ A → ∃ k k : c ⟶ B ∧ ∀ r ∈ B ∃ s ∈ c r ⊆ k ⁡ s → cf ⁡ B ⊆ c
22 3simpb ⊢ k : c ⟶ B ∧ Smo ⁡ k ∧ ∀ r ∈ B ∃ s ∈ c r ⊆ k ⁡ s → k : c ⟶ B ∧ ∀ r ∈ B ∃ s ∈ c r ⊆ k ⁡ s
23 22 eximi ⊢ ∃ k k : c ⟶ B ∧ Smo ⁡ k ∧ ∀ r ∈ B ∃ s ∈ c r ⊆ k ⁡ s → ∃ k k : c ⟶ B ∧ ∀ r ∈ B ∃ s ∈ c r ⊆ k ⁡ s
24 21 23 impel ⊢ B ∈ On ∧ c ∈ suc ⁡ cf ⁡ A ∧ ∃ k k : c ⟶ B ∧ Smo ⁡ k ∧ ∀ r ∈ B ∃ s ∈ c r ⊆ k ⁡ s → cf ⁡ B ⊆ c
25 onsssuc ⊢ c ∈ On ∧ cf ⁡ A ∈ On → c ⊆ cf ⁡ A ↔ c ∈ suc ⁡ cf ⁡ A
26 19 12 25 sylancl ⊢ c ∈ suc ⁡ cf ⁡ A → c ⊆ cf ⁡ A ↔ c ∈ suc ⁡ cf ⁡ A
27 26 ibir ⊢ c ∈ suc ⁡ cf ⁡ A → c ⊆ cf ⁡ A
28 27 ad2antlr ⊢ B ∈ On ∧ c ∈ suc ⁡ cf ⁡ A ∧ ∃ k k : c ⟶ B ∧ Smo ⁡ k ∧ ∀ r ∈ B ∃ s ∈ c r ⊆ k ⁡ s → c ⊆ cf ⁡ A
29 24 28 sstrd ⊢ B ∈ On ∧ c ∈ suc ⁡ cf ⁡ A ∧ ∃ k k : c ⟶ B ∧ Smo ⁡ k ∧ ∀ r ∈ B ∃ s ∈ c r ⊆ k ⁡ s → cf ⁡ B ⊆ cf ⁡ A
30 29 rexlimdva2 ⊢ B ∈ On → ∃ c ∈ suc ⁡ cf ⁡ A ∃ k k : c ⟶ B ∧ Smo ⁡ k ∧ ∀ r ∈ B ∃ s ∈ c r ⊆ k ⁡ s → cf ⁡ B ⊆ cf ⁡ A
31 17 30 syld ⊢ B ∈ On → ∃ h h : cf ⁡ A ⟶ B ∧ ∀ r ∈ B ∃ t ∈ cf ⁡ A r ⊆ h ⁡ t → cf ⁡ B ⊆ cf ⁡ A
32 10 31 sylan9 ⊢ A ∈ On ∧ B ∈ On → ∃ f f : B ⟶ A ∧ Smo ⁡ f ∧ ∀ z ∈ A ∃ w ∈ B z ⊆ f ⁡ w → cf ⁡ B ⊆ cf ⁡ A
33 32 imp ⊢ A ∈ On ∧ B ∈ On ∧ ∃ f f : B ⟶ A ∧ Smo ⁡ f ∧ ∀ z ∈ A ∃ w ∈ B z ⊆ f ⁡ w → cf ⁡ B ⊆ cf ⁡ A
34 2 33 eqssd ⊢ A ∈ On ∧ B ∈ On ∧ ∃ f f : B ⟶ A ∧ Smo ⁡ f ∧ ∀ z ∈ A ∃ w ∈ B z ⊆ f ⁡ w → cf ⁡ A = cf ⁡ B
35 34 ex ⊢ A ∈ On ∧ B ∈ On → ∃ f f : B ⟶ A ∧ Smo ⁡ f ∧ ∀ z ∈ A ∃ w ∈ B z ⊆ f ⁡ w → cf ⁡ A = cf ⁡ B