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 bitrid ( 𝑦 ⊆ 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 ‘ 𝐴 ) = ∅ ↔ 𝐴 = ∅ ) )