Mathbox for Glauco Siliprandi < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  fzisoeu Structured version   Visualization version   GIF version

Theorem fzisoeu 38975
 Description: A finite ordered set has a unique order isomorphism to a generic finite sequence of integers. This theorem generalizes fz1iso 13184 for the base index and also states the uniqueness condition. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypotheses
Ref Expression
fzisoeu.h (𝜑𝐻 ∈ Fin)
fzisoeu.or (𝜑 → < Or 𝐻)
fzisoeu.m (𝜑𝑀 ∈ ℤ)
fzisoeu.4 𝑁 = ((#‘𝐻) + (𝑀 − 1))
Assertion
Ref Expression
fzisoeu (𝜑 → ∃!𝑓 𝑓 Isom < , < ((𝑀...𝑁), 𝐻))
Distinct variable groups:   𝑓,𝐻   𝑓,𝑀   𝑓,𝑁
Allowed substitution hint:   𝜑(𝑓)

Proof of Theorem fzisoeu
Dummy variables 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fzssz 12285 . . . . . . . . 9 (𝑀...𝑁) ⊆ ℤ
2 zssre 11328 . . . . . . . . 9 ℤ ⊆ ℝ
31, 2sstri 3592 . . . . . . . 8 (𝑀...𝑁) ⊆ ℝ
4 ltso 10062 . . . . . . . 8 < Or ℝ
5 soss 5013 . . . . . . . 8 ((𝑀...𝑁) ⊆ ℝ → ( < Or ℝ → < Or (𝑀...𝑁)))
63, 4, 5mp2 9 . . . . . . 7 < Or (𝑀...𝑁)
7 fzfi 12711 . . . . . . 7 (𝑀...𝑁) ∈ Fin
8 fz1iso 13184 . . . . . . 7 (( < Or (𝑀...𝑁) ∧ (𝑀...𝑁) ∈ Fin) → ∃ Isom < , < ((1...(#‘(𝑀...𝑁))), (𝑀...𝑁)))
96, 7, 8mp2an 707 . . . . . 6 Isom < , < ((1...(#‘(𝑀...𝑁))), (𝑀...𝑁))
10 fzisoeu.4 . . . . . . . . . . . . . . . 16 𝑁 = ((#‘𝐻) + (𝑀 − 1))
11 fveq2 6148 . . . . . . . . . . . . . . . . . 18 (𝐻 = ∅ → (#‘𝐻) = (#‘∅))
12 hash0 13098 . . . . . . . . . . . . . . . . . 18 (#‘∅) = 0
1311, 12syl6eq 2671 . . . . . . . . . . . . . . . . 17 (𝐻 = ∅ → (#‘𝐻) = 0)
1413oveq1d 6619 . . . . . . . . . . . . . . . 16 (𝐻 = ∅ → ((#‘𝐻) + (𝑀 − 1)) = (0 + (𝑀 − 1)))
1510, 14syl5eq 2667 . . . . . . . . . . . . . . 15 (𝐻 = ∅ → 𝑁 = (0 + (𝑀 − 1)))
1615oveq2d 6620 . . . . . . . . . . . . . 14 (𝐻 = ∅ → (𝑀...𝑁) = (𝑀...(0 + (𝑀 − 1))))
1716adantl 482 . . . . . . . . . . . . 13 ((𝜑𝐻 = ∅) → (𝑀...𝑁) = (𝑀...(0 + (𝑀 − 1))))
18 fzisoeu.m . . . . . . . . . . . . . . . . . . 19 (𝜑𝑀 ∈ ℤ)
1918zcnd 11427 . . . . . . . . . . . . . . . . . 18 (𝜑𝑀 ∈ ℂ)
20 1cnd 10000 . . . . . . . . . . . . . . . . . 18 (𝜑 → 1 ∈ ℂ)
2119, 20subcld 10336 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑀 − 1) ∈ ℂ)
2221addid2d 10181 . . . . . . . . . . . . . . . 16 (𝜑 → (0 + (𝑀 − 1)) = (𝑀 − 1))
2322oveq2d 6620 . . . . . . . . . . . . . . 15 (𝜑 → (𝑀...(0 + (𝑀 − 1))) = (𝑀...(𝑀 − 1)))
2418zred 11426 . . . . . . . . . . . . . . . . 17 (𝜑𝑀 ∈ ℝ)
2524ltm1d 10900 . . . . . . . . . . . . . . . 16 (𝜑 → (𝑀 − 1) < 𝑀)
26 peano2zm 11364 . . . . . . . . . . . . . . . . . 18 (𝑀 ∈ ℤ → (𝑀 − 1) ∈ ℤ)
2718, 26syl 17 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝑀 − 1) ∈ ℤ)
28 fzn 12299 . . . . . . . . . . . . . . . . 17 ((𝑀 ∈ ℤ ∧ (𝑀 − 1) ∈ ℤ) → ((𝑀 − 1) < 𝑀 ↔ (𝑀...(𝑀 − 1)) = ∅))
2918, 27, 28syl2anc 692 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑀 − 1) < 𝑀 ↔ (𝑀...(𝑀 − 1)) = ∅))
3025, 29mpbid 222 . . . . . . . . . . . . . . 15 (𝜑 → (𝑀...(𝑀 − 1)) = ∅)
3123, 30eqtrd 2655 . . . . . . . . . . . . . 14 (𝜑 → (𝑀...(0 + (𝑀 − 1))) = ∅)
3231adantr 481 . . . . . . . . . . . . 13 ((𝜑𝐻 = ∅) → (𝑀...(0 + (𝑀 − 1))) = ∅)
33 eqcom 2628 . . . . . . . . . . . . . . 15 (𝐻 = ∅ ↔ ∅ = 𝐻)
3433biimpi 206 . . . . . . . . . . . . . 14 (𝐻 = ∅ → ∅ = 𝐻)
3534adantl 482 . . . . . . . . . . . . 13 ((𝜑𝐻 = ∅) → ∅ = 𝐻)
3617, 32, 353eqtrd 2659 . . . . . . . . . . . 12 ((𝜑𝐻 = ∅) → (𝑀...𝑁) = 𝐻)
3736fveq2d 6152 . . . . . . . . . . 11 ((𝜑𝐻 = ∅) → (#‘(𝑀...𝑁)) = (#‘𝐻))
3820, 19pncan3d 10339 . . . . . . . . . . . . . . . . 17 (𝜑 → (1 + (𝑀 − 1)) = 𝑀)
3938eqcomd 2627 . . . . . . . . . . . . . . . 16 (𝜑𝑀 = (1 + (𝑀 − 1)))
4039adantr 481 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ 𝐻 = ∅) → 𝑀 = (1 + (𝑀 − 1)))
41 1red 9999 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ¬ 𝐻 = ∅) → 1 ∈ ℝ)
42 neqne 2798 . . . . . . . . . . . . . . . . . . . 20 𝐻 = ∅ → 𝐻 ≠ ∅)
4342adantl 482 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ¬ 𝐻 = ∅) → 𝐻 ≠ ∅)
44 fzisoeu.h . . . . . . . . . . . . . . . . . . . . 21 (𝜑𝐻 ∈ Fin)
4544adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((𝜑 ∧ ¬ 𝐻 = ∅) → 𝐻 ∈ Fin)
46 hashnncl 13097 . . . . . . . . . . . . . . . . . . . 20 (𝐻 ∈ Fin → ((#‘𝐻) ∈ ℕ ↔ 𝐻 ≠ ∅))
4745, 46syl 17 . . . . . . . . . . . . . . . . . . 19 ((𝜑 ∧ ¬ 𝐻 = ∅) → ((#‘𝐻) ∈ ℕ ↔ 𝐻 ≠ ∅))
4843, 47mpbird 247 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ ¬ 𝐻 = ∅) → (#‘𝐻) ∈ ℕ)
4948nnred 10979 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ¬ 𝐻 = ∅) → (#‘𝐻) ∈ ℝ)
5027zred 11426 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑀 − 1) ∈ ℝ)
5150adantr 481 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ¬ 𝐻 = ∅) → (𝑀 − 1) ∈ ℝ)
5248nnge1d 11007 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ ¬ 𝐻 = ∅) → 1 ≤ (#‘𝐻))
5341, 49, 51, 52leadd1dd 10585 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ ¬ 𝐻 = ∅) → (1 + (𝑀 − 1)) ≤ ((#‘𝐻) + (𝑀 − 1)))
5453, 10syl6breqr 4655 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ 𝐻 = ∅) → (1 + (𝑀 − 1)) ≤ 𝑁)
5540, 54eqbrtrd 4635 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ 𝐻 = ∅) → 𝑀𝑁)
5618adantr 481 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ 𝐻 = ∅) → 𝑀 ∈ ℤ)
57 hashcl 13087 . . . . . . . . . . . . . . . . . . 19 (𝐻 ∈ Fin → (#‘𝐻) ∈ ℕ0)
58 nn0z 11344 . . . . . . . . . . . . . . . . . . 19 ((#‘𝐻) ∈ ℕ0 → (#‘𝐻) ∈ ℤ)
5944, 57, 583syl 18 . . . . . . . . . . . . . . . . . 18 (𝜑 → (#‘𝐻) ∈ ℤ)
6059, 27zaddcld 11430 . . . . . . . . . . . . . . . . 17 (𝜑 → ((#‘𝐻) + (𝑀 − 1)) ∈ ℤ)
6110, 60syl5eqel 2702 . . . . . . . . . . . . . . . 16 (𝜑𝑁 ∈ ℤ)
6261adantr 481 . . . . . . . . . . . . . . 15 ((𝜑 ∧ ¬ 𝐻 = ∅) → 𝑁 ∈ ℤ)
63 eluz 11645 . . . . . . . . . . . . . . 15 ((𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈ (ℤ𝑀) ↔ 𝑀𝑁))
6456, 62, 63syl2anc 692 . . . . . . . . . . . . . 14 ((𝜑 ∧ ¬ 𝐻 = ∅) → (𝑁 ∈ (ℤ𝑀) ↔ 𝑀𝑁))
6555, 64mpbird 247 . . . . . . . . . . . . 13 ((𝜑 ∧ ¬ 𝐻 = ∅) → 𝑁 ∈ (ℤ𝑀))
66 hashfz 13154 . . . . . . . . . . . . 13 (𝑁 ∈ (ℤ𝑀) → (#‘(𝑀...𝑁)) = ((𝑁𝑀) + 1))
6765, 66syl 17 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ 𝐻 = ∅) → (#‘(𝑀...𝑁)) = ((𝑁𝑀) + 1))
6810oveq1i 6614 . . . . . . . . . . . . . . . 16 (𝑁𝑀) = (((#‘𝐻) + (𝑀 − 1)) − 𝑀)
6944, 57syl 17 . . . . . . . . . . . . . . . . . 18 (𝜑 → (#‘𝐻) ∈ ℕ0)
7069nn0cnd 11297 . . . . . . . . . . . . . . . . 17 (𝜑 → (#‘𝐻) ∈ ℂ)
7170, 21, 19addsubassd 10356 . . . . . . . . . . . . . . . 16 (𝜑 → (((#‘𝐻) + (𝑀 − 1)) − 𝑀) = ((#‘𝐻) + ((𝑀 − 1) − 𝑀)))
7268, 71syl5eq 2667 . . . . . . . . . . . . . . 15 (𝜑 → (𝑁𝑀) = ((#‘𝐻) + ((𝑀 − 1) − 𝑀)))
7319, 20negsubd 10342 . . . . . . . . . . . . . . . . . . 19 (𝜑 → (𝑀 + -1) = (𝑀 − 1))
7473eqcomd 2627 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑀 − 1) = (𝑀 + -1))
7574oveq1d 6619 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑀 − 1) − 𝑀) = ((𝑀 + -1) − 𝑀))
7620negcld 10323 . . . . . . . . . . . . . . . . . 18 (𝜑 → -1 ∈ ℂ)
7719, 76pncan2d 10338 . . . . . . . . . . . . . . . . 17 (𝜑 → ((𝑀 + -1) − 𝑀) = -1)
7875, 77eqtrd 2655 . . . . . . . . . . . . . . . 16 (𝜑 → ((𝑀 − 1) − 𝑀) = -1)
7978oveq2d 6620 . . . . . . . . . . . . . . 15 (𝜑 → ((#‘𝐻) + ((𝑀 − 1) − 𝑀)) = ((#‘𝐻) + -1))
8072, 79eqtrd 2655 . . . . . . . . . . . . . 14 (𝜑 → (𝑁𝑀) = ((#‘𝐻) + -1))
8180oveq1d 6619 . . . . . . . . . . . . 13 (𝜑 → ((𝑁𝑀) + 1) = (((#‘𝐻) + -1) + 1))
8281adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ 𝐻 = ∅) → ((𝑁𝑀) + 1) = (((#‘𝐻) + -1) + 1))
8370, 20negsubd 10342 . . . . . . . . . . . . . . 15 (𝜑 → ((#‘𝐻) + -1) = ((#‘𝐻) − 1))
8483oveq1d 6619 . . . . . . . . . . . . . 14 (𝜑 → (((#‘𝐻) + -1) + 1) = (((#‘𝐻) − 1) + 1))
8570, 20npcand 10340 . . . . . . . . . . . . . 14 (𝜑 → (((#‘𝐻) − 1) + 1) = (#‘𝐻))
8684, 85eqtrd 2655 . . . . . . . . . . . . 13 (𝜑 → (((#‘𝐻) + -1) + 1) = (#‘𝐻))
8786adantr 481 . . . . . . . . . . . 12 ((𝜑 ∧ ¬ 𝐻 = ∅) → (((#‘𝐻) + -1) + 1) = (#‘𝐻))
8867, 82, 873eqtrd 2659 . . . . . . . . . . 11 ((𝜑 ∧ ¬ 𝐻 = ∅) → (#‘(𝑀...𝑁)) = (#‘𝐻))
8937, 88pm2.61dan 831 . . . . . . . . . 10 (𝜑 → (#‘(𝑀...𝑁)) = (#‘𝐻))
9089oveq2d 6620 . . . . . . . . 9 (𝜑 → (1...(#‘(𝑀...𝑁))) = (1...(#‘𝐻)))
91 isoeq4 6524 . . . . . . . . 9 ((1...(#‘(𝑀...𝑁))) = (1...(#‘𝐻)) → ( Isom < , < ((1...(#‘(𝑀...𝑁))), (𝑀...𝑁)) ↔ Isom < , < ((1...(#‘𝐻)), (𝑀...𝑁))))
9290, 91syl 17 . . . . . . . 8 (𝜑 → ( Isom < , < ((1...(#‘(𝑀...𝑁))), (𝑀...𝑁)) ↔ Isom < , < ((1...(#‘𝐻)), (𝑀...𝑁))))
9392biimpd 219 . . . . . . 7 (𝜑 → ( Isom < , < ((1...(#‘(𝑀...𝑁))), (𝑀...𝑁)) → Isom < , < ((1...(#‘𝐻)), (𝑀...𝑁))))
9493eximdv 1843 . . . . . 6 (𝜑 → (∃ Isom < , < ((1...(#‘(𝑀...𝑁))), (𝑀...𝑁)) → ∃ Isom < , < ((1...(#‘𝐻)), (𝑀...𝑁))))
959, 94mpi 20 . . . . 5 (𝜑 → ∃ Isom < , < ((1...(#‘𝐻)), (𝑀...𝑁)))
96 fzisoeu.or . . . . . 6 (𝜑 → < Or 𝐻)
97 fz1iso 13184 . . . . . 6 (( < Or 𝐻𝐻 ∈ Fin) → ∃𝑔 𝑔 Isom < , < ((1...(#‘𝐻)), 𝐻))
9896, 44, 97syl2anc 692 . . . . 5 (𝜑 → ∃𝑔 𝑔 Isom < , < ((1...(#‘𝐻)), 𝐻))
99 eeanv 2181 . . . . 5 (∃𝑔( Isom < , < ((1...(#‘𝐻)), (𝑀...𝑁)) ∧ 𝑔 Isom < , < ((1...(#‘𝐻)), 𝐻)) ↔ (∃ Isom < , < ((1...(#‘𝐻)), (𝑀...𝑁)) ∧ ∃𝑔 𝑔 Isom < , < ((1...(#‘𝐻)), 𝐻)))
10095, 98, 99sylanbrc 697 . . . 4 (𝜑 → ∃𝑔( Isom < , < ((1...(#‘𝐻)), (𝑀...𝑁)) ∧ 𝑔 Isom < , < ((1...(#‘𝐻)), 𝐻)))
101 isocnv 6534 . . . . . . . 8 ( Isom < , < ((1...(#‘𝐻)), (𝑀...𝑁)) → Isom < , < ((𝑀...𝑁), (1...(#‘𝐻))))
102101ad2antrl 763 . . . . . . 7 ((𝜑 ∧ ( Isom < , < ((1...(#‘𝐻)), (𝑀...𝑁)) ∧ 𝑔 Isom < , < ((1...(#‘𝐻)), 𝐻))) → Isom < , < ((𝑀...𝑁), (1...(#‘𝐻))))
103 simprr 795 . . . . . . 7 ((𝜑 ∧ ( Isom < , < ((1...(#‘𝐻)), (𝑀...𝑁)) ∧ 𝑔 Isom < , < ((1...(#‘𝐻)), 𝐻))) → 𝑔 Isom < , < ((1...(#‘𝐻)), 𝐻))
104 isotr 6540 . . . . . . 7 (( Isom < , < ((𝑀...𝑁), (1...(#‘𝐻))) ∧ 𝑔 Isom < , < ((1...(#‘𝐻)), 𝐻)) → (𝑔) Isom < , < ((𝑀...𝑁), 𝐻))
105102, 103, 104syl2anc 692 . . . . . 6 ((𝜑 ∧ ( Isom < , < ((1...(#‘𝐻)), (𝑀...𝑁)) ∧ 𝑔 Isom < , < ((1...(#‘𝐻)), 𝐻))) → (𝑔) Isom < , < ((𝑀...𝑁), 𝐻))
106105ex 450 . . . . 5 (𝜑 → (( Isom < , < ((1...(#‘𝐻)), (𝑀...𝑁)) ∧ 𝑔 Isom < , < ((1...(#‘𝐻)), 𝐻)) → (𝑔) Isom < , < ((𝑀...𝑁), 𝐻)))
1071062eximdv 1845 . . . 4 (𝜑 → (∃𝑔( Isom < , < ((1...(#‘𝐻)), (𝑀...𝑁)) ∧ 𝑔 Isom < , < ((1...(#‘𝐻)), 𝐻)) → ∃𝑔(𝑔) Isom < , < ((𝑀...𝑁), 𝐻)))
108100, 107mpd 15 . . 3 (𝜑 → ∃𝑔(𝑔) Isom < , < ((𝑀...𝑁), 𝐻))
109 vex 3189 . . . . . . 7 𝑔 ∈ V
110 vex 3189 . . . . . . . 8 ∈ V
111110cnvex 7060 . . . . . . 7 ∈ V
112109, 111coex 7065 . . . . . 6 (𝑔) ∈ V
113 isoeq1 6521 . . . . . 6 (𝑓 = (𝑔) → (𝑓 Isom < , < ((𝑀...𝑁), 𝐻) ↔ (𝑔) Isom < , < ((𝑀...𝑁), 𝐻)))
114112, 113spcev 3286 . . . . 5 ((𝑔) Isom < , < ((𝑀...𝑁), 𝐻) → ∃𝑓 𝑓 Isom < , < ((𝑀...𝑁), 𝐻))
115114a1i 11 . . . 4 (𝜑 → ((𝑔) Isom < , < ((𝑀...𝑁), 𝐻) → ∃𝑓 𝑓 Isom < , < ((𝑀...𝑁), 𝐻)))
116115exlimdvv 1859 . . 3 (𝜑 → (∃𝑔(𝑔) Isom < , < ((𝑀...𝑁), 𝐻) → ∃𝑓 𝑓 Isom < , < ((𝑀...𝑁), 𝐻)))
117108, 116mpd 15 . 2 (𝜑 → ∃𝑓 𝑓 Isom < , < ((𝑀...𝑁), 𝐻))
118 ltwefz 12702 . . 3 < We (𝑀...𝑁)
119 wemoiso 7098 . . 3 ( < We (𝑀...𝑁) → ∃*𝑓 𝑓 Isom < , < ((𝑀...𝑁), 𝐻))
120118, 119mp1i 13 . 2 (𝜑 → ∃*𝑓 𝑓 Isom < , < ((𝑀...𝑁), 𝐻))
121 eu5 2495 . 2 (∃!𝑓 𝑓 Isom < , < ((𝑀...𝑁), 𝐻) ↔ (∃𝑓 𝑓 Isom < , < ((𝑀...𝑁), 𝐻) ∧ ∃*𝑓 𝑓 Isom < , < ((𝑀...𝑁), 𝐻)))
122117, 120, 121sylanbrc 697 1 (𝜑 → ∃!𝑓 𝑓 Isom < , < ((𝑀...𝑁), 𝐻))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 196   ∧ wa 384   = wceq 1480  ∃wex 1701   ∈ wcel 1987  ∃!weu 2469  ∃*wmo 2470   ≠ wne 2790   ⊆ wss 3555  ∅c0 3891   class class class wbr 4613   Or wor 4994   We wwe 5032  ◡ccnv 5073   ∘ ccom 5078  ‘cfv 5847   Isom wiso 5848  (class class class)co 6604  Fincfn 7899  ℝcr 9879  0cc0 9880  1c1 9881   + caddc 9883   < clt 10018   ≤ cle 10019   − cmin 10210  -cneg 10211  ℕcn 10964  ℕ0cn0 11236  ℤcz 11321  ℤ≥cuz 11631  ...cfz 12268  #chash 13057 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 4731  ax-sep 4741  ax-nul 4749  ax-pow 4803  ax-pr 4867  ax-un 6902  ax-inf2 8482  ax-cnex 9936  ax-resscn 9937  ax-1cn 9938  ax-icn 9939  ax-addcl 9940  ax-addrcl 9941  ax-mulcl 9942  ax-mulrcl 9943  ax-mulcom 9944  ax-addass 9945  ax-mulass 9946  ax-distr 9947  ax-i2m1 9948  ax-1ne0 9949  ax-1rid 9950  ax-rnegex 9951  ax-rrecex 9952  ax-cnre 9953  ax-pre-lttri 9954  ax-pre-lttrn 9955  ax-pre-ltadd 9956  ax-pre-mulgt0 9957 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 3188  df-sbc 3418  df-csb 3515  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-pss 3571  df-nul 3892  df-if 4059  df-pw 4132  df-sn 4149  df-pr 4151  df-tp 4153  df-op 4155  df-uni 4403  df-int 4441  df-iun 4487  df-br 4614  df-opab 4674  df-mpt 4675  df-tr 4713  df-eprel 4985  df-id 4989  df-po 4995  df-so 4996  df-fr 5033  df-se 5034  df-we 5035  df-xp 5080  df-rel 5081  df-cnv 5082  df-co 5083  df-dm 5084  df-rn 5085  df-res 5086  df-ima 5087  df-pred 5639  df-ord 5685  df-on 5686  df-lim 5687  df-suc 5688  df-iota 5810  df-fun 5849  df-fn 5850  df-f 5851  df-f1 5852  df-fo 5853  df-f1o 5854  df-fv 5855  df-isom 5856  df-riota 6565  df-ov 6607  df-oprab 6608  df-mpt2 6609  df-om 7013  df-1st 7113  df-2nd 7114  df-wrecs 7352  df-recs 7413  df-rdg 7451  df-1o 7505  df-er 7687  df-en 7900  df-dom 7901  df-sdom 7902  df-fin 7903  df-oi 8359  df-card 8709  df-pnf 10020  df-mnf 10021  df-xr 10022  df-ltxr 10023  df-le 10024  df-sub 10212  df-neg 10213  df-nn 10965  df-n0 11237  df-z 11322  df-uz 11632  df-fz 12269  df-hash 13058 This theorem is referenced by:  fourierdlem36  39664
 Copyright terms: Public domain W3C validator