Metamath Proof Explorer

Theorem cfflb

Description: If there is a cofinal map from B to A , then B is at least ( cfA ) . This theorem and cff1 motivate the picture of ( cfA ) as the greatest lower bound of the domain of cofinal maps into A . (Contributed by Mario Carneiro, 28-Feb-2013)

Ref Expression
Assertion cfflb ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ∃ 𝑓 ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) → ( cf ‘ 𝐴 ) ⊆ 𝐵 ) )

Proof

Step Hyp Ref Expression
1 frn ⊢ ( 𝑓 : 𝐵 ⟶ 𝐴 → ran 𝑓 ⊆ 𝐴 )
2 1 adantr ⊢ ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) → ran 𝑓 ⊆ 𝐴 )
3 ffn ⊢ ( 𝑓 : 𝐵 ⟶ 𝐴 → 𝑓 Fn 𝐵 )
4 fnfvelrn ⊢ ( ( 𝑓 Fn 𝐵 ∧ 𝑤 ∈ 𝐵 ) → ( 𝑓 ‘ 𝑤 ) ∈ ran 𝑓 )
5 3 4 sylan ⊢ ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ 𝑤 ∈ 𝐵 ) → ( 𝑓 ‘ 𝑤 ) ∈ ran 𝑓 )
6 sseq2 ⊢ ( 𝑠 = ( 𝑓 ‘ 𝑤 ) → ( 𝑧 ⊆ 𝑠 ↔ 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) )
7 6 rspcev ⊢ ( ( ( 𝑓 ‘ 𝑤 ) ∈ ran 𝑓 ∧ 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) → ∃ 𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠 )
8 5 7 sylan ⊢ ( ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ 𝑤 ∈ 𝐵 ) ∧ 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) → ∃ 𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠 )
9 8 rexlimdva2 ⊢ ( 𝑓 : 𝐵 ⟶ 𝐴 → ( ∃ 𝑤 ∈ 𝐵 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) → ∃ 𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠 ) )
10 9 ralimdv ⊢ ( 𝑓 : 𝐵 ⟶ 𝐴 → ( ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) → ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠 ) )
11 10 imp ⊢ ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) → ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠 )
12 2 11 jca ⊢ ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) → ( ran 𝑓 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠 ) )
13 fvex ⊢ ( card ‘ ran 𝑓 ) ∈ V
14 cfval ⊢ ( 𝐴 ∈ On → ( cf ‘ 𝐴 ) = ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ) ) } )
15 14 adantr ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( cf ‘ 𝐴 ) = ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ) ) } )
16 15 3ad2ant2 ⊢ ( ( 𝑥 = ( card ‘ ran 𝑓 ) ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( ran 𝑓 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠 ) ) → ( cf ‘ 𝐴 ) = ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ) ) } )
17 vex ⊢ 𝑓 ∈ V
18 17 rnex ⊢ ran 𝑓 ∈ V
19 fveq2 ⊢ ( 𝑦 = ran 𝑓 → ( card ‘ 𝑦 ) = ( card ‘ ran 𝑓 ) )
20 19 eqeq2d ⊢ ( 𝑦 = ran 𝑓 → ( 𝑥 = ( card ‘ 𝑦 ) ↔ 𝑥 = ( card ‘ ran 𝑓 ) ) )
21 sseq1 ⊢ ( 𝑦 = ran 𝑓 → ( 𝑦 ⊆ 𝐴 ↔ ran 𝑓 ⊆ 𝐴 ) )
22 rexeq ⊢ ( 𝑦 = ran 𝑓 → ( ∃ 𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ↔ ∃ 𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠 ) )
23 22 ralbidv ⊢ ( 𝑦 = ran 𝑓 → ( ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ↔ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠 ) )
24 21 23 anbi12d ⊢ ( 𝑦 = ran 𝑓 → ( ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ) ↔ ( ran 𝑓 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠 ) ) )
25 20 24 anbi12d ⊢ ( 𝑦 = ran 𝑓 → ( ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ) ) ↔ ( 𝑥 = ( card ‘ ran 𝑓 ) ∧ ( ran 𝑓 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠 ) ) ) )
26 18 25 spcev ⊢ ( ( 𝑥 = ( card ‘ ran 𝑓 ) ∧ ( ran 𝑓 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠 ) ) → ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ) ) )
27 abid ⊢ ( 𝑥 ∈ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ) ) } ↔ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ) ) )
28 26 27 sylibr ⊢ ( ( 𝑥 = ( card ‘ ran 𝑓 ) ∧ ( ran 𝑓 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠 ) ) → 𝑥 ∈ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ) ) } )
29 intss1 ⊢ ( 𝑥 ∈ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ) ) } → ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ) ) } ⊆ 𝑥 )
30 28 29 syl ⊢ ( ( 𝑥 = ( card ‘ ran 𝑓 ) ∧ ( ran 𝑓 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠 ) ) → ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ) ) } ⊆ 𝑥 )
31 30 3adant2 ⊢ ( ( 𝑥 = ( card ‘ ran 𝑓 ) ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( ran 𝑓 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠 ) ) → ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ 𝑦 𝑧 ⊆ 𝑠 ) ) } ⊆ 𝑥 )
32 16 31 eqsstrd ⊢ ( ( 𝑥 = ( card ‘ ran 𝑓 ) ∧ ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( ran 𝑓 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠 ) ) → ( cf ‘ 𝐴 ) ⊆ 𝑥 )
33 32 3expib ⊢ ( 𝑥 = ( card ‘ ran 𝑓 ) → ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( ran 𝑓 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠 ) ) → ( cf ‘ 𝐴 ) ⊆ 𝑥 ) )
34 sseq2 ⊢ ( 𝑥 = ( card ‘ ran 𝑓 ) → ( ( cf ‘ 𝐴 ) ⊆ 𝑥 ↔ ( cf ‘ 𝐴 ) ⊆ ( card ‘ ran 𝑓 ) ) )
35 33 34 sylibd ⊢ ( 𝑥 = ( card ‘ ran 𝑓 ) → ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( ran 𝑓 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠 ) ) → ( cf ‘ 𝐴 ) ⊆ ( card ‘ ran 𝑓 ) ) )
36 13 35 vtocle ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( ran 𝑓 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑠 ∈ ran 𝑓 𝑧 ⊆ 𝑠 ) ) → ( cf ‘ 𝐴 ) ⊆ ( card ‘ ran 𝑓 ) )
37 12 36 sylan2 ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) ) → ( cf ‘ 𝐴 ) ⊆ ( card ‘ ran 𝑓 ) )
38 cardidm ⊢ ( card ‘ ( card ‘ ran 𝑓 ) ) = ( card ‘ ran 𝑓 )
39 onss ⊢ ( 𝐴 ∈ On → 𝐴 ⊆ On )
40 1 39 sylan9ssr ⊢ ( ( 𝐴 ∈ On ∧ 𝑓 : 𝐵 ⟶ 𝐴 ) → ran 𝑓 ⊆ On )
41 40 3adant2 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓 : 𝐵 ⟶ 𝐴 ) → ran 𝑓 ⊆ On )
42 onssnum ⊢ ( ( ran 𝑓 ∈ V ∧ ran 𝑓 ⊆ On ) → ran 𝑓 ∈ dom card )
43 18 41 42 sylancr ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓 : 𝐵 ⟶ 𝐴 ) → ran 𝑓 ∈ dom card )
44 cardid2 ⊢ ( ran 𝑓 ∈ dom card → ( card ‘ ran 𝑓 ) ≈ ran 𝑓 )
45 43 44 syl ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓 : 𝐵 ⟶ 𝐴 ) → ( card ‘ ran 𝑓 ) ≈ ran 𝑓 )
46 onenon ⊢ ( 𝐵 ∈ On → 𝐵 ∈ dom card )
47 dffn4 ⊢ ( 𝑓 Fn 𝐵 ↔ 𝑓 : 𝐵 –onto→ ran 𝑓 )
48 3 47 sylib ⊢ ( 𝑓 : 𝐵 ⟶ 𝐴 → 𝑓 : 𝐵 –onto→ ran 𝑓 )
49 fodomnum ⊢ ( 𝐵 ∈ dom card → ( 𝑓 : 𝐵 –onto→ ran 𝑓 → ran 𝑓 ≼ 𝐵 ) )
50 46 48 49 syl2im ⊢ ( 𝐵 ∈ On → ( 𝑓 : 𝐵 ⟶ 𝐴 → ran 𝑓 ≼ 𝐵 ) )
51 50 imp ⊢ ( ( 𝐵 ∈ On ∧ 𝑓 : 𝐵 ⟶ 𝐴 ) → ran 𝑓 ≼ 𝐵 )
52 51 3adant1 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓 : 𝐵 ⟶ 𝐴 ) → ran 𝑓 ≼ 𝐵 )
53 endomtr ⊢ ( ( ( card ‘ ran 𝑓 ) ≈ ran 𝑓 ∧ ran 𝑓 ≼ 𝐵 ) → ( card ‘ ran 𝑓 ) ≼ 𝐵 )
54 45 52 53 syl2anc ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓 : 𝐵 ⟶ 𝐴 ) → ( card ‘ ran 𝑓 ) ≼ 𝐵 )
55 cardon ⊢ ( card ‘ ran 𝑓 ) ∈ On
56 onenon ⊢ ( ( card ‘ ran 𝑓 ) ∈ On → ( card ‘ ran 𝑓 ) ∈ dom card )
57 55 56 ax-mp ⊢ ( card ‘ ran 𝑓 ) ∈ dom card
58 carddom2 ⊢ ( ( ( card ‘ ran 𝑓 ) ∈ dom card ∧ 𝐵 ∈ dom card ) → ( ( card ‘ ( card ‘ ran 𝑓 ) ) ⊆ ( card ‘ 𝐵 ) ↔ ( card ‘ ran 𝑓 ) ≼ 𝐵 ) )
59 57 46 58 sylancr ⊢ ( 𝐵 ∈ On → ( ( card ‘ ( card ‘ ran 𝑓 ) ) ⊆ ( card ‘ 𝐵 ) ↔ ( card ‘ ran 𝑓 ) ≼ 𝐵 ) )
60 59 3ad2ant2 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓 : 𝐵 ⟶ 𝐴 ) → ( ( card ‘ ( card ‘ ran 𝑓 ) ) ⊆ ( card ‘ 𝐵 ) ↔ ( card ‘ ran 𝑓 ) ≼ 𝐵 ) )
61 54 60 mpbird ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓 : 𝐵 ⟶ 𝐴 ) → ( card ‘ ( card ‘ ran 𝑓 ) ) ⊆ ( card ‘ 𝐵 ) )
62 cardonle ⊢ ( 𝐵 ∈ On → ( card ‘ 𝐵 ) ⊆ 𝐵 )
63 62 3ad2ant2 ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓 : 𝐵 ⟶ 𝐴 ) → ( card ‘ 𝐵 ) ⊆ 𝐵 )
64 61 63 sstrd ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓 : 𝐵 ⟶ 𝐴 ) → ( card ‘ ( card ‘ ran 𝑓 ) ) ⊆ 𝐵 )
65 38 64 eqsstrrid ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑓 : 𝐵 ⟶ 𝐴 ) → ( card ‘ ran 𝑓 ) ⊆ 𝐵 )
66 65 3expa ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ 𝑓 : 𝐵 ⟶ 𝐴 ) → ( card ‘ ran 𝑓 ) ⊆ 𝐵 )
67 66 adantrr ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) ) → ( card ‘ ran 𝑓 ) ⊆ 𝐵 )
68 37 67 sstrd ⊢ ( ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) ∧ ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) ) → ( cf ‘ 𝐴 ) ⊆ 𝐵 )
69 68 ex ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) → ( cf ‘ 𝐴 ) ⊆ 𝐵 ) )
70 69 exlimdv ⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( ∃ 𝑓 ( 𝑓 : 𝐵 ⟶ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝐵 𝑧 ⊆ ( 𝑓 ‘ 𝑤 ) ) → ( cf ‘ 𝐴 ) ⊆ 𝐵 ) )