Metamath Proof Explorer

Theorem fzennn

Description: The cardinality of a finite set of sequential integers. (See om2uz0i for a description of the hypothesis.) (Contributed by Mario Carneiro, 12-Feb-2013) (Revised by Mario Carneiro, 7-Mar-2014)

Ref Expression
Hypothesis fzennn.1 
|- G = ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om )
Assertion fzennn 
|- ( N e. NN0 -> ( 1 ... N ) ~~ ( `' G ` N ) )

Proof

Step Hyp Ref Expression
1 fzennn.1 
 |-  G = ( rec ( ( x e. _V |-> ( x + 1 ) ) , 0 ) |` _om )
2 oveq2 
 |-  ( n = 0 -> ( 1 ... n ) = ( 1 ... 0 ) )
3 fveq2 
 |-  ( n = 0 -> ( `' G ` n ) = ( `' G ` 0 ) )
4 2 3 breq12d 
 |-  ( n = 0 -> ( ( 1 ... n ) ~~ ( `' G ` n ) <-> ( 1 ... 0 ) ~~ ( `' G ` 0 ) ) )
5 oveq2 
 |-  ( n = m -> ( 1 ... n ) = ( 1 ... m ) )
6 fveq2 
 |-  ( n = m -> ( `' G ` n ) = ( `' G ` m ) )
7 5 6 breq12d 
 |-  ( n = m -> ( ( 1 ... n ) ~~ ( `' G ` n ) <-> ( 1 ... m ) ~~ ( `' G ` m ) ) )
8 oveq2 
 |-  ( n = ( m + 1 ) -> ( 1 ... n ) = ( 1 ... ( m + 1 ) ) )
9 fveq2 
 |-  ( n = ( m + 1 ) -> ( `' G ` n ) = ( `' G ` ( m + 1 ) ) )
10 8 9 breq12d 
 |-  ( n = ( m + 1 ) -> ( ( 1 ... n ) ~~ ( `' G ` n ) <-> ( 1 ... ( m + 1 ) ) ~~ ( `' G ` ( m + 1 ) ) ) )
11 oveq2 
 |-  ( n = N -> ( 1 ... n ) = ( 1 ... N ) )
12 fveq2 
 |-  ( n = N -> ( `' G ` n ) = ( `' G ` N ) )
13 11 12 breq12d 
 |-  ( n = N -> ( ( 1 ... n ) ~~ ( `' G ` n ) <-> ( 1 ... N ) ~~ ( `' G ` N ) ) )
14 0ex 
 |-  (/) e. _V
15 14 enref 
 |-  (/) ~~ (/)
16 fz10 
 |-  ( 1 ... 0 ) = (/)
17 0z 
 |-  0 e. ZZ
18 17 1 om2uzf1oi 
 |-  G : _om -1-1-onto-> ( ZZ>= ` 0 )
19 peano1 
 |-  (/) e. _om
20 18 19 pm3.2i 
 |-  ( G : _om -1-1-onto-> ( ZZ>= ` 0 ) /\ (/) e. _om )
21 17 1 om2uz0i 
 |-  ( G ` (/) ) = 0
22 f1ocnvfv 
 |-  ( ( G : _om -1-1-onto-> ( ZZ>= ` 0 ) /\ (/) e. _om ) -> ( ( G ` (/) ) = 0 -> ( `' G ` 0 ) = (/) ) )
23 20 21 22 mp2 
 |-  ( `' G ` 0 ) = (/)
24 15 16 23 3brtr4i 
 |-  ( 1 ... 0 ) ~~ ( `' G ` 0 )
25 simpr 
 |-  ( ( m e. NN0 /\ ( 1 ... m ) ~~ ( `' G ` m ) ) -> ( 1 ... m ) ~~ ( `' G ` m ) )
26 ovex 
 |-  ( m + 1 ) e. _V
27 fvex 
 |-  ( `' G ` m ) e. _V
28 en2sn 
 |-  ( ( ( m + 1 ) e. _V /\ ( `' G ` m ) e. _V ) -> { ( m + 1 ) } ~~ { ( `' G ` m ) } )
29 26 27 28 mp2an 
 |-  { ( m + 1 ) } ~~ { ( `' G ` m ) }
30 29 a1i 
 |-  ( ( m e. NN0 /\ ( 1 ... m ) ~~ ( `' G ` m ) ) -> { ( m + 1 ) } ~~ { ( `' G ` m ) } )
31 fzp1disj 
 |-  ( ( 1 ... m ) i^i { ( m + 1 ) } ) = (/)
32 31 a1i 
 |-  ( ( m e. NN0 /\ ( 1 ... m ) ~~ ( `' G ` m ) ) -> ( ( 1 ... m ) i^i { ( m + 1 ) } ) = (/) )
33 f1ocnvdm 
 |-  ( ( G : _om -1-1-onto-> ( ZZ>= ` 0 ) /\ m e. ( ZZ>= ` 0 ) ) -> ( `' G ` m ) e. _om )
34 18 33 mpan 
 |-  ( m e. ( ZZ>= ` 0 ) -> ( `' G ` m ) e. _om )
35 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
36 34 35 eleq2s 
 |-  ( m e. NN0 -> ( `' G ` m ) e. _om )
37 nnord 
 |-  ( ( `' G ` m ) e. _om -> Ord ( `' G ` m ) )
38 ordirr 
 |-  ( Ord ( `' G ` m ) -> -. ( `' G ` m ) e. ( `' G ` m ) )
39 36 37 38 3syl 
 |-  ( m e. NN0 -> -. ( `' G ` m ) e. ( `' G ` m ) )
40 39 adantr 
 |-  ( ( m e. NN0 /\ ( 1 ... m ) ~~ ( `' G ` m ) ) -> -. ( `' G ` m ) e. ( `' G ` m ) )
41 disjsn 
 |-  ( ( ( `' G ` m ) i^i { ( `' G ` m ) } ) = (/) <-> -. ( `' G ` m ) e. ( `' G ` m ) )
42 40 41 sylibr 
 |-  ( ( m e. NN0 /\ ( 1 ... m ) ~~ ( `' G ` m ) ) -> ( ( `' G ` m ) i^i { ( `' G ` m ) } ) = (/) )
43 unen 
 |-  ( ( ( ( 1 ... m ) ~~ ( `' G ` m ) /\ { ( m + 1 ) } ~~ { ( `' G ` m ) } ) /\ ( ( ( 1 ... m ) i^i { ( m + 1 ) } ) = (/) /\ ( ( `' G ` m ) i^i { ( `' G ` m ) } ) = (/) ) ) -> ( ( 1 ... m ) u. { ( m + 1 ) } ) ~~ ( ( `' G ` m ) u. { ( `' G ` m ) } ) )
44 25 30 32 42 43 syl22anc 
 |-  ( ( m e. NN0 /\ ( 1 ... m ) ~~ ( `' G ` m ) ) -> ( ( 1 ... m ) u. { ( m + 1 ) } ) ~~ ( ( `' G ` m ) u. { ( `' G ` m ) } ) )
45 1z 
 |-  1 e. ZZ
46 1m1e0 
 |-  ( 1 - 1 ) = 0
47 46 fveq2i 
 |-  ( ZZ>= ` ( 1 - 1 ) ) = ( ZZ>= ` 0 )
48 35 47 eqtr4i 
 |-  NN0 = ( ZZ>= ` ( 1 - 1 ) )
49 48 eleq2i 
 |-  ( m e. NN0 <-> m e. ( ZZ>= ` ( 1 - 1 ) ) )
50 49 biimpi 
 |-  ( m e. NN0 -> m e. ( ZZ>= ` ( 1 - 1 ) ) )
51 fzsuc2 
 |-  ( ( 1 e. ZZ /\ m e. ( ZZ>= ` ( 1 - 1 ) ) ) -> ( 1 ... ( m + 1 ) ) = ( ( 1 ... m ) u. { ( m + 1 ) } ) )
52 45 50 51 sylancr 
 |-  ( m e. NN0 -> ( 1 ... ( m + 1 ) ) = ( ( 1 ... m ) u. { ( m + 1 ) } ) )
53 52 adantr 
 |-  ( ( m e. NN0 /\ ( 1 ... m ) ~~ ( `' G ` m ) ) -> ( 1 ... ( m + 1 ) ) = ( ( 1 ... m ) u. { ( m + 1 ) } ) )
54 peano2 
 |-  ( ( `' G ` m ) e. _om -> suc ( `' G ` m ) e. _om )
55 36 54 syl 
 |-  ( m e. NN0 -> suc ( `' G ` m ) e. _om )
56 55 18 jctil 
 |-  ( m e. NN0 -> ( G : _om -1-1-onto-> ( ZZ>= ` 0 ) /\ suc ( `' G ` m ) e. _om ) )
57 17 1 om2uzsuci 
 |-  ( ( `' G ` m ) e. _om -> ( G ` suc ( `' G ` m ) ) = ( ( G ` ( `' G ` m ) ) + 1 ) )
58 36 57 syl 
 |-  ( m e. NN0 -> ( G ` suc ( `' G ` m ) ) = ( ( G ` ( `' G ` m ) ) + 1 ) )
59 35 eleq2i 
 |-  ( m e. NN0 <-> m e. ( ZZ>= ` 0 ) )
60 59 biimpi 
 |-  ( m e. NN0 -> m e. ( ZZ>= ` 0 ) )
61 f1ocnvfv2 
 |-  ( ( G : _om -1-1-onto-> ( ZZ>= ` 0 ) /\ m e. ( ZZ>= ` 0 ) ) -> ( G ` ( `' G ` m ) ) = m )
62 18 60 61 sylancr 
 |-  ( m e. NN0 -> ( G ` ( `' G ` m ) ) = m )
63 62 oveq1d 
 |-  ( m e. NN0 -> ( ( G ` ( `' G ` m ) ) + 1 ) = ( m + 1 ) )
64 58 63 eqtrd 
 |-  ( m e. NN0 -> ( G ` suc ( `' G ` m ) ) = ( m + 1 ) )
65 f1ocnvfv 
 |-  ( ( G : _om -1-1-onto-> ( ZZ>= ` 0 ) /\ suc ( `' G ` m ) e. _om ) -> ( ( G ` suc ( `' G ` m ) ) = ( m + 1 ) -> ( `' G ` ( m + 1 ) ) = suc ( `' G ` m ) ) )
66 56 64 65 sylc 
 |-  ( m e. NN0 -> ( `' G ` ( m + 1 ) ) = suc ( `' G ` m ) )
67 66 adantr 
 |-  ( ( m e. NN0 /\ ( 1 ... m ) ~~ ( `' G ` m ) ) -> ( `' G ` ( m + 1 ) ) = suc ( `' G ` m ) )
68 df-suc 
 |-  suc ( `' G ` m ) = ( ( `' G ` m ) u. { ( `' G ` m ) } )
69 67 68 eqtrdi 
 |-  ( ( m e. NN0 /\ ( 1 ... m ) ~~ ( `' G ` m ) ) -> ( `' G ` ( m + 1 ) ) = ( ( `' G ` m ) u. { ( `' G ` m ) } ) )
70 44 53 69 3brtr4d 
 |-  ( ( m e. NN0 /\ ( 1 ... m ) ~~ ( `' G ` m ) ) -> ( 1 ... ( m + 1 ) ) ~~ ( `' G ` ( m + 1 ) ) )
71 70 ex 
 |-  ( m e. NN0 -> ( ( 1 ... m ) ~~ ( `' G ` m ) -> ( 1 ... ( m + 1 ) ) ~~ ( `' G ` ( m + 1 ) ) ) )
72 4 7 10 13 24 71 nn0ind 
 |-  ( N e. NN0 -> ( 1 ... N ) ~~ ( `' G ` N ) )