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

Theorem fz1isolem 13283
Description: Lemma for fz1iso 13284. (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 13185 . . . . . . . . 9 (𝐴 ∈ Fin → (#‘𝐴) ∈ ℕ0)
21adantl 481 . . . . . . . 8 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (#‘𝐴) ∈ ℕ0)
3 nnuz 11761 . . . . . . . . . . 11 ℕ = (ℤ‘1)
4 1z 11445 . . . . . . . . . . . . 13 1 ∈ ℤ
5 fz1iso.1 . . . . . . . . . . . . 13 𝐺 = (rec((𝑛 ∈ V ↦ (𝑛 + 1)), 1) ↾ ω)
64, 5om2uzisoi 12793 . . . . . . . . . . . 12 𝐺 Isom E , < (ω, (ℤ‘1))
7 isoeq5 6611 . . . . . . . . . . . 12 (ℕ = (ℤ‘1) → (𝐺 Isom E , < (ω, ℕ) ↔ 𝐺 Isom E , < (ω, (ℤ‘1))))
86, 7mpbiri 248 . . . . . . . . . . 11 (ℕ = (ℤ‘1) → 𝐺 Isom E , < (ω, ℕ))
93, 8ax-mp 5 . . . . . . . . . 10 𝐺 Isom E , < (ω, ℕ)
10 isocnv 6620 . . . . . . . . . 10 (𝐺 Isom E , < (ω, ℕ) → 𝐺 Isom < , E (ℕ, ω))
119, 10ax-mp 5 . . . . . . . . 9 𝐺 Isom < , E (ℕ, ω)
12 nn0p1nn 11370 . . . . . . . . 9 ((#‘𝐴) ∈ ℕ0 → ((#‘𝐴) + 1) ∈ ℕ)
13 fz1iso.2 . . . . . . . . . 10 𝐵 = (ℕ ∩ ( < “ {((#‘𝐴) + 1)}))
14 fz1iso.3 . . . . . . . . . . 11 𝐶 = (ω ∩ (𝐺‘((#‘𝐴) + 1)))
15 fvex 6239 . . . . . . . . . . . . 13 (𝐺‘((#‘𝐴) + 1)) ∈ V
1615epini 5530 . . . . . . . . . . . 12 ( E “ {(𝐺‘((#‘𝐴) + 1))}) = (𝐺‘((#‘𝐴) + 1))
1716ineq2i 3844 . . . . . . . . . . 11 (ω ∩ ( E “ {(𝐺‘((#‘𝐴) + 1))})) = (ω ∩ (𝐺‘((#‘𝐴) + 1)))
1814, 17eqtr4i 2676 . . . . . . . . . 10 𝐶 = (ω ∩ ( E “ {(𝐺‘((#‘𝐴) + 1))}))
1913, 18isoini2 6629 . . . . . . . . 9 ((𝐺 Isom < , E (ℕ, ω) ∧ ((#‘𝐴) + 1) ∈ ℕ) → (𝐺𝐵) Isom < , E (𝐵, 𝐶))
2011, 12, 19sylancr 696 . . . . . . . 8 ((#‘𝐴) ∈ ℕ0 → (𝐺𝐵) Isom < , E (𝐵, 𝐶))
212, 20syl 17 . . . . . . 7 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝐺𝐵) Isom < , E (𝐵, 𝐶))
22 nnz 11437 . . . . . . . . . . . . 13 (𝑓 ∈ ℕ → 𝑓 ∈ ℤ)
232nn0zd 11518 . . . . . . . . . . . . 13 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (#‘𝐴) ∈ ℤ)
24 eluz 11739 . . . . . . . . . . . . 13 ((𝑓 ∈ ℤ ∧ (#‘𝐴) ∈ ℤ) → ((#‘𝐴) ∈ (ℤ𝑓) ↔ 𝑓 ≤ (#‘𝐴)))
2522, 23, 24syl2anr 494 . . . . . . . . . . . 12 (((𝑅 Or 𝐴𝐴 ∈ Fin) ∧ 𝑓 ∈ ℕ) → ((#‘𝐴) ∈ (ℤ𝑓) ↔ 𝑓 ≤ (#‘𝐴)))
26 zleltp1 11466 . . . . . . . . . . . . . 14 ((𝑓 ∈ ℤ ∧ (#‘𝐴) ∈ ℤ) → (𝑓 ≤ (#‘𝐴) ↔ 𝑓 < ((#‘𝐴) + 1)))
2722, 23, 26syl2anr 494 . . . . . . . . . . . . 13 (((𝑅 Or 𝐴𝐴 ∈ Fin) ∧ 𝑓 ∈ ℕ) → (𝑓 ≤ (#‘𝐴) ↔ 𝑓 < ((#‘𝐴) + 1)))
28 ovex 6718 . . . . . . . . . . . . . 14 ((#‘𝐴) + 1) ∈ V
29 vex 3234 . . . . . . . . . . . . . . 15 𝑓 ∈ V
3029eliniseg 5529 . . . . . . . . . . . . . 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 674 . . . . . . . . . 10 ((𝑅 Or 𝐴𝐴 ∈ Fin) → ((𝑓 ∈ ℕ ∧ 𝑓 ∈ ( < “ {((#‘𝐴) + 1)})) ↔ (𝑓 ∈ ℕ ∧ (#‘𝐴) ∈ (ℤ𝑓))))
3513elin2 3834 . . . . . . . . . 10 (𝑓𝐵 ↔ (𝑓 ∈ ℕ ∧ 𝑓 ∈ ( < “ {((#‘𝐴) + 1)})))
36 elfzuzb 12374 . . . . . . . . . . 11 (𝑓 ∈ (1...(#‘𝐴)) ↔ (𝑓 ∈ (ℤ‘1) ∧ (#‘𝐴) ∈ (ℤ𝑓)))
37 elnnuz 11762 . . . . . . . . . . . 12 (𝑓 ∈ ℕ ↔ 𝑓 ∈ (ℤ‘1))
3837anbi1i 731 . . . . . . . . . . 11 ((𝑓 ∈ ℕ ∧ (#‘𝐴) ∈ (ℤ𝑓)) ↔ (𝑓 ∈ (ℤ‘1) ∧ (#‘𝐴) ∈ (ℤ𝑓)))
3936, 38bitr4i 267 . . . . . . . . . 10 (𝑓 ∈ (1...(#‘𝐴)) ↔ (𝑓 ∈ ℕ ∧ (#‘𝐴) ∈ (ℤ𝑓)))
4034, 35, 393bitr4g 303 . . . . . . . . 9 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝑓𝐵𝑓 ∈ (1...(#‘𝐴))))
4140eqrdv 2649 . . . . . . . 8 ((𝑅 Or 𝐴𝐴 ∈ Fin) → 𝐵 = (1...(#‘𝐴)))
42 isoeq4 6610 . . . . . . . 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 8482 . . . . . . . . . . . . . . . . 17 (𝐴 ∈ Fin → dom 𝑂 ∈ On)
4746adantl 481 . . . . . . . . . . . . . . . 16 ((𝑅 Or 𝐴𝐴 ∈ Fin) → dom 𝑂 ∈ On)
48 simpr 476 . . . . . . . . . . . . . . . . 17 ((𝑅 Or 𝐴𝐴 ∈ Fin) → 𝐴 ∈ Fin)
49 wofi 8250 . . . . . . . . . . . . . . . . . 18 ((𝑅 Or 𝐴𝐴 ∈ Fin) → 𝑅 We 𝐴)
5045oien 8484 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ Fin ∧ 𝑅 We 𝐴) → dom 𝑂𝐴)
5148, 49, 50syl2anc 694 . . . . . . . . . . . . . . . . 17 ((𝑅 Or 𝐴𝐴 ∈ Fin) → dom 𝑂𝐴)
52 enfii 8218 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ Fin ∧ dom 𝑂𝐴) → dom 𝑂 ∈ Fin)
5348, 51, 52syl2anc 694 . . . . . . . . . . . . . . . 16 ((𝑅 Or 𝐴𝐴 ∈ Fin) → dom 𝑂 ∈ Fin)
5447, 53elind 3831 . . . . . . . . . . . . . . 15 ((𝑅 Or 𝐴𝐴 ∈ Fin) → dom 𝑂 ∈ (On ∩ Fin))
55 onfin2 8193 . . . . . . . . . . . . . . 15 ω = (On ∩ Fin)
5654, 55syl6eleqr 2741 . . . . . . . . . . . . . 14 ((𝑅 Or 𝐴𝐴 ∈ Fin) → dom 𝑂 ∈ ω)
57 eqid 2651 . . . . . . . . . . . . . . . 16 (rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω) = (rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)
58 0z 11426 . . . . . . . . . . . . . . . 16 0 ∈ ℤ
595, 57, 4, 58uzrdgxfr 12806 . . . . . . . . . . . . . . 15 (dom 𝑂 ∈ ω → (𝐺‘dom 𝑂) = (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂) + (1 − 0)))
60 1m0e1 11169 . . . . . . . . . . . . . . . 16 (1 − 0) = 1
6160oveq2i 6701 . . . . . . . . . . . . . . 15 (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂) + (1 − 0)) = (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂) + 1)
6259, 61syl6eq 2701 . . . . . . . . . . . . . 14 (dom 𝑂 ∈ ω → (𝐺‘dom 𝑂) = (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂) + 1))
6356, 62syl 17 . . . . . . . . . . . . 13 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝐺‘dom 𝑂) = (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂) + 1))
6451ensymd 8048 . . . . . . . . . . . . . . . . 17 ((𝑅 Or 𝐴𝐴 ∈ Fin) → 𝐴 ≈ dom 𝑂)
65 cardennn 8847 . . . . . . . . . . . . . . . . 17 ((𝐴 ≈ dom 𝑂 ∧ dom 𝑂 ∈ ω) → (card‘𝐴) = dom 𝑂)
6664, 56, 65syl2anc 694 . . . . . . . . . . . . . . . 16 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (card‘𝐴) = dom 𝑂)
6766fveq2d 6233 . . . . . . . . . . . . . . 15 ((𝑅 Or 𝐴𝐴 ∈ Fin) → ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘(card‘𝐴)) = ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂))
6857hashgval 13160 . . . . . . . . . . . . . . . 16 (𝐴 ∈ Fin → ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘(card‘𝐴)) = (#‘𝐴))
6968adantl 481 . . . . . . . . . . . . . . 15 ((𝑅 Or 𝐴𝐴 ∈ Fin) → ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘(card‘𝐴)) = (#‘𝐴))
7067, 69eqtr3d 2687 . . . . . . . . . . . . . 14 ((𝑅 Or 𝐴𝐴 ∈ Fin) → ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂) = (#‘𝐴))
7170oveq1d 6705 . . . . . . . . . . . . 13 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂) + 1) = ((#‘𝐴) + 1))
7263, 71eqtrd 2685 . . . . . . . . . . . 12 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝐺‘dom 𝑂) = ((#‘𝐴) + 1))
7372fveq2d 6233 . . . . . . . . . . 11 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝐺‘(𝐺‘dom 𝑂)) = (𝐺‘((#‘𝐴) + 1)))
74 isof1o 6613 . . . . . . . . . . . . 13 (𝐺 Isom E , < (ω, ℕ) → 𝐺:ω–1-1-onto→ℕ)
759, 74ax-mp 5 . . . . . . . . . . . 12 𝐺:ω–1-1-onto→ℕ
76 f1ocnvfv1 6572 . . . . . . . . . . . 12 ((𝐺:ω–1-1-onto→ℕ ∧ dom 𝑂 ∈ ω) → (𝐺‘(𝐺‘dom 𝑂)) = dom 𝑂)
7775, 56, 76sylancr 696 . . . . . . . . . . 11 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝐺‘(𝐺‘dom 𝑂)) = dom 𝑂)
7873, 77eqtr3d 2687 . . . . . . . . . 10 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝐺‘((#‘𝐴) + 1)) = dom 𝑂)
7978ineq2d 3847 . . . . . . . . 9 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (ω ∩ (𝐺‘((#‘𝐴) + 1))) = (ω ∩ dom 𝑂))
80 ordom 7116 . . . . . . . . . . 11 Ord ω
81 ordelss 5777 . . . . . . . . . . 11 ((Ord ω ∧ dom 𝑂 ∈ ω) → dom 𝑂 ⊆ ω)
8280, 56, 81sylancr 696 . . . . . . . . . 10 ((𝑅 Or 𝐴𝐴 ∈ Fin) → dom 𝑂 ⊆ ω)
83 sseqin2 3850 . . . . . . . . . 10 (dom 𝑂 ⊆ ω ↔ (ω ∩ dom 𝑂) = dom 𝑂)
8482, 83sylib 208 . . . . . . . . 9 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (ω ∩ dom 𝑂) = dom 𝑂)
8579, 84eqtrd 2685 . . . . . . . 8 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (ω ∩ (𝐺‘((#‘𝐴) + 1))) = dom 𝑂)
8614, 85syl5eq 2697 . . . . . . 7 ((𝑅 Or 𝐴𝐴 ∈ Fin) → 𝐶 = dom 𝑂)
87 isoeq5 6611 . . . . . . 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 8483 . . . . . 6 ((𝐴 ∈ Fin ∧ 𝑅 We 𝐴) → 𝑂 Isom E , 𝑅 (dom 𝑂, 𝐴))
9148, 49, 90syl2anc 694 . . . . 5 ((𝑅 Or 𝐴𝐴 ∈ Fin) → 𝑂 Isom E , 𝑅 (dom 𝑂, 𝐴))
92 isotr 6626 . . . . 5 (((𝐺𝐵) Isom < , E ((1...(#‘𝐴)), dom 𝑂) ∧ 𝑂 Isom E , 𝑅 (dom 𝑂, 𝐴)) → (𝑂 ∘ (𝐺𝐵)) Isom < , 𝑅 ((1...(#‘𝐴)), 𝐴))
9389, 91, 92syl2anc 694 . . . 4 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝑂 ∘ (𝐺𝐵)) Isom < , 𝑅 ((1...(#‘𝐴)), 𝐴))
94 isof1o 6613 . . . 4 ((𝑂 ∘ (𝐺𝐵)) Isom < , 𝑅 ((1...(#‘𝐴)), 𝐴) → (𝑂 ∘ (𝐺𝐵)):(1...(#‘𝐴))–1-1-onto𝐴)
95 f1of 6175 . . . 4 ((𝑂 ∘ (𝐺𝐵)):(1...(#‘𝐴))–1-1-onto𝐴 → (𝑂 ∘ (𝐺𝐵)):(1...(#‘𝐴))⟶𝐴)
9693, 94, 953syl 18 . . 3 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝑂 ∘ (𝐺𝐵)):(1...(#‘𝐴))⟶𝐴)
97 fzfid 12812 . . 3 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (1...(#‘𝐴)) ∈ Fin)
98 fex 6530 . . 3 (((𝑂 ∘ (𝐺𝐵)):(1...(#‘𝐴))⟶𝐴 ∧ (1...(#‘𝐴)) ∈ Fin) → (𝑂 ∘ (𝐺𝐵)) ∈ V)
9996, 97, 98syl2anc 694 . 2 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝑂 ∘ (𝐺𝐵)) ∈ V)
100 isoeq1 6607 . . 3 (𝑓 = (𝑂 ∘ (𝐺𝐵)) → (𝑓 Isom < , 𝑅 ((1...(#‘𝐴)), 𝐴) ↔ (𝑂 ∘ (𝐺𝐵)) Isom < , 𝑅 ((1...(#‘𝐴)), 𝐴)))
101100spcegv 3325 . 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 383   = wceq 1523  wex 1744  wcel 2030  Vcvv 3231  cin 3606  wss 3607  {csn 4210   class class class wbr 4685  cmpt 4762   E cep 5057   Or wor 5063   We wwe 5101  ccnv 5142  dom cdm 5143  cres 5145  cima 5146  ccom 5147  Ord word 5760  Oncon0 5761  wf 5922  1-1-ontowf1o 5925  cfv 5926   Isom wiso 5927  (class class class)co 6690  ωcom 7107  reccrdg 7550  cen 7994  Fincfn 7997  OrdIsocoi 8455  cardccrd 8799  0cc0 9974  1c1 9975   + caddc 9977   < clt 10112  cle 10113  cmin 10304  cn 11058  0cn0 11330  cz 11415  cuz 11725  ...cfz 12364  #chash 13157
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-er 7787  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-oi 8456  df-card 8803  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-nn 11059  df-n0 11331  df-z 11416  df-uz 11726  df-fz 12365  df-hash 13158
This theorem is referenced by:  fz1iso  13284
  Copyright terms: Public domain W3C validator