Metamath Proof Explorer


Theorem isinfOLD

Description: Obsolete version of isinf as of 2-Jan-2025. (Contributed by Mario Carneiro, 15-Jan-2013) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion isinfOLD ¬ A Fin n ω x x A x n

Proof

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