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

Theorem fz1isolem 13447
Description: Lemma for fz1iso 13448. (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 13349 . . . . . . . . 9 (𝐴 ∈ Fin → (♯‘𝐴) ∈ ℕ0)
21adantl 467 . . . . . . . 8 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (♯‘𝐴) ∈ ℕ0)
3 nnuz 11925 . . . . . . . . . . 11 ℕ = (ℤ‘1)
4 1z 11609 . . . . . . . . . . . . 13 1 ∈ ℤ
5 fz1iso.1 . . . . . . . . . . . . 13 𝐺 = (rec((𝑛 ∈ V ↦ (𝑛 + 1)), 1) ↾ ω)
64, 5om2uzisoi 12961 . . . . . . . . . . . 12 𝐺 Isom E , < (ω, (ℤ‘1))
7 isoeq5 6714 . . . . . . . . . . . 12 (ℕ = (ℤ‘1) → (𝐺 Isom E , < (ω, ℕ) ↔ 𝐺 Isom E , < (ω, (ℤ‘1))))
86, 7mpbiri 248 . . . . . . . . . . 11 (ℕ = (ℤ‘1) → 𝐺 Isom E , < (ω, ℕ))
93, 8ax-mp 5 . . . . . . . . . 10 𝐺 Isom E , < (ω, ℕ)
10 isocnv 6723 . . . . . . . . . 10 (𝐺 Isom E , < (ω, ℕ) → 𝐺 Isom < , E (ℕ, ω))
119, 10ax-mp 5 . . . . . . . . 9 𝐺 Isom < , E (ℕ, ω)
12 nn0p1nn 11534 . . . . . . . . 9 ((♯‘𝐴) ∈ ℕ0 → ((♯‘𝐴) + 1) ∈ ℕ)
13 fz1iso.2 . . . . . . . . . 10 𝐵 = (ℕ ∩ ( < “ {((♯‘𝐴) + 1)}))
14 fz1iso.3 . . . . . . . . . . 11 𝐶 = (ω ∩ (𝐺‘((♯‘𝐴) + 1)))
15 fvex 6342 . . . . . . . . . . . . 13 (𝐺‘((♯‘𝐴) + 1)) ∈ V
1615epini 5636 . . . . . . . . . . . 12 ( E “ {(𝐺‘((♯‘𝐴) + 1))}) = (𝐺‘((♯‘𝐴) + 1))
1716ineq2i 3962 . . . . . . . . . . 11 (ω ∩ ( E “ {(𝐺‘((♯‘𝐴) + 1))})) = (ω ∩ (𝐺‘((♯‘𝐴) + 1)))
1814, 17eqtr4i 2796 . . . . . . . . . 10 𝐶 = (ω ∩ ( E “ {(𝐺‘((♯‘𝐴) + 1))}))
1913, 18isoini2 6732 . . . . . . . . 9 ((𝐺 Isom < , E (ℕ, ω) ∧ ((♯‘𝐴) + 1) ∈ ℕ) → (𝐺𝐵) Isom < , E (𝐵, 𝐶))
2011, 12, 19sylancr 575 . . . . . . . 8 ((♯‘𝐴) ∈ ℕ0 → (𝐺𝐵) Isom < , E (𝐵, 𝐶))
212, 20syl 17 . . . . . . 7 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝐺𝐵) Isom < , E (𝐵, 𝐶))
22 nnz 11601 . . . . . . . . . . . . 13 (𝑓 ∈ ℕ → 𝑓 ∈ ℤ)
232nn0zd 11682 . . . . . . . . . . . . 13 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (♯‘𝐴) ∈ ℤ)
24 eluz 11902 . . . . . . . . . . . . 13 ((𝑓 ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ) → ((♯‘𝐴) ∈ (ℤ𝑓) ↔ 𝑓 ≤ (♯‘𝐴)))
2522, 23, 24syl2anr 584 . . . . . . . . . . . 12 (((𝑅 Or 𝐴𝐴 ∈ Fin) ∧ 𝑓 ∈ ℕ) → ((♯‘𝐴) ∈ (ℤ𝑓) ↔ 𝑓 ≤ (♯‘𝐴)))
26 zleltp1 11630 . . . . . . . . . . . . . 14 ((𝑓 ∈ ℤ ∧ (♯‘𝐴) ∈ ℤ) → (𝑓 ≤ (♯‘𝐴) ↔ 𝑓 < ((♯‘𝐴) + 1)))
2722, 23, 26syl2anr 584 . . . . . . . . . . . . 13 (((𝑅 Or 𝐴𝐴 ∈ Fin) ∧ 𝑓 ∈ ℕ) → (𝑓 ≤ (♯‘𝐴) ↔ 𝑓 < ((♯‘𝐴) + 1)))
28 ovex 6823 . . . . . . . . . . . . . 14 ((♯‘𝐴) + 1) ∈ V
29 vex 3354 . . . . . . . . . . . . . . 15 𝑓 ∈ V
3029eliniseg 5635 . . . . . . . . . . . . . 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 568 . . . . . . . . . 10 ((𝑅 Or 𝐴𝐴 ∈ Fin) → ((𝑓 ∈ ℕ ∧ 𝑓 ∈ ( < “ {((♯‘𝐴) + 1)})) ↔ (𝑓 ∈ ℕ ∧ (♯‘𝐴) ∈ (ℤ𝑓))))
3513elin2 3952 . . . . . . . . . 10 (𝑓𝐵 ↔ (𝑓 ∈ ℕ ∧ 𝑓 ∈ ( < “ {((♯‘𝐴) + 1)})))
36 elfzuzb 12543 . . . . . . . . . . 11 (𝑓 ∈ (1...(♯‘𝐴)) ↔ (𝑓 ∈ (ℤ‘1) ∧ (♯‘𝐴) ∈ (ℤ𝑓)))
37 elnnuz 11926 . . . . . . . . . . . 12 (𝑓 ∈ ℕ ↔ 𝑓 ∈ (ℤ‘1))
3837anbi1i 610 . . . . . . . . . . 11 ((𝑓 ∈ ℕ ∧ (♯‘𝐴) ∈ (ℤ𝑓)) ↔ (𝑓 ∈ (ℤ‘1) ∧ (♯‘𝐴) ∈ (ℤ𝑓)))
3936, 38bitr4i 267 . . . . . . . . . 10 (𝑓 ∈ (1...(♯‘𝐴)) ↔ (𝑓 ∈ ℕ ∧ (♯‘𝐴) ∈ (ℤ𝑓)))
4034, 35, 393bitr4g 303 . . . . . . . . 9 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝑓𝐵𝑓 ∈ (1...(♯‘𝐴))))
4140eqrdv 2769 . . . . . . . 8 ((𝑅 Or 𝐴𝐴 ∈ Fin) → 𝐵 = (1...(♯‘𝐴)))
42 isoeq4 6713 . . . . . . . 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 8597 . . . . . . . . . . . . . . . . 17 (𝐴 ∈ Fin → dom 𝑂 ∈ On)
4746adantl 467 . . . . . . . . . . . . . . . 16 ((𝑅 Or 𝐴𝐴 ∈ Fin) → dom 𝑂 ∈ On)
48 simpr 471 . . . . . . . . . . . . . . . . 17 ((𝑅 Or 𝐴𝐴 ∈ Fin) → 𝐴 ∈ Fin)
49 wofi 8365 . . . . . . . . . . . . . . . . . 18 ((𝑅 Or 𝐴𝐴 ∈ Fin) → 𝑅 We 𝐴)
5045oien 8599 . . . . . . . . . . . . . . . . . 18 ((𝐴 ∈ Fin ∧ 𝑅 We 𝐴) → dom 𝑂𝐴)
5148, 49, 50syl2anc 573 . . . . . . . . . . . . . . . . 17 ((𝑅 Or 𝐴𝐴 ∈ Fin) → dom 𝑂𝐴)
52 enfii 8333 . . . . . . . . . . . . . . . . 17 ((𝐴 ∈ Fin ∧ dom 𝑂𝐴) → dom 𝑂 ∈ Fin)
5348, 51, 52syl2anc 573 . . . . . . . . . . . . . . . 16 ((𝑅 Or 𝐴𝐴 ∈ Fin) → dom 𝑂 ∈ Fin)
5447, 53elind 3949 . . . . . . . . . . . . . . 15 ((𝑅 Or 𝐴𝐴 ∈ Fin) → dom 𝑂 ∈ (On ∩ Fin))
55 onfin2 8308 . . . . . . . . . . . . . . 15 ω = (On ∩ Fin)
5654, 55syl6eleqr 2861 . . . . . . . . . . . . . 14 ((𝑅 Or 𝐴𝐴 ∈ Fin) → dom 𝑂 ∈ ω)
57 eqid 2771 . . . . . . . . . . . . . . . 16 (rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω) = (rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)
58 0z 11590 . . . . . . . . . . . . . . . 16 0 ∈ ℤ
595, 57, 4, 58uzrdgxfr 12974 . . . . . . . . . . . . . . 15 (dom 𝑂 ∈ ω → (𝐺‘dom 𝑂) = (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂) + (1 − 0)))
60 1m0e1 11333 . . . . . . . . . . . . . . . 16 (1 − 0) = 1
6160oveq2i 6804 . . . . . . . . . . . . . . 15 (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂) + (1 − 0)) = (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂) + 1)
6259, 61syl6eq 2821 . . . . . . . . . . . . . 14 (dom 𝑂 ∈ ω → (𝐺‘dom 𝑂) = (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂) + 1))
6356, 62syl 17 . . . . . . . . . . . . 13 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝐺‘dom 𝑂) = (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂) + 1))
6451ensymd 8160 . . . . . . . . . . . . . . . . 17 ((𝑅 Or 𝐴𝐴 ∈ Fin) → 𝐴 ≈ dom 𝑂)
65 cardennn 9009 . . . . . . . . . . . . . . . . 17 ((𝐴 ≈ dom 𝑂 ∧ dom 𝑂 ∈ ω) → (card‘𝐴) = dom 𝑂)
6664, 56, 65syl2anc 573 . . . . . . . . . . . . . . . 16 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (card‘𝐴) = dom 𝑂)
6766fveq2d 6336 . . . . . . . . . . . . . . 15 ((𝑅 Or 𝐴𝐴 ∈ Fin) → ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘(card‘𝐴)) = ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂))
6857hashgval 13324 . . . . . . . . . . . . . . . 16 (𝐴 ∈ Fin → ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘(card‘𝐴)) = (♯‘𝐴))
6968adantl 467 . . . . . . . . . . . . . . 15 ((𝑅 Or 𝐴𝐴 ∈ Fin) → ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘(card‘𝐴)) = (♯‘𝐴))
7067, 69eqtr3d 2807 . . . . . . . . . . . . . 14 ((𝑅 Or 𝐴𝐴 ∈ Fin) → ((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂) = (♯‘𝐴))
7170oveq1d 6808 . . . . . . . . . . . . 13 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (((rec((𝑛 ∈ V ↦ (𝑛 + 1)), 0) ↾ ω)‘dom 𝑂) + 1) = ((♯‘𝐴) + 1))
7263, 71eqtrd 2805 . . . . . . . . . . . 12 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝐺‘dom 𝑂) = ((♯‘𝐴) + 1))
7372fveq2d 6336 . . . . . . . . . . 11 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝐺‘(𝐺‘dom 𝑂)) = (𝐺‘((♯‘𝐴) + 1)))
74 isof1o 6716 . . . . . . . . . . . . 13 (𝐺 Isom E , < (ω, ℕ) → 𝐺:ω–1-1-onto→ℕ)
759, 74ax-mp 5 . . . . . . . . . . . 12 𝐺:ω–1-1-onto→ℕ
76 f1ocnvfv1 6675 . . . . . . . . . . . 12 ((𝐺:ω–1-1-onto→ℕ ∧ dom 𝑂 ∈ ω) → (𝐺‘(𝐺‘dom 𝑂)) = dom 𝑂)
7775, 56, 76sylancr 575 . . . . . . . . . . 11 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝐺‘(𝐺‘dom 𝑂)) = dom 𝑂)
7873, 77eqtr3d 2807 . . . . . . . . . 10 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝐺‘((♯‘𝐴) + 1)) = dom 𝑂)
7978ineq2d 3965 . . . . . . . . 9 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (ω ∩ (𝐺‘((♯‘𝐴) + 1))) = (ω ∩ dom 𝑂))
80 ordom 7221 . . . . . . . . . . 11 Ord ω
81 ordelss 5882 . . . . . . . . . . 11 ((Ord ω ∧ dom 𝑂 ∈ ω) → dom 𝑂 ⊆ ω)
8280, 56, 81sylancr 575 . . . . . . . . . 10 ((𝑅 Or 𝐴𝐴 ∈ Fin) → dom 𝑂 ⊆ ω)
83 sseqin2 3968 . . . . . . . . . 10 (dom 𝑂 ⊆ ω ↔ (ω ∩ dom 𝑂) = dom 𝑂)
8482, 83sylib 208 . . . . . . . . 9 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (ω ∩ dom 𝑂) = dom 𝑂)
8579, 84eqtrd 2805 . . . . . . . 8 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (ω ∩ (𝐺‘((♯‘𝐴) + 1))) = dom 𝑂)
8614, 85syl5eq 2817 . . . . . . 7 ((𝑅 Or 𝐴𝐴 ∈ Fin) → 𝐶 = dom 𝑂)
87 isoeq5 6714 . . . . . . 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 8598 . . . . . 6 ((𝐴 ∈ Fin ∧ 𝑅 We 𝐴) → 𝑂 Isom E , 𝑅 (dom 𝑂, 𝐴))
9148, 49, 90syl2anc 573 . . . . 5 ((𝑅 Or 𝐴𝐴 ∈ Fin) → 𝑂 Isom E , 𝑅 (dom 𝑂, 𝐴))
92 isotr 6729 . . . . 5 (((𝐺𝐵) Isom < , E ((1...(♯‘𝐴)), dom 𝑂) ∧ 𝑂 Isom E , 𝑅 (dom 𝑂, 𝐴)) → (𝑂 ∘ (𝐺𝐵)) Isom < , 𝑅 ((1...(♯‘𝐴)), 𝐴))
9389, 91, 92syl2anc 573 . . . 4 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝑂 ∘ (𝐺𝐵)) Isom < , 𝑅 ((1...(♯‘𝐴)), 𝐴))
94 isof1o 6716 . . . 4 ((𝑂 ∘ (𝐺𝐵)) Isom < , 𝑅 ((1...(♯‘𝐴)), 𝐴) → (𝑂 ∘ (𝐺𝐵)):(1...(♯‘𝐴))–1-1-onto𝐴)
95 f1of 6278 . . . 4 ((𝑂 ∘ (𝐺𝐵)):(1...(♯‘𝐴))–1-1-onto𝐴 → (𝑂 ∘ (𝐺𝐵)):(1...(♯‘𝐴))⟶𝐴)
9693, 94, 953syl 18 . . 3 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝑂 ∘ (𝐺𝐵)):(1...(♯‘𝐴))⟶𝐴)
97 fzfid 12980 . . 3 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (1...(♯‘𝐴)) ∈ Fin)
98 fex 6633 . . 3 (((𝑂 ∘ (𝐺𝐵)):(1...(♯‘𝐴))⟶𝐴 ∧ (1...(♯‘𝐴)) ∈ Fin) → (𝑂 ∘ (𝐺𝐵)) ∈ V)
9996, 97, 98syl2anc 573 . 2 ((𝑅 Or 𝐴𝐴 ∈ Fin) → (𝑂 ∘ (𝐺𝐵)) ∈ V)
100 isoeq1 6710 . . 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 196  wa 382   = wceq 1631  wex 1852  wcel 2145  Vcvv 3351  cin 3722  wss 3723  {csn 4316   class class class wbr 4786  cmpt 4863   E cep 5161   Or wor 5169   We wwe 5207  ccnv 5248  dom cdm 5249  cres 5251  cima 5252  ccom 5253  Ord word 5865  Oncon0 5866  wf 6027  1-1-ontowf1o 6030  cfv 6031   Isom wiso 6032  (class class class)co 6793  ωcom 7212  reccrdg 7658  cen 8106  Fincfn 8109  OrdIsocoi 8570  cardccrd 8961  0cc0 10138  1c1 10139   + caddc 10141   < clt 10276  cle 10277  cmin 10468  cn 11222  0cn0 11494  cz 11579  cuz 11888  ...cfz 12533  chash 13321
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4904  ax-sep 4915  ax-nul 4923  ax-pow 4974  ax-pr 5034  ax-un 7096  ax-cnex 10194  ax-resscn 10195  ax-1cn 10196  ax-icn 10197  ax-addcl 10198  ax-addrcl 10199  ax-mulcl 10200  ax-mulrcl 10201  ax-mulcom 10202  ax-addass 10203  ax-mulass 10204  ax-distr 10205  ax-i2m1 10206  ax-1ne0 10207  ax-1rid 10208  ax-rnegex 10209  ax-rrecex 10210  ax-cnre 10211  ax-pre-lttri 10212  ax-pre-lttrn 10213  ax-pre-ltadd 10214  ax-pre-mulgt0 10215
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4226  df-pw 4299  df-sn 4317  df-pr 4319  df-tp 4321  df-op 4323  df-uni 4575  df-int 4612  df-iun 4656  df-br 4787  df-opab 4847  df-mpt 4864  df-tr 4887  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-se 5209  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-isom 6040  df-riota 6754  df-ov 6796  df-oprab 6797  df-mpt2 6798  df-om 7213  df-1st 7315  df-2nd 7316  df-wrecs 7559  df-recs 7621  df-rdg 7659  df-1o 7713  df-er 7896  df-en 8110  df-dom 8111  df-sdom 8112  df-fin 8113  df-oi 8571  df-card 8965  df-pnf 10278  df-mnf 10279  df-xr 10280  df-ltxr 10281  df-le 10282  df-sub 10470  df-neg 10471  df-nn 11223  df-n0 11495  df-z 11580  df-uz 11889  df-fz 12534  df-hash 13322
This theorem is referenced by:  fz1iso  13448
  Copyright terms: Public domain W3C validator