Metamath Proof Explorer

Theorem fz1isolem

Description: Lemma for fz1iso . (Contributed by Mario Carneiro, 2-Apr-2014)

Ref Expression
Hypotheses fz1iso.1 ⊢ G = rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω
fz1iso.2 ⊢ B = ℕ ∩ < -1 A + 1
fz1iso.3 ⊢ C = ω ∩ G -1 ⁡ A + 1
fz1iso.4 ⊢ O = OrdIso R A
Assertion fz1isolem ⊢ R Or A ∧ A ∈ Fin → ∃ f f Isom < , R 1 … A A

Proof

Step Hyp Ref Expression
1 fz1iso.1 ⊢ G = rec ⁡ n ∈ V ⟼ n + 1 1 ↾ ω
2 fz1iso.2 ⊢ B = ℕ ∩ < -1 A + 1
3 fz1iso.3 ⊢ C = ω ∩ G -1 ⁡ A + 1
4 fz1iso.4 ⊢ O = OrdIso R A
5 hashcl ⊢ A ∈ Fin → A ∈ ℕ 0
6 5 adantl ⊢ R Or A ∧ A ∈ Fin → A ∈ ℕ 0
7 nnuz ⊢ ℕ = ℤ ≥ 1
8 1z ⊢ 1 ∈ ℤ
9 8 1 om2uzisoi ⊢ G Isom E , < ω ℤ ≥ 1
10 isoeq5 ⊢ ℕ = ℤ ≥ 1 → G Isom E , < ω ℕ ↔ G Isom E , < ω ℤ ≥ 1
11 9 10 mpbiri ⊢ ℕ = ℤ ≥ 1 → G Isom E , < ω ℕ
12 7 11 ax-mp ⊢ G Isom E , < ω ℕ
13 isocnv ⊢ G Isom E , < ω ℕ → G -1 Isom < , E ℕ ω
14 12 13 ax-mp ⊢ G -1 Isom < , E ℕ ω
15 nn0p1nn ⊢ A ∈ ℕ 0 → A + 1 ∈ ℕ
16 fvex ⊢ G -1 ⁡ A + 1 ∈ V
17 16 epini ⊢ E -1 G -1 ⁡ A + 1 = G -1 ⁡ A + 1
18 17 ineq2i ⊢ ω ∩ E -1 G -1 ⁡ A + 1 = ω ∩ G -1 ⁡ A + 1
19 3 18 eqtr4i ⊢ C = ω ∩ E -1 G -1 ⁡ A + 1
20 2 19 isoini2 ⊢ G -1 Isom < , E ℕ ω ∧ A + 1 ∈ ℕ → G -1 ↾ B Isom < , E B C
21 14 15 20 sylancr ⊢ A ∈ ℕ 0 → G -1 ↾ B Isom < , E B C
22 6 21 syl ⊢ R Or A ∧ A ∈ Fin → G -1 ↾ B Isom < , E B C
23 nnz ⊢ f ∈ ℕ → f ∈ ℤ
24 6 nn0zd ⊢ R Or A ∧ A ∈ Fin → A ∈ ℤ
25 eluz ⊢ f ∈ ℤ ∧ A ∈ ℤ → A ∈ ℤ ≥ f ↔ f ≤ A
26 23 24 25 syl2anr ⊢ R Or A ∧ A ∈ Fin ∧ f ∈ ℕ → A ∈ ℤ ≥ f ↔ f ≤ A
27 zleltp1 ⊢ f ∈ ℤ ∧ A ∈ ℤ → f ≤ A ↔ f < A + 1
28 23 24 27 syl2anr ⊢ R Or A ∧ A ∈ Fin ∧ f ∈ ℕ → f ≤ A ↔ f < A + 1
29 ovex ⊢ A + 1 ∈ V
30 vex ⊢ f ∈ V
31 30 eliniseg ⊢ A + 1 ∈ V → f ∈ < -1 A + 1 ↔ f < A + 1
32 29 31 ax-mp ⊢ f ∈ < -1 A + 1 ↔ f < A + 1
33 28 32 syl6bbr ⊢ R Or A ∧ A ∈ Fin ∧ f ∈ ℕ → f ≤ A ↔ f ∈ < -1 A + 1
34 26 33 bitr2d ⊢ R Or A ∧ A ∈ Fin ∧ f ∈ ℕ → f ∈ < -1 A + 1 ↔ A ∈ ℤ ≥ f
35 34 pm5.32da ⊢ R Or A ∧ A ∈ Fin → f ∈ ℕ ∧ f ∈ < -1 A + 1 ↔ f ∈ ℕ ∧ A ∈ ℤ ≥ f
36 2 elin2 ⊢ f ∈ B ↔ f ∈ ℕ ∧ f ∈ < -1 A + 1
37 elfzuzb ⊢ f ∈ 1 … A ↔ f ∈ ℤ ≥ 1 ∧ A ∈ ℤ ≥ f
38 elnnuz ⊢ f ∈ ℕ ↔ f ∈ ℤ ≥ 1
39 38 anbi1i ⊢ f ∈ ℕ ∧ A ∈ ℤ ≥ f ↔ f ∈ ℤ ≥ 1 ∧ A ∈ ℤ ≥ f
40 37 39 bitr4i ⊢ f ∈ 1 … A ↔ f ∈ ℕ ∧ A ∈ ℤ ≥ f
41 35 36 40 3bitr4g ⊢ R Or A ∧ A ∈ Fin → f ∈ B ↔ f ∈ 1 … A
42 41 eqrdv ⊢ R Or A ∧ A ∈ Fin → B = 1 … A
43 isoeq4 ⊢ B = 1 … A → G -1 ↾ B Isom < , E B C ↔ G -1 ↾ B Isom < , E 1 … A C
44 42 43 syl ⊢ R Or A ∧ A ∈ Fin → G -1 ↾ B Isom < , E B C ↔ G -1 ↾ B Isom < , E 1 … A C
45 22 44 mpbid ⊢ R Or A ∧ A ∈ Fin → G -1 ↾ B Isom < , E 1 … A C
46 4 oion ⊢ A ∈ Fin → dom ⁡ O ∈ On
47 46 adantl ⊢ R Or A ∧ A ∈ Fin → dom ⁡ O ∈ On
48 simpr ⊢ R Or A ∧ A ∈ Fin → A ∈ Fin
49 wofi ⊢ R Or A ∧ A ∈ Fin → R We A
50 4 oien ⊢ A ∈ Fin ∧ R We A → dom ⁡ O ≈ A
51 48 49 50 syl2anc ⊢ R Or A ∧ A ∈ Fin → dom ⁡ O ≈ A
52 enfii ⊢ A ∈ Fin ∧ dom ⁡ O ≈ A → dom ⁡ O ∈ Fin
53 48 51 52 syl2anc ⊢ R Or A ∧ A ∈ Fin → dom ⁡ O ∈ Fin
54 47 53 elind ⊢ R Or A ∧ A ∈ Fin → dom ⁡ O ∈ On ∩ Fin
55 onfin2 ⊢ ω = On ∩ Fin
56 54 55 eleqtrrdi ⊢ R Or A ∧ A ∈ Fin → dom ⁡ O ∈ ω
57 eqid ⊢ rec ⁡ n ∈ V ⟼ n + 1 0 ↾ ω = rec ⁡ n ∈ V ⟼ n + 1 0 ↾ ω
58 0z ⊢ 0 ∈ ℤ
59 1 57 8 58 uzrdgxfr ⊢ dom ⁡ O ∈ ω → G ⁡ dom ⁡ O = rec ⁡ n ∈ V ⟼ n + 1 0 ↾ ω ⁡ dom ⁡ O + 1 - 0
60 1m0e1 ⊢ 1 − 0 = 1
61 60 oveq2i ⊢ rec ⁡ n ∈ V ⟼ n + 1 0 ↾ ω ⁡ dom ⁡ O + 1 - 0 = rec ⁡ n ∈ V ⟼ n + 1 0 ↾ ω ⁡ dom ⁡ O + 1
62 59 61 syl6eq ⊢ dom ⁡ O ∈ ω → G ⁡ dom ⁡ O = rec ⁡ n ∈ V ⟼ n + 1 0 ↾ ω ⁡ dom ⁡ O + 1
63 56 62 syl ⊢ R Or A ∧ A ∈ Fin → G ⁡ dom ⁡ O = rec ⁡ n ∈ V ⟼ n + 1 0 ↾ ω ⁡ dom ⁡ O + 1
64 51 ensymd ⊢ R Or A ∧ A ∈ Fin → A ≈ dom ⁡ O
65 cardennn ⊢ A ≈ dom ⁡ O ∧ dom ⁡ O ∈ ω → card ⁡ A = dom ⁡ O
66 64 56 65 syl2anc ⊢ R Or A ∧ A ∈ Fin → card ⁡ A = dom ⁡ O
67 66 fveq2d ⊢ R Or A ∧ A ∈ Fin → rec ⁡ n ∈ V ⟼ n + 1 0 ↾ ω ⁡ card ⁡ A = rec ⁡ n ∈ V ⟼ n + 1 0 ↾ ω ⁡ dom ⁡ O
68 57 hashgval ⊢ A ∈ Fin → rec ⁡ n ∈ V ⟼ n + 1 0 ↾ ω ⁡ card ⁡ A = A
69 68 adantl ⊢ R Or A ∧ A ∈ Fin → rec ⁡ n ∈ V ⟼ n + 1 0 ↾ ω ⁡ card ⁡ A = A
70 67 69 eqtr3d ⊢ R Or A ∧ A ∈ Fin → rec ⁡ n ∈ V ⟼ n + 1 0 ↾ ω ⁡ dom ⁡ O = A
71 70 oveq1d ⊢ R Or A ∧ A ∈ Fin → rec ⁡ n ∈ V ⟼ n + 1 0 ↾ ω ⁡ dom ⁡ O + 1 = A + 1
72 63 71 eqtrd ⊢ R Or A ∧ A ∈ Fin → G ⁡ dom ⁡ O = A + 1
73 72 fveq2d ⊢ R Or A ∧ A ∈ Fin → G -1 ⁡ G ⁡ dom ⁡ O = G -1 ⁡ A + 1
74 isof1o ⊢ G Isom E , < ω ℕ → G : ω ⟶ 1-1 onto ℕ
75 12 74 ax-mp ⊢ G : ω ⟶ 1-1 onto ℕ
76 f1ocnvfv1 ⊢ G : ω ⟶ 1-1 onto ℕ ∧ dom ⁡ O ∈ ω → G -1 ⁡ G ⁡ dom ⁡ O = dom ⁡ O
77 75 56 76 sylancr ⊢ R Or A ∧ A ∈ Fin → G -1 ⁡ G ⁡ dom ⁡ O = dom ⁡ O
78 73 77 eqtr3d ⊢ R Or A ∧ A ∈ Fin → G -1 ⁡ A + 1 = dom ⁡ O
79 78 ineq2d ⊢ R Or A ∧ A ∈ Fin → ω ∩ G -1 ⁡ A + 1 = ω ∩ dom ⁡ O
80 ordom ⊢ Ord ⁡ ω
81 ordelss ⊢ Ord ⁡ ω ∧ dom ⁡ O ∈ ω → dom ⁡ O ⊆ ω
82 80 56 81 sylancr ⊢ R Or A ∧ A ∈ Fin → dom ⁡ O ⊆ ω
83 sseqin2 ⊢ dom ⁡ O ⊆ ω ↔ ω ∩ dom ⁡ O = dom ⁡ O
84 82 83 sylib ⊢ R Or A ∧ A ∈ Fin → ω ∩ dom ⁡ O = dom ⁡ O
85 79 84 eqtrd ⊢ R Or A ∧ A ∈ Fin → ω ∩ G -1 ⁡ A + 1 = dom ⁡ O
86 3 85 syl5eq ⊢ R Or A ∧ A ∈ Fin → C = dom ⁡ O
87 isoeq5 ⊢ C = dom ⁡ O → G -1 ↾ B Isom < , E 1 … A C ↔ G -1 ↾ B Isom < , E 1 … A dom ⁡ O
88 86 87 syl ⊢ R Or A ∧ A ∈ Fin → G -1 ↾ B Isom < , E 1 … A C ↔ G -1 ↾ B Isom < , E 1 … A dom ⁡ O
89 45 88 mpbid ⊢ R Or A ∧ A ∈ Fin → G -1 ↾ B Isom < , E 1 … A dom ⁡ O
90 4 oiiso ⊢ A ∈ Fin ∧ R We A → O Isom E , R dom ⁡ O A
91 48 49 90 syl2anc ⊢ R Or A ∧ A ∈ Fin → O Isom E , R dom ⁡ O A
92 isotr ⊢ G -1 ↾ B Isom < , E 1 … A dom ⁡ O ∧ O Isom E , R dom ⁡ O A → O ∘ G -1 ↾ B Isom < , R 1 … A A
93 89 91 92 syl2anc ⊢ R Or A ∧ A ∈ Fin → O ∘ G -1 ↾ B Isom < , R 1 … A A
94 isof1o ⊢ O ∘ G -1 ↾ B Isom < , R 1 … A A → O ∘ G -1 ↾ B : 1 … A ⟶ 1-1 onto A
95 f1of ⊢ O ∘ G -1 ↾ B : 1 … A ⟶ 1-1 onto A → O ∘ G -1 ↾ B : 1 … A ⟶ A
96 93 94 95 3syl ⊢ R Or A ∧ A ∈ Fin → O ∘ G -1 ↾ B : 1 … A ⟶ A
97 fzfid ⊢ R Or A ∧ A ∈ Fin → 1 … A ∈ Fin
98 fex ⊢ O ∘ G -1 ↾ B : 1 … A ⟶ A ∧ 1 … A ∈ Fin → O ∘ G -1 ↾ B ∈ V
99 96 97 98 syl2anc ⊢ R Or A ∧ A ∈ Fin → O ∘ G -1 ↾ B ∈ V
100 isoeq1 ⊢ f = O ∘ G -1 ↾ B → f Isom < , R 1 … A A ↔ O ∘ G -1 ↾ B Isom < , R 1 … A A
101 99 93 100 spcedv ⊢ R Or A ∧ A ∈ Fin → ∃ f f Isom < , R 1 … A A