![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > natffn | Structured version Visualization version GIF version |
Description: The natural transformation set operation is a well-defined function. (Contributed by Mario Carneiro, 12-Jan-2017.) |
Ref | Expression |
---|---|
natrcl.1 | ⊢ 𝑁 = (𝐶 Nat 𝐷) |
Ref | Expression |
---|---|
natffn | ⊢ 𝑁 Fn ((𝐶 Func 𝐷) × (𝐶 Func 𝐷)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | natrcl.1 | . . 3 ⊢ 𝑁 = (𝐶 Nat 𝐷) | |
2 | eqid 2795 | . . 3 ⊢ (Base‘𝐶) = (Base‘𝐶) | |
3 | eqid 2795 | . . 3 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶) | |
4 | eqid 2795 | . . 3 ⊢ (Hom ‘𝐷) = (Hom ‘𝐷) | |
5 | eqid 2795 | . . 3 ⊢ (comp‘𝐷) = (comp‘𝐷) | |
6 | 1, 2, 3, 4, 5 | natfval 17050 | . 2 ⊢ 𝑁 = (𝑓 ∈ (𝐶 Func 𝐷), 𝑔 ∈ (𝐶 Func 𝐷) ↦ ⦋(1st ‘𝑓) / 𝑟⦌⦋(1st ‘𝑔) / 𝑠⦌{𝑎 ∈ X𝑥 ∈ (Base‘𝐶)((𝑟‘𝑥)(Hom ‘𝐷)(𝑠‘𝑥)) ∣ ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)∀ℎ ∈ (𝑥(Hom ‘𝐶)𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉(comp‘𝐷)(𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉(comp‘𝐷)(𝑠‘𝑦))(𝑎‘𝑥))}) |
7 | ovex 7053 | . . . . . . 7 ⊢ ((𝑟‘𝑥)(Hom ‘𝐷)(𝑠‘𝑥)) ∈ V | |
8 | 7 | rgenw 3117 | . . . . . 6 ⊢ ∀𝑥 ∈ (Base‘𝐶)((𝑟‘𝑥)(Hom ‘𝐷)(𝑠‘𝑥)) ∈ V |
9 | ixpexg 8339 | . . . . . 6 ⊢ (∀𝑥 ∈ (Base‘𝐶)((𝑟‘𝑥)(Hom ‘𝐷)(𝑠‘𝑥)) ∈ V → X𝑥 ∈ (Base‘𝐶)((𝑟‘𝑥)(Hom ‘𝐷)(𝑠‘𝑥)) ∈ V) | |
10 | 8, 9 | ax-mp 5 | . . . . 5 ⊢ X𝑥 ∈ (Base‘𝐶)((𝑟‘𝑥)(Hom ‘𝐷)(𝑠‘𝑥)) ∈ V |
11 | 10 | rabex 5131 | . . . 4 ⊢ {𝑎 ∈ X𝑥 ∈ (Base‘𝐶)((𝑟‘𝑥)(Hom ‘𝐷)(𝑠‘𝑥)) ∣ ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)∀ℎ ∈ (𝑥(Hom ‘𝐶)𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉(comp‘𝐷)(𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉(comp‘𝐷)(𝑠‘𝑦))(𝑎‘𝑥))} ∈ V |
12 | 11 | csbex 5111 | . . 3 ⊢ ⦋(1st ‘𝑔) / 𝑠⦌{𝑎 ∈ X𝑥 ∈ (Base‘𝐶)((𝑟‘𝑥)(Hom ‘𝐷)(𝑠‘𝑥)) ∣ ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)∀ℎ ∈ (𝑥(Hom ‘𝐶)𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉(comp‘𝐷)(𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉(comp‘𝐷)(𝑠‘𝑦))(𝑎‘𝑥))} ∈ V |
13 | 12 | csbex 5111 | . 2 ⊢ ⦋(1st ‘𝑓) / 𝑟⦌⦋(1st ‘𝑔) / 𝑠⦌{𝑎 ∈ X𝑥 ∈ (Base‘𝐶)((𝑟‘𝑥)(Hom ‘𝐷)(𝑠‘𝑥)) ∣ ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)∀ℎ ∈ (𝑥(Hom ‘𝐶)𝑦)((𝑎‘𝑦)(〈(𝑟‘𝑥), (𝑟‘𝑦)〉(comp‘𝐷)(𝑠‘𝑦))((𝑥(2nd ‘𝑓)𝑦)‘ℎ)) = (((𝑥(2nd ‘𝑔)𝑦)‘ℎ)(〈(𝑟‘𝑥), (𝑠‘𝑥)〉(comp‘𝐷)(𝑠‘𝑦))(𝑎‘𝑥))} ∈ V |
14 | 6, 13 | fnmpoi 7629 | 1 ⊢ 𝑁 Fn ((𝐶 Func 𝐷) × (𝐶 Func 𝐷)) |
Colors of variables: wff setvar class |
Syntax hints: = wceq 1522 ∈ wcel 2081 ∀wral 3105 {crab 3109 Vcvv 3437 ⦋csb 3815 〈cop 4482 × cxp 5446 Fn wfn 6225 ‘cfv 6230 (class class class)co 7021 1st c1st 7548 2nd c2nd 7549 Xcixp 8315 Basecbs 16317 Hom chom 16410 compcco 16411 Func cfunc 16958 Nat cnat 17045 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1777 ax-4 1791 ax-5 1888 ax-6 1947 ax-7 1992 ax-8 2083 ax-9 2091 ax-10 2112 ax-11 2126 ax-12 2141 ax-13 2344 ax-ext 2769 ax-rep 5086 ax-sep 5099 ax-nul 5106 ax-pow 5162 ax-pr 5226 ax-un 7324 |
This theorem depends on definitions: df-bi 208 df-an 397 df-or 843 df-3an 1082 df-tru 1525 df-fal 1535 df-ex 1762 df-nf 1766 df-sb 2043 df-mo 2576 df-eu 2612 df-clab 2776 df-cleq 2788 df-clel 2863 df-nfc 2935 df-ne 2985 df-ral 3110 df-rex 3111 df-reu 3112 df-rab 3114 df-v 3439 df-sbc 3710 df-csb 3816 df-dif 3866 df-un 3868 df-in 3870 df-ss 3878 df-nul 4216 df-if 4386 df-pw 4459 df-sn 4477 df-pr 4479 df-op 4483 df-uni 4750 df-iun 4831 df-br 4967 df-opab 5029 df-mpt 5046 df-id 5353 df-xp 5454 df-rel 5455 df-cnv 5456 df-co 5457 df-dm 5458 df-rn 5459 df-res 5460 df-ima 5461 df-iota 6194 df-fun 6232 df-fn 6233 df-f 6234 df-f1 6235 df-fo 6236 df-f1o 6237 df-fv 6238 df-ov 7024 df-oprab 7025 df-mpo 7026 df-1st 7550 df-2nd 7551 df-ixp 8316 df-func 16962 df-nat 17047 |
This theorem is referenced by: fuchom 17065 |
Copyright terms: Public domain | W3C validator |