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 A On cf A = A =

Proof

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