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 ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ∃ 𝑓 ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) → ( cf ‘ 𝐴 ) = ( cf ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 cfcoflem ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ∃ 𝑓 ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) → ( cf ‘ 𝐴 ) ⊆ ( cf ‘ 𝐵 ) ) )
2 1 imp ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ∃ 𝑓 ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) ) → ( cf ‘ 𝐴 ) ⊆ ( cf ‘ 𝐵 ) )
3 cff1 ⊢ ( 𝐴 ∈ On → ∃ 𝑔 ( 𝑔 : ( cf ‘ 𝐴 ) –1-1→ 𝐴 ∧ ∀ 𝑠 ∈ 𝐴 ∃ 𝑡 ∈ ( cf ‘ 𝐴 ) 𝑠 ⊆ ( 𝑔 ‘ 𝑡 ) ) )
4 f1f ⊢ ( 𝑔 : ( cf ‘ 𝐴 ) –1-1→ 𝐴 → 𝑔 : ( cf ‘ 𝐴 ) ⟶ 𝐴 )
5 4 anim1i ⊢ ( ( 𝑔 : ( cf ‘ 𝐴 ) –1-1→ 𝐴 ∧ ∀ 𝑠 ∈ 𝐴 ∃ 𝑡 ∈ ( cf ‘ 𝐴 ) 𝑠 ⊆ ( 𝑔 ‘ 𝑡 ) ) → ( 𝑔 : ( cf ‘ 𝐴 ) ⟶ 𝐴 ∧ ∀ 𝑠 ∈ 𝐴 ∃ 𝑡 ∈ ( cf ‘ 𝐴 ) 𝑠 ⊆ ( 𝑔 ‘ 𝑡 ) ) )
6 5 eximi ⊢ ( ∃ 𝑔 ( 𝑔 : ( cf ‘ 𝐴 ) –1-1→ 𝐴 ∧ ∀ 𝑠 ∈ 𝐴 ∃ 𝑡 ∈ ( cf ‘ 𝐴 ) 𝑠 ⊆ ( 𝑔 ‘ 𝑡 ) ) → ∃ 𝑔 ( 𝑔 : ( cf ‘ 𝐴 ) ⟶ 𝐴 ∧ ∀ 𝑠 ∈ 𝐴 ∃ 𝑡 ∈ ( cf ‘ 𝐴 ) 𝑠 ⊆ ( 𝑔 ‘ 𝑡 ) ) )
7 3 6 syl ⊢ ( 𝐴 ∈ On → ∃ 𝑔 ( 𝑔 : ( cf ‘ 𝐴 ) ⟶ 𝐴 ∧ ∀ 𝑠 ∈ 𝐴 ∃ 𝑡 ∈ ( cf ‘ 𝐴 ) 𝑠 ⊆ ( 𝑔 ‘ 𝑡 ) ) )
8 eqid ⊢ ( 𝑦 ∈ ( cf ‘ 𝐴 ) ↦ ∩ { 𝑣 ∈ 𝐵 ∣ ( 𝑔 ‘ 𝑦 ) ⊆ ( 𝑓 ‘ 𝑣 ) } ) = ( 𝑦 ∈ ( cf ‘ 𝐴 ) ↦ ∩ { 𝑣 ∈ 𝐵 ∣ ( 𝑔 ‘ 𝑦 ) ⊆ ( 𝑓 ‘ 𝑣 ) } )
9 8 coftr ⊢ ( ∃ 𝑓 ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) → ( ∃ 𝑔 ( 𝑔 : ( cf ‘ 𝐴 ) ⟶ 𝐴 ∧ ∀ 𝑠 ∈ 𝐴 ∃ 𝑡 ∈ ( cf ‘ 𝐴 ) 𝑠 ⊆ ( 𝑔 ‘ 𝑡 ) ) → ∃ ℎ ( ℎ : ( cf ‘ 𝐴 ) ⟶ 𝐵 ∧ ∀ 𝑟 ∈ 𝐵 ∃ 𝑡 ∈ ( cf ‘ 𝐴 ) 𝑟 ⊆ ( ℎ ‘ 𝑡 ) ) ) )
10 7 9 syl5com ⊢ ( 𝐴 ∈ On → ( ∃ 𝑓 ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) → ∃ ℎ ( ℎ : ( cf ‘ 𝐴 ) ⟶ 𝐵 ∧ ∀ 𝑟 ∈ 𝐵 ∃ 𝑡 ∈ ( cf ‘ 𝐴 ) 𝑟 ⊆ ( ℎ ‘ 𝑡 ) ) ) )
11 eloni ⊢ ( 𝐵 ∈ On → Ord 𝐵 )
12 cfon ⊢ ( cf ‘ 𝐴 ) ∈ On
13 eqid ⊢ { 𝑥 ∈ ( cf ‘ 𝐴 ) ∣ ∀ 𝑡 ∈ 𝑥 ( ℎ ‘ 𝑡 ) ∈ ( ℎ ‘ 𝑥 ) } = { 𝑥 ∈ ( cf ‘ 𝐴 ) ∣ ∀ 𝑡 ∈ 𝑥 ( ℎ ‘ 𝑡 ) ∈ ( ℎ ‘ 𝑥 ) }
14 eqid ⊢ ∩ { 𝑐 ∈ ( cf ‘ 𝐴 ) ∣ 𝑟 ⊆ ( ℎ ‘ 𝑐 ) } = ∩ { 𝑐 ∈ ( cf ‘ 𝐴 ) ∣ 𝑟 ⊆ ( ℎ ‘ 𝑐 ) }
15 eqid ⊢ OrdIso ( E , { 𝑥 ∈ ( cf ‘ 𝐴 ) ∣ ∀ 𝑡 ∈ 𝑥 ( ℎ ‘ 𝑡 ) ∈ ( ℎ ‘ 𝑥 ) } ) = OrdIso ( E , { 𝑥 ∈ ( cf ‘ 𝐴 ) ∣ ∀ 𝑡 ∈ 𝑥 ( ℎ ‘ 𝑡 ) ∈ ( ℎ ‘ 𝑥 ) } )
16 13 14 15 cofsmo ⊢ ( ( Ord 𝐵 ∧ ( cf ‘ 𝐴 ) ∈ On ) → ( ∃ ℎ ( ℎ : ( cf ‘ 𝐴 ) ⟶ 𝐵 ∧ ∀ 𝑟 ∈ 𝐵 ∃ 𝑡 ∈ ( cf ‘ 𝐴 ) 𝑟 ⊆ ( ℎ ‘ 𝑡 ) ) → ∃ 𝑐 ∈ suc ( cf ‘ 𝐴 ) ∃ 𝑘 ( 𝑘 : 𝑐 ⟶ 𝐵 ∧ Smo 𝑘 ∧ ∀ 𝑟 ∈ 𝐵 ∃ 𝑠 ∈ 𝑐 𝑟 ⊆ ( 𝑘 ‘ 𝑠 ) ) ) )
17 11 12 16 sylancl ⊢ ( 𝐵 ∈ On → ( ∃ ℎ ( ℎ : ( cf ‘ 𝐴 ) ⟶ 𝐵 ∧ ∀ 𝑟 ∈ 𝐵 ∃ 𝑡 ∈ ( cf ‘ 𝐴 ) 𝑟 ⊆ ( ℎ ‘ 𝑡 ) ) → ∃ 𝑐 ∈ suc ( cf ‘ 𝐴 ) ∃ 𝑘 ( 𝑘 : 𝑐 ⟶ 𝐵 ∧ Smo 𝑘 ∧ ∀ 𝑟 ∈ 𝐵 ∃ 𝑠 ∈ 𝑐 𝑟 ⊆ ( 𝑘 ‘ 𝑠 ) ) ) )
18 12 onsuci ⊢ suc ( cf ‘ 𝐴 ) ∈ On
19 18 oneli ⊢ ( 𝑐 ∈ suc ( cf ‘ 𝐴 ) → 𝑐 ∈ On )
20 cfflb ⊢ ( ( 𝐵 ∈ On ∧ 𝑐 ∈ On ) → ( ∃ 𝑘 ( 𝑘 : 𝑐 ⟶ 𝐵 ∧ ∀ 𝑟 ∈ 𝐵 ∃ 𝑠 ∈ 𝑐 𝑟 ⊆ ( 𝑘 ‘ 𝑠 ) ) → ( cf ‘ 𝐵 ) ⊆ 𝑐 ) )
21 19 20 sylan2 ⊢ ( ( 𝐵 ∈ On ∧ 𝑐 ∈ suc ( cf ‘ 𝐴 ) ) → ( ∃ 𝑘 ( 𝑘 : 𝑐 ⟶ 𝐵 ∧ ∀ 𝑟 ∈ 𝐵 ∃ 𝑠 ∈ 𝑐 𝑟 ⊆ ( 𝑘 ‘ 𝑠 ) ) → ( cf ‘ 𝐵 ) ⊆ 𝑐 ) )
22 3simpb ⊢ ( ( 𝑘 : 𝑐 ⟶ 𝐵 ∧ Smo 𝑘 ∧ ∀ 𝑟 ∈ 𝐵 ∃ 𝑠 ∈ 𝑐 𝑟 ⊆ ( 𝑘 ‘ 𝑠 ) ) → ( 𝑘 : 𝑐 ⟶ 𝐵 ∧ ∀ 𝑟 ∈ 𝐵 ∃ 𝑠 ∈ 𝑐 𝑟 ⊆ ( 𝑘 ‘ 𝑠 ) ) )
23 22 eximi ⊢ ( ∃ 𝑘 ( 𝑘 : 𝑐 ⟶ 𝐵 ∧ Smo 𝑘 ∧ ∀ 𝑟 ∈ 𝐵 ∃ 𝑠 ∈ 𝑐 𝑟 ⊆ ( 𝑘 ‘ 𝑠 ) ) → ∃ 𝑘 ( 𝑘 : 𝑐 ⟶ 𝐵 ∧ ∀ 𝑟 ∈ 𝐵 ∃ 𝑠 ∈ 𝑐 𝑟 ⊆ ( 𝑘 ‘ 𝑠 ) ) )
24 21 23 impel ⊢ ( ( ( 𝐵 ∈ On ∧ 𝑐 ∈ suc ( cf ‘ 𝐴 ) ) ∧ ∃ 𝑘 ( 𝑘 : 𝑐 ⟶ 𝐵 ∧ Smo 𝑘 ∧ ∀ 𝑟 ∈ 𝐵 ∃ 𝑠 ∈ 𝑐 𝑟 ⊆ ( 𝑘 ‘ 𝑠 ) ) ) → ( cf ‘ 𝐵 ) ⊆ 𝑐 )
25 onsssuc ⊢ ( ( 𝑐 ∈ On ∧ ( cf ‘ 𝐴 ) ∈ On ) → ( 𝑐 ⊆ ( cf ‘ 𝐴 ) ↔ 𝑐 ∈ suc ( cf ‘ 𝐴 ) ) )
26 19 12 25 sylancl ⊢ ( 𝑐 ∈ suc ( cf ‘ 𝐴 ) → ( 𝑐 ⊆ ( cf ‘ 𝐴 ) ↔ 𝑐 ∈ suc ( cf ‘ 𝐴 ) ) )
27 26 ibir ⊢ ( 𝑐 ∈ suc ( cf ‘ 𝐴 ) → 𝑐 ⊆ ( cf ‘ 𝐴 ) )
28 27 ad2antlr ⊢ ( ( ( 𝐵 ∈ On ∧ 𝑐 ∈ suc ( cf ‘ 𝐴 ) ) ∧ ∃ 𝑘 ( 𝑘 : 𝑐 ⟶ 𝐵 ∧ Smo 𝑘 ∧ ∀ 𝑟 ∈ 𝐵 ∃ 𝑠 ∈ 𝑐 𝑟 ⊆ ( 𝑘 ‘ 𝑠 ) ) ) → 𝑐 ⊆ ( cf ‘ 𝐴 ) )
29 24 28 sstrd ⊢ ( ( ( 𝐵 ∈ On ∧ 𝑐 ∈ suc ( cf ‘ 𝐴 ) ) ∧ ∃ 𝑘 ( 𝑘 : 𝑐 ⟶ 𝐵 ∧ Smo 𝑘 ∧ ∀ 𝑟 ∈ 𝐵 ∃ 𝑠 ∈ 𝑐 𝑟 ⊆ ( 𝑘 ‘ 𝑠 ) ) ) → ( cf ‘ 𝐵 ) ⊆ ( cf ‘ 𝐴 ) )
30 29 rexlimdva2 ⊢ ( 𝐵 ∈ On → ( ∃ 𝑐 ∈ suc ( cf ‘ 𝐴 ) ∃ 𝑘 ( 𝑘 : 𝑐 ⟶ 𝐵 ∧ Smo 𝑘 ∧ ∀ 𝑟 ∈ 𝐵 ∃ 𝑠 ∈ 𝑐 𝑟 ⊆ ( 𝑘 ‘ 𝑠 ) ) → ( cf ‘ 𝐵 ) ⊆ ( cf ‘ 𝐴 ) ) )
31 17 30 syld ⊢ ( 𝐵 ∈ On → ( ∃ ℎ ( ℎ : ( cf ‘ 𝐴 ) ⟶ 𝐵 ∧ ∀ 𝑟 ∈ 𝐵 ∃ 𝑡 ∈ ( cf ‘ 𝐴 ) 𝑟 ⊆ ( ℎ ‘ 𝑡 ) ) → ( cf ‘ 𝐵 ) ⊆ ( cf ‘ 𝐴 ) ) )
32 10 31 sylan9 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ∃ 𝑓 ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) → ( cf ‘ 𝐵 ) ⊆ ( cf ‘ 𝐴 ) ) )
33 32 imp ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ∃ 𝑓 ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) ) → ( cf ‘ 𝐵 ) ⊆ ( cf ‘ 𝐴 ) )
34 2 33 eqssd ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ∃ 𝑓 ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) ) → ( cf ‘ 𝐴 ) = ( cf ‘ 𝐵 ) )
35 34 ex ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ∃ 𝑓 ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ Smo 𝑓 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) → ( cf ‘ 𝐴 ) = ( cf ‘ 𝐵 ) ) )