Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  fz1isolem Structured version   Visualization version   GIF version

Theorem fz1isolem 13102
 Description: Lemma for fz1iso 13103. (Contributed by Mario Carneiro, 2-Apr-2014.)
Hypotheses
Ref Expression
fz1iso.1 𝐺 = (rec((𝑛 ∈ V ↦ (𝑛 + 1)), 1) ↾ ω)
fz1iso.2 𝐵 = (ℕ ∩ ( < “ {((#‘𝐴) + 1)}))
fz1iso.3 𝐶 = (ω ∩ (𝐺‘((#‘𝐴) + 1)))
fz1iso.4 𝑂 = OrdIso(𝑅, 𝐴)
Assertion
Ref Expression
fz1isolem ((𝑅 Or 𝐴𝐴 ∈ Fin) → ∃𝑓 𝑓 Isom < , 𝑅 ((1...(#‘𝐴)), 𝐴))
Distinct variable groups:   𝑓,𝑛,𝐴   𝐵,𝑓   𝑓,𝐺   𝑓,𝑂   𝑅,𝑓
Allowed substitution hints:   𝐵(𝑛)   𝐶(𝑓,𝑛)   𝑅(𝑛)   𝐺(𝑛)   𝑂(𝑛)

Proof of Theorem fz1isolem
StepHypRef Expression
1 hashcl 13009 . . . . . . . . 9 (𝐴 ∈ Fin → (#‘𝐴) ∈ ℕ0)
21adantl 481 . . . . . . . 8 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (#‘𝐴) ∈ ℕ0)
3 nnuz 11599 . . . . . . . . . . 11 ℕ = (ℤ‘1)
4 1z 11284 . . . . . . . . . . . . 13 1 ∈ ℤ
5 fz1iso.1 . . . . . . . . . . . . 13 𝐺 = (rec((𝑛 ∈ V ↦ (𝑛 + 1)), 1) ↾ ω)
64, 5om2uzisoi 12615 . . . . . . . . . . . 12 𝐺 Isom E , < (ω, (ℤ‘1))
7 isoeq5 6471 . . . . . . . . . . . 12 (ℕ = (ℤ‘1) → (𝐺 Isom E , < (ω, ℕ) ↔ 𝐺 Isom E , < (ω, (ℤ‘1))))
86, 7mpbiri 247 . . . . . . . . . . 11 (ℕ = (ℤ‘1) → 𝐺 Isom E , < (ω, ℕ))
93, 8ax-mp 5 . . . . . . . . . 10 𝐺 Isom E , < (ω, ℕ)
10 isocnv 6480 . . . . . . . . . 10 (𝐺 Isom E , < (ω, ℕ) → 𝐺 Isom < , E (ℕ, ω))
119, 10ax-mp 5 . . . . . . . . 9 𝐺 Isom < , E (ℕ, ω)
12 nn0p1nn 11209 . . . . . . . . 9 ((#‘𝐴) ∈ ℕ0 → ((#‘𝐴) + 1) ∈ ℕ)
13 fz1iso.2 . . . . . . . . . 10 𝐵 = (ℕ ∩ ( < “ {((#‘𝐴) + 1)}))
14 fz1iso.3 . . . . . . . . . . 11 𝐶 = (ω ∩ (𝐺‘((#‘𝐴) + 1)))
15 fvex 6113 . . . . . . . . . . . . 13 (𝐺‘((#‘𝐴) + 1)) ∈ V
1615epini 5414 . . . . . . . . . . . 12 ( E “ {(𝐺‘((#‘𝐴) + 1))}) = (𝐺‘((#‘𝐴) + 1))
1716ineq2i 3773 . . . . . . . . . . 11 (ω ∩ ( E “ {(𝐺‘((#‘𝐴) + 1))})) = (ω ∩ (𝐺‘((#‘𝐴) + 1)))
1814, 17eqtr4i 2635 . . . . . . . . . 10 𝐶 = (ω ∩ ( E “ {(𝐺‘((#‘𝐴) + 1))}))
1913, 18isoini2 6489 . . . . . . . . 9 ((𝐺 Isom < , E (ℕ, ω) ∧ ((#‘𝐴) + 1) ∈ ℕ) → (𝐺𝐵) Isom < , E (𝐵, 𝐶))
2011, 12, 19sylancr 694 . . . . . . . 8 ((#‘𝐴) ∈ ℕ0 → (𝐺𝐵) Isom < , E (𝐵, 𝐶))
212, 20syl 17 . . . . . . 7 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝐺𝐵) Isom < , E (𝐵, 𝐶))
22 nnz 11276 . . . . . . . . . . . . 13 (𝑓 ∈ ℕ → 𝑓 ∈ ℤ)
232nn0zd 11356 . . . . . . . . . . . . 13 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (#‘𝐴) ∈ ℤ)
24 eluz 11577 . . . . . . . . . . . . 13 ((𝑓 ∈ ℤ ∧ (#‘𝐴) ∈ ℤ) → ((#‘𝐴) ∈ (ℤ𝑓) ↔ 𝑓 ≤ (#‘𝐴)))
2522, 23, 24syl2anr 494 . . . . . . . . . . . 12 (((𝑅 Or 𝐴𝐴 ∈ Fin) ∧ 𝑓 ∈ ℕ) → ((#‘𝐴) ∈ (ℤ𝑓) ↔ 𝑓 ≤ (#‘𝐴)))
26 zleltp1 11305 . . . . . . . . . . . . . 14 ((𝑓 ∈ ℤ ∧ (#‘𝐴) ∈ ℤ) → (𝑓 ≤ (#‘𝐴) ↔ 𝑓 < ((#‘𝐴) + 1)))
2722, 23, 26syl2anr 494 . . . . . . . . . . . . 13 (((𝑅 Or 𝐴𝐴 ∈ Fin) ∧ 𝑓 ∈ ℕ) → (𝑓 ≤ (#‘𝐴) ↔ 𝑓 < ((#‘𝐴) + 1)))
28 ovex 6577 . . . . . . . . . . . . . 14 ((#‘𝐴) + 1) ∈ V
29 vex 3176 . . . . . . . . . . . . . . 15 𝑓 ∈ V
3029eliniseg 5413 . . . . . . . . . . . . . 14 (((#‘𝐴) + 1) ∈ V → (𝑓 ∈ ( < “ {((#‘𝐴) + 1)}) ↔ 𝑓 < ((#‘𝐴) + 1)))
3128, 30ax-mp 5 . . . . . . . . . . . . 13 (𝑓 ∈ ( < “ {((#‘𝐴) + 1)}) ↔ 𝑓 < ((#‘𝐴) + 1))
3227, 31syl6bbr 277 . . . . . . . . . . . 12 (((𝑅 Or 𝐴𝐴 ∈ Fin) ∧ 𝑓 ∈ ℕ) → (𝑓 ≤ (#‘𝐴) ↔ 𝑓 ∈ ( < “ {((#‘𝐴) + 1)})))
3325, 32bitr2d 268 . . . . . . . . . . 11 (((𝑅 Or 𝐴𝐴 ∈ Fin) ∧ 𝑓 ∈ ℕ) → (𝑓 ∈ ( < “ {((#‘𝐴) + 1)}) ↔ (#‘𝐴) ∈ (ℤ𝑓)))
3433pm5.32da 671 . . . . . . . . . 10 ((𝑅 Or 𝐴𝐴 ∈ Fin) → ((𝑓 ∈ ℕ ∧ 𝑓 ∈ ( < “ {((#‘𝐴) + 1)})) ↔ (𝑓 ∈ ℕ ∧ (#‘𝐴) ∈ (ℤ𝑓))))
3513elin2 3763 . . . . . . . . . 10 (𝑓𝐵 ↔ (𝑓 ∈ ℕ ∧ 𝑓 ∈ ( < “ {((#‘𝐴) + 1)})))
36 elfzuzb 12207 . . . . . . . . . . 11 (𝑓 ∈ (1...(#‘𝐴)) ↔ (𝑓 ∈ (ℤ‘1) ∧ (#‘𝐴) ∈ (ℤ𝑓)))
37 elnnuz 11600 . . . . . . . . . . . 12 (𝑓 ∈ ℕ ↔ 𝑓 ∈ (ℤ‘1))
3837anbi1i 727 . . . . . . . . . . 11 ((𝑓 ∈ ℕ ∧ (#‘𝐴) ∈ (ℤ𝑓)) ↔ (𝑓 ∈ (ℤ‘1) ∧ (#‘𝐴) ∈ (ℤ𝑓)))
3936, 38bitr4i 266 . . . . . . . . . 10 (𝑓 ∈ (1...(#‘𝐴)) ↔ (𝑓 ∈ ℕ ∧ (#‘𝐴) ∈ (ℤ𝑓)))
4034, 35, 393bitr4g 302 . . . . . . . . 9 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝑓𝐵𝑓 ∈ (1...(#‘𝐴))))
4140eqrdv 2608 . . . . . . . 8 ((𝑅 Or 𝐴𝐴 ∈ Fin) → 𝐵 = (1...(#‘𝐴)))
42 isoeq4 6470 . . . . . . . 8 (𝐵 = (1...(#‘𝐴)) → ((𝐺𝐵) Isom < , E (𝐵, 𝐶) ↔ (𝐺𝐵) Isom < , E ((1...(#‘𝐴)), 𝐶)))
4341, 42syl 17 . . . . . . 7 ((𝑅 Or 𝐴𝐴 ∈ Fin) → ((𝐺𝐵) Isom < , E (𝐵, 𝐶) ↔ (𝐺𝐵) Isom < , E ((1...(#‘𝐴)), 𝐶)))
4421, 43mpbid 221 . . . . . 6 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝐺𝐵) Isom < , E ((1...(#‘𝐴)), 𝐶))
45 fz1iso.4 . . . . . . . . . . . . . . . . . 18 𝑂 = OrdIso(𝑅, 𝐴)
4645oion 8324 . . . . . . . . . . . . . . . . 17 (𝐴 ∈ Fin → dom 𝑂 ∈ On)
4746adantl 481 . . . . . . . . . . . . . . . 16 ((𝑅 Or 𝐴𝐴 ∈ Fin) → dom 𝑂 ∈ On)
48 simpr 476 . . . . . . . . . . . . . . . . 17 ((𝑅 Or 𝐴𝐴 ∈ Fin) → 𝐴 ∈ Fin)
49 wofi 8094 . . . . . . . . . . . . . . . . . 18 ((𝑅 Or 𝐴𝐴 ∈ Fin) → 𝑅 We 𝐴)
5045oien 8326 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ Fin ∧ 𝑅 We 𝐴) → dom 𝑂𝐴)
5148, 49, 50syl2anc 691 . . . . . . . . . . . . . . . . 17 ((𝑅 Or 𝐴𝐴 ∈ Fin) → dom 𝑂𝐴)
52 enfii 8062 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ Fin ∧ dom 𝑂𝐴) → dom 𝑂 ∈ Fin)
5348, 51, 52syl2anc 691 . . . . . . . . . . . . . . . 16 ((𝑅 Or 𝐴𝐴 ∈ Fin) → dom 𝑂 ∈ Fin)
5447, 53elind 3760 . . . . . . . . . . . . . . 15 ((𝑅 Or 𝐴𝐴 ∈ Fin) → dom 𝑂 ∈ (On ∩ Fin))
55 onfin2 8037 . . . . . . . . . . . . . . 15 ω = (On ∩ Fin)
5654, 55syl6eleqr 2699 . . . . . . . . . . . . . 14 ((𝑅 Or 𝐴𝐴 ∈ Fin) → dom 𝑂 ∈ ω)
57 eqid 2610 . . . . . . . . . . . . . . . 16 (rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω) = (rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)
58 0z 11265 . . . . . . . . . . . . . . . 16 0 ∈ ℤ
595, 57, 4, 58uzrdgxfr 12628 . . . . . . . . . . . . . . 15 (dom 𝑂 ∈ ω → (𝐺‘dom 𝑂) = (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂) + (1 − 0)))
60 1m0e1 11008 . . . . . . . . . . . . . . . 16 (1 − 0) = 1
6160oveq2i 6560 . . . . . . . . . . . . . . 15 (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂) + (1 − 0)) = (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂) + 1)
6259, 61syl6eq 2660 . . . . . . . . . . . . . 14 (dom 𝑂 ∈ ω → (𝐺‘dom 𝑂) = (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂) + 1))
6356, 62syl 17 . . . . . . . . . . . . 13 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝐺‘dom 𝑂) = (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂) + 1))
6451ensymd 7893 . . . . . . . . . . . . . . . . 17 ((𝑅 Or 𝐴𝐴 ∈ Fin) → 𝐴 ≈ dom 𝑂)
65 cardennn 8692 . . . . . . . . . . . . . . . . 17 ((𝐴 ≈ dom 𝑂 ∧ dom 𝑂 ∈ ω) → (card‘𝐴) = dom 𝑂)
6664, 56, 65syl2anc 691 . . . . . . . . . . . . . . . 16 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (card‘𝐴) = dom 𝑂)
6766fveq2d 6107 . . . . . . . . . . . . . . 15 ((𝑅 Or 𝐴𝐴 ∈ Fin) → ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘(card‘𝐴)) = ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂))
6857hashgval 12982 . . . . . . . . . . . . . . . 16 (𝐴 ∈ Fin → ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘(card‘𝐴)) = (#‘𝐴))
6968adantl 481 . . . . . . . . . . . . . . 15 ((𝑅 Or 𝐴𝐴 ∈ Fin) → ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘(card‘𝐴)) = (#‘𝐴))
7067, 69eqtr3d 2646 . . . . . . . . . . . . . 14 ((𝑅 Or 𝐴𝐴 ∈ Fin) → ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂) = (#‘𝐴))
7170oveq1d 6564 . . . . . . . . . . . . 13 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂) + 1) = ((#‘𝐴) + 1))
7263, 71eqtrd 2644 . . . . . . . . . . . 12 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝐺‘dom 𝑂) = ((#‘𝐴) + 1))
7372fveq2d 6107 . . . . . . . . . . 11 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝐺‘(𝐺‘dom 𝑂)) = (𝐺‘((#‘𝐴) + 1)))
74 isof1o 6473 . . . . . . . . . . . . 13 (𝐺 Isom E , < (ω, ℕ) → 𝐺:ω–1-1-onto→ℕ)
759, 74ax-mp 5 . . . . . . . . . . . 12 𝐺:ω–1-1-onto→ℕ
76 f1ocnvfv1 6432 . . . . . . . . . . . 12 ((𝐺:ω–1-1-onto→ℕ ∧ dom 𝑂 ∈ ω) → (𝐺‘(𝐺‘dom 𝑂)) = dom 𝑂)
7775, 56, 76sylancr 694 . . . . . . . . . . 11 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝐺‘(𝐺‘dom 𝑂)) = dom 𝑂)
7873, 77eqtr3d 2646 . . . . . . . . . 10 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝐺‘((#‘𝐴) + 1)) = dom 𝑂)
7978ineq2d 3776 . . . . . . . . 9 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (ω ∩ (𝐺‘((#‘𝐴) + 1))) = (ω ∩ dom 𝑂))
80 ordom 6966 . . . . . . . . . . 11 Ord ω
81 ordelss 5656 . . . . . . . . . . 11 ((Ord ω ∧ dom 𝑂 ∈ ω) → dom 𝑂 ⊆ ω)
8280, 56, 81sylancr 694 . . . . . . . . . 10 ((𝑅 Or 𝐴𝐴 ∈ Fin) → dom 𝑂 ⊆ ω)
83 sseqin2 3779 . . . . . . . . . 10 (dom 𝑂 ⊆ ω ↔ (ω ∩ dom 𝑂) = dom 𝑂)
8482, 83sylib 207 . . . . . . . . 9 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (ω ∩ dom 𝑂) = dom 𝑂)
8579, 84eqtrd 2644 . . . . . . . 8 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (ω ∩ (𝐺‘((#‘𝐴) + 1))) = dom 𝑂)
8614, 85syl5eq 2656 . . . . . . 7 ((𝑅 Or 𝐴𝐴 ∈ Fin) → 𝐶 = dom 𝑂)
87 isoeq5 6471 . . . . . . 7 (𝐶 = dom 𝑂 → ((𝐺𝐵) Isom < , E ((1...(#‘𝐴)), 𝐶) ↔ (𝐺𝐵) Isom < , E ((1...(#‘𝐴)), dom 𝑂)))
8886, 87syl 17 . . . . . 6 ((𝑅 Or 𝐴𝐴 ∈ Fin) → ((𝐺𝐵) Isom < , E ((1...(#‘𝐴)), 𝐶) ↔ (𝐺𝐵) Isom < , E ((1...(#‘𝐴)), dom 𝑂)))
8944, 88mpbid 221 . . . . 5 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝐺𝐵) Isom < , E ((1...(#‘𝐴)), dom 𝑂))
9045oiiso 8325 . . . . . 6 ((𝐴 ∈ Fin ∧ 𝑅 We 𝐴) → 𝑂 Isom E , 𝑅 (dom 𝑂, 𝐴))
9148, 49, 90syl2anc 691 . . . . 5 ((𝑅 Or 𝐴𝐴 ∈ Fin) → 𝑂 Isom E , 𝑅 (dom 𝑂, 𝐴))
92 isotr 6486 . . . . 5 (((𝐺𝐵) Isom < , E ((1...(#‘𝐴)), dom 𝑂) ∧ 𝑂 Isom E , 𝑅 (dom 𝑂, 𝐴)) → (𝑂 ∘ (𝐺𝐵)) Isom < , 𝑅 ((1...(#‘𝐴)), 𝐴))
9389, 91, 92syl2anc 691 . . . 4 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝑂 ∘ (𝐺𝐵)) Isom < , 𝑅 ((1...(#‘𝐴)), 𝐴))
94 isof1o 6473 . . . 4 ((𝑂 ∘ (𝐺𝐵)) Isom < , 𝑅 ((1...(#‘𝐴)), 𝐴) → (𝑂 ∘ (𝐺𝐵)):(1...(#‘𝐴))–1-1-onto𝐴)
95 f1of 6050 . . . 4 ((𝑂 ∘ (𝐺𝐵)):(1...(#‘𝐴))–1-1-onto𝐴 → (𝑂 ∘ (𝐺𝐵)):(1...(#‘𝐴))⟶𝐴)
9693, 94, 953syl 18 . . 3 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝑂 ∘ (𝐺𝐵)):(1...(#‘𝐴))⟶𝐴)
97 fzfid 12634 . . 3 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (1...(#‘𝐴)) ∈ Fin)
98 fex 6394 . . 3 (((𝑂 ∘ (𝐺𝐵)):(1...(#‘𝐴))⟶𝐴 ∧ (1...(#‘𝐴)) ∈ Fin) → (𝑂 ∘ (𝐺𝐵)) ∈ V)
9996, 97, 98syl2anc 691 . 2 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝑂 ∘ (𝐺𝐵)) ∈ V)
100 isoeq1 6467 . . 3 (𝑓 = (𝑂 ∘ (𝐺𝐵)) → (𝑓 Isom < , 𝑅 ((1...(#‘𝐴)), 𝐴) ↔ (𝑂 ∘ (𝐺𝐵)) Isom < , 𝑅 ((1...(#‘𝐴)), 𝐴)))
101100spcegv 3267 . 2 ((𝑂 ∘ (𝐺𝐵)) ∈ V → ((𝑂 ∘ (𝐺𝐵)) Isom < , 𝑅 ((1...(#‘𝐴)), 𝐴) → ∃𝑓 𝑓 Isom < , 𝑅 ((1...(#‘𝐴)), 𝐴)))
10299, 93, 101sylc 63 1 ((𝑅 Or 𝐴𝐴 ∈ Fin) → ∃𝑓 𝑓 Isom < , 𝑅 ((1...(#‘𝐴)), 𝐴))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∧ wa 383   = wceq 1475  ∃wex 1695   ∈ wcel 1977  Vcvv 3173   ∩ cin 3539   ⊆ wss 3540  {csn 4125   class class class wbr 4583   ↦ cmpt 4643   E cep 4947   Or wor 4958   We wwe 4996  ◡ccnv 5037  dom cdm 5038   ↾ cres 5040   “ cima 5041   ∘ ccom 5042  Ord word 5639  Oncon0 5640  ⟶wf 5800  –1-1-onto→wf1o 5803  ‘cfv 5804   Isom wiso 5805  (class class class)co 6549  ωcom 6957  reccrdg 7392   ≈ cen 7838  Fincfn 7841  OrdIsocoi 8297  cardccrd 8644  0cc0 9815  1c1 9816   + caddc 9818   < clt 9953   ≤ cle 9954   − cmin 10145  ℕcn 10897  ℕ0cn0 11169  ℤcz 11254  ℤ≥cuz 11563  ...cfz 12197  #chash 12979 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-se 4998  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-isom 5813  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-oi 8298  df-card 8648  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-n0 11170  df-z 11255  df-uz 11564  df-fz 12198  df-hash 12980 This theorem is referenced by:  fz1iso  13103
 Copyright terms: Public domain W3C validator