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

Theorem fz1isolem 14497
Description: Lemma for fz1iso 14498. (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 14392 . . . . . . . . 9 (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℕ0)
21adantl 481 . . . . . . . 8 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (♯‘𝐴) ∈ ℕ0)
3 nnuz 12919 . . . . . . . . . . 11 ℕ = (ℤ‘1)
4 1z 12645 . . . . . . . . . . . . 13 1 ∈ ℤ
5 fz1iso.1 . . . . . . . . . . . . 13 𝐺 = (rec((𝑛 ∈ V ↦ (𝑛 + 1)), 1) ↾ ω)
64, 5om2uzisoi 13992 . . . . . . . . . . . 12 𝐺 Isom E , < (ω, (ℤ‘1))
7 isoeq5 7341 . . . . . . . . . . . 12 (ℕ = (ℤ‘1) → (𝐺 Isom E , < (ω, ℕ) ↔ 𝐺 Isom E , < (ω, (ℤ‘1))))
86, 7mpbiri 258 . . . . . . . . . . 11 (ℕ = (ℤ‘1) → 𝐺 Isom E , < (ω, ℕ))
93, 8ax-mp 5 . . . . . . . . . 10 𝐺 Isom E , < (ω, ℕ)
10 isocnv 7350 . . . . . . . . . 10 (𝐺 Isom E , < (ω, ℕ) → 𝐺 Isom < , E (ℕ, ω))
119, 10ax-mp 5 . . . . . . . . 9 𝐺 Isom < , E (ℕ, ω)
12 nn0p1nn 12563 . . . . . . . . 9 ((♯‘𝐴) ∈ ℕ0 → ((♯‘𝐴) + 1) ∈ ℕ)
13 fz1iso.2 . . . . . . . . . 10 𝐵 = (ℕ ∩ ( < “ {((♯‘𝐴) + 1)}))
14 fz1iso.3 . . . . . . . . . . 11 𝐶 = (ω ∩ (𝐺‘((♯‘𝐴) + 1)))
15 fvex 6920 . . . . . . . . . . . . 13 (𝐺‘((♯‘𝐴) + 1)) ∈ V
1615epini 6117 . . . . . . . . . . . 12 ( E “ {(𝐺‘((♯‘𝐴) + 1))}) = (𝐺‘((♯‘𝐴) + 1))
1716ineq2i 4225 . . . . . . . . . . 11 (ω ∩ ( E “ {(𝐺‘((♯‘𝐴) + 1))})) = (ω ∩ (𝐺‘((♯‘𝐴) + 1)))
1814, 17eqtr4i 2766 . . . . . . . . . 10 𝐶 = (ω ∩ ( E “ {(𝐺‘((♯‘𝐴) + 1))}))
1913, 18isoini2 7359 . . . . . . . . 9 ((𝐺 Isom < , E (ℕ, ω) ∧ ((♯‘𝐴) + 1) ∈ ℕ) → (𝐺𝐵) Isom < , E (𝐵, 𝐶))
2011, 12, 19sylancr 587 . . . . . . . 8 ((♯‘𝐴) ∈ ℕ0 → (𝐺𝐵) Isom < , E (𝐵, 𝐶))
212, 20syl 17 . . . . . . 7 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝐺𝐵) Isom < , E (𝐵, 𝐶))
22 nnz 12632 . . . . . . . . . . . . 13 (𝑓 ∈ ℕ → 𝑓 ∈ ℤ)
232nn0zd 12637 . . . . . . . . . . . . 13 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (♯‘𝐴) ∈ ℤ)
24 eluz 12890 . . . . . . . . . . . . 13 ((𝑓 ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ) → ((♯‘𝐴) ∈ (ℤ𝑓) ↔ 𝑓 ≤ (♯‘𝐴)))
2522, 23, 24syl2anr 597 . . . . . . . . . . . 12 (((𝑅 Or 𝐴𝐴 ∈ Fin) ∧ 𝑓 ∈ ℕ) → ((♯‘𝐴) ∈ (ℤ𝑓) ↔ 𝑓 ≤ (♯‘𝐴)))
26 zleltp1 12666 . . . . . . . . . . . . . 14 ((𝑓 ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ) → (𝑓 ≤ (♯‘𝐴) ↔ 𝑓 < ((♯‘𝐴) + 1)))
2722, 23, 26syl2anr 597 . . . . . . . . . . . . 13 (((𝑅 Or 𝐴𝐴 ∈ Fin) ∧ 𝑓 ∈ ℕ) → (𝑓 ≤ (♯‘𝐴) ↔ 𝑓 < ((♯‘𝐴) + 1)))
28 ovex 7464 . . . . . . . . . . . . . 14 ((♯‘𝐴) + 1) ∈ V
29 vex 3482 . . . . . . . . . . . . . . 15 𝑓 ∈ V
3029eliniseg 6115 . . . . . . . . . . . . . 14 (((♯‘𝐴) + 1) ∈ V → (𝑓 ∈ ( < “ {((♯‘𝐴) + 1)}) ↔ 𝑓 < ((♯‘𝐴) + 1)))
3128, 30ax-mp 5 . . . . . . . . . . . . 13 (𝑓 ∈ ( < “ {((♯‘𝐴) + 1)}) ↔ 𝑓 < ((♯‘𝐴) + 1))
3227, 31bitr4di 289 . . . . . . . . . . . 12 (((𝑅 Or 𝐴𝐴 ∈ Fin) ∧ 𝑓 ∈ ℕ) → (𝑓 ≤ (♯‘𝐴) ↔ 𝑓 ∈ ( < “ {((♯‘𝐴) + 1)})))
3325, 32bitr2d 280 . . . . . . . . . . 11 (((𝑅 Or 𝐴𝐴 ∈ Fin) ∧ 𝑓 ∈ ℕ) → (𝑓 ∈ ( < “ {((♯‘𝐴) + 1)}) ↔ (♯‘𝐴) ∈ (ℤ𝑓)))
3433pm5.32da 579 . . . . . . . . . 10 ((𝑅 Or 𝐴𝐴 ∈ Fin) → ((𝑓 ∈ ℕ ∧ 𝑓 ∈ ( < “ {((♯‘𝐴) + 1)})) ↔ (𝑓 ∈ ℕ ∧ (♯‘𝐴) ∈ (ℤ𝑓))))
3513elin2 4213 . . . . . . . . . 10 (𝑓𝐵 ↔ (𝑓 ∈ ℕ ∧ 𝑓 ∈ ( < “ {((♯‘𝐴) + 1)})))
36 elfzuzb 13555 . . . . . . . . . . 11 (𝑓 ∈ (1...(♯‘𝐴)) ↔ (𝑓 ∈ (ℤ‘1) ∧ (♯‘𝐴) ∈ (ℤ𝑓)))
37 elnnuz 12920 . . . . . . . . . . . 12 (𝑓 ∈ ℕ ↔ 𝑓 ∈ (ℤ‘1))
3837anbi1i 624 . . . . . . . . . . 11 ((𝑓 ∈ ℕ ∧ (♯‘𝐴) ∈ (ℤ𝑓)) ↔ (𝑓 ∈ (ℤ‘1) ∧ (♯‘𝐴) ∈ (ℤ𝑓)))
3936, 38bitr4i 278 . . . . . . . . . 10 (𝑓 ∈ (1...(♯‘𝐴)) ↔ (𝑓 ∈ ℕ ∧ (♯‘𝐴) ∈ (ℤ𝑓)))
4034, 35, 393bitr4g 314 . . . . . . . . 9 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝑓𝐵𝑓 ∈ (1...(♯‘𝐴))))
4140eqrdv 2733 . . . . . . . 8 ((𝑅 Or 𝐴𝐴 ∈ Fin) → 𝐵 = (1...(♯‘𝐴)))
42 isoeq4 7340 . . . . . . . 8 (𝐵 = (1...(♯‘𝐴)) → ((𝐺𝐵) Isom < , E (𝐵, 𝐶) ↔ (𝐺𝐵) Isom < , E ((1...(♯‘𝐴)), 𝐶)))
4341, 42syl 17 . . . . . . 7 ((𝑅 Or 𝐴𝐴 ∈ Fin) → ((𝐺𝐵) Isom < , E (𝐵, 𝐶) ↔ (𝐺𝐵) Isom < , E ((1...(♯‘𝐴)), 𝐶)))
4421, 43mpbid 232 . . . . . 6 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝐺𝐵) Isom < , E ((1...(♯‘𝐴)), 𝐶))
45 fz1iso.4 . . . . . . . . . . . . . . . . . 18 𝑂 = OrdIso(𝑅, 𝐴)
4645oion 9574 . . . . . . . . . . . . . . . . 17 (𝐴 ∈ Fin → dom 𝑂 ∈ On)
4746adantl 481 . . . . . . . . . . . . . . . 16 ((𝑅 Or 𝐴𝐴 ∈ Fin) → dom 𝑂 ∈ On)
48 simpr 484 . . . . . . . . . . . . . . . . 17 ((𝑅 Or 𝐴𝐴 ∈ Fin) → 𝐴 ∈ Fin)
49 wofi 9323 . . . . . . . . . . . . . . . . . 18 ((𝑅 Or 𝐴𝐴 ∈ Fin) → 𝑅 We 𝐴)
5045oien 9576 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ Fin ∧ 𝑅 We 𝐴) → dom 𝑂𝐴)
5148, 49, 50syl2anc 584 . . . . . . . . . . . . . . . . 17 ((𝑅 Or 𝐴𝐴 ∈ Fin) → dom 𝑂𝐴)
52 enfii 9224 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ Fin ∧ dom 𝑂𝐴) → dom 𝑂 ∈ Fin)
5348, 51, 52syl2anc 584 . . . . . . . . . . . . . . . 16 ((𝑅 Or 𝐴𝐴 ∈ Fin) → dom 𝑂 ∈ Fin)
5447, 53elind 4210 . . . . . . . . . . . . . . 15 ((𝑅 Or 𝐴𝐴 ∈ Fin) → dom 𝑂 ∈ (On ∩ Fin))
55 onfin2 9266 . . . . . . . . . . . . . . 15 ω = (On ∩ Fin)
5654, 55eleqtrrdi 2850 . . . . . . . . . . . . . 14 ((𝑅 Or 𝐴𝐴 ∈ Fin) → dom 𝑂 ∈ ω)
57 eqid 2735 . . . . . . . . . . . . . . . 16 (rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω) = (rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)
58 0z 12622 . . . . . . . . . . . . . . . 16 0 ∈ ℤ
595, 57, 4, 58uzrdgxfr 14005 . . . . . . . . . . . . . . 15 (dom 𝑂 ∈ ω → (𝐺‘dom 𝑂) = (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂) + (1 − 0)))
60 1m0e1 12385 . . . . . . . . . . . . . . . 16 (1 − 0) = 1
6160oveq2i 7442 . . . . . . . . . . . . . . 15 (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂) + (1 − 0)) = (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂) + 1)
6259, 61eqtrdi 2791 . . . . . . . . . . . . . 14 (dom 𝑂 ∈ ω → (𝐺‘dom 𝑂) = (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂) + 1))
6356, 62syl 17 . . . . . . . . . . . . 13 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝐺‘dom 𝑂) = (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂) + 1))
6451ensymd 9044 . . . . . . . . . . . . . . . . 17 ((𝑅 Or 𝐴𝐴 ∈ Fin) → 𝐴 ≈ dom 𝑂)
65 cardennn 10021 . . . . . . . . . . . . . . . . 17 ((𝐴 ≈ dom 𝑂 ∧ dom 𝑂 ∈ ω) → (card‘𝐴) = dom 𝑂)
6664, 56, 65syl2anc 584 . . . . . . . . . . . . . . . 16 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (card‘𝐴) = dom 𝑂)
6766fveq2d 6911 . . . . . . . . . . . . . . 15 ((𝑅 Or 𝐴𝐴 ∈ Fin) → ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘(card‘𝐴)) = ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂))
6857hashgval 14369 . . . . . . . . . . . . . . . 16 (𝐴 ∈ Fin → ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘(card‘𝐴)) = (♯‘𝐴))
6968adantl 481 . . . . . . . . . . . . . . 15 ((𝑅 Or 𝐴𝐴 ∈ Fin) → ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘(card‘𝐴)) = (♯‘𝐴))
7067, 69eqtr3d 2777 . . . . . . . . . . . . . 14 ((𝑅 Or 𝐴𝐴 ∈ Fin) → ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂) = (♯‘𝐴))
7170oveq1d 7446 . . . . . . . . . . . . 13 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂) + 1) = ((♯‘𝐴) + 1))
7263, 71eqtrd 2775 . . . . . . . . . . . 12 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝐺‘dom 𝑂) = ((♯‘𝐴) + 1))
7372fveq2d 6911 . . . . . . . . . . 11 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝐺‘(𝐺‘dom 𝑂)) = (𝐺‘((♯‘𝐴) + 1)))
74 isof1o 7343 . . . . . . . . . . . . 13 (𝐺 Isom E , < (ω, ℕ) → 𝐺:ω–1-1-onto→ℕ)
759, 74ax-mp 5 . . . . . . . . . . . 12 𝐺:ω–1-1-onto→ℕ
76 f1ocnvfv1 7296 . . . . . . . . . . . 12 ((𝐺:ω–1-1-onto→ℕ ∧ dom 𝑂 ∈ ω) → (𝐺‘(𝐺‘dom 𝑂)) = dom 𝑂)
7775, 56, 76sylancr 587 . . . . . . . . . . 11 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝐺‘(𝐺‘dom 𝑂)) = dom 𝑂)
7873, 77eqtr3d 2777 . . . . . . . . . 10 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝐺‘((♯‘𝐴) + 1)) = dom 𝑂)
7978ineq2d 4228 . . . . . . . . 9 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (ω ∩ (𝐺‘((♯‘𝐴) + 1))) = (ω ∩ dom 𝑂))
80 ordom 7897 . . . . . . . . . . 11 Ord ω
81 ordelss 6402 . . . . . . . . . . 11 ((Ord ω ∧ dom 𝑂 ∈ ω) → dom 𝑂 ⊆ ω)
8280, 56, 81sylancr 587 . . . . . . . . . 10 ((𝑅 Or 𝐴𝐴 ∈ Fin) → dom 𝑂 ⊆ ω)
83 sseqin2 4231 . . . . . . . . . 10 (dom 𝑂 ⊆ ω ↔ (ω ∩ dom 𝑂) = dom 𝑂)
8482, 83sylib 218 . . . . . . . . 9 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (ω ∩ dom 𝑂) = dom 𝑂)
8579, 84eqtrd 2775 . . . . . . . 8 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (ω ∩ (𝐺‘((♯‘𝐴) + 1))) = dom 𝑂)
8614, 85eqtrid 2787 . . . . . . 7 ((𝑅 Or 𝐴𝐴 ∈ Fin) → 𝐶 = dom 𝑂)
87 isoeq5 7341 . . . . . . 7 (𝐶 = dom 𝑂 → ((𝐺𝐵) Isom < , E ((1...(♯‘𝐴)), 𝐶) ↔ (𝐺𝐵) Isom < , E ((1...(♯‘𝐴)), dom 𝑂)))
8886, 87syl 17 . . . . . 6 ((𝑅 Or 𝐴𝐴 ∈ Fin) → ((𝐺𝐵) Isom < , E ((1...(♯‘𝐴)), 𝐶) ↔ (𝐺𝐵) Isom < , E ((1...(♯‘𝐴)), dom 𝑂)))
8944, 88mpbid 232 . . . . 5 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝐺𝐵) Isom < , E ((1...(♯‘𝐴)), dom 𝑂))
9045oiiso 9575 . . . . . 6 ((𝐴 ∈ Fin ∧ 𝑅 We 𝐴) → 𝑂 Isom E , 𝑅 (dom 𝑂, 𝐴))
9148, 49, 90syl2anc 584 . . . . 5 ((𝑅 Or 𝐴𝐴 ∈ Fin) → 𝑂 Isom E , 𝑅 (dom 𝑂, 𝐴))
92 isotr 7356 . . . . 5 (((𝐺𝐵) Isom < , E ((1...(♯‘𝐴)), dom 𝑂) ∧ 𝑂 Isom E , 𝑅 (dom 𝑂, 𝐴)) → (𝑂 ∘ (𝐺𝐵)) Isom < , 𝑅 ((1...(♯‘𝐴)), 𝐴))
9389, 91, 92syl2anc 584 . . . 4 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝑂 ∘ (𝐺𝐵)) Isom < , 𝑅 ((1...(♯‘𝐴)), 𝐴))
94 isof1o 7343 . . . 4 ((𝑂 ∘ (𝐺𝐵)) Isom < , 𝑅 ((1...(♯‘𝐴)), 𝐴) → (𝑂 ∘ (𝐺𝐵)):(1...(♯‘𝐴))–1-1-onto𝐴)
95 f1of 6849 . . . 4 ((𝑂 ∘ (𝐺𝐵)):(1...(♯‘𝐴))–1-1-onto𝐴 → (𝑂 ∘ (𝐺𝐵)):(1...(♯‘𝐴))⟶𝐴)
9693, 94, 953syl 18 . . 3 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝑂 ∘ (𝐺𝐵)):(1...(♯‘𝐴))⟶𝐴)
97 fzfid 14011 . . 3 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (1...(♯‘𝐴)) ∈ Fin)
9896, 97fexd 7247 . 2 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝑂 ∘ (𝐺𝐵)) ∈ V)
99 isoeq1 7337 . 2 (𝑓 = (𝑂 ∘ (𝐺𝐵)) → (𝑓 Isom < , 𝑅 ((1...(♯‘𝐴)), 𝐴) ↔ (𝑂 ∘ (𝐺𝐵)) Isom < , 𝑅 ((1...(♯‘𝐴)), 𝐴)))
10098, 93, 99spcedv 3598 1 ((𝑅 Or 𝐴𝐴 ∈ Fin) → ∃𝑓 𝑓 Isom < , 𝑅 ((1...(♯‘𝐴)), 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395   = wceq 1537  wex 1776  wcel 2106  Vcvv 3478  cin 3962  wss 3963  {csn 4631   class class class wbr 5148  cmpt 5231   E cep 5588   Or wor 5596   We wwe 5640  ccnv 5688  dom cdm 5689  cres 5691  cima 5692  ccom 5693  Ord word 6385  Oncon0 6386  wf 6559  1-1-ontowf1o 6562  cfv 6563   Isom wiso 6564  (class class class)co 7431  ωcom 7887  reccrdg 8448  cen 8981  Fincfn 8984  OrdIsocoi 9547  cardccrd 9973  0cc0 11153  1c1 11154   + caddc 11156   < clt 11293  cle 11294  cmin 11490  cn 12264  0cn0 12524  cz 12611  cuz 12876  ...cfz 13544  chash 14366
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754  ax-cnex 11209  ax-resscn 11210  ax-1cn 11211  ax-icn 11212  ax-addcl 11213  ax-addrcl 11214  ax-mulcl 11215  ax-mulrcl 11216  ax-mulcom 11217  ax-addass 11218  ax-mulass 11219  ax-distr 11220  ax-i2m1 11221  ax-1ne0 11222  ax-1rid 11223  ax-rnegex 11224  ax-rrecex 11225  ax-cnre 11226  ax-pre-lttri 11227  ax-pre-lttrn 11228  ax-pre-ltadd 11229  ax-pre-mulgt0 11230
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-pss 3983  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-int 4952  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-tr 5266  df-id 5583  df-eprel 5589  df-po 5597  df-so 5598  df-fr 5641  df-se 5642  df-we 5643  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-pred 6323  df-ord 6389  df-on 6390  df-lim 6391  df-suc 6392  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-isom 6572  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-om 7888  df-1st 8013  df-2nd 8014  df-frecs 8305  df-wrecs 8336  df-recs 8410  df-rdg 8449  df-1o 8505  df-er 8744  df-en 8985  df-dom 8986  df-sdom 8987  df-fin 8988  df-oi 9548  df-card 9977  df-pnf 11295  df-mnf 11296  df-xr 11297  df-ltxr 11298  df-le 11299  df-sub 11492  df-neg 11493  df-nn 12265  df-n0 12525  df-z 12612  df-uz 12877  df-fz 13545  df-hash 14367
This theorem is referenced by:  fz1iso  14498
  Copyright terms: Public domain W3C validator