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

Theorem fucco 17750
Description: Value of the composition of natural transformations. (Contributed by Mario Carneiro, 6-Jan-2017.)
Hypotheses
Ref Expression
fucco.q 𝑄 = (𝐶 FuncCat 𝐷)
fucco.n 𝑁 = (𝐶 Nat 𝐷)
fucco.a 𝐴 = (Base‘𝐶)
fucco.o · = (comp‘𝐷)
fucco.x = (comp‘𝑄)
fucco.f (𝜑𝑅 ∈ (𝐹𝑁𝐺))
fucco.g (𝜑𝑆 ∈ (𝐺𝑁𝐻))
Assertion
Ref Expression
fucco (𝜑 → (𝑆(⟨𝐹, 𝐺 𝐻)𝑅) = (𝑥𝐴 ↦ ((𝑆𝑥)(⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩ · ((1st𝐻)‘𝑥))(𝑅𝑥))))
Distinct variable groups:   𝑥,𝐴   𝜑,𝑥   𝑥,𝑅   𝑥,𝑆   𝑥,𝐶   𝑥,𝐷   𝑥, ·   𝑥,𝐹   𝑥,𝐺   𝑥,𝐻
Allowed substitution hints:   𝑄(𝑥)   (𝑥)   𝑁(𝑥)

Proof of Theorem fucco
Dummy variables 𝑎 𝑏 𝑓 𝑔 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fucco.q . . . 4 𝑄 = (𝐶 FuncCat 𝐷)
2 eqid 2737 . . . 4 (𝐶 Func 𝐷) = (𝐶 Func 𝐷)
3 fucco.n . . . 4 𝑁 = (𝐶 Nat 𝐷)
4 fucco.a . . . 4 𝐴 = (Base‘𝐶)
5 fucco.o . . . 4 · = (comp‘𝐷)
6 fucco.f . . . . . . . 8 (𝜑𝑅 ∈ (𝐹𝑁𝐺))
73natrcl 17736 . . . . . . . 8 (𝑅 ∈ (𝐹𝑁𝐺) → (𝐹 ∈ (𝐶 Func 𝐷) ∧ 𝐺 ∈ (𝐶 Func 𝐷)))
86, 7syl 17 . . . . . . 7 (𝜑 → (𝐹 ∈ (𝐶 Func 𝐷) ∧ 𝐺 ∈ (𝐶 Func 𝐷)))
98simpld 495 . . . . . 6 (𝜑𝐹 ∈ (𝐶 Func 𝐷))
10 funcrcl 17648 . . . . . 6 (𝐹 ∈ (𝐶 Func 𝐷) → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat))
119, 10syl 17 . . . . 5 (𝜑 → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat))
1211simpld 495 . . . 4 (𝜑𝐶 ∈ Cat)
1311simprd 496 . . . 4 (𝜑𝐷 ∈ Cat)
14 fucco.x . . . 4 = (comp‘𝑄)
151, 2, 3, 4, 5, 12, 13, 14fuccofval 17746 . . 3 (𝜑 = (𝑣 ∈ ((𝐶 Func 𝐷) × (𝐶 Func 𝐷)), ∈ (𝐶 Func 𝐷) ↦ (1st𝑣) / 𝑓(2nd𝑣) / 𝑔(𝑏 ∈ (𝑔𝑁), 𝑎 ∈ (𝑓𝑁𝑔) ↦ (𝑥𝐴 ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩ · ((1st)‘𝑥))(𝑎𝑥))))))
16 fvexd 6826 . . . 4 ((𝜑 ∧ (𝑣 = ⟨𝐹, 𝐺⟩ ∧ = 𝐻)) → (1st𝑣) ∈ V)
17 simprl 768 . . . . . 6 ((𝜑 ∧ (𝑣 = ⟨𝐹, 𝐺⟩ ∧ = 𝐻)) → 𝑣 = ⟨𝐹, 𝐺⟩)
1817fveq2d 6815 . . . . 5 ((𝜑 ∧ (𝑣 = ⟨𝐹, 𝐺⟩ ∧ = 𝐻)) → (1st𝑣) = (1st ‘⟨𝐹, 𝐺⟩))
19 op1stg 7888 . . . . . . 7 ((𝐹 ∈ (𝐶 Func 𝐷) ∧ 𝐺 ∈ (𝐶 Func 𝐷)) → (1st ‘⟨𝐹, 𝐺⟩) = 𝐹)
208, 19syl 17 . . . . . 6 (𝜑 → (1st ‘⟨𝐹, 𝐺⟩) = 𝐹)
2120adantr 481 . . . . 5 ((𝜑 ∧ (𝑣 = ⟨𝐹, 𝐺⟩ ∧ = 𝐻)) → (1st ‘⟨𝐹, 𝐺⟩) = 𝐹)
2218, 21eqtrd 2777 . . . 4 ((𝜑 ∧ (𝑣 = ⟨𝐹, 𝐺⟩ ∧ = 𝐻)) → (1st𝑣) = 𝐹)
23 fvexd 6826 . . . . 5 (((𝜑 ∧ (𝑣 = ⟨𝐹, 𝐺⟩ ∧ = 𝐻)) ∧ 𝑓 = 𝐹) → (2nd𝑣) ∈ V)
2417adantr 481 . . . . . . 7 (((𝜑 ∧ (𝑣 = ⟨𝐹, 𝐺⟩ ∧ = 𝐻)) ∧ 𝑓 = 𝐹) → 𝑣 = ⟨𝐹, 𝐺⟩)
2524fveq2d 6815 . . . . . 6 (((𝜑 ∧ (𝑣 = ⟨𝐹, 𝐺⟩ ∧ = 𝐻)) ∧ 𝑓 = 𝐹) → (2nd𝑣) = (2nd ‘⟨𝐹, 𝐺⟩))
26 op2ndg 7889 . . . . . . . 8 ((𝐹 ∈ (𝐶 Func 𝐷) ∧ 𝐺 ∈ (𝐶 Func 𝐷)) → (2nd ‘⟨𝐹, 𝐺⟩) = 𝐺)
278, 26syl 17 . . . . . . 7 (𝜑 → (2nd ‘⟨𝐹, 𝐺⟩) = 𝐺)
2827ad2antrr 723 . . . . . 6 (((𝜑 ∧ (𝑣 = ⟨𝐹, 𝐺⟩ ∧ = 𝐻)) ∧ 𝑓 = 𝐹) → (2nd ‘⟨𝐹, 𝐺⟩) = 𝐺)
2925, 28eqtrd 2777 . . . . 5 (((𝜑 ∧ (𝑣 = ⟨𝐹, 𝐺⟩ ∧ = 𝐻)) ∧ 𝑓 = 𝐹) → (2nd𝑣) = 𝐺)
30 simpr 485 . . . . . . 7 ((((𝜑 ∧ (𝑣 = ⟨𝐹, 𝐺⟩ ∧ = 𝐻)) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → 𝑔 = 𝐺)
31 simprr 770 . . . . . . . 8 ((𝜑 ∧ (𝑣 = ⟨𝐹, 𝐺⟩ ∧ = 𝐻)) → = 𝐻)
3231ad2antrr 723 . . . . . . 7 ((((𝜑 ∧ (𝑣 = ⟨𝐹, 𝐺⟩ ∧ = 𝐻)) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → = 𝐻)
3330, 32oveq12d 7333 . . . . . 6 ((((𝜑 ∧ (𝑣 = ⟨𝐹, 𝐺⟩ ∧ = 𝐻)) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑔𝑁) = (𝐺𝑁𝐻))
34 simplr 766 . . . . . . 7 ((((𝜑 ∧ (𝑣 = ⟨𝐹, 𝐺⟩ ∧ = 𝐻)) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → 𝑓 = 𝐹)
3534, 30oveq12d 7333 . . . . . 6 ((((𝜑 ∧ (𝑣 = ⟨𝐹, 𝐺⟩ ∧ = 𝐻)) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑓𝑁𝑔) = (𝐹𝑁𝐺))
3634fveq2d 6815 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑣 = ⟨𝐹, 𝐺⟩ ∧ = 𝐻)) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (1st𝑓) = (1st𝐹))
3736fveq1d 6813 . . . . . . . . . 10 ((((𝜑 ∧ (𝑣 = ⟨𝐹, 𝐺⟩ ∧ = 𝐻)) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → ((1st𝑓)‘𝑥) = ((1st𝐹)‘𝑥))
3830fveq2d 6815 . . . . . . . . . . 11 ((((𝜑 ∧ (𝑣 = ⟨𝐹, 𝐺⟩ ∧ = 𝐻)) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (1st𝑔) = (1st𝐺))
3938fveq1d 6813 . . . . . . . . . 10 ((((𝜑 ∧ (𝑣 = ⟨𝐹, 𝐺⟩ ∧ = 𝐻)) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → ((1st𝑔)‘𝑥) = ((1st𝐺)‘𝑥))
4037, 39opeq12d 4823 . . . . . . . . 9 ((((𝜑 ∧ (𝑣 = ⟨𝐹, 𝐺⟩ ∧ = 𝐻)) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → ⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩ = ⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩)
4132fveq2d 6815 . . . . . . . . . 10 ((((𝜑 ∧ (𝑣 = ⟨𝐹, 𝐺⟩ ∧ = 𝐻)) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (1st) = (1st𝐻))
4241fveq1d 6813 . . . . . . . . 9 ((((𝜑 ∧ (𝑣 = ⟨𝐹, 𝐺⟩ ∧ = 𝐻)) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → ((1st)‘𝑥) = ((1st𝐻)‘𝑥))
4340, 42oveq12d 7333 . . . . . . . 8 ((((𝜑 ∧ (𝑣 = ⟨𝐹, 𝐺⟩ ∧ = 𝐻)) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩ · ((1st)‘𝑥)) = (⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩ · ((1st𝐻)‘𝑥)))
4443oveqd 7332 . . . . . . 7 ((((𝜑 ∧ (𝑣 = ⟨𝐹, 𝐺⟩ ∧ = 𝐻)) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩ · ((1st)‘𝑥))(𝑎𝑥)) = ((𝑏𝑥)(⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩ · ((1st𝐻)‘𝑥))(𝑎𝑥)))
4544mpteq2dv 5189 . . . . . 6 ((((𝜑 ∧ (𝑣 = ⟨𝐹, 𝐺⟩ ∧ = 𝐻)) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑥𝐴 ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩ · ((1st)‘𝑥))(𝑎𝑥))) = (𝑥𝐴 ↦ ((𝑏𝑥)(⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩ · ((1st𝐻)‘𝑥))(𝑎𝑥))))
4633, 35, 45mpoeq123dv 7390 . . . . 5 ((((𝜑 ∧ (𝑣 = ⟨𝐹, 𝐺⟩ ∧ = 𝐻)) ∧ 𝑓 = 𝐹) ∧ 𝑔 = 𝐺) → (𝑏 ∈ (𝑔𝑁), 𝑎 ∈ (𝑓𝑁𝑔) ↦ (𝑥𝐴 ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩ · ((1st)‘𝑥))(𝑎𝑥)))) = (𝑏 ∈ (𝐺𝑁𝐻), 𝑎 ∈ (𝐹𝑁𝐺) ↦ (𝑥𝐴 ↦ ((𝑏𝑥)(⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩ · ((1st𝐻)‘𝑥))(𝑎𝑥)))))
4723, 29, 46csbied2 3882 . . . 4 (((𝜑 ∧ (𝑣 = ⟨𝐹, 𝐺⟩ ∧ = 𝐻)) ∧ 𝑓 = 𝐹) → (2nd𝑣) / 𝑔(𝑏 ∈ (𝑔𝑁), 𝑎 ∈ (𝑓𝑁𝑔) ↦ (𝑥𝐴 ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩ · ((1st)‘𝑥))(𝑎𝑥)))) = (𝑏 ∈ (𝐺𝑁𝐻), 𝑎 ∈ (𝐹𝑁𝐺) ↦ (𝑥𝐴 ↦ ((𝑏𝑥)(⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩ · ((1st𝐻)‘𝑥))(𝑎𝑥)))))
4816, 22, 47csbied2 3882 . . 3 ((𝜑 ∧ (𝑣 = ⟨𝐹, 𝐺⟩ ∧ = 𝐻)) → (1st𝑣) / 𝑓(2nd𝑣) / 𝑔(𝑏 ∈ (𝑔𝑁), 𝑎 ∈ (𝑓𝑁𝑔) ↦ (𝑥𝐴 ↦ ((𝑏𝑥)(⟨((1st𝑓)‘𝑥), ((1st𝑔)‘𝑥)⟩ · ((1st)‘𝑥))(𝑎𝑥)))) = (𝑏 ∈ (𝐺𝑁𝐻), 𝑎 ∈ (𝐹𝑁𝐺) ↦ (𝑥𝐴 ↦ ((𝑏𝑥)(⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩ · ((1st𝐻)‘𝑥))(𝑎𝑥)))))
49 opelxpi 5644 . . . 4 ((𝐹 ∈ (𝐶 Func 𝐷) ∧ 𝐺 ∈ (𝐶 Func 𝐷)) → ⟨𝐹, 𝐺⟩ ∈ ((𝐶 Func 𝐷) × (𝐶 Func 𝐷)))
508, 49syl 17 . . 3 (𝜑 → ⟨𝐹, 𝐺⟩ ∈ ((𝐶 Func 𝐷) × (𝐶 Func 𝐷)))
51 fucco.g . . . . 5 (𝜑𝑆 ∈ (𝐺𝑁𝐻))
523natrcl 17736 . . . . 5 (𝑆 ∈ (𝐺𝑁𝐻) → (𝐺 ∈ (𝐶 Func 𝐷) ∧ 𝐻 ∈ (𝐶 Func 𝐷)))
5351, 52syl 17 . . . 4 (𝜑 → (𝐺 ∈ (𝐶 Func 𝐷) ∧ 𝐻 ∈ (𝐶 Func 𝐷)))
5453simprd 496 . . 3 (𝜑𝐻 ∈ (𝐶 Func 𝐷))
55 ovex 7348 . . . . 5 (𝐺𝑁𝐻) ∈ V
56 ovex 7348 . . . . 5 (𝐹𝑁𝐺) ∈ V
5755, 56mpoex 7965 . . . 4 (𝑏 ∈ (𝐺𝑁𝐻), 𝑎 ∈ (𝐹𝑁𝐺) ↦ (𝑥𝐴 ↦ ((𝑏𝑥)(⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩ · ((1st𝐻)‘𝑥))(𝑎𝑥)))) ∈ V
5857a1i 11 . . 3 (𝜑 → (𝑏 ∈ (𝐺𝑁𝐻), 𝑎 ∈ (𝐹𝑁𝐺) ↦ (𝑥𝐴 ↦ ((𝑏𝑥)(⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩ · ((1st𝐻)‘𝑥))(𝑎𝑥)))) ∈ V)
5915, 48, 50, 54, 58ovmpod 7465 . 2 (𝜑 → (⟨𝐹, 𝐺 𝐻) = (𝑏 ∈ (𝐺𝑁𝐻), 𝑎 ∈ (𝐹𝑁𝐺) ↦ (𝑥𝐴 ↦ ((𝑏𝑥)(⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩ · ((1st𝐻)‘𝑥))(𝑎𝑥)))))
60 simprl 768 . . . . 5 ((𝜑 ∧ (𝑏 = 𝑆𝑎 = 𝑅)) → 𝑏 = 𝑆)
6160fveq1d 6813 . . . 4 ((𝜑 ∧ (𝑏 = 𝑆𝑎 = 𝑅)) → (𝑏𝑥) = (𝑆𝑥))
62 simprr 770 . . . . 5 ((𝜑 ∧ (𝑏 = 𝑆𝑎 = 𝑅)) → 𝑎 = 𝑅)
6362fveq1d 6813 . . . 4 ((𝜑 ∧ (𝑏 = 𝑆𝑎 = 𝑅)) → (𝑎𝑥) = (𝑅𝑥))
6461, 63oveq12d 7333 . . 3 ((𝜑 ∧ (𝑏 = 𝑆𝑎 = 𝑅)) → ((𝑏𝑥)(⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩ · ((1st𝐻)‘𝑥))(𝑎𝑥)) = ((𝑆𝑥)(⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩ · ((1st𝐻)‘𝑥))(𝑅𝑥)))
6564mpteq2dv 5189 . 2 ((𝜑 ∧ (𝑏 = 𝑆𝑎 = 𝑅)) → (𝑥𝐴 ↦ ((𝑏𝑥)(⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩ · ((1st𝐻)‘𝑥))(𝑎𝑥))) = (𝑥𝐴 ↦ ((𝑆𝑥)(⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩ · ((1st𝐻)‘𝑥))(𝑅𝑥))))
664fvexi 6825 . . . 4 𝐴 ∈ V
6766mptex 7138 . . 3 (𝑥𝐴 ↦ ((𝑆𝑥)(⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩ · ((1st𝐻)‘𝑥))(𝑅𝑥))) ∈ V
6867a1i 11 . 2 (𝜑 → (𝑥𝐴 ↦ ((𝑆𝑥)(⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩ · ((1st𝐻)‘𝑥))(𝑅𝑥))) ∈ V)
6959, 65, 51, 6, 68ovmpod 7465 1 (𝜑 → (𝑆(⟨𝐹, 𝐺 𝐻)𝑅) = (𝑥𝐴 ↦ ((𝑆𝑥)(⟨((1st𝐹)‘𝑥), ((1st𝐺)‘𝑥)⟩ · ((1st𝐻)‘𝑥))(𝑅𝑥))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1540  wcel 2105  Vcvv 3441  csb 3842  cop 4577  cmpt 5170   × cxp 5605  cfv 6465  (class class class)co 7315  cmpo 7317  1st c1st 7874  2nd c2nd 7875  Basecbs 16982  compcco 17044  Catccat 17443   Func cfunc 17639   Nat cnat 17727   FuncCat cfuc 17728
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-rep 5224  ax-sep 5238  ax-nul 5245  ax-pow 5303  ax-pr 5367  ax-un 7628  ax-cnex 11000  ax-resscn 11001  ax-1cn 11002  ax-icn 11003  ax-addcl 11004  ax-addrcl 11005  ax-mulcl 11006  ax-mulrcl 11007  ax-mulcom 11008  ax-addass 11009  ax-mulass 11010  ax-distr 11011  ax-i2m1 11012  ax-1ne0 11013  ax-1rid 11014  ax-rnegex 11015  ax-rrecex 11016  ax-cnre 11017  ax-pre-lttri 11018  ax-pre-lttrn 11019  ax-pre-ltadd 11020  ax-pre-mulgt0 11021
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-reu 3351  df-rab 3405  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3916  df-nul 4268  df-if 4472  df-pw 4547  df-sn 4572  df-pr 4574  df-tp 4576  df-op 4578  df-uni 4851  df-iun 4939  df-br 5088  df-opab 5150  df-mpt 5171  df-tr 5205  df-id 5507  df-eprel 5513  df-po 5521  df-so 5522  df-fr 5562  df-we 5564  df-xp 5613  df-rel 5614  df-cnv 5615  df-co 5616  df-dm 5617  df-rn 5618  df-res 5619  df-ima 5620  df-pred 6224  df-ord 6291  df-on 6292  df-lim 6293  df-suc 6294  df-iota 6417  df-fun 6467  df-fn 6468  df-f 6469  df-f1 6470  df-fo 6471  df-f1o 6472  df-fv 6473  df-riota 7272  df-ov 7318  df-oprab 7319  df-mpo 7320  df-om 7758  df-1st 7876  df-2nd 7877  df-frecs 8144  df-wrecs 8175  df-recs 8249  df-rdg 8288  df-1o 8344  df-er 8546  df-ixp 8734  df-en 8782  df-dom 8783  df-sdom 8784  df-fin 8785  df-pnf 11084  df-mnf 11085  df-xr 11086  df-ltxr 11087  df-le 11088  df-sub 11280  df-neg 11281  df-nn 12047  df-2 12109  df-3 12110  df-4 12111  df-5 12112  df-6 12113  df-7 12114  df-8 12115  df-9 12116  df-n0 12307  df-z 12393  df-dec 12511  df-uz 12656  df-fz 13313  df-struct 16918  df-slot 16953  df-ndx 16965  df-base 16983  df-hom 17056  df-cco 17057  df-func 17643  df-nat 17729  df-fuc 17730
This theorem is referenced by:  fuccoval  17751  fuccocl  17752  fuclid  17754  fucrid  17755  fucass  17756  fucsect  17760  curfcl  18020
  Copyright terms: Public domain W3C validator