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→∃ff:B⟶A∧Smo⁡f∧∀z∈A∃w∈Bz⊆f⁡w→cf⁡A=cf⁡B

Proof

Step Hyp Ref Expression
1 cfcoflem ⊢A∈On∧B∈On→∃ff:B⟶A∧Smo⁡f∧∀z∈A∃w∈Bz⊆f⁡w→cf⁡A⊆cf⁡B
2 1 imp ⊢A∈On∧B∈On∧∃ff:B⟶A∧Smo⁡f∧∀z∈A∃w∈Bz⊆f⁡w→cf⁡A⊆cf⁡B
3 cff1 ⊢A∈On→∃gg:cf⁡A⟶1-1A∧∀s∈A∃t∈cf⁡As⊆g⁡t
4 f1f ⊢g:cf⁡A⟶1-1A→g:cf⁡A⟶A
5 4 anim1i ⊢g:cf⁡A⟶1-1A∧∀s∈A∃t∈cf⁡As⊆g⁡t→g:cf⁡A⟶A∧∀s∈A∃t∈cf⁡As⊆g⁡t
6 5 eximi ⊢∃gg:cf⁡A⟶1-1A∧∀s∈A∃t∈cf⁡As⊆g⁡t→∃gg:cf⁡A⟶A∧∀s∈A∃t∈cf⁡As⊆g⁡t
7 3 6 syl ⊢A∈On→∃gg:cf⁡A⟶A∧∀s∈A∃t∈cf⁡As⊆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 ⊢∃ff:B⟶A∧Smo⁡f∧∀z∈A∃w∈Bz⊆f⁡w→∃gg:cf⁡A⟶A∧∀s∈A∃t∈cf⁡As⊆g⁡t→∃hh:cf⁡A⟶B∧∀r∈B∃t∈cf⁡Ar⊆h⁡t
10 7 9 syl5com ⊢A∈On→∃ff:B⟶A∧Smo⁡f∧∀z∈A∃w∈Bz⊆f⁡w→∃hh:cf⁡A⟶B∧∀r∈B∃t∈cf⁡Ar⊆h⁡t
11 eloni ⊢B∈On→Ord⁡B
12 cfon ⊢cf⁡A∈On
13 eqid ⊢x∈cf⁡A|∀t∈xh⁡t∈h⁡x=x∈cf⁡A|∀t∈xh⁡t∈h⁡x
14 eqid ⊢⋂c∈cf⁡A|r⊆h⁡c=⋂c∈cf⁡A|r⊆h⁡c
15 eqid ⊢OrdIsoEx∈cf⁡A|∀t∈xh⁡t∈h⁡x=OrdIsoEx∈cf⁡A|∀t∈xh⁡t∈h⁡x
16 13 14 15 cofsmo ⊢Ord⁡B∧cf⁡A∈On→∃hh:cf⁡A⟶B∧∀r∈B∃t∈cf⁡Ar⊆h⁡t→∃c∈suc⁡cf⁡A∃kk:c⟶B∧Smo⁡k∧∀r∈B∃s∈cr⊆k⁡s
17 11 12 16 sylancl ⊢B∈On→∃hh:cf⁡A⟶B∧∀r∈B∃t∈cf⁡Ar⊆h⁡t→∃c∈suc⁡cf⁡A∃kk:c⟶B∧Smo⁡k∧∀r∈B∃s∈cr⊆k⁡s
18 12 onsuci ⊢suc⁡cf⁡A∈On
19 18 oneli ⊢c∈suc⁡cf⁡A→c∈On
20 cfflb ⊢B∈On∧c∈On→∃kk:c⟶B∧∀r∈B∃s∈cr⊆k⁡s→cf⁡B⊆c
21 19 20 sylan2 ⊢B∈On∧c∈suc⁡cf⁡A→∃kk:c⟶B∧∀r∈B∃s∈cr⊆k⁡s→cf⁡B⊆c
22 3simpb ⊢k:c⟶B∧Smo⁡k∧∀r∈B∃s∈cr⊆k⁡s→k:c⟶B∧∀r∈B∃s∈cr⊆k⁡s
23 22 eximi ⊢∃kk:c⟶B∧Smo⁡k∧∀r∈B∃s∈cr⊆k⁡s→∃kk:c⟶B∧∀r∈B∃s∈cr⊆k⁡s
24 21 23 impel ⊢B∈On∧c∈suc⁡cf⁡A∧∃kk:c⟶B∧Smo⁡k∧∀r∈B∃s∈cr⊆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∧∃kk:c⟶B∧Smo⁡k∧∀r∈B∃s∈cr⊆k⁡s→c⊆cf⁡A
29 24 28 sstrd ⊢B∈On∧c∈suc⁡cf⁡A∧∃kk:c⟶B∧Smo⁡k∧∀r∈B∃s∈cr⊆k⁡s→cf⁡B⊆cf⁡A
30 29 rexlimdva2 ⊢B∈On→∃c∈suc⁡cf⁡A∃kk:c⟶B∧Smo⁡k∧∀r∈B∃s∈cr⊆k⁡s→cf⁡B⊆cf⁡A
31 17 30 syld ⊢B∈On→∃hh:cf⁡A⟶B∧∀r∈B∃t∈cf⁡Ar⊆h⁡t→cf⁡B⊆cf⁡A
32 10 31 sylan9 ⊢A∈On∧B∈On→∃ff:B⟶A∧Smo⁡f∧∀z∈A∃w∈Bz⊆f⁡w→cf⁡B⊆cf⁡A
33 32 imp ⊢A∈On∧B∈On∧∃ff:B⟶A∧Smo⁡f∧∀z∈A∃w∈Bz⊆f⁡w→cf⁡B⊆cf⁡A
34 2 33 eqssd ⊢A∈On∧B∈On∧∃ff:B⟶A∧Smo⁡f∧∀z∈A∃w∈Bz⊆f⁡w→cf⁡A=cf⁡B
35 34 ex ⊢A∈On∧B∈On→∃ff:B⟶A∧Smo⁡f∧∀z∈A∃w∈Bz⊆f⁡w→cf⁡A=cf⁡B