Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  fprodf1o GIF version

Theorem fprodf1o 11462
 Description: Re-index a finite product using a bijection. (Contributed by Scott Fenton, 7-Dec-2017.)
Hypotheses
Ref Expression
fprodf1o.1 (𝑘 = 𝐺𝐵 = 𝐷)
fprodf1o.2 (𝜑𝐶 ∈ Fin)
fprodf1o.3 (𝜑𝐹:𝐶1-1-onto𝐴)
fprodf1o.4 ((𝜑𝑛𝐶) → (𝐹𝑛) = 𝐺)
fprodf1o.5 ((𝜑𝑘𝐴) → 𝐵 ∈ ℂ)
Assertion
Ref Expression
fprodf1o (𝜑 → ∏𝑘𝐴 𝐵 = ∏𝑛𝐶 𝐷)
Distinct variable groups:   𝐴,𝑘,𝑛   𝐵,𝑛   𝐶,𝑛   𝐷,𝑘   𝑛,𝐹   𝑘,𝐺   𝜑,𝑘,𝑛
Allowed substitution hints:   𝐵(𝑘)   𝐶(𝑘)   𝐷(𝑛)   𝐹(𝑘)   𝐺(𝑛)

Proof of Theorem fprodf1o
Dummy variables 𝑓 𝑚 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 prod0 11459 . . . 4 𝑘 ∈ ∅ 𝐵 = 1
2 fprodf1o.3 . . . . . . . . 9 (𝜑𝐹:𝐶1-1-onto𝐴)
32adantr 274 . . . . . . . 8 ((𝜑𝐶 = ∅) → 𝐹:𝐶1-1-onto𝐴)
4 f1oeq2 5397 . . . . . . . . 9 (𝐶 = ∅ → (𝐹:𝐶1-1-onto𝐴𝐹:∅–1-1-onto𝐴))
54adantl 275 . . . . . . . 8 ((𝜑𝐶 = ∅) → (𝐹:𝐶1-1-onto𝐴𝐹:∅–1-1-onto𝐴))
63, 5mpbid 146 . . . . . . 7 ((𝜑𝐶 = ∅) → 𝐹:∅–1-1-onto𝐴)
7 f1ofo 5414 . . . . . . 7 (𝐹:∅–1-1-onto𝐴𝐹:∅–onto𝐴)
86, 7syl 14 . . . . . 6 ((𝜑𝐶 = ∅) → 𝐹:∅–onto𝐴)
9 fo00 5443 . . . . . . 7 (𝐹:∅–onto𝐴 ↔ (𝐹 = ∅ ∧ 𝐴 = ∅))
109simprbi 273 . . . . . 6 (𝐹:∅–onto𝐴𝐴 = ∅)
118, 10syl 14 . . . . 5 ((𝜑𝐶 = ∅) → 𝐴 = ∅)
1211prodeq1d 11438 . . . 4 ((𝜑𝐶 = ∅) → ∏𝑘𝐴 𝐵 = ∏𝑘 ∈ ∅ 𝐵)
13 prodeq1 11427 . . . . . 6 (𝐶 = ∅ → ∏𝑛𝐶 𝐷 = ∏𝑛 ∈ ∅ 𝐷)
14 prod0 11459 . . . . . 6 𝑛 ∈ ∅ 𝐷 = 1
1513, 14eqtrdi 2203 . . . . 5 (𝐶 = ∅ → ∏𝑛𝐶 𝐷 = 1)
1615adantl 275 . . . 4 ((𝜑𝐶 = ∅) → ∏𝑛𝐶 𝐷 = 1)
171, 12, 163eqtr4a 2213 . . 3 ((𝜑𝐶 = ∅) → ∏𝑘𝐴 𝐵 = ∏𝑛𝐶 𝐷)
1817ex 114 . 2 (𝜑 → (𝐶 = ∅ → ∏𝑘𝐴 𝐵 = ∏𝑛𝐶 𝐷))
19 2fveq3 5466 . . . . . . . 8 (𝑚 = (𝑓𝑛) → ((𝑘𝐴𝐵)‘(𝐹𝑚)) = ((𝑘𝐴𝐵)‘(𝐹‘(𝑓𝑛))))
20 simprl 521 . . . . . . . 8 ((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto𝐶)) → (♯‘𝐶) ∈ ℕ)
21 simprr 522 . . . . . . . 8 ((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto𝐶)) → 𝑓:(1...(♯‘𝐶))–1-1-onto𝐶)
22 f1of 5407 . . . . . . . . . . . 12 (𝐹:𝐶1-1-onto𝐴𝐹:𝐶𝐴)
232, 22syl 14 . . . . . . . . . . 11 (𝜑𝐹:𝐶𝐴)
2423ffvelrnda 5595 . . . . . . . . . 10 ((𝜑𝑚𝐶) → (𝐹𝑚) ∈ 𝐴)
25 fprodf1o.5 . . . . . . . . . . . 12 ((𝜑𝑘𝐴) → 𝐵 ∈ ℂ)
2625fmpttd 5615 . . . . . . . . . . 11 (𝜑 → (𝑘𝐴𝐵):𝐴⟶ℂ)
2726ffvelrnda 5595 . . . . . . . . . 10 ((𝜑 ∧ (𝐹𝑚) ∈ 𝐴) → ((𝑘𝐴𝐵)‘(𝐹𝑚)) ∈ ℂ)
2824, 27syldan 280 . . . . . . . . 9 ((𝜑𝑚𝐶) → ((𝑘𝐴𝐵)‘(𝐹𝑚)) ∈ ℂ)
2928adantlr 469 . . . . . . . 8 (((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto𝐶)) ∧ 𝑚𝐶) → ((𝑘𝐴𝐵)‘(𝐹𝑚)) ∈ ℂ)
30 simpr 109 . . . . . . . . . . . 12 (((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto𝐶) → 𝑓:(1...(♯‘𝐶))–1-1-onto𝐶)
31 f1oco 5430 . . . . . . . . . . . 12 ((𝐹:𝐶1-1-onto𝐴𝑓:(1...(♯‘𝐶))–1-1-onto𝐶) → (𝐹𝑓):(1...(♯‘𝐶))–1-1-onto𝐴)
322, 30, 31syl2an 287 . . . . . . . . . . 11 ((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto𝐶)) → (𝐹𝑓):(1...(♯‘𝐶))–1-1-onto𝐴)
33 f1of 5407 . . . . . . . . . . 11 ((𝐹𝑓):(1...(♯‘𝐶))–1-1-onto𝐴 → (𝐹𝑓):(1...(♯‘𝐶))⟶𝐴)
3432, 33syl 14 . . . . . . . . . 10 ((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto𝐶)) → (𝐹𝑓):(1...(♯‘𝐶))⟶𝐴)
35 fvco3 5532 . . . . . . . . . 10 (((𝐹𝑓):(1...(♯‘𝐶))⟶𝐴𝑛 ∈ (1...(♯‘𝐶))) → (((𝑘𝐴𝐵) ∘ (𝐹𝑓))‘𝑛) = ((𝑘𝐴𝐵)‘((𝐹𝑓)‘𝑛)))
3634, 35sylan 281 . . . . . . . . 9 (((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto𝐶)) ∧ 𝑛 ∈ (1...(♯‘𝐶))) → (((𝑘𝐴𝐵) ∘ (𝐹𝑓))‘𝑛) = ((𝑘𝐴𝐵)‘((𝐹𝑓)‘𝑛)))
37 f1of 5407 . . . . . . . . . . . . 13 (𝑓:(1...(♯‘𝐶))–1-1-onto𝐶𝑓:(1...(♯‘𝐶))⟶𝐶)
3837adantl 275 . . . . . . . . . . . 12 (((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto𝐶) → 𝑓:(1...(♯‘𝐶))⟶𝐶)
3938adantl 275 . . . . . . . . . . 11 ((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto𝐶)) → 𝑓:(1...(♯‘𝐶))⟶𝐶)
40 fvco3 5532 . . . . . . . . . . 11 ((𝑓:(1...(♯‘𝐶))⟶𝐶𝑛 ∈ (1...(♯‘𝐶))) → ((𝐹𝑓)‘𝑛) = (𝐹‘(𝑓𝑛)))
4139, 40sylan 281 . . . . . . . . . 10 (((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto𝐶)) ∧ 𝑛 ∈ (1...(♯‘𝐶))) → ((𝐹𝑓)‘𝑛) = (𝐹‘(𝑓𝑛)))
4241fveq2d 5465 . . . . . . . . 9 (((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto𝐶)) ∧ 𝑛 ∈ (1...(♯‘𝐶))) → ((𝑘𝐴𝐵)‘((𝐹𝑓)‘𝑛)) = ((𝑘𝐴𝐵)‘(𝐹‘(𝑓𝑛))))
4336, 42eqtrd 2187 . . . . . . . 8 (((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto𝐶)) ∧ 𝑛 ∈ (1...(♯‘𝐶))) → (((𝑘𝐴𝐵) ∘ (𝐹𝑓))‘𝑛) = ((𝑘𝐴𝐵)‘(𝐹‘(𝑓𝑛))))
4419, 20, 21, 29, 43fprodseq 11457 . . . . . . 7 ((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto𝐶)) → ∏𝑚𝐶 ((𝑘𝐴𝐵)‘(𝐹𝑚)) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐶), (((𝑘𝐴𝐵) ∘ (𝐹𝑓))‘𝑛), 1)))‘(♯‘𝐶)))
45 eqid 2154 . . . . . . . . . . . . 13 (𝑘𝐴𝐵) = (𝑘𝐴𝐵)
46 fprodf1o.1 . . . . . . . . . . . . 13 (𝑘 = 𝐺𝐵 = 𝐷)
47 fprodf1o.4 . . . . . . . . . . . . . 14 ((𝜑𝑛𝐶) → (𝐹𝑛) = 𝐺)
4823ffvelrnda 5595 . . . . . . . . . . . . . 14 ((𝜑𝑛𝐶) → (𝐹𝑛) ∈ 𝐴)
4947, 48eqeltrrd 2232 . . . . . . . . . . . . 13 ((𝜑𝑛𝐶) → 𝐺𝐴)
5046eleq1d 2223 . . . . . . . . . . . . . 14 (𝑘 = 𝐺 → (𝐵 ∈ ℂ ↔ 𝐷 ∈ ℂ))
5125ralrimiva 2527 . . . . . . . . . . . . . . 15 (𝜑 → ∀𝑘𝐴 𝐵 ∈ ℂ)
5251adantr 274 . . . . . . . . . . . . . 14 ((𝜑𝑛𝐶) → ∀𝑘𝐴 𝐵 ∈ ℂ)
5350, 52, 49rspcdva 2818 . . . . . . . . . . . . 13 ((𝜑𝑛𝐶) → 𝐷 ∈ ℂ)
5445, 46, 49, 53fvmptd3 5554 . . . . . . . . . . . 12 ((𝜑𝑛𝐶) → ((𝑘𝐴𝐵)‘𝐺) = 𝐷)
5547fveq2d 5465 . . . . . . . . . . . 12 ((𝜑𝑛𝐶) → ((𝑘𝐴𝐵)‘(𝐹𝑛)) = ((𝑘𝐴𝐵)‘𝐺))
56 simpr 109 . . . . . . . . . . . . 13 ((𝜑𝑛𝐶) → 𝑛𝐶)
57 eqid 2154 . . . . . . . . . . . . . 14 (𝑛𝐶𝐷) = (𝑛𝐶𝐷)
5857fvmpt2 5544 . . . . . . . . . . . . 13 ((𝑛𝐶𝐷 ∈ ℂ) → ((𝑛𝐶𝐷)‘𝑛) = 𝐷)
5956, 53, 58syl2anc 409 . . . . . . . . . . . 12 ((𝜑𝑛𝐶) → ((𝑛𝐶𝐷)‘𝑛) = 𝐷)
6054, 55, 593eqtr4rd 2198 . . . . . . . . . . 11 ((𝜑𝑛𝐶) → ((𝑛𝐶𝐷)‘𝑛) = ((𝑘𝐴𝐵)‘(𝐹𝑛)))
6160ralrimiva 2527 . . . . . . . . . 10 (𝜑 → ∀𝑛𝐶 ((𝑛𝐶𝐷)‘𝑛) = ((𝑘𝐴𝐵)‘(𝐹𝑛)))
62 nffvmpt1 5472 . . . . . . . . . . . 12 𝑛((𝑛𝐶𝐷)‘𝑚)
6362nfeq1 2306 . . . . . . . . . . 11 𝑛((𝑛𝐶𝐷)‘𝑚) = ((𝑘𝐴𝐵)‘(𝐹𝑚))
64 fveq2 5461 . . . . . . . . . . . 12 (𝑛 = 𝑚 → ((𝑛𝐶𝐷)‘𝑛) = ((𝑛𝐶𝐷)‘𝑚))
65 2fveq3 5466 . . . . . . . . . . . 12 (𝑛 = 𝑚 → ((𝑘𝐴𝐵)‘(𝐹𝑛)) = ((𝑘𝐴𝐵)‘(𝐹𝑚)))
6664, 65eqeq12d 2169 . . . . . . . . . . 11 (𝑛 = 𝑚 → (((𝑛𝐶𝐷)‘𝑛) = ((𝑘𝐴𝐵)‘(𝐹𝑛)) ↔ ((𝑛𝐶𝐷)‘𝑚) = ((𝑘𝐴𝐵)‘(𝐹𝑚))))
6763, 66rspc 2807 . . . . . . . . . 10 (𝑚𝐶 → (∀𝑛𝐶 ((𝑛𝐶𝐷)‘𝑛) = ((𝑘𝐴𝐵)‘(𝐹𝑛)) → ((𝑛𝐶𝐷)‘𝑚) = ((𝑘𝐴𝐵)‘(𝐹𝑚))))
6861, 67mpan9 279 . . . . . . . . 9 ((𝜑𝑚𝐶) → ((𝑛𝐶𝐷)‘𝑚) = ((𝑘𝐴𝐵)‘(𝐹𝑚)))
6968adantlr 469 . . . . . . . 8 (((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto𝐶)) ∧ 𝑚𝐶) → ((𝑛𝐶𝐷)‘𝑚) = ((𝑘𝐴𝐵)‘(𝐹𝑚)))
7069prodeq2dv 11440 . . . . . . 7 ((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto𝐶)) → ∏𝑚𝐶 ((𝑛𝐶𝐷)‘𝑚) = ∏𝑚𝐶 ((𝑘𝐴𝐵)‘(𝐹𝑚)))
71 fveq2 5461 . . . . . . . 8 (𝑚 = ((𝐹𝑓)‘𝑛) → ((𝑘𝐴𝐵)‘𝑚) = ((𝑘𝐴𝐵)‘((𝐹𝑓)‘𝑛)))
7226adantr 274 . . . . . . . . 9 ((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto𝐶)) → (𝑘𝐴𝐵):𝐴⟶ℂ)
7372ffvelrnda 5595 . . . . . . . 8 (((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto𝐶)) ∧ 𝑚𝐴) → ((𝑘𝐴𝐵)‘𝑚) ∈ ℂ)
7471, 20, 32, 73, 36fprodseq 11457 . . . . . . 7 ((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto𝐶)) → ∏𝑚𝐴 ((𝑘𝐴𝐵)‘𝑚) = (seq1( · , (𝑛 ∈ ℕ ↦ if(𝑛 ≤ (♯‘𝐶), (((𝑘𝐴𝐵) ∘ (𝐹𝑓))‘𝑛), 1)))‘(♯‘𝐶)))
7544, 70, 743eqtr4rd 2198 . . . . . 6 ((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto𝐶)) → ∏𝑚𝐴 ((𝑘𝐴𝐵)‘𝑚) = ∏𝑚𝐶 ((𝑛𝐶𝐷)‘𝑚))
7651adantr 274 . . . . . . 7 ((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto𝐶)) → ∀𝑘𝐴 𝐵 ∈ ℂ)
77 prodfct 11461 . . . . . . 7 (∀𝑘𝐴 𝐵 ∈ ℂ → ∏𝑚𝐴 ((𝑘𝐴𝐵)‘𝑚) = ∏𝑘𝐴 𝐵)
7876, 77syl 14 . . . . . 6 ((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto𝐶)) → ∏𝑚𝐴 ((𝑘𝐴𝐵)‘𝑚) = ∏𝑘𝐴 𝐵)
7953ralrimiva 2527 . . . . . . . 8 (𝜑 → ∀𝑛𝐶 𝐷 ∈ ℂ)
8079adantr 274 . . . . . . 7 ((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto𝐶)) → ∀𝑛𝐶 𝐷 ∈ ℂ)
81 prodfct 11461 . . . . . . 7 (∀𝑛𝐶 𝐷 ∈ ℂ → ∏𝑚𝐶 ((𝑛𝐶𝐷)‘𝑚) = ∏𝑛𝐶 𝐷)
8280, 81syl 14 . . . . . 6 ((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto𝐶)) → ∏𝑚𝐶 ((𝑛𝐶𝐷)‘𝑚) = ∏𝑛𝐶 𝐷)
8375, 78, 823eqtr3d 2195 . . . . 5 ((𝜑 ∧ ((♯‘𝐶) ∈ ℕ ∧ 𝑓:(1...(♯‘𝐶))–1-1-onto𝐶)) → ∏𝑘𝐴 𝐵 = ∏𝑛𝐶 𝐷)
8483expr 373 . . . 4 ((𝜑 ∧ (♯‘𝐶) ∈ ℕ) → (𝑓:(1...(♯‘𝐶))–1-1-onto𝐶 → ∏𝑘𝐴 𝐵 = ∏𝑛𝐶 𝐷))
8584exlimdv 1796 . . 3 ((𝜑 ∧ (♯‘𝐶) ∈ ℕ) → (∃𝑓 𝑓:(1...(♯‘𝐶))–1-1-onto𝐶 → ∏𝑘𝐴 𝐵 = ∏𝑛𝐶 𝐷))
8685expimpd 361 . 2 (𝜑 → (((♯‘𝐶) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘𝐶))–1-1-onto𝐶) → ∏𝑘𝐴 𝐵 = ∏𝑛𝐶 𝐷))
87 fprodf1o.2 . . 3 (𝜑𝐶 ∈ Fin)
88 fz1f1o 11249 . . 3 (𝐶 ∈ Fin → (𝐶 = ∅ ∨ ((♯‘𝐶) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘𝐶))–1-1-onto𝐶)))
8987, 88syl 14 . 2 (𝜑 → (𝐶 = ∅ ∨ ((♯‘𝐶) ∈ ℕ ∧ ∃𝑓 𝑓:(1...(♯‘𝐶))–1-1-onto𝐶)))
9018, 86, 89mpjaod 708 1 (𝜑 → ∏𝑘𝐴 𝐵 = ∏𝑛𝐶 𝐷)
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 698   = wceq 1332  ∃wex 1469   ∈ wcel 2125  ∀wral 2432  ∅c0 3390  ifcif 3501   class class class wbr 3961   ↦ cmpt 4021   ∘ ccom 4583  ⟶wf 5159  –onto→wfo 5161  –1-1-onto→wf1o 5162  ‘cfv 5163  (class class class)co 5814  Fincfn 6674  ℂcc 7709  1c1 7712   · cmul 7716   ≤ cle 7892  ℕcn 8812  ...cfz 9890  seqcseq 10322  ♯chash 10626  ∏cprod 11424 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1481  ax-10 1482  ax-11 1483  ax-i12 1484  ax-bndl 1486  ax-4 1487  ax-17 1503  ax-i9 1507  ax-ial 1511  ax-i5r 1512  ax-13 2127  ax-14 2128  ax-ext 2136  ax-coll 4075  ax-sep 4078  ax-nul 4086  ax-pow 4130  ax-pr 4164  ax-un 4388  ax-setind 4490  ax-iinf 4541  ax-cnex 7802  ax-resscn 7803  ax-1cn 7804  ax-1re 7805  ax-icn 7806  ax-addcl 7807  ax-addrcl 7808  ax-mulcl 7809  ax-mulrcl 7810  ax-addcom 7811  ax-mulcom 7812  ax-addass 7813  ax-mulass 7814  ax-distr 7815  ax-i2m1 7816  ax-0lt1 7817  ax-1rid 7818  ax-0id 7819  ax-rnegex 7820  ax-precex 7821  ax-cnre 7822  ax-pre-ltirr 7823  ax-pre-ltwlin 7824  ax-pre-lttrn 7825  ax-pre-apti 7826  ax-pre-ltadd 7827  ax-pre-mulgt0 7828  ax-pre-mulext 7829  ax-arch 7830  ax-caucvg 7831 This theorem depends on definitions:  df-bi 116  df-dc 821  df-3or 964  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1740  df-eu 2006  df-mo 2007  df-clab 2141  df-cleq 2147  df-clel 2150  df-nfc 2285  df-ne 2325  df-nel 2420  df-ral 2437  df-rex 2438  df-reu 2439  df-rmo 2440  df-rab 2441  df-v 2711  df-sbc 2934  df-csb 3028  df-dif 3100  df-un 3102  df-in 3104  df-ss 3111  df-nul 3391  df-if 3502  df-pw 3541  df-sn 3562  df-pr 3563  df-op 3565  df-uni 3769  df-int 3804  df-iun 3847  df-br 3962  df-opab 4022  df-mpt 4023  df-tr 4059  df-id 4248  df-po 4251  df-iso 4252  df-iord 4321  df-on 4323  df-ilim 4324  df-suc 4326  df-iom 4544  df-xp 4585  df-rel 4586  df-cnv 4587  df-co 4588  df-dm 4589  df-rn 4590  df-res 4591  df-ima 4592  df-iota 5128  df-fun 5165  df-fn 5166  df-f 5167  df-f1 5168  df-fo 5169  df-f1o 5170  df-fv 5171  df-isom 5172  df-riota 5770  df-ov 5817  df-oprab 5818  df-mpo 5819  df-1st 6078  df-2nd 6079  df-recs 6242  df-irdg 6307  df-frec 6328  df-1o 6353  df-oadd 6357  df-er 6469  df-en 6675  df-dom 6676  df-fin 6677  df-pnf 7893  df-mnf 7894  df-xr 7895  df-ltxr 7896  df-le 7897  df-sub 8027  df-neg 8028  df-reap 8429  df-ap 8436  df-div 8525  df-inn 8813  df-2 8871  df-3 8872  df-4 8873  df-n0 9070  df-z 9147  df-uz 9419  df-q 9507  df-rp 9539  df-fz 9891  df-fzo 10020  df-seqfrec 10323  df-exp 10397  df-ihash 10627  df-cj 10719  df-re 10720  df-im 10721  df-rsqrt 10875  df-abs 10876  df-clim 11153  df-proddc 11425 This theorem is referenced by:  fprodssdc  11464  fprodshft  11492  fprodrev  11493  fprod2dlemstep  11496  fprodcnv  11499
 Copyright terms: Public domain W3C validator