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

Theorem fz1isolem 13445
Description: Lemma for fz1iso 13446. (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 13348 . . . . . . . . 9 (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℕ0)
21adantl 473 . . . . . . . 8 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (♯‘𝐴) ∈ ℕ0)
3 nnuz 11922 . . . . . . . . . . 11 ℕ = (ℤ‘1)
4 1z 11653 . . . . . . . . . . . . 13 1 ∈ ℤ
5 fz1iso.1 . . . . . . . . . . . . 13 𝐺 = (rec((𝑛 ∈ V ↦ (𝑛 + 1)), 1) ↾ ω)
64, 5om2uzisoi 12960 . . . . . . . . . . . 12 𝐺 Isom E , < (ω, (ℤ‘1))
7 isoeq5 6762 . . . . . . . . . . . 12 (ℕ = (ℤ‘1) → (𝐺 Isom E , < (ω, ℕ) ↔ 𝐺 Isom E , < (ω, (ℤ‘1))))
86, 7mpbiri 249 . . . . . . . . . . 11 (ℕ = (ℤ‘1) → 𝐺 Isom E , < (ω, ℕ))
93, 8ax-mp 5 . . . . . . . . . 10 𝐺 Isom E , < (ω, ℕ)
10 isocnv 6771 . . . . . . . . . 10 (𝐺 Isom E , < (ω, ℕ) → 𝐺 Isom < , E (ℕ, ω))
119, 10ax-mp 5 . . . . . . . . 9 𝐺 Isom < , E (ℕ, ω)
12 nn0p1nn 11578 . . . . . . . . 9 ((♯‘𝐴) ∈ ℕ0 → ((♯‘𝐴) + 1) ∈ ℕ)
13 fz1iso.2 . . . . . . . . . 10 𝐵 = (ℕ ∩ ( < “ {((♯‘𝐴) + 1)}))
14 fz1iso.3 . . . . . . . . . . 11 𝐶 = (ω ∩ (𝐺‘((♯‘𝐴) + 1)))
15 fvex 6387 . . . . . . . . . . . . 13 (𝐺‘((♯‘𝐴) + 1)) ∈ V
1615epini 5676 . . . . . . . . . . . 12 ( E “ {(𝐺‘((♯‘𝐴) + 1))}) = (𝐺‘((♯‘𝐴) + 1))
1716ineq2i 3972 . . . . . . . . . . 11 (ω ∩ ( E “ {(𝐺‘((♯‘𝐴) + 1))})) = (ω ∩ (𝐺‘((♯‘𝐴) + 1)))
1814, 17eqtr4i 2789 . . . . . . . . . 10 𝐶 = (ω ∩ ( E “ {(𝐺‘((♯‘𝐴) + 1))}))
1913, 18isoini2 6780 . . . . . . . . 9 ((𝐺 Isom < , E (ℕ, ω) ∧ ((♯‘𝐴) + 1) ∈ ℕ) → (𝐺𝐵) Isom < , E (𝐵, 𝐶))
2011, 12, 19sylancr 581 . . . . . . . 8 ((♯‘𝐴) ∈ ℕ0 → (𝐺𝐵) Isom < , E (𝐵, 𝐶))
212, 20syl 17 . . . . . . 7 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝐺𝐵) Isom < , E (𝐵, 𝐶))
22 nnz 11645 . . . . . . . . . . . . 13 (𝑓 ∈ ℕ → 𝑓 ∈ ℤ)
232nn0zd 11726 . . . . . . . . . . . . 13 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (♯‘𝐴) ∈ ℤ)
24 eluz 11899 . . . . . . . . . . . . 13 ((𝑓 ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ) → ((♯‘𝐴) ∈ (ℤ𝑓) ↔ 𝑓 ≤ (♯‘𝐴)))
2522, 23, 24syl2anr 590 . . . . . . . . . . . 12 (((𝑅 Or 𝐴𝐴 ∈ Fin) ∧ 𝑓 ∈ ℕ) → ((♯‘𝐴) ∈ (ℤ𝑓) ↔ 𝑓 ≤ (♯‘𝐴)))
26 zleltp1 11674 . . . . . . . . . . . . . 14 ((𝑓 ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ) → (𝑓 ≤ (♯‘𝐴) ↔ 𝑓 < ((♯‘𝐴) + 1)))
2722, 23, 26syl2anr 590 . . . . . . . . . . . . 13 (((𝑅 Or 𝐴𝐴 ∈ Fin) ∧ 𝑓 ∈ ℕ) → (𝑓 ≤ (♯‘𝐴) ↔ 𝑓 < ((♯‘𝐴) + 1)))
28 ovex 6873 . . . . . . . . . . . . . 14 ((♯‘𝐴) + 1) ∈ V
29 vex 3352 . . . . . . . . . . . . . . 15 𝑓 ∈ V
3029eliniseg 5675 . . . . . . . . . . . . . 14 (((♯‘𝐴) + 1) ∈ V → (𝑓 ∈ ( < “ {((♯‘𝐴) + 1)}) ↔ 𝑓 < ((♯‘𝐴) + 1)))
3128, 30ax-mp 5 . . . . . . . . . . . . 13 (𝑓 ∈ ( < “ {((♯‘𝐴) + 1)}) ↔ 𝑓 < ((♯‘𝐴) + 1))
3227, 31syl6bbr 280 . . . . . . . . . . . 12 (((𝑅 Or 𝐴𝐴 ∈ Fin) ∧ 𝑓 ∈ ℕ) → (𝑓 ≤ (♯‘𝐴) ↔ 𝑓 ∈ ( < “ {((♯‘𝐴) + 1)})))
3325, 32bitr2d 271 . . . . . . . . . . 11 (((𝑅 Or 𝐴𝐴 ∈ Fin) ∧ 𝑓 ∈ ℕ) → (𝑓 ∈ ( < “ {((♯‘𝐴) + 1)}) ↔ (♯‘𝐴) ∈ (ℤ𝑓)))
3433pm5.32da 574 . . . . . . . . . 10 ((𝑅 Or 𝐴𝐴 ∈ Fin) → ((𝑓 ∈ ℕ ∧ 𝑓 ∈ ( < “ {((♯‘𝐴) + 1)})) ↔ (𝑓 ∈ ℕ ∧ (♯‘𝐴) ∈ (ℤ𝑓))))
3513elin2 3962 . . . . . . . . . 10 (𝑓𝐵 ↔ (𝑓 ∈ ℕ ∧ 𝑓 ∈ ( < “ {((♯‘𝐴) + 1)})))
36 elfzuzb 12542 . . . . . . . . . . 11 (𝑓 ∈ (1...(♯‘𝐴)) ↔ (𝑓 ∈ (ℤ‘1) ∧ (♯‘𝐴) ∈ (ℤ𝑓)))
37 elnnuz 11923 . . . . . . . . . . . 12 (𝑓 ∈ ℕ ↔ 𝑓 ∈ (ℤ‘1))
3837anbi1i 617 . . . . . . . . . . 11 ((𝑓 ∈ ℕ ∧ (♯‘𝐴) ∈ (ℤ𝑓)) ↔ (𝑓 ∈ (ℤ‘1) ∧ (♯‘𝐴) ∈ (ℤ𝑓)))
3936, 38bitr4i 269 . . . . . . . . . 10 (𝑓 ∈ (1...(♯‘𝐴)) ↔ (𝑓 ∈ ℕ ∧ (♯‘𝐴) ∈ (ℤ𝑓)))
4034, 35, 393bitr4g 305 . . . . . . . . 9 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝑓𝐵𝑓 ∈ (1...(♯‘𝐴))))
4140eqrdv 2762 . . . . . . . 8 ((𝑅 Or 𝐴𝐴 ∈ Fin) → 𝐵 = (1...(♯‘𝐴)))
42 isoeq4 6761 . . . . . . . 8 (𝐵 = (1...(♯‘𝐴)) → ((𝐺𝐵) Isom < , E (𝐵, 𝐶) ↔ (𝐺𝐵) Isom < , E ((1...(♯‘𝐴)), 𝐶)))
4341, 42syl 17 . . . . . . 7 ((𝑅 Or 𝐴𝐴 ∈ Fin) → ((𝐺𝐵) Isom < , E (𝐵, 𝐶) ↔ (𝐺𝐵) Isom < , E ((1...(♯‘𝐴)), 𝐶)))
4421, 43mpbid 223 . . . . . 6 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝐺𝐵) Isom < , E ((1...(♯‘𝐴)), 𝐶))
45 fz1iso.4 . . . . . . . . . . . . . . . . . 18 𝑂 = OrdIso(𝑅, 𝐴)
4645oion 8647 . . . . . . . . . . . . . . . . 17 (𝐴 ∈ Fin → dom 𝑂 ∈ On)
4746adantl 473 . . . . . . . . . . . . . . . 16 ((𝑅 Or 𝐴𝐴 ∈ Fin) → dom 𝑂 ∈ On)
48 simpr 477 . . . . . . . . . . . . . . . . 17 ((𝑅 Or 𝐴𝐴 ∈ Fin) → 𝐴 ∈ Fin)
49 wofi 8415 . . . . . . . . . . . . . . . . . 18 ((𝑅 Or 𝐴𝐴 ∈ Fin) → 𝑅 We 𝐴)
5045oien 8649 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ Fin ∧ 𝑅 We 𝐴) → dom 𝑂𝐴)
5148, 49, 50syl2anc 579 . . . . . . . . . . . . . . . . 17 ((𝑅 Or 𝐴𝐴 ∈ Fin) → dom 𝑂𝐴)
52 enfii 8383 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ Fin ∧ dom 𝑂𝐴) → dom 𝑂 ∈ Fin)
5348, 51, 52syl2anc 579 . . . . . . . . . . . . . . . 16 ((𝑅 Or 𝐴𝐴 ∈ Fin) → dom 𝑂 ∈ Fin)
5447, 53elind 3959 . . . . . . . . . . . . . . 15 ((𝑅 Or 𝐴𝐴 ∈ Fin) → dom 𝑂 ∈ (On ∩ Fin))
55 onfin2 8358 . . . . . . . . . . . . . . 15 ω = (On ∩ Fin)
5654, 55syl6eleqr 2854 . . . . . . . . . . . . . 14 ((𝑅 Or 𝐴𝐴 ∈ Fin) → dom 𝑂 ∈ ω)
57 eqid 2764 . . . . . . . . . . . . . . . 16 (rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω) = (rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)
58 0z 11634 . . . . . . . . . . . . . . . 16 0 ∈ ℤ
595, 57, 4, 58uzrdgxfr 12973 . . . . . . . . . . . . . . 15 (dom 𝑂 ∈ ω → (𝐺‘dom 𝑂) = (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂) + (1 − 0)))
60 1m0e1 11399 . . . . . . . . . . . . . . . 16 (1 − 0) = 1
6160oveq2i 6852 . . . . . . . . . . . . . . 15 (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂) + (1 − 0)) = (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂) + 1)
6259, 61syl6eq 2814 . . . . . . . . . . . . . 14 (dom 𝑂 ∈ ω → (𝐺‘dom 𝑂) = (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂) + 1))
6356, 62syl 17 . . . . . . . . . . . . 13 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝐺‘dom 𝑂) = (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂) + 1))
6451ensymd 8210 . . . . . . . . . . . . . . . . 17 ((𝑅 Or 𝐴𝐴 ∈ Fin) → 𝐴 ≈ dom 𝑂)
65 cardennn 9059 . . . . . . . . . . . . . . . . 17 ((𝐴 ≈ dom 𝑂 ∧ dom 𝑂 ∈ ω) → (card‘𝐴) = dom 𝑂)
6664, 56, 65syl2anc 579 . . . . . . . . . . . . . . . 16 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (card‘𝐴) = dom 𝑂)
6766fveq2d 6378 . . . . . . . . . . . . . . 15 ((𝑅 Or 𝐴𝐴 ∈ Fin) → ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘(card‘𝐴)) = ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂))
6857hashgval 13323 . . . . . . . . . . . . . . . 16 (𝐴 ∈ Fin → ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘(card‘𝐴)) = (♯‘𝐴))
6968adantl 473 . . . . . . . . . . . . . . 15 ((𝑅 Or 𝐴𝐴 ∈ Fin) → ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘(card‘𝐴)) = (♯‘𝐴))
7067, 69eqtr3d 2800 . . . . . . . . . . . . . 14 ((𝑅 Or 𝐴𝐴 ∈ Fin) → ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂) = (♯‘𝐴))
7170oveq1d 6856 . . . . . . . . . . . . 13 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂) + 1) = ((♯‘𝐴) + 1))
7263, 71eqtrd 2798 . . . . . . . . . . . 12 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝐺‘dom 𝑂) = ((♯‘𝐴) + 1))
7372fveq2d 6378 . . . . . . . . . . 11 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝐺‘(𝐺‘dom 𝑂)) = (𝐺‘((♯‘𝐴) + 1)))
74 isof1o 6764 . . . . . . . . . . . . 13 (𝐺 Isom E , < (ω, ℕ) → 𝐺:ω–1-1-onto→ℕ)
759, 74ax-mp 5 . . . . . . . . . . . 12 𝐺:ω–1-1-onto→ℕ
76 f1ocnvfv1 6723 . . . . . . . . . . . 12 ((𝐺:ω–1-1-onto→ℕ ∧ dom 𝑂 ∈ ω) → (𝐺‘(𝐺‘dom 𝑂)) = dom 𝑂)
7775, 56, 76sylancr 581 . . . . . . . . . . 11 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝐺‘(𝐺‘dom 𝑂)) = dom 𝑂)
7873, 77eqtr3d 2800 . . . . . . . . . 10 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝐺‘((♯‘𝐴) + 1)) = dom 𝑂)
7978ineq2d 3975 . . . . . . . . 9 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (ω ∩ (𝐺‘((♯‘𝐴) + 1))) = (ω ∩ dom 𝑂))
80 ordom 7271 . . . . . . . . . . 11 Ord ω
81 ordelss 5923 . . . . . . . . . . 11 ((Ord ω ∧ dom 𝑂 ∈ ω) → dom 𝑂 ⊆ ω)
8280, 56, 81sylancr 581 . . . . . . . . . 10 ((𝑅 Or 𝐴𝐴 ∈ Fin) → dom 𝑂 ⊆ ω)
83 sseqin2 3978 . . . . . . . . . 10 (dom 𝑂 ⊆ ω ↔ (ω ∩ dom 𝑂) = dom 𝑂)
8482, 83sylib 209 . . . . . . . . 9 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (ω ∩ dom 𝑂) = dom 𝑂)
8579, 84eqtrd 2798 . . . . . . . 8 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (ω ∩ (𝐺‘((♯‘𝐴) + 1))) = dom 𝑂)
8614, 85syl5eq 2810 . . . . . . 7 ((𝑅 Or 𝐴𝐴 ∈ Fin) → 𝐶 = dom 𝑂)
87 isoeq5 6762 . . . . . . 7 (𝐶 = dom 𝑂 → ((𝐺𝐵) Isom < , E ((1...(♯‘𝐴)), 𝐶) ↔ (𝐺𝐵) Isom < , E ((1...(♯‘𝐴)), dom 𝑂)))
8886, 87syl 17 . . . . . 6 ((𝑅 Or 𝐴𝐴 ∈ Fin) → ((𝐺𝐵) Isom < , E ((1...(♯‘𝐴)), 𝐶) ↔ (𝐺𝐵) Isom < , E ((1...(♯‘𝐴)), dom 𝑂)))
8944, 88mpbid 223 . . . . 5 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝐺𝐵) Isom < , E ((1...(♯‘𝐴)), dom 𝑂))
9045oiiso 8648 . . . . . 6 ((𝐴 ∈ Fin ∧ 𝑅 We 𝐴) → 𝑂 Isom E , 𝑅 (dom 𝑂, 𝐴))
9148, 49, 90syl2anc 579 . . . . 5 ((𝑅 Or 𝐴𝐴 ∈ Fin) → 𝑂 Isom E , 𝑅 (dom 𝑂, 𝐴))
92 isotr 6777 . . . . 5 (((𝐺𝐵) Isom < , E ((1...(♯‘𝐴)), dom 𝑂) ∧ 𝑂 Isom E , 𝑅 (dom 𝑂, 𝐴)) → (𝑂 ∘ (𝐺𝐵)) Isom < , 𝑅 ((1...(♯‘𝐴)), 𝐴))
9389, 91, 92syl2anc 579 . . . 4 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝑂 ∘ (𝐺𝐵)) Isom < , 𝑅 ((1...(♯‘𝐴)), 𝐴))
94 isof1o 6764 . . . 4 ((𝑂 ∘ (𝐺𝐵)) Isom < , 𝑅 ((1...(♯‘𝐴)), 𝐴) → (𝑂 ∘ (𝐺𝐵)):(1...(♯‘𝐴))–1-1-onto𝐴)
95 f1of 6319 . . . 4 ((𝑂 ∘ (𝐺𝐵)):(1...(♯‘𝐴))–1-1-onto𝐴 → (𝑂 ∘ (𝐺𝐵)):(1...(♯‘𝐴))⟶𝐴)
9693, 94, 953syl 18 . . 3 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝑂 ∘ (𝐺𝐵)):(1...(♯‘𝐴))⟶𝐴)
97 fzfid 12979 . . 3 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (1...(♯‘𝐴)) ∈ Fin)
98 fex 6681 . . 3 (((𝑂 ∘ (𝐺𝐵)):(1...(♯‘𝐴))⟶𝐴 ∧ (1...(♯‘𝐴)) ∈ Fin) → (𝑂 ∘ (𝐺𝐵)) ∈ V)
9996, 97, 98syl2anc 579 . 2 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝑂 ∘ (𝐺𝐵)) ∈ V)
100 isoeq1 6758 . . 3 (𝑓 = (𝑂 ∘ (𝐺𝐵)) → (𝑓 Isom < , 𝑅 ((1...(♯‘𝐴)), 𝐴) ↔ (𝑂 ∘ (𝐺𝐵)) Isom < , 𝑅 ((1...(♯‘𝐴)), 𝐴)))
101100spcegv 3445 . 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 197  wa 384   = wceq 1652  wex 1874  wcel 2155  Vcvv 3349  cin 3730  wss 3731  {csn 4333   class class class wbr 4808  cmpt 4887   E cep 5188   Or wor 5196   We wwe 5234  ccnv 5275  dom cdm 5276  cres 5278  cima 5279  ccom 5280  Ord word 5906  Oncon0 5907  wf 6063  1-1-ontowf1o 6066  cfv 6067   Isom wiso 6068  (class class class)co 6841  ωcom 7262  reccrdg 7708  cen 8156  Fincfn 8159  OrdIsocoi 8620  cardccrd 9011  0cc0 10188  1c1 10189   + caddc 10191   < clt 10327  cle 10328  cmin 10519  cn 11273  0cn0 11537  cz 11623  cuz 11885  ...cfz 12532  chash 13320
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2069  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2349  ax-ext 2742  ax-rep 4929  ax-sep 4940  ax-nul 4948  ax-pow 5000  ax-pr 5061  ax-un 7146  ax-cnex 10244  ax-resscn 10245  ax-1cn 10246  ax-icn 10247  ax-addcl 10248  ax-addrcl 10249  ax-mulcl 10250  ax-mulrcl 10251  ax-mulcom 10252  ax-addass 10253  ax-mulass 10254  ax-distr 10255  ax-i2m1 10256  ax-1ne0 10257  ax-1rid 10258  ax-rnegex 10259  ax-rrecex 10260  ax-cnre 10261  ax-pre-lttri 10262  ax-pre-lttrn 10263  ax-pre-ltadd 10264  ax-pre-mulgt0 10265
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3or 1108  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2062  df-mo 2564  df-eu 2581  df-clab 2751  df-cleq 2757  df-clel 2760  df-nfc 2895  df-ne 2937  df-nel 3040  df-ral 3059  df-rex 3060  df-reu 3061  df-rmo 3062  df-rab 3063  df-v 3351  df-sbc 3596  df-csb 3691  df-dif 3734  df-un 3736  df-in 3738  df-ss 3745  df-pss 3747  df-nul 4079  df-if 4243  df-pw 4316  df-sn 4334  df-pr 4336  df-tp 4338  df-op 4340  df-uni 4594  df-int 4633  df-iun 4677  df-br 4809  df-opab 4871  df-mpt 4888  df-tr 4911  df-id 5184  df-eprel 5189  df-po 5197  df-so 5198  df-fr 5235  df-se 5236  df-we 5237  df-xp 5282  df-rel 5283  df-cnv 5284  df-co 5285  df-dm 5286  df-rn 5287  df-res 5288  df-ima 5289  df-pred 5864  df-ord 5910  df-on 5911  df-lim 5912  df-suc 5913  df-iota 6030  df-fun 6069  df-fn 6070  df-f 6071  df-f1 6072  df-fo 6073  df-f1o 6074  df-fv 6075  df-isom 6076  df-riota 6802  df-ov 6844  df-oprab 6845  df-mpt2 6846  df-om 7263  df-1st 7365  df-2nd 7366  df-wrecs 7609  df-recs 7671  df-rdg 7709  df-1o 7763  df-er 7946  df-en 8160  df-dom 8161  df-sdom 8162  df-fin 8163  df-oi 8621  df-card 9015  df-pnf 10329  df-mnf 10330  df-xr 10331  df-ltxr 10332  df-le 10333  df-sub 10521  df-neg 10522  df-nn 11274  df-n0 11538  df-z 11624  df-uz 11886  df-fz 12533  df-hash 13321
This theorem is referenced by:  fz1iso  13446
  Copyright terms: Public domain W3C validator