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 ... 𝑁 ) ≈ ( ◡ 𝐺 ‘ 𝑁 ) )