Metamath Proof Explorer

Theorem cfeq0

Description: Only the ordinal zero has cofinality zero. (Contributed by NM, 24-Apr-2004) (Revised by Mario Carneiro, 12-Feb-2013)

Ref Expression
Assertion cfeq0 ( 𝐴 ∈ On → ( ( cf ‘ 𝐴 ) = ∅ ↔ 𝐴 = ∅ ) )

Proof

Step Hyp Ref Expression
1 cfval ⊢ ( 𝐴 ∈ On → ( cf ‘ 𝐴 ) = ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } )
2 1 eqeq1d ⊢ ( 𝐴 ∈ On → ( ( cf ‘ 𝐴 ) = ∅ ↔ ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } = ∅ ) )
3 vex ⊢ 𝑣 ∈ V
4 eqeq1 ⊢ ( 𝑥 = 𝑣 → ( 𝑥 = ( card ‘ 𝑦 ) ↔ 𝑣 = ( card ‘ 𝑦 ) ) )
5 4 anbi1d ⊢ ( 𝑥 = 𝑣 → ( ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) ↔ ( 𝑣 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) ) )
6 5 exbidv ⊢ ( 𝑥 = 𝑣 → ( ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) ↔ ∃ 𝑦 ( 𝑣 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) ) )
7 3 6 elab ⊢ ( 𝑣 ∈ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } ↔ ∃ 𝑦 ( 𝑣 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) )
8 fveq2 ⊢ ( 𝑣 = ( card ‘ 𝑦 ) → ( card ‘ 𝑣 ) = ( card ‘ ( card ‘ 𝑦 ) ) )
9 cardidm ⊢ ( card ‘ ( card ‘ 𝑦 ) ) = ( card ‘ 𝑦 )
10 8 9 eqtrdi ⊢ ( 𝑣 = ( card ‘ 𝑦 ) → ( card ‘ 𝑣 ) = ( card ‘ 𝑦 ) )
11 eqeq2 ⊢ ( 𝑣 = ( card ‘ 𝑦 ) → ( ( card ‘ 𝑣 ) = 𝑣 ↔ ( card ‘ 𝑣 ) = ( card ‘ 𝑦 ) ) )
12 10 11 mpbird ⊢ ( 𝑣 = ( card ‘ 𝑦 ) → ( card ‘ 𝑣 ) = 𝑣 )
13 12 adantr ⊢ ( ( 𝑣 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) → ( card ‘ 𝑣 ) = 𝑣 )
14 13 exlimiv ⊢ ( ∃ 𝑦 ( 𝑣 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) → ( card ‘ 𝑣 ) = 𝑣 )
15 7 14 sylbi ⊢ ( 𝑣 ∈ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } → ( card ‘ 𝑣 ) = 𝑣 )
16 cardon ⊢ ( card ‘ 𝑣 ) ∈ On
17 15 16 eqeltrrdi ⊢ ( 𝑣 ∈ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } → 𝑣 ∈ On )
18 17 ssriv ⊢ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } ⊆ On
19 onint0 ⊢ ( { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } ⊆ On → ( ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } = ∅ ↔ ∅ ∈ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } ) )
20 18 19 ax-mp ⊢ ( ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } = ∅ ↔ ∅ ∈ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } )
21 0ex ⊢ ∅ ∈ V
22 eqeq1 ⊢ ( 𝑥 = ∅ → ( 𝑥 = ( card ‘ 𝑦 ) ↔ ∅ = ( card ‘ 𝑦 ) ) )
23 22 anbi1d ⊢ ( 𝑥 = ∅ → ( ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) ↔ ( ∅ = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) ) )
24 23 exbidv ⊢ ( 𝑥 = ∅ → ( ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) ↔ ∃ 𝑦 ( ∅ = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) ) )
25 21 24 elab ⊢ ( ∅ ∈ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } ↔ ∃ 𝑦 ( ∅ = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) )
26 onss ⊢ ( 𝐴 ∈ On → 𝐴 ⊆ On )
27 sstr ⊢ ( ( 𝑦 ⊆ 𝐴 ∧ 𝐴 ⊆ On ) → 𝑦 ⊆ On )
28 27 ancoms ⊢ ( ( 𝐴 ⊆ On ∧ 𝑦 ⊆ 𝐴 ) → 𝑦 ⊆ On )
29 26 28 sylan ⊢ ( ( 𝐴 ∈ On ∧ 𝑦 ⊆ 𝐴 ) → 𝑦 ⊆ On )
30 29 3adant2 ⊢ ( ( 𝐴 ∈ On ∧ ∅ = ( card ‘ 𝑦 ) ∧ 𝑦 ⊆ 𝐴 ) → 𝑦 ⊆ On )
31 30 3adant3r ⊢ ( ( 𝐴 ∈ On ∧ ∅ = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) → 𝑦 ⊆ On )
32 simp2 ⊢ ( ( 𝐴 ∈ On ∧ ∅ = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) → ∅ = ( card ‘ 𝑦 ) )
33 simp3 ⊢ ( ( 𝐴 ∈ On ∧ ∅ = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) → ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) )
34 eqcom ⊢ ( ∅ = ( card ‘ 𝑦 ) ↔ ( card ‘ 𝑦 ) = ∅ )
35 vex ⊢ 𝑦 ∈ V
36 onssnum ⊢ ( ( 𝑦 ∈ V ∧ 𝑦 ⊆ On ) → 𝑦 ∈ dom card )
37 35 36 mpan ⊢ ( 𝑦 ⊆ On → 𝑦 ∈ dom card )
38 cardnueq0 ⊢ ( 𝑦 ∈ dom card → ( ( card ‘ 𝑦 ) = ∅ ↔ 𝑦 = ∅ ) )
39 37 38 syl ⊢ ( 𝑦 ⊆ On → ( ( card ‘ 𝑦 ) = ∅ ↔ 𝑦 = ∅ ) )
40 34 39 syl5bb ⊢ ( 𝑦 ⊆ On → ( ∅ = ( card ‘ 𝑦 ) ↔ 𝑦 = ∅ ) )
41 40 biimpa ⊢ ( ( 𝑦 ⊆ On ∧ ∅ = ( card ‘ 𝑦 ) ) → 𝑦 = ∅ )
42 sseq1 ⊢ ( 𝑦 = ∅ → ( 𝑦 ⊆ 𝐴 ↔ ∅ ⊆ 𝐴 ) )
43 rexeq ⊢ ( 𝑦 = ∅ → ( ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ↔ ∃ 𝑤 ∈ ∅ 𝑧 ⊆ 𝑤 ) )
44 43 ralbidv ⊢ ( 𝑦 = ∅ → ( ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ↔ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ ∅ 𝑧 ⊆ 𝑤 ) )
45 42 44 anbi12d ⊢ ( 𝑦 = ∅ → ( ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ↔ ( ∅ ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ ∅ 𝑧 ⊆ 𝑤 ) ) )
46 45 biimpa ⊢ ( ( 𝑦 = ∅ ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) → ( ∅ ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ ∅ 𝑧 ⊆ 𝑤 ) )
47 41 46 sylan ⊢ ( ( ( 𝑦 ⊆ On ∧ ∅ = ( card ‘ 𝑦 ) ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) → ( ∅ ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ ∅ 𝑧 ⊆ 𝑤 ) )
48 rex0 ⊢ ¬ ∃ 𝑤 ∈ ∅ 𝑧 ⊆ 𝑤
49 48 rgenw ⊢ ∀ 𝑧 ∈ 𝐴 ¬ ∃ 𝑤 ∈ ∅ 𝑧 ⊆ 𝑤
50 r19.2z ⊢ ( ( 𝐴 ≠ ∅ ∧ ∀ 𝑧 ∈ 𝐴 ¬ ∃ 𝑤 ∈ ∅ 𝑧 ⊆ 𝑤 ) → ∃ 𝑧 ∈ 𝐴 ¬ ∃ 𝑤 ∈ ∅ 𝑧 ⊆ 𝑤 )
51 49 50 mpan2 ⊢ ( 𝐴 ≠ ∅ → ∃ 𝑧 ∈ 𝐴 ¬ ∃ 𝑤 ∈ ∅ 𝑧 ⊆ 𝑤 )
52 rexnal ⊢ ( ∃ 𝑧 ∈ 𝐴 ¬ ∃ 𝑤 ∈ ∅ 𝑧 ⊆ 𝑤 ↔ ¬ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ ∅ 𝑧 ⊆ 𝑤 )
53 51 52 sylib ⊢ ( 𝐴 ≠ ∅ → ¬ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ ∅ 𝑧 ⊆ 𝑤 )
54 53 necon4ai ⊢ ( ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ ∅ 𝑧 ⊆ 𝑤 → 𝐴 = ∅ )
55 47 54 simpl2im ⊢ ( ( ( 𝑦 ⊆ On ∧ ∅ = ( card ‘ 𝑦 ) ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) → 𝐴 = ∅ )
56 31 32 33 55 syl21anc ⊢ ( ( 𝐴 ∈ On ∧ ∅ = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) → 𝐴 = ∅ )
57 56 3expib ⊢ ( 𝐴 ∈ On → ( ( ∅ = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) → 𝐴 = ∅ ) )
58 57 exlimdv ⊢ ( 𝐴 ∈ On → ( ∃ 𝑦 ( ∅ = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) → 𝐴 = ∅ ) )
59 25 58 syl5bi ⊢ ( 𝐴 ∈ On → ( ∅ ∈ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } → 𝐴 = ∅ ) )
60 20 59 syl5bi ⊢ ( 𝐴 ∈ On → ( ∩ { 𝑥 ∣ ∃ 𝑦 ( 𝑥 = ( card ‘ 𝑦 ) ∧ ( 𝑦 ⊆ 𝐴 ∧ ∀ 𝑧 ∈ 𝐴 ∃ 𝑤 ∈ 𝑦 𝑧 ⊆ 𝑤 ) ) } = ∅ → 𝐴 = ∅ ) )
61 2 60 sylbid ⊢ ( 𝐴 ∈ On → ( ( cf ‘ 𝐴 ) = ∅ → 𝐴 = ∅ ) )
62 fveq2 ⊢ ( 𝐴 = ∅ → ( cf ‘ 𝐴 ) = ( cf ‘ ∅ ) )
63 cf0 ⊢ ( cf ‘ ∅ ) = ∅
64 62 63 eqtrdi ⊢ ( 𝐴 = ∅ → ( cf ‘ 𝐴 ) = ∅ )
65 61 64 impbid1 ⊢ ( 𝐴 ∈ On → ( ( cf ‘ 𝐴 ) = ∅ ↔ 𝐴 = ∅ ) )