Metamath Proof Explorer


Theorem cflecard

Description: Cofinality is bounded by the cardinality of its argument. (Contributed by NM, 24-Apr-2004) (Revised by Mario Carneiro, 15-Sep-2013)

Ref Expression
Assertion cflecard cfAcardA

Proof

Step Hyp Ref Expression
1 cfval AOncfA=x|yx=cardyyAzAwyzw
2 df-sn cardA=x|x=cardA
3 ssid AA
4 ssid zz
5 sseq2 w=zzwzz
6 5 rspcev zAzzwAzw
7 4 6 mpan2 zAwAzw
8 7 rgen zAwAzw
9 3 8 pm3.2i AAzAwAzw
10 fveq2 y=Acardy=cardA
11 10 eqeq2d y=Ax=cardyx=cardA
12 sseq1 y=AyAAA
13 rexeq y=AwyzwwAzw
14 13 ralbidv y=AzAwyzwzAwAzw
15 12 14 anbi12d y=AyAzAwyzwAAzAwAzw
16 11 15 anbi12d y=Ax=cardyyAzAwyzwx=cardAAAzAwAzw
17 16 spcegv AOnx=cardAAAzAwAzwyx=cardyyAzAwyzw
18 9 17 mpan2i AOnx=cardAyx=cardyyAzAwyzw
19 18 ss2abdv AOnx|x=cardAx|yx=cardyyAzAwyzw
20 2 19 eqsstrid AOncardAx|yx=cardyyAzAwyzw
21 intss cardAx|yx=cardyyAzAwyzwx|yx=cardyyAzAwyzwcardA
22 20 21 syl AOnx|yx=cardyyAzAwyzwcardA
23 fvex cardAV
24 23 intsn cardA=cardA
25 22 24 sseqtrdi AOnx|yx=cardyyAzAwyzwcardA
26 1 25 eqsstrd AOncfAcardA
27 cff cf:OnOn
28 27 fdmi domcf=On
29 28 eleq2i AdomcfAOn
30 ndmfv ¬AdomcfcfA=
31 29 30 sylnbir ¬AOncfA=
32 0ss cardA
33 31 32 eqsstrdi ¬AOncfAcardA
34 26 33 pm2.61i cfAcardA