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 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω )
Assertion fzennn ( 𝑁 ∈ ℕ0 → ( 1 ... 𝑁 ) ≈ ( 𝐺𝑁 ) )

Proof

Step Hyp Ref Expression
1 fzennn.1 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω )
2 oveq2 ( 𝑛 = 0 → ( 1 ... 𝑛 ) = ( 1 ... 0 ) )
3 fveq2 ( 𝑛 = 0 → ( 𝐺𝑛 ) = ( 𝐺 ‘ 0 ) )
4 2 3 breq12d ( 𝑛 = 0 → ( ( 1 ... 𝑛 ) ≈ ( 𝐺𝑛 ) ↔ ( 1 ... 0 ) ≈ ( 𝐺 ‘ 0 ) ) )
5 oveq2 ( 𝑛 = 𝑚 → ( 1 ... 𝑛 ) = ( 1 ... 𝑚 ) )
6 fveq2 ( 𝑛 = 𝑚 → ( 𝐺𝑛 ) = ( 𝐺𝑚 ) )
7 5 6 breq12d ( 𝑛 = 𝑚 → ( ( 1 ... 𝑛 ) ≈ ( 𝐺𝑛 ) ↔ ( 1 ... 𝑚 ) ≈ ( 𝐺𝑚 ) ) )
8 oveq2 ( 𝑛 = ( 𝑚 + 1 ) → ( 1 ... 𝑛 ) = ( 1 ... ( 𝑚 + 1 ) ) )
9 fveq2 ( 𝑛 = ( 𝑚 + 1 ) → ( 𝐺𝑛 ) = ( 𝐺 ‘ ( 𝑚 + 1 ) ) )
10 8 9 breq12d ( 𝑛 = ( 𝑚 + 1 ) → ( ( 1 ... 𝑛 ) ≈ ( 𝐺𝑛 ) ↔ ( 1 ... ( 𝑚 + 1 ) ) ≈ ( 𝐺 ‘ ( 𝑚 + 1 ) ) ) )
11 oveq2 ( 𝑛 = 𝑁 → ( 1 ... 𝑛 ) = ( 1 ... 𝑁 ) )
12 fveq2 ( 𝑛 = 𝑁 → ( 𝐺𝑛 ) = ( 𝐺𝑁 ) )
13 11 12 breq12d ( 𝑛 = 𝑁 → ( ( 1 ... 𝑛 ) ≈ ( 𝐺𝑛 ) ↔ ( 1 ... 𝑁 ) ≈ ( 𝐺𝑁 ) ) )
14 0ex ∅ ∈ V
15 14 enref ∅ ≈ ∅
16 fz10 ( 1 ... 0 ) = ∅
17 0z 0 ∈ ℤ
18 17 1 om2uzf1oi 𝐺 : ω –1-1-onto→ ( ℤ ‘ 0 )
19 peano1 ∅ ∈ ω
20 18 19 pm3.2i ( 𝐺 : ω –1-1-onto→ ( ℤ ‘ 0 ) ∧ ∅ ∈ ω )
21 17 1 om2uz0i ( 𝐺 ‘ ∅ ) = 0
22 f1ocnvfv ( ( 𝐺 : ω –1-1-onto→ ( ℤ ‘ 0 ) ∧ ∅ ∈ ω ) → ( ( 𝐺 ‘ ∅ ) = 0 → ( 𝐺 ‘ 0 ) = ∅ ) )
23 20 21 22 mp2 ( 𝐺 ‘ 0 ) = ∅
24 15 16 23 3brtr4i ( 1 ... 0 ) ≈ ( 𝐺 ‘ 0 )
25 simpr ( ( 𝑚 ∈ ℕ0 ∧ ( 1 ... 𝑚 ) ≈ ( 𝐺𝑚 ) ) → ( 1 ... 𝑚 ) ≈ ( 𝐺𝑚 ) )
26 ovex ( 𝑚 + 1 ) ∈ V
27 fvex ( 𝐺𝑚 ) ∈ V
28 en2sn ( ( ( 𝑚 + 1 ) ∈ V ∧ ( 𝐺𝑚 ) ∈ V ) → { ( 𝑚 + 1 ) } ≈ { ( 𝐺𝑚 ) } )
29 26 27 28 mp2an { ( 𝑚 + 1 ) } ≈ { ( 𝐺𝑚 ) }
30 29 a1i ( ( 𝑚 ∈ ℕ0 ∧ ( 1 ... 𝑚 ) ≈ ( 𝐺𝑚 ) ) → { ( 𝑚 + 1 ) } ≈ { ( 𝐺𝑚 ) } )
31 fzp1disj ( ( 1 ... 𝑚 ) ∩ { ( 𝑚 + 1 ) } ) = ∅
32 31 a1i ( ( 𝑚 ∈ ℕ0 ∧ ( 1 ... 𝑚 ) ≈ ( 𝐺𝑚 ) ) → ( ( 1 ... 𝑚 ) ∩ { ( 𝑚 + 1 ) } ) = ∅ )
33 f1ocnvdm ( ( 𝐺 : ω –1-1-onto→ ( ℤ ‘ 0 ) ∧ 𝑚 ∈ ( ℤ ‘ 0 ) ) → ( 𝐺𝑚 ) ∈ ω )
34 18 33 mpan ( 𝑚 ∈ ( ℤ ‘ 0 ) → ( 𝐺𝑚 ) ∈ ω )
35 nn0uz 0 = ( ℤ ‘ 0 )
36 34 35 eleq2s ( 𝑚 ∈ ℕ0 → ( 𝐺𝑚 ) ∈ ω )
37 nnord ( ( 𝐺𝑚 ) ∈ ω → Ord ( 𝐺𝑚 ) )
38 ordirr ( Ord ( 𝐺𝑚 ) → ¬ ( 𝐺𝑚 ) ∈ ( 𝐺𝑚 ) )
39 36 37 38 3syl ( 𝑚 ∈ ℕ0 → ¬ ( 𝐺𝑚 ) ∈ ( 𝐺𝑚 ) )
40 39 adantr ( ( 𝑚 ∈ ℕ0 ∧ ( 1 ... 𝑚 ) ≈ ( 𝐺𝑚 ) ) → ¬ ( 𝐺𝑚 ) ∈ ( 𝐺𝑚 ) )
41 disjsn ( ( ( 𝐺𝑚 ) ∩ { ( 𝐺𝑚 ) } ) = ∅ ↔ ¬ ( 𝐺𝑚 ) ∈ ( 𝐺𝑚 ) )
42 40 41 sylibr ( ( 𝑚 ∈ ℕ0 ∧ ( 1 ... 𝑚 ) ≈ ( 𝐺𝑚 ) ) → ( ( 𝐺𝑚 ) ∩ { ( 𝐺𝑚 ) } ) = ∅ )
43 unen ( ( ( ( 1 ... 𝑚 ) ≈ ( 𝐺𝑚 ) ∧ { ( 𝑚 + 1 ) } ≈ { ( 𝐺𝑚 ) } ) ∧ ( ( ( 1 ... 𝑚 ) ∩ { ( 𝑚 + 1 ) } ) = ∅ ∧ ( ( 𝐺𝑚 ) ∩ { ( 𝐺𝑚 ) } ) = ∅ ) ) → ( ( 1 ... 𝑚 ) ∪ { ( 𝑚 + 1 ) } ) ≈ ( ( 𝐺𝑚 ) ∪ { ( 𝐺𝑚 ) } ) )
44 25 30 32 42 43 syl22anc ( ( 𝑚 ∈ ℕ0 ∧ ( 1 ... 𝑚 ) ≈ ( 𝐺𝑚 ) ) → ( ( 1 ... 𝑚 ) ∪ { ( 𝑚 + 1 ) } ) ≈ ( ( 𝐺𝑚 ) ∪ { ( 𝐺𝑚 ) } ) )
45 1z 1 ∈ ℤ
46 1m1e0 ( 1 − 1 ) = 0
47 46 fveq2i ( ℤ ‘ ( 1 − 1 ) ) = ( ℤ ‘ 0 )
48 35 47 eqtr4i 0 = ( ℤ ‘ ( 1 − 1 ) )
49 48 eleq2i ( 𝑚 ∈ ℕ0𝑚 ∈ ( ℤ ‘ ( 1 − 1 ) ) )
50 49 biimpi ( 𝑚 ∈ ℕ0𝑚 ∈ ( ℤ ‘ ( 1 − 1 ) ) )
51 fzsuc2 ( ( 1 ∈ ℤ ∧ 𝑚 ∈ ( ℤ ‘ ( 1 − 1 ) ) ) → ( 1 ... ( 𝑚 + 1 ) ) = ( ( 1 ... 𝑚 ) ∪ { ( 𝑚 + 1 ) } ) )
52 45 50 51 sylancr ( 𝑚 ∈ ℕ0 → ( 1 ... ( 𝑚 + 1 ) ) = ( ( 1 ... 𝑚 ) ∪ { ( 𝑚 + 1 ) } ) )
53 52 adantr ( ( 𝑚 ∈ ℕ0 ∧ ( 1 ... 𝑚 ) ≈ ( 𝐺𝑚 ) ) → ( 1 ... ( 𝑚 + 1 ) ) = ( ( 1 ... 𝑚 ) ∪ { ( 𝑚 + 1 ) } ) )
54 peano2 ( ( 𝐺𝑚 ) ∈ ω → suc ( 𝐺𝑚 ) ∈ ω )
55 36 54 syl ( 𝑚 ∈ ℕ0 → suc ( 𝐺𝑚 ) ∈ ω )
56 55 18 jctil ( 𝑚 ∈ ℕ0 → ( 𝐺 : ω –1-1-onto→ ( ℤ ‘ 0 ) ∧ suc ( 𝐺𝑚 ) ∈ ω ) )
57 17 1 om2uzsuci ( ( 𝐺𝑚 ) ∈ ω → ( 𝐺 ‘ suc ( 𝐺𝑚 ) ) = ( ( 𝐺 ‘ ( 𝐺𝑚 ) ) + 1 ) )
58 36 57 syl ( 𝑚 ∈ ℕ0 → ( 𝐺 ‘ suc ( 𝐺𝑚 ) ) = ( ( 𝐺 ‘ ( 𝐺𝑚 ) ) + 1 ) )
59 35 eleq2i ( 𝑚 ∈ ℕ0𝑚 ∈ ( ℤ ‘ 0 ) )
60 59 biimpi ( 𝑚 ∈ ℕ0𝑚 ∈ ( ℤ ‘ 0 ) )
61 f1ocnvfv2 ( ( 𝐺 : ω –1-1-onto→ ( ℤ ‘ 0 ) ∧ 𝑚 ∈ ( ℤ ‘ 0 ) ) → ( 𝐺 ‘ ( 𝐺𝑚 ) ) = 𝑚 )
62 18 60 61 sylancr ( 𝑚 ∈ ℕ0 → ( 𝐺 ‘ ( 𝐺𝑚 ) ) = 𝑚 )
63 62 oveq1d ( 𝑚 ∈ ℕ0 → ( ( 𝐺 ‘ ( 𝐺𝑚 ) ) + 1 ) = ( 𝑚 + 1 ) )
64 58 63 eqtrd ( 𝑚 ∈ ℕ0 → ( 𝐺 ‘ suc ( 𝐺𝑚 ) ) = ( 𝑚 + 1 ) )
65 f1ocnvfv ( ( 𝐺 : ω –1-1-onto→ ( ℤ ‘ 0 ) ∧ suc ( 𝐺𝑚 ) ∈ ω ) → ( ( 𝐺 ‘ suc ( 𝐺𝑚 ) ) = ( 𝑚 + 1 ) → ( 𝐺 ‘ ( 𝑚 + 1 ) ) = suc ( 𝐺𝑚 ) ) )
66 56 64 65 sylc ( 𝑚 ∈ ℕ0 → ( 𝐺 ‘ ( 𝑚 + 1 ) ) = suc ( 𝐺𝑚 ) )
67 66 adantr ( ( 𝑚 ∈ ℕ0 ∧ ( 1 ... 𝑚 ) ≈ ( 𝐺𝑚 ) ) → ( 𝐺 ‘ ( 𝑚 + 1 ) ) = suc ( 𝐺𝑚 ) )
68 df-suc suc ( 𝐺𝑚 ) = ( ( 𝐺𝑚 ) ∪ { ( 𝐺𝑚 ) } )
69 67 68 eqtrdi ( ( 𝑚 ∈ ℕ0 ∧ ( 1 ... 𝑚 ) ≈ ( 𝐺𝑚 ) ) → ( 𝐺 ‘ ( 𝑚 + 1 ) ) = ( ( 𝐺𝑚 ) ∪ { ( 𝐺𝑚 ) } ) )
70 44 53 69 3brtr4d ( ( 𝑚 ∈ ℕ0 ∧ ( 1 ... 𝑚 ) ≈ ( 𝐺𝑚 ) ) → ( 1 ... ( 𝑚 + 1 ) ) ≈ ( 𝐺 ‘ ( 𝑚 + 1 ) ) )
71 70 ex ( 𝑚 ∈ ℕ0 → ( ( 1 ... 𝑚 ) ≈ ( 𝐺𝑚 ) → ( 1 ... ( 𝑚 + 1 ) ) ≈ ( 𝐺 ‘ ( 𝑚 + 1 ) ) ) )
72 4 7 10 13 24 71 nn0ind ( 𝑁 ∈ ℕ0 → ( 1 ... 𝑁 ) ≈ ( 𝐺𝑁 ) )