Metamath Proof Explorer


Theorem isinf

Description: Any set that is not finite is literally infinite, in the sense that it contains subsets of arbitrarily large finite cardinality. (It cannot be proven that the set hascountably infinite subsets unless AC is invoked.) The proof does not require the Axiom of Infinity. (Contributed by Mario Carneiro, 15-Jan-2013) Avoid ax-pow . (Revised by BTernaryTau, 2-Jan-2025)

Ref Expression
Assertion isinf ¬AFinnωxxAxn

Proof

Step Hyp Ref Expression
1 breq2 n=xnx
2 1 anbi2d n=xAxnxAx
3 2 exbidv n=xxAxnxxAx
4 breq2 n=mxnxm
5 4 anbi2d n=mxAxnxAxm
6 5 exbidv n=mxxAxnxxAxm
7 sseq1 x=yxAyA
8 7 adantl n=sucmx=yxAyA
9 breq1 x=yxnyn
10 breq2 n=sucmynysucm
11 9 10 sylan9bbr n=sucmx=yxnysucm
12 8 11 anbi12d n=sucmx=yxAxnyAysucm
13 12 cbvexdvaw n=sucmxxAxnyyAysucm
14 0ss A
15 peano1 ω
16 enrefnn ω
17 15 16 ax-mp
18 0ex V
19 sseq1 x=xAA
20 breq1 x=x
21 19 20 anbi12d x=xAxA
22 18 21 spcev AxxAx
23 14 17 22 mp2an xxAx
24 23 a1i ¬AFinxxAx
25 ssdif0 AxAx=
26 eqss x=AxAAx
27 breq1 x=AxmAm
28 27 biimpa x=AxmAm
29 rspe mωAmmωAm
30 28 29 sylan2 mωx=AxmmωAm
31 isfi AFinmωAm
32 30 31 sylibr mωx=AxmAFin
33 32 expcom x=AxmmωAFin
34 26 33 sylanbr xAAxxmmωAFin
35 34 ex xAAxxmmωAFin
36 25 35 sylan2br xAAx=xmmωAFin
37 36 expcom Ax=xAxmmωAFin
38 37 3impd Ax=xAxmmωAFin
39 38 com12 xAxmmωAx=AFin
40 39 con3d xAxmmω¬AFin¬Ax=
41 bren xmff:x1-1 ontom
42 neq0 ¬Ax=zzAx
43 eldifi zAxzA
44 43 snssd zAxzA
45 unss xAzAxzA
46 45 biimpi xAzAxzA
47 44 46 sylan2 xAzAxxzA
48 47 ad2ant2r xAf:x1-1 ontomzAxmωxzA
49 vex zV
50 vex mV
51 49 50 f1osn zm:z1-1 ontom
52 51 jctr f:x1-1 ontomf:x1-1 ontomzm:z1-1 ontom
53 eldifn zAx¬zx
54 disjsn xz=¬zx
55 53 54 sylibr zAxxz=
56 nnord mωOrdm
57 orddisj Ordmmm=
58 56 57 syl mωmm=
59 55 58 anim12i zAxmωxz=mm=
60 f1oun f:x1-1 ontomzm:z1-1 ontomxz=mm=fzm:xz1-1 ontomm
61 52 59 60 syl2an f:x1-1 ontomzAxmωfzm:xz1-1 ontomm
62 df-suc sucm=mm
63 f1oeq3 sucm=mmfzm:xz1-1 ontosucmfzm:xz1-1 ontomm
64 62 63 ax-mp fzm:xz1-1 ontosucmfzm:xz1-1 ontomm
65 vex fV
66 snex zmV
67 65 66 unex fzmV
68 f1oeq1 g=fzmg:xz1-1 ontosucmfzm:xz1-1 ontosucm
69 67 68 spcev fzm:xz1-1 ontosucmgg:xz1-1 ontosucm
70 bren xzsucmgg:xz1-1 ontosucm
71 69 70 sylibr fzm:xz1-1 ontosucmxzsucm
72 64 71 sylbir fzm:xz1-1 ontommxzsucm
73 61 72 syl f:x1-1 ontomzAxmωxzsucm
74 73 adantll xAf:x1-1 ontomzAxmωxzsucm
75 vex xV
76 snex zV
77 75 76 unex xzV
78 sseq1 y=xzyAxzA
79 breq1 y=xzysucmxzsucm
80 78 79 anbi12d y=xzyAysucmxzAxzsucm
81 77 80 spcev xzAxzsucmyyAysucm
82 48 74 81 syl2anc xAf:x1-1 ontomzAxmωyyAysucm
83 82 expcom zAxmωxAf:x1-1 ontomyyAysucm
84 83 ex zAxmωxAf:x1-1 ontomyyAysucm
85 84 exlimiv zzAxmωxAf:x1-1 ontomyyAysucm
86 42 85 sylbi ¬Ax=mωxAf:x1-1 ontomyyAysucm
87 86 com13 xAf:x1-1 ontommω¬Ax=yyAysucm
88 87 expcom f:x1-1 ontomxAmω¬Ax=yyAysucm
89 88 exlimiv ff:x1-1 ontomxAmω¬Ax=yyAysucm
90 41 89 sylbi xmxAmω¬Ax=yyAysucm
91 90 3imp21 xAxmmω¬Ax=yyAysucm
92 40 91 syld xAxmmω¬AFinyyAysucm
93 92 3expia xAxmmω¬AFinyyAysucm
94 93 exlimiv xxAxmmω¬AFinyyAysucm
95 94 com3l mω¬AFinxxAxmyyAysucm
96 3 6 13 24 95 finds2 nω¬AFinxxAxn
97 96 com12 ¬AFinnωxxAxn
98 97 ralrimiv ¬AFinnωxxAxn