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

Theorem fz1isolem 13190
Description: Lemma for fz1iso 13191. (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 13094 . . . . . . . . 9 (𝐴 ∈ Fin → (#‘𝐴) ∈ ℕ0)
21adantl 482 . . . . . . . 8 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (#‘𝐴) ∈ ℕ0)
3 nnuz 11674 . . . . . . . . . . 11 ℕ = (ℤ‘1)
4 1z 11358 . . . . . . . . . . . . 13 1 ∈ ℤ
5 fz1iso.1 . . . . . . . . . . . . 13 𝐺 = (rec((𝑛 ∈ V ↦ (𝑛 + 1)), 1) ↾ ω)
64, 5om2uzisoi 12700 . . . . . . . . . . . 12 𝐺 Isom E , < (ω, (ℤ‘1))
7 isoeq5 6531 . . . . . . . . . . . 12 (ℕ = (ℤ‘1) → (𝐺 Isom E , < (ω, ℕ) ↔ 𝐺 Isom E , < (ω, (ℤ‘1))))
86, 7mpbiri 248 . . . . . . . . . . 11 (ℕ = (ℤ‘1) → 𝐺 Isom E , < (ω, ℕ))
93, 8ax-mp 5 . . . . . . . . . 10 𝐺 Isom E , < (ω, ℕ)
10 isocnv 6540 . . . . . . . . . 10 (𝐺 Isom E , < (ω, ℕ) → 𝐺 Isom < , E (ℕ, ω))
119, 10ax-mp 5 . . . . . . . . 9 𝐺 Isom < , E (ℕ, ω)
12 nn0p1nn 11283 . . . . . . . . 9 ((#‘𝐴) ∈ ℕ0 → ((#‘𝐴) + 1) ∈ ℕ)
13 fz1iso.2 . . . . . . . . . 10 𝐵 = (ℕ ∩ ( < “ {((#‘𝐴) + 1)}))
14 fz1iso.3 . . . . . . . . . . 11 𝐶 = (ω ∩ (𝐺‘((#‘𝐴) + 1)))
15 fvex 6163 . . . . . . . . . . . . 13 (𝐺‘((#‘𝐴) + 1)) ∈ V
1615epini 5459 . . . . . . . . . . . 12 ( E “ {(𝐺‘((#‘𝐴) + 1))}) = (𝐺‘((#‘𝐴) + 1))
1716ineq2i 3794 . . . . . . . . . . 11 (ω ∩ ( E “ {(𝐺‘((#‘𝐴) + 1))})) = (ω ∩ (𝐺‘((#‘𝐴) + 1)))
1814, 17eqtr4i 2646 . . . . . . . . . 10 𝐶 = (ω ∩ ( E “ {(𝐺‘((#‘𝐴) + 1))}))
1913, 18isoini2 6549 . . . . . . . . 9 ((𝐺 Isom < , E (ℕ, ω) ∧ ((#‘𝐴) + 1) ∈ ℕ) → (𝐺𝐵) Isom < , E (𝐵, 𝐶))
2011, 12, 19sylancr 694 . . . . . . . 8 ((#‘𝐴) ∈ ℕ0 → (𝐺𝐵) Isom < , E (𝐵, 𝐶))
212, 20syl 17 . . . . . . 7 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝐺𝐵) Isom < , E (𝐵, 𝐶))
22 nnz 11350 . . . . . . . . . . . . 13 (𝑓 ∈ ℕ → 𝑓 ∈ ℤ)
232nn0zd 11431 . . . . . . . . . . . . 13 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (#‘𝐴) ∈ ℤ)
24 eluz 11652 . . . . . . . . . . . . 13 ((𝑓 ∈ ℤ ∧ (#‘𝐴) ∈ ℤ) → ((#‘𝐴) ∈ (ℤ𝑓) ↔ 𝑓 ≤ (#‘𝐴)))
2522, 23, 24syl2anr 495 . . . . . . . . . . . 12 (((𝑅 Or 𝐴𝐴 ∈ Fin) ∧ 𝑓 ∈ ℕ) → ((#‘𝐴) ∈ (ℤ𝑓) ↔ 𝑓 ≤ (#‘𝐴)))
26 zleltp1 11379 . . . . . . . . . . . . . 14 ((𝑓 ∈ ℤ ∧ (#‘𝐴) ∈ ℤ) → (𝑓 ≤ (#‘𝐴) ↔ 𝑓 < ((#‘𝐴) + 1)))
2722, 23, 26syl2anr 495 . . . . . . . . . . . . 13 (((𝑅 Or 𝐴𝐴 ∈ Fin) ∧ 𝑓 ∈ ℕ) → (𝑓 ≤ (#‘𝐴) ↔ 𝑓 < ((#‘𝐴) + 1)))
28 ovex 6638 . . . . . . . . . . . . . 14 ((#‘𝐴) + 1) ∈ V
29 vex 3192 . . . . . . . . . . . . . . 15 𝑓 ∈ V
3029eliniseg 5458 . . . . . . . . . . . . . 14 (((#‘𝐴) + 1) ∈ V → (𝑓 ∈ ( < “ {((#‘𝐴) + 1)}) ↔ 𝑓 < ((#‘𝐴) + 1)))
3128, 30ax-mp 5 . . . . . . . . . . . . 13 (𝑓 ∈ ( < “ {((#‘𝐴) + 1)}) ↔ 𝑓 < ((#‘𝐴) + 1))
3227, 31syl6bbr 278 . . . . . . . . . . . 12 (((𝑅 Or 𝐴𝐴 ∈ Fin) ∧ 𝑓 ∈ ℕ) → (𝑓 ≤ (#‘𝐴) ↔ 𝑓 ∈ ( < “ {((#‘𝐴) + 1)})))
3325, 32bitr2d 269 . . . . . . . . . . 11 (((𝑅 Or 𝐴𝐴 ∈ Fin) ∧ 𝑓 ∈ ℕ) → (𝑓 ∈ ( < “ {((#‘𝐴) + 1)}) ↔ (#‘𝐴) ∈ (ℤ𝑓)))
3433pm5.32da 672 . . . . . . . . . 10 ((𝑅 Or 𝐴𝐴 ∈ Fin) → ((𝑓 ∈ ℕ ∧ 𝑓 ∈ ( < “ {((#‘𝐴) + 1)})) ↔ (𝑓 ∈ ℕ ∧ (#‘𝐴) ∈ (ℤ𝑓))))
3513elin2 3784 . . . . . . . . . 10 (𝑓𝐵 ↔ (𝑓 ∈ ℕ ∧ 𝑓 ∈ ( < “ {((#‘𝐴) + 1)})))
36 elfzuzb 12285 . . . . . . . . . . 11 (𝑓 ∈ (1...(#‘𝐴)) ↔ (𝑓 ∈ (ℤ‘1) ∧ (#‘𝐴) ∈ (ℤ𝑓)))
37 elnnuz 11675 . . . . . . . . . . . 12 (𝑓 ∈ ℕ ↔ 𝑓 ∈ (ℤ‘1))
3837anbi1i 730 . . . . . . . . . . 11 ((𝑓 ∈ ℕ ∧ (#‘𝐴) ∈ (ℤ𝑓)) ↔ (𝑓 ∈ (ℤ‘1) ∧ (#‘𝐴) ∈ (ℤ𝑓)))
3936, 38bitr4i 267 . . . . . . . . . 10 (𝑓 ∈ (1...(#‘𝐴)) ↔ (𝑓 ∈ ℕ ∧ (#‘𝐴) ∈ (ℤ𝑓)))
4034, 35, 393bitr4g 303 . . . . . . . . 9 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝑓𝐵𝑓 ∈ (1...(#‘𝐴))))
4140eqrdv 2619 . . . . . . . 8 ((𝑅 Or 𝐴𝐴 ∈ Fin) → 𝐵 = (1...(#‘𝐴)))
42 isoeq4 6530 . . . . . . . 8 (𝐵 = (1...(#‘𝐴)) → ((𝐺𝐵) Isom < , E (𝐵, 𝐶) ↔ (𝐺𝐵) Isom < , E ((1...(#‘𝐴)), 𝐶)))
4341, 42syl 17 . . . . . . 7 ((𝑅 Or 𝐴𝐴 ∈ Fin) → ((𝐺𝐵) Isom < , E (𝐵, 𝐶) ↔ (𝐺𝐵) Isom < , E ((1...(#‘𝐴)), 𝐶)))
4421, 43mpbid 222 . . . . . 6 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝐺𝐵) Isom < , E ((1...(#‘𝐴)), 𝐶))
45 fz1iso.4 . . . . . . . . . . . . . . . . . 18 𝑂 = OrdIso(𝑅, 𝐴)
4645oion 8392 . . . . . . . . . . . . . . . . 17 (𝐴 ∈ Fin → dom 𝑂 ∈ On)
4746adantl 482 . . . . . . . . . . . . . . . 16 ((𝑅 Or 𝐴𝐴 ∈ Fin) → dom 𝑂 ∈ On)
48 simpr 477 . . . . . . . . . . . . . . . . 17 ((𝑅 Or 𝐴𝐴 ∈ Fin) → 𝐴 ∈ Fin)
49 wofi 8160 . . . . . . . . . . . . . . . . . 18 ((𝑅 Or 𝐴𝐴 ∈ Fin) → 𝑅 We 𝐴)
5045oien 8394 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ Fin ∧ 𝑅 We 𝐴) → dom 𝑂𝐴)
5148, 49, 50syl2anc 692 . . . . . . . . . . . . . . . . 17 ((𝑅 Or 𝐴𝐴 ∈ Fin) → dom 𝑂𝐴)
52 enfii 8128 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ Fin ∧ dom 𝑂𝐴) → dom 𝑂 ∈ Fin)
5348, 51, 52syl2anc 692 . . . . . . . . . . . . . . . 16 ((𝑅 Or 𝐴𝐴 ∈ Fin) → dom 𝑂 ∈ Fin)
5447, 53elind 3781 . . . . . . . . . . . . . . 15 ((𝑅 Or 𝐴𝐴 ∈ Fin) → dom 𝑂 ∈ (On ∩ Fin))
55 onfin2 8103 . . . . . . . . . . . . . . 15 ω = (On ∩ Fin)
5654, 55syl6eleqr 2709 . . . . . . . . . . . . . 14 ((𝑅 Or 𝐴𝐴 ∈ Fin) → dom 𝑂 ∈ ω)
57 eqid 2621 . . . . . . . . . . . . . . . 16 (rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω) = (rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)
58 0z 11339 . . . . . . . . . . . . . . . 16 0 ∈ ℤ
595, 57, 4, 58uzrdgxfr 12713 . . . . . . . . . . . . . . 15 (dom 𝑂 ∈ ω → (𝐺‘dom 𝑂) = (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂) + (1 − 0)))
60 1m0e1 11082 . . . . . . . . . . . . . . . 16 (1 − 0) = 1
6160oveq2i 6621 . . . . . . . . . . . . . . 15 (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂) + (1 − 0)) = (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂) + 1)
6259, 61syl6eq 2671 . . . . . . . . . . . . . 14 (dom 𝑂 ∈ ω → (𝐺‘dom 𝑂) = (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂) + 1))
6356, 62syl 17 . . . . . . . . . . . . 13 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝐺‘dom 𝑂) = (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂) + 1))
6451ensymd 7958 . . . . . . . . . . . . . . . . 17 ((𝑅 Or 𝐴𝐴 ∈ Fin) → 𝐴 ≈ dom 𝑂)
65 cardennn 8760 . . . . . . . . . . . . . . . . 17 ((𝐴 ≈ dom 𝑂 ∧ dom 𝑂 ∈ ω) → (card‘𝐴) = dom 𝑂)
6664, 56, 65syl2anc 692 . . . . . . . . . . . . . . . 16 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (card‘𝐴) = dom 𝑂)
6766fveq2d 6157 . . . . . . . . . . . . . . 15 ((𝑅 Or 𝐴𝐴 ∈ Fin) → ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘(card‘𝐴)) = ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂))
6857hashgval 13067 . . . . . . . . . . . . . . . 16 (𝐴 ∈ Fin → ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘(card‘𝐴)) = (#‘𝐴))
6968adantl 482 . . . . . . . . . . . . . . 15 ((𝑅 Or 𝐴𝐴 ∈ Fin) → ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘(card‘𝐴)) = (#‘𝐴))
7067, 69eqtr3d 2657 . . . . . . . . . . . . . 14 ((𝑅 Or 𝐴𝐴 ∈ Fin) → ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂) = (#‘𝐴))
7170oveq1d 6625 . . . . . . . . . . . . 13 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂) + 1) = ((#‘𝐴) + 1))
7263, 71eqtrd 2655 . . . . . . . . . . . 12 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝐺‘dom 𝑂) = ((#‘𝐴) + 1))
7372fveq2d 6157 . . . . . . . . . . 11 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝐺‘(𝐺‘dom 𝑂)) = (𝐺‘((#‘𝐴) + 1)))
74 isof1o 6533 . . . . . . . . . . . . 13 (𝐺 Isom E , < (ω, ℕ) → 𝐺:ω–1-1-onto→ℕ)
759, 74ax-mp 5 . . . . . . . . . . . 12 𝐺:ω–1-1-onto→ℕ
76 f1ocnvfv1 6492 . . . . . . . . . . . 12 ((𝐺:ω–1-1-onto→ℕ ∧ dom 𝑂 ∈ ω) → (𝐺‘(𝐺‘dom 𝑂)) = dom 𝑂)
7775, 56, 76sylancr 694 . . . . . . . . . . 11 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝐺‘(𝐺‘dom 𝑂)) = dom 𝑂)
7873, 77eqtr3d 2657 . . . . . . . . . 10 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝐺‘((#‘𝐴) + 1)) = dom 𝑂)
7978ineq2d 3797 . . . . . . . . 9 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (ω ∩ (𝐺‘((#‘𝐴) + 1))) = (ω ∩ dom 𝑂))
80 ordom 7028 . . . . . . . . . . 11 Ord ω
81 ordelss 5703 . . . . . . . . . . 11 ((Ord ω ∧ dom 𝑂 ∈ ω) → dom 𝑂 ⊆ ω)
8280, 56, 81sylancr 694 . . . . . . . . . 10 ((𝑅 Or 𝐴𝐴 ∈ Fin) → dom 𝑂 ⊆ ω)
83 sseqin2 3800 . . . . . . . . . 10 (dom 𝑂 ⊆ ω ↔ (ω ∩ dom 𝑂) = dom 𝑂)
8482, 83sylib 208 . . . . . . . . 9 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (ω ∩ dom 𝑂) = dom 𝑂)
8579, 84eqtrd 2655 . . . . . . . 8 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (ω ∩ (𝐺‘((#‘𝐴) + 1))) = dom 𝑂)
8614, 85syl5eq 2667 . . . . . . 7 ((𝑅 Or 𝐴𝐴 ∈ Fin) → 𝐶 = dom 𝑂)
87 isoeq5 6531 . . . . . . 7 (𝐶 = dom 𝑂 → ((𝐺𝐵) Isom < , E ((1...(#‘𝐴)), 𝐶) ↔ (𝐺𝐵) Isom < , E ((1...(#‘𝐴)), dom 𝑂)))
8886, 87syl 17 . . . . . 6 ((𝑅 Or 𝐴𝐴 ∈ Fin) → ((𝐺𝐵) Isom < , E ((1...(#‘𝐴)), 𝐶) ↔ (𝐺𝐵) Isom < , E ((1...(#‘𝐴)), dom 𝑂)))
8944, 88mpbid 222 . . . . 5 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝐺𝐵) Isom < , E ((1...(#‘𝐴)), dom 𝑂))
9045oiiso 8393 . . . . . 6 ((𝐴 ∈ Fin ∧ 𝑅 We 𝐴) → 𝑂 Isom E , 𝑅 (dom 𝑂, 𝐴))
9148, 49, 90syl2anc 692 . . . . 5 ((𝑅 Or 𝐴𝐴 ∈ Fin) → 𝑂 Isom E , 𝑅 (dom 𝑂, 𝐴))
92 isotr 6546 . . . . 5 (((𝐺𝐵) Isom < , E ((1...(#‘𝐴)), dom 𝑂) ∧ 𝑂 Isom E , 𝑅 (dom 𝑂, 𝐴)) → (𝑂 ∘ (𝐺𝐵)) Isom < , 𝑅 ((1...(#‘𝐴)), 𝐴))
9389, 91, 92syl2anc 692 . . . 4 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝑂 ∘ (𝐺𝐵)) Isom < , 𝑅 ((1...(#‘𝐴)), 𝐴))
94 isof1o 6533 . . . 4 ((𝑂 ∘ (𝐺𝐵)) Isom < , 𝑅 ((1...(#‘𝐴)), 𝐴) → (𝑂 ∘ (𝐺𝐵)):(1...(#‘𝐴))–1-1-onto𝐴)
95 f1of 6099 . . . 4 ((𝑂 ∘ (𝐺𝐵)):(1...(#‘𝐴))–1-1-onto𝐴 → (𝑂 ∘ (𝐺𝐵)):(1...(#‘𝐴))⟶𝐴)
9693, 94, 953syl 18 . . 3 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝑂 ∘ (𝐺𝐵)):(1...(#‘𝐴))⟶𝐴)
97 fzfid 12719 . . 3 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (1...(#‘𝐴)) ∈ Fin)
98 fex 6450 . . 3 (((𝑂 ∘ (𝐺𝐵)):(1...(#‘𝐴))⟶𝐴 ∧ (1...(#‘𝐴)) ∈ Fin) → (𝑂 ∘ (𝐺𝐵)) ∈ V)
9996, 97, 98syl2anc 692 . 2 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝑂 ∘ (𝐺𝐵)) ∈ V)
100 isoeq1 6527 . . 3 (𝑓 = (𝑂 ∘ (𝐺𝐵)) → (𝑓 Isom < , 𝑅 ((1...(#‘𝐴)), 𝐴) ↔ (𝑂 ∘ (𝐺𝐵)) Isom < , 𝑅 ((1...(#‘𝐴)), 𝐴)))
101100spcegv 3283 . 2 ((𝑂 ∘ (𝐺𝐵)) ∈ V → ((𝑂 ∘ (𝐺𝐵)) Isom < , 𝑅 ((1...(#‘𝐴)), 𝐴) → ∃𝑓 𝑓 Isom < , 𝑅 ((1...(#‘𝐴)), 𝐴)))
10299, 93, 101sylc 65 1 ((𝑅 Or 𝐴𝐴 ∈ Fin) → ∃𝑓 𝑓 Isom < , 𝑅 ((1...(#‘𝐴)), 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480  wex 1701  wcel 1987  Vcvv 3189  cin 3558  wss 3559  {csn 4153   class class class wbr 4618  cmpt 4678   E cep 4988   Or wor 4999   We wwe 5037  ccnv 5078  dom cdm 5079  cres 5081  cima 5082  ccom 5083  Ord word 5686  Oncon0 5687  wf 5848  1-1-ontowf1o 5851  cfv 5852   Isom wiso 5853  (class class class)co 6610  ωcom 7019  reccrdg 7457  cen 7903  Fincfn 7906  OrdIsocoi 8365  cardccrd 8712  0cc0 9887  1c1 9888   + caddc 9890   < clt 10025  cle 10026  cmin 10217  cn 10971  0cn0 11243  cz 11328  cuz 11638  ...cfz 12275  #chash 13064
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4736  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6909  ax-cnex 9943  ax-resscn 9944  ax-1cn 9945  ax-icn 9946  ax-addcl 9947  ax-addrcl 9948  ax-mulcl 9949  ax-mulrcl 9950  ax-mulcom 9951  ax-addass 9952  ax-mulass 9953  ax-distr 9954  ax-i2m1 9955  ax-1ne0 9956  ax-1rid 9957  ax-rnegex 9958  ax-rrecex 9959  ax-cnre 9960  ax-pre-lttri 9961  ax-pre-lttrn 9962  ax-pre-ltadd 9963  ax-pre-mulgt0 9964
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2912  df-rex 2913  df-reu 2914  df-rmo 2915  df-rab 2916  df-v 3191  df-sbc 3422  df-csb 3519  df-dif 3562  df-un 3564  df-in 3566  df-ss 3573  df-pss 3575  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-tp 4158  df-op 4160  df-uni 4408  df-int 4446  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-tr 4718  df-eprel 4990  df-id 4994  df-po 5000  df-so 5001  df-fr 5038  df-se 5039  df-we 5040  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-pred 5644  df-ord 5690  df-on 5691  df-lim 5692  df-suc 5693  df-iota 5815  df-fun 5854  df-fn 5855  df-f 5856  df-f1 5857  df-fo 5858  df-f1o 5859  df-fv 5860  df-isom 5861  df-riota 6571  df-ov 6613  df-oprab 6614  df-mpt2 6615  df-om 7020  df-1st 7120  df-2nd 7121  df-wrecs 7359  df-recs 7420  df-rdg 7458  df-1o 7512  df-er 7694  df-en 7907  df-dom 7908  df-sdom 7909  df-fin 7910  df-oi 8366  df-card 8716  df-pnf 10027  df-mnf 10028  df-xr 10029  df-ltxr 10030  df-le 10031  df-sub 10219  df-neg 10220  df-nn 10972  df-n0 11244  df-z 11329  df-uz 11639  df-fz 12276  df-hash 13065
This theorem is referenced by:  fz1iso  13191
  Copyright terms: Public domain W3C validator