This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- ( -. A e. Fin -> A. n e. _om E. x ( x C_ A /\ x ~~ n ) )

Proof

Step Hyp Ref Expression
1 breq2 
 |-  ( n = (/) -> ( x ~~ n <-> x ~~ (/) ) )
2 1 anbi2d 
 |-  ( n = (/) -> ( ( x C_ A /\ x ~~ n ) <-> ( x C_ A /\ x ~~ (/) ) ) )
3 2 exbidv 
 |-  ( n = (/) -> ( E. x ( x C_ A /\ x ~~ n ) <-> E. x ( x C_ A /\ x ~~ (/) ) ) )
4 breq2 
 |-  ( n = m -> ( x ~~ n <-> x ~~ m ) )
5 4 anbi2d 
 |-  ( n = m -> ( ( x C_ A /\ x ~~ n ) <-> ( x C_ A /\ x ~~ m ) ) )
6 5 exbidv 
 |-  ( n = m -> ( E. x ( x C_ A /\ x ~~ n ) <-> E. x ( x C_ A /\ x ~~ m ) ) )
7 sseq1 
 |-  ( x = y -> ( x C_ A <-> y C_ A ) )
8 7 adantl 
 |-  ( ( n = suc m /\ x = y ) -> ( x C_ A <-> y C_ A ) )
9 breq1 
 |-  ( x = y -> ( x ~~ n <-> y ~~ n ) )
10 breq2 
 |-  ( n = suc m -> ( y ~~ n <-> y ~~ suc m ) )
11 9 10 sylan9bbr 
 |-  ( ( n = suc m /\ x = y ) -> ( x ~~ n <-> y ~~ suc m ) )
12 8 11 anbi12d 
 |-  ( ( n = suc m /\ x = y ) -> ( ( x C_ A /\ x ~~ n ) <-> ( y C_ A /\ y ~~ suc m ) ) )
13 12 cbvexdvaw 
 |-  ( n = suc m -> ( E. x ( x C_ A /\ x ~~ n ) <-> E. y ( y C_ A /\ y ~~ suc m ) ) )
14 0ss 
 |-  (/) C_ A
15 peano1 
 |-  (/) e. _om
16 enrefnn 
 |-  ( (/) e. _om -> (/) ~~ (/) )
17 15 16 ax-mp 
 |-  (/) ~~ (/)
18 0ex 
 |-  (/) e. _V
19 sseq1 
 |-  ( x = (/) -> ( x C_ A <-> (/) C_ A ) )
20 breq1 
 |-  ( x = (/) -> ( x ~~ (/) <-> (/) ~~ (/) ) )
21 19 20 anbi12d 
 |-  ( x = (/) -> ( ( x C_ A /\ x ~~ (/) ) <-> ( (/) C_ A /\ (/) ~~ (/) ) ) )
22 18 21 spcev 
 |-  ( ( (/) C_ A /\ (/) ~~ (/) ) -> E. x ( x C_ A /\ x ~~ (/) ) )
23 14 17 22 mp2an 
 |-  E. x ( x C_ A /\ x ~~ (/) )
24 23 a1i 
 |-  ( -. A e. Fin -> E. x ( x C_ A /\ x ~~ (/) ) )
25 ssdif0 
 |-  ( A C_ x <-> ( A \ x ) = (/) )
26 eqss 
 |-  ( x = A <-> ( x C_ A /\ A C_ x ) )
27 breq1 
 |-  ( x = A -> ( x ~~ m <-> A ~~ m ) )
28 27 biimpa 
 |-  ( ( x = A /\ x ~~ m ) -> A ~~ m )
29 rspe 
 |-  ( ( m e. _om /\ A ~~ m ) -> E. m e. _om A ~~ m )
30 28 29 sylan2 
 |-  ( ( m e. _om /\ ( x = A /\ x ~~ m ) ) -> E. m e. _om A ~~ m )
31 isfi 
 |-  ( A e. Fin <-> E. m e. _om A ~~ m )
32 30 31 sylibr 
 |-  ( ( m e. _om /\ ( x = A /\ x ~~ m ) ) -> A e. Fin )
33 32 expcom 
 |-  ( ( x = A /\ x ~~ m ) -> ( m e. _om -> A e. Fin ) )
34 26 33 sylanbr 
 |-  ( ( ( x C_ A /\ A C_ x ) /\ x ~~ m ) -> ( m e. _om -> A e. Fin ) )
35 34 ex 
 |-  ( ( x C_ A /\ A C_ x ) -> ( x ~~ m -> ( m e. _om -> A e. Fin ) ) )
36 25 35 sylan2br 
 |-  ( ( x C_ A /\ ( A \ x ) = (/) ) -> ( x ~~ m -> ( m e. _om -> A e. Fin ) ) )
37 36 expcom 
 |-  ( ( A \ x ) = (/) -> ( x C_ A -> ( x ~~ m -> ( m e. _om -> A e. Fin ) ) ) )
38 37 3impd 
 |-  ( ( A \ x ) = (/) -> ( ( x C_ A /\ x ~~ m /\ m e. _om ) -> A e. Fin ) )
39 38 com12 
 |-  ( ( x C_ A /\ x ~~ m /\ m e. _om ) -> ( ( A \ x ) = (/) -> A e. Fin ) )
40 39 con3d 
 |-  ( ( x C_ A /\ x ~~ m /\ m e. _om ) -> ( -. A e. Fin -> -. ( A \ x ) = (/) ) )
41 bren 
 |-  ( x ~~ m <-> E. f f : x -1-1-onto-> m )
42 neq0 
 |-  ( -. ( A \ x ) = (/) <-> E. z z e. ( A \ x ) )
43 eldifi 
 |-  ( z e. ( A \ x ) -> z e. A )
44 43 snssd 
 |-  ( z e. ( A \ x ) -> { z } C_ A )
45 unss 
 |-  ( ( x C_ A /\ { z } C_ A ) <-> ( x u. { z } ) C_ A )
46 45 biimpi 
 |-  ( ( x C_ A /\ { z } C_ A ) -> ( x u. { z } ) C_ A )
47 44 46 sylan2 
 |-  ( ( x C_ A /\ z e. ( A \ x ) ) -> ( x u. { z } ) C_ A )
48 47 ad2ant2r 
 |-  ( ( ( x C_ A /\ f : x -1-1-onto-> m ) /\ ( z e. ( A \ x ) /\ m e. _om ) ) -> ( x u. { z } ) C_ A )
49 vex 
 |-  z e. _V
50 vex 
 |-  m e. _V
51 49 50 f1osn 
 |-  { <. z , m >. } : { z } -1-1-onto-> { m }
52 51 jctr 
 |-  ( f : x -1-1-onto-> m -> ( f : x -1-1-onto-> m /\ { <. z , m >. } : { z } -1-1-onto-> { m } ) )
53 eldifn 
 |-  ( z e. ( A \ x ) -> -. z e. x )
54 disjsn 
 |-  ( ( x i^i { z } ) = (/) <-> -. z e. x )
55 53 54 sylibr 
 |-  ( z e. ( A \ x ) -> ( x i^i { z } ) = (/) )
56 nnord 
 |-  ( m e. _om -> Ord m )
57 orddisj 
 |-  ( Ord m -> ( m i^i { m } ) = (/) )
58 56 57 syl 
 |-  ( m e. _om -> ( m i^i { m } ) = (/) )
59 55 58 anim12i 
 |-  ( ( z e. ( A \ x ) /\ m e. _om ) -> ( ( x i^i { z } ) = (/) /\ ( m i^i { m } ) = (/) ) )
60 f1oun 
 |-  ( ( ( f : x -1-1-onto-> m /\ { <. z , m >. } : { z } -1-1-onto-> { m } ) /\ ( ( x i^i { z } ) = (/) /\ ( m i^i { m } ) = (/) ) ) -> ( f u. { <. z , m >. } ) : ( x u. { z } ) -1-1-onto-> ( m u. { m } ) )
61 52 59 60 syl2an 
 |-  ( ( f : x -1-1-onto-> m /\ ( z e. ( A \ x ) /\ m e. _om ) ) -> ( f u. { <. z , m >. } ) : ( x u. { z } ) -1-1-onto-> ( m u. { m } ) )
62 df-suc 
 |-  suc m = ( m u. { m } )
63 f1oeq3 
 |-  ( suc m = ( m u. { m } ) -> ( ( f u. { <. z , m >. } ) : ( x u. { z } ) -1-1-onto-> suc m <-> ( f u. { <. z , m >. } ) : ( x u. { z } ) -1-1-onto-> ( m u. { m } ) ) )
64 62 63 ax-mp 
 |-  ( ( f u. { <. z , m >. } ) : ( x u. { z } ) -1-1-onto-> suc m <-> ( f u. { <. z , m >. } ) : ( x u. { z } ) -1-1-onto-> ( m u. { m } ) )
65 vex 
 |-  f e. _V
66 snex 
 |-  { <. z , m >. } e. _V
67 65 66 unex 
 |-  ( f u. { <. z , m >. } ) e. _V
68 f1oeq1 
 |-  ( g = ( f u. { <. z , m >. } ) -> ( g : ( x u. { z } ) -1-1-onto-> suc m <-> ( f u. { <. z , m >. } ) : ( x u. { z } ) -1-1-onto-> suc m ) )
69 67 68 spcev 
 |-  ( ( f u. { <. z , m >. } ) : ( x u. { z } ) -1-1-onto-> suc m -> E. g g : ( x u. { z } ) -1-1-onto-> suc m )
70 bren 
 |-  ( ( x u. { z } ) ~~ suc m <-> E. g g : ( x u. { z } ) -1-1-onto-> suc m )
71 69 70 sylibr 
 |-  ( ( f u. { <. z , m >. } ) : ( x u. { z } ) -1-1-onto-> suc m -> ( x u. { z } ) ~~ suc m )
72 64 71 sylbir 
 |-  ( ( f u. { <. z , m >. } ) : ( x u. { z } ) -1-1-onto-> ( m u. { m } ) -> ( x u. { z } ) ~~ suc m )
73 61 72 syl 
 |-  ( ( f : x -1-1-onto-> m /\ ( z e. ( A \ x ) /\ m e. _om ) ) -> ( x u. { z } ) ~~ suc m )
74 73 adantll 
 |-  ( ( ( x C_ A /\ f : x -1-1-onto-> m ) /\ ( z e. ( A \ x ) /\ m e. _om ) ) -> ( x u. { z } ) ~~ suc m )
75 vex 
 |-  x e. _V
76 snex 
 |-  { z } e. _V
77 75 76 unex 
 |-  ( x u. { z } ) e. _V
78 sseq1 
 |-  ( y = ( x u. { z } ) -> ( y C_ A <-> ( x u. { z } ) C_ A ) )
79 breq1 
 |-  ( y = ( x u. { z } ) -> ( y ~~ suc m <-> ( x u. { z } ) ~~ suc m ) )
80 78 79 anbi12d 
 |-  ( y = ( x u. { z } ) -> ( ( y C_ A /\ y ~~ suc m ) <-> ( ( x u. { z } ) C_ A /\ ( x u. { z } ) ~~ suc m ) ) )
81 77 80 spcev 
 |-  ( ( ( x u. { z } ) C_ A /\ ( x u. { z } ) ~~ suc m ) -> E. y ( y C_ A /\ y ~~ suc m ) )
82 48 74 81 syl2anc 
 |-  ( ( ( x C_ A /\ f : x -1-1-onto-> m ) /\ ( z e. ( A \ x ) /\ m e. _om ) ) -> E. y ( y C_ A /\ y ~~ suc m ) )
83 82 expcom 
 |-  ( ( z e. ( A \ x ) /\ m e. _om ) -> ( ( x C_ A /\ f : x -1-1-onto-> m ) -> E. y ( y C_ A /\ y ~~ suc m ) ) )
84 83 ex 
 |-  ( z e. ( A \ x ) -> ( m e. _om -> ( ( x C_ A /\ f : x -1-1-onto-> m ) -> E. y ( y C_ A /\ y ~~ suc m ) ) ) )
85 84 exlimiv 
 |-  ( E. z z e. ( A \ x ) -> ( m e. _om -> ( ( x C_ A /\ f : x -1-1-onto-> m ) -> E. y ( y C_ A /\ y ~~ suc m ) ) ) )
86 42 85 sylbi 
 |-  ( -. ( A \ x ) = (/) -> ( m e. _om -> ( ( x C_ A /\ f : x -1-1-onto-> m ) -> E. y ( y C_ A /\ y ~~ suc m ) ) ) )
87 86 com13 
 |-  ( ( x C_ A /\ f : x -1-1-onto-> m ) -> ( m e. _om -> ( -. ( A \ x ) = (/) -> E. y ( y C_ A /\ y ~~ suc m ) ) ) )
88 87 expcom 
 |-  ( f : x -1-1-onto-> m -> ( x C_ A -> ( m e. _om -> ( -. ( A \ x ) = (/) -> E. y ( y C_ A /\ y ~~ suc m ) ) ) ) )
89 88 exlimiv 
 |-  ( E. f f : x -1-1-onto-> m -> ( x C_ A -> ( m e. _om -> ( -. ( A \ x ) = (/) -> E. y ( y C_ A /\ y ~~ suc m ) ) ) ) )
90 41 89 sylbi 
 |-  ( x ~~ m -> ( x C_ A -> ( m e. _om -> ( -. ( A \ x ) = (/) -> E. y ( y C_ A /\ y ~~ suc m ) ) ) ) )
91 90 3imp21 
 |-  ( ( x C_ A /\ x ~~ m /\ m e. _om ) -> ( -. ( A \ x ) = (/) -> E. y ( y C_ A /\ y ~~ suc m ) ) )
92 40 91 syld 
 |-  ( ( x C_ A /\ x ~~ m /\ m e. _om ) -> ( -. A e. Fin -> E. y ( y C_ A /\ y ~~ suc m ) ) )
93 92 3expia 
 |-  ( ( x C_ A /\ x ~~ m ) -> ( m e. _om -> ( -. A e. Fin -> E. y ( y C_ A /\ y ~~ suc m ) ) ) )
94 93 exlimiv 
 |-  ( E. x ( x C_ A /\ x ~~ m ) -> ( m e. _om -> ( -. A e. Fin -> E. y ( y C_ A /\ y ~~ suc m ) ) ) )
95 94 com3l 
 |-  ( m e. _om -> ( -. A e. Fin -> ( E. x ( x C_ A /\ x ~~ m ) -> E. y ( y C_ A /\ y ~~ suc m ) ) ) )
96 3 6 13 24 95 finds2 
 |-  ( n e. _om -> ( -. A e. Fin -> E. x ( x C_ A /\ x ~~ n ) ) )
97 96 com12 
 |-  ( -. A e. Fin -> ( n e. _om -> E. x ( x C_ A /\ x ~~ n ) ) )
98 97 ralrimiv 
 |-  ( -. A e. Fin -> A. n e. _om E. x ( x C_ A /\ x ~~ n ) )