Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  funcrngcsetcALT Structured version   Visualization version   GIF version

Theorem funcrngcsetcALT 41303
Description: Alternate proof of funcrngcsetc 41302, using cofuval2 16471 to construct the "natural forgetful functor" from the category of non-unital rings into the category of sets by composing the "inclusion functor" from the category of non-unital rings into the category of extensible structures, see rngcifuestrc 41301, and the "natural forgetful functor" from the category of extensible structures into the category of sets, see funcestrcsetc 16713. Surprisingly, this proof is longer than the direct proof given in funcrngcsetc 41302. (Contributed by AV, 30-Mar-2020.) (Proof modification is discouraged.) (New usage is discouraged.)
Hypotheses
Ref Expression
funcrngcsetcALT.r 𝑅 = (RngCat‘𝑈)
funcrngcsetcALT.s 𝑆 = (SetCat‘𝑈)
funcrngcsetcALT.b 𝐵 = (Base‘𝑅)
funcrngcsetcALT.u (𝜑𝑈 ∈ WUni)
funcrngcsetcALT.f (𝜑𝐹 = (𝑥𝐵 ↦ (Base‘𝑥)))
funcrngcsetcALT.g (𝜑𝐺 = (𝑥𝐵, 𝑦𝐵 ↦ ( I ↾ (𝑥 RngHomo 𝑦))))
Assertion
Ref Expression
funcrngcsetcALT (𝜑𝐹(𝑅 Func 𝑆)𝐺)
Distinct variable groups:   𝑥,𝐵,𝑦   𝑥,𝑅,𝑦   𝑥,𝑈,𝑦   𝜑,𝑥,𝑦
Allowed substitution hints:   𝑆(𝑥,𝑦)   𝐹(𝑥,𝑦)   𝐺(𝑥,𝑦)

Proof of Theorem funcrngcsetcALT
Dummy variables 𝑓 𝑔 𝑢 𝑤 𝑧 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 funcrngcsetcALT.f . . . . . . 7 (𝜑𝐹 = (𝑥𝐵 ↦ (Base‘𝑥)))
2 fveq2 6150 . . . . . . . 8 (𝑥 = 𝑢 → (Base‘𝑥) = (Base‘𝑢))
32cbvmptv 4712 . . . . . . 7 (𝑥𝐵 ↦ (Base‘𝑥)) = (𝑢𝐵 ↦ (Base‘𝑢))
41, 3syl6eq 2671 . . . . . 6 (𝜑𝐹 = (𝑢𝐵 ↦ (Base‘𝑢)))
5 coires1 5614 . . . . . . 7 ((𝑢𝑈 ↦ (Base‘𝑢)) ∘ ( I ↾ 𝐵)) = ((𝑢𝑈 ↦ (Base‘𝑢)) ↾ 𝐵)
6 funcrngcsetcALT.r . . . . . . . . . . . 12 𝑅 = (RngCat‘𝑈)
7 funcrngcsetcALT.b . . . . . . . . . . . 12 𝐵 = (Base‘𝑅)
8 funcrngcsetcALT.u . . . . . . . . . . . 12 (𝜑𝑈 ∈ WUni)
96, 7, 8rngcbas 41269 . . . . . . . . . . 11 (𝜑𝐵 = (𝑈 ∩ Rng))
109eleq2d 2684 . . . . . . . . . 10 (𝜑 → (𝑥𝐵𝑥 ∈ (𝑈 ∩ Rng)))
11 elin 3776 . . . . . . . . . . 11 (𝑥 ∈ (𝑈 ∩ Rng) ↔ (𝑥𝑈𝑥 ∈ Rng))
1211simplbi 476 . . . . . . . . . 10 (𝑥 ∈ (𝑈 ∩ Rng) → 𝑥𝑈)
1310, 12syl6bi 243 . . . . . . . . 9 (𝜑 → (𝑥𝐵𝑥𝑈))
1413ssrdv 3590 . . . . . . . 8 (𝜑𝐵𝑈)
1514resmptd 5413 . . . . . . 7 (𝜑 → ((𝑢𝑈 ↦ (Base‘𝑢)) ↾ 𝐵) = (𝑢𝐵 ↦ (Base‘𝑢)))
165, 15syl5req 2668 . . . . . 6 (𝜑 → (𝑢𝐵 ↦ (Base‘𝑢)) = ((𝑢𝑈 ↦ (Base‘𝑢)) ∘ ( I ↾ 𝐵)))
174, 16eqtrd 2655 . . . . 5 (𝜑𝐹 = ((𝑢𝑈 ↦ (Base‘𝑢)) ∘ ( I ↾ 𝐵)))
18 funcrngcsetcALT.g . . . . . . 7 (𝜑𝐺 = (𝑥𝐵, 𝑦𝐵 ↦ ( I ↾ (𝑥 RngHomo 𝑦))))
19 coires1 5614 . . . . . . . . 9 (( I ↾ ((Base‘𝑦) ↑𝑚 (Base‘𝑥))) ∘ ( I ↾ (𝑥 RngHomo 𝑦))) = (( I ↾ ((Base‘𝑦) ↑𝑚 (Base‘𝑥))) ↾ (𝑥 RngHomo 𝑦))
20 eqid 2621 . . . . . . . . . . . . 13 (Base‘𝑥) = (Base‘𝑥)
21 eqid 2621 . . . . . . . . . . . . 13 (Base‘𝑦) = (Base‘𝑦)
2220, 21rnghmf 41203 . . . . . . . . . . . 12 (𝑧 ∈ (𝑥 RngHomo 𝑦) → 𝑧:(Base‘𝑥)⟶(Base‘𝑦))
23 fvex 6160 . . . . . . . . . . . . . 14 (Base‘𝑦) ∈ V
24 fvex 6160 . . . . . . . . . . . . . 14 (Base‘𝑥) ∈ V
2523, 24pm3.2i 471 . . . . . . . . . . . . 13 ((Base‘𝑦) ∈ V ∧ (Base‘𝑥) ∈ V)
26 elmapg 7818 . . . . . . . . . . . . 13 (((Base‘𝑦) ∈ V ∧ (Base‘𝑥) ∈ V) → (𝑧 ∈ ((Base‘𝑦) ↑𝑚 (Base‘𝑥)) ↔ 𝑧:(Base‘𝑥)⟶(Base‘𝑦)))
2725, 26mp1i 13 . . . . . . . . . . . 12 ((𝜑𝑥𝐵𝑦𝐵) → (𝑧 ∈ ((Base‘𝑦) ↑𝑚 (Base‘𝑥)) ↔ 𝑧:(Base‘𝑥)⟶(Base‘𝑦)))
2822, 27syl5ibr 236 . . . . . . . . . . 11 ((𝜑𝑥𝐵𝑦𝐵) → (𝑧 ∈ (𝑥 RngHomo 𝑦) → 𝑧 ∈ ((Base‘𝑦) ↑𝑚 (Base‘𝑥))))
2928ssrdv 3590 . . . . . . . . . 10 ((𝜑𝑥𝐵𝑦𝐵) → (𝑥 RngHomo 𝑦) ⊆ ((Base‘𝑦) ↑𝑚 (Base‘𝑥)))
3029resabs1d 5389 . . . . . . . . 9 ((𝜑𝑥𝐵𝑦𝐵) → (( I ↾ ((Base‘𝑦) ↑𝑚 (Base‘𝑥))) ↾ (𝑥 RngHomo 𝑦)) = ( I ↾ (𝑥 RngHomo 𝑦)))
3119, 30syl5req 2668 . . . . . . . 8 ((𝜑𝑥𝐵𝑦𝐵) → ( I ↾ (𝑥 RngHomo 𝑦)) = (( I ↾ ((Base‘𝑦) ↑𝑚 (Base‘𝑥))) ∘ ( I ↾ (𝑥 RngHomo 𝑦))))
3231mpt2eq3dva 6675 . . . . . . 7 (𝜑 → (𝑥𝐵, 𝑦𝐵 ↦ ( I ↾ (𝑥 RngHomo 𝑦))) = (𝑥𝐵, 𝑦𝐵 ↦ (( I ↾ ((Base‘𝑦) ↑𝑚 (Base‘𝑥))) ∘ ( I ↾ (𝑥 RngHomo 𝑦)))))
3318, 32eqtrd 2655 . . . . . 6 (𝜑𝐺 = (𝑥𝐵, 𝑦𝐵 ↦ (( I ↾ ((Base‘𝑦) ↑𝑚 (Base‘𝑥))) ∘ ( I ↾ (𝑥 RngHomo 𝑦)))))
347a1i 11 . . . . . . 7 (𝜑𝐵 = (Base‘𝑅))
357a1i 11 . . . . . . 7 ((𝜑𝑥𝐵) → 𝐵 = (Base‘𝑅))
36 fvresi 6396 . . . . . . . . . . . 12 (𝑥𝐵 → (( I ↾ 𝐵)‘𝑥) = 𝑥)
3736adantr 481 . . . . . . . . . . 11 ((𝑥𝐵𝑦𝐵) → (( I ↾ 𝐵)‘𝑥) = 𝑥)
3837adantl 482 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (( I ↾ 𝐵)‘𝑥) = 𝑥)
39 fvresi 6396 . . . . . . . . . . . 12 (𝑦𝐵 → (( I ↾ 𝐵)‘𝑦) = 𝑦)
4039adantl 482 . . . . . . . . . . 11 ((𝑥𝐵𝑦𝐵) → (( I ↾ 𝐵)‘𝑦) = 𝑦)
4140adantl 482 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (( I ↾ 𝐵)‘𝑦) = 𝑦)
4238, 41oveq12d 6625 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ((( I ↾ 𝐵)‘𝑥)(𝑤𝑈, 𝑧𝑈 ↦ ( I ↾ ((Base‘𝑧) ↑𝑚 (Base‘𝑤))))(( I ↾ 𝐵)‘𝑦)) = (𝑥(𝑤𝑈, 𝑧𝑈 ↦ ( I ↾ ((Base‘𝑧) ↑𝑚 (Base‘𝑤))))𝑦))
43 eqidd 2622 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑤𝑈, 𝑧𝑈 ↦ ( I ↾ ((Base‘𝑧) ↑𝑚 (Base‘𝑤)))) = (𝑤𝑈, 𝑧𝑈 ↦ ( I ↾ ((Base‘𝑧) ↑𝑚 (Base‘𝑤)))))
44 simprr 795 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑤 = 𝑥𝑧 = 𝑦)) → 𝑧 = 𝑦)
4544fveq2d 6154 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑤 = 𝑥𝑧 = 𝑦)) → (Base‘𝑧) = (Base‘𝑦))
46 simprl 793 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑤 = 𝑥𝑧 = 𝑦)) → 𝑤 = 𝑥)
4746fveq2d 6154 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑤 = 𝑥𝑧 = 𝑦)) → (Base‘𝑤) = (Base‘𝑥))
4845, 47oveq12d 6625 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑤 = 𝑥𝑧 = 𝑦)) → ((Base‘𝑧) ↑𝑚 (Base‘𝑤)) = ((Base‘𝑦) ↑𝑚 (Base‘𝑥)))
4948reseq2d 5358 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑤 = 𝑥𝑧 = 𝑦)) → ( I ↾ ((Base‘𝑧) ↑𝑚 (Base‘𝑤))) = ( I ↾ ((Base‘𝑦) ↑𝑚 (Base‘𝑥))))
5013com12 32 . . . . . . . . . . . 12 (𝑥𝐵 → (𝜑𝑥𝑈))
5150adantr 481 . . . . . . . . . . 11 ((𝑥𝐵𝑦𝐵) → (𝜑𝑥𝑈))
5251impcom 446 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑥𝑈)
539eleq2d 2684 . . . . . . . . . . . . 13 (𝜑 → (𝑦𝐵𝑦 ∈ (𝑈 ∩ Rng)))
54 elin 3776 . . . . . . . . . . . . . 14 (𝑦 ∈ (𝑈 ∩ Rng) ↔ (𝑦𝑈𝑦 ∈ Rng))
5554simplbi 476 . . . . . . . . . . . . 13 (𝑦 ∈ (𝑈 ∩ Rng) → 𝑦𝑈)
5653, 55syl6bi 243 . . . . . . . . . . . 12 (𝜑 → (𝑦𝐵𝑦𝑈))
5756a1d 25 . . . . . . . . . . 11 (𝜑 → (𝑥𝐵 → (𝑦𝐵𝑦𝑈)))
5857imp32 449 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑦𝑈)
59 ovex 6635 . . . . . . . . . . . 12 ((Base‘𝑦) ↑𝑚 (Base‘𝑥)) ∈ V
6059a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ((Base‘𝑦) ↑𝑚 (Base‘𝑥)) ∈ V)
6160resiexd 6437 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ( I ↾ ((Base‘𝑦) ↑𝑚 (Base‘𝑥))) ∈ V)
6243, 49, 52, 58, 61ovmpt2d 6744 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑥(𝑤𝑈, 𝑧𝑈 ↦ ( I ↾ ((Base‘𝑧) ↑𝑚 (Base‘𝑤))))𝑦) = ( I ↾ ((Base‘𝑦) ↑𝑚 (Base‘𝑥))))
6342, 62eqtr2d 2656 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ( I ↾ ((Base‘𝑦) ↑𝑚 (Base‘𝑥))) = ((( I ↾ 𝐵)‘𝑥)(𝑤𝑈, 𝑧𝑈 ↦ ( I ↾ ((Base‘𝑧) ↑𝑚 (Base‘𝑤))))(( I ↾ 𝐵)‘𝑦)))
64 eqidd 2622 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑓𝐵, 𝑔𝐵 ↦ ( I ↾ (𝑓 RngHomo 𝑔))) = (𝑓𝐵, 𝑔𝐵 ↦ ( I ↾ (𝑓 RngHomo 𝑔))))
65 oveq12 6616 . . . . . . . . . . . 12 ((𝑓 = 𝑥𝑔 = 𝑦) → (𝑓 RngHomo 𝑔) = (𝑥 RngHomo 𝑦))
6665reseq2d 5358 . . . . . . . . . . 11 ((𝑓 = 𝑥𝑔 = 𝑦) → ( I ↾ (𝑓 RngHomo 𝑔)) = ( I ↾ (𝑥 RngHomo 𝑦)))
6766adantl 482 . . . . . . . . . 10 (((𝜑 ∧ (𝑥𝐵𝑦𝐵)) ∧ (𝑓 = 𝑥𝑔 = 𝑦)) → ( I ↾ (𝑓 RngHomo 𝑔)) = ( I ↾ (𝑥 RngHomo 𝑦)))
68 simprl 793 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑥𝐵)
69 simprr 795 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → 𝑦𝐵)
70 ovex 6635 . . . . . . . . . . . 12 (𝑥 RngHomo 𝑦) ∈ V
7170a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑥 RngHomo 𝑦) ∈ V)
7271resiexd 6437 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ( I ↾ (𝑥 RngHomo 𝑦)) ∈ V)
7364, 67, 68, 69, 72ovmpt2d 6744 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (𝑥(𝑓𝐵, 𝑔𝐵 ↦ ( I ↾ (𝑓 RngHomo 𝑔)))𝑦) = ( I ↾ (𝑥 RngHomo 𝑦)))
7473eqcomd 2627 . . . . . . . 8 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → ( I ↾ (𝑥 RngHomo 𝑦)) = (𝑥(𝑓𝐵, 𝑔𝐵 ↦ ( I ↾ (𝑓 RngHomo 𝑔)))𝑦))
7563, 74coeq12d 5248 . . . . . . 7 ((𝜑 ∧ (𝑥𝐵𝑦𝐵)) → (( I ↾ ((Base‘𝑦) ↑𝑚 (Base‘𝑥))) ∘ ( I ↾ (𝑥 RngHomo 𝑦))) = (((( I ↾ 𝐵)‘𝑥)(𝑤𝑈, 𝑧𝑈 ↦ ( I ↾ ((Base‘𝑧) ↑𝑚 (Base‘𝑤))))(( I ↾ 𝐵)‘𝑦)) ∘ (𝑥(𝑓𝐵, 𝑔𝐵 ↦ ( I ↾ (𝑓 RngHomo 𝑔)))𝑦)))
7634, 35, 75mpt2eq123dva 6672 . . . . . 6 (𝜑 → (𝑥𝐵, 𝑦𝐵 ↦ (( I ↾ ((Base‘𝑦) ↑𝑚 (Base‘𝑥))) ∘ ( I ↾ (𝑥 RngHomo 𝑦)))) = (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑅) ↦ (((( I ↾ 𝐵)‘𝑥)(𝑤𝑈, 𝑧𝑈 ↦ ( I ↾ ((Base‘𝑧) ↑𝑚 (Base‘𝑤))))(( I ↾ 𝐵)‘𝑦)) ∘ (𝑥(𝑓𝐵, 𝑔𝐵 ↦ ( I ↾ (𝑓 RngHomo 𝑔)))𝑦))))
7733, 76eqtrd 2655 . . . . 5 (𝜑𝐺 = (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑅) ↦ (((( I ↾ 𝐵)‘𝑥)(𝑤𝑈, 𝑧𝑈 ↦ ( I ↾ ((Base‘𝑧) ↑𝑚 (Base‘𝑤))))(( I ↾ 𝐵)‘𝑦)) ∘ (𝑥(𝑓𝐵, 𝑔𝐵 ↦ ( I ↾ (𝑓 RngHomo 𝑔)))𝑦))))
7817, 77opeq12d 4380 . . . 4 (𝜑 → ⟨𝐹, 𝐺⟩ = ⟨((𝑢𝑈 ↦ (Base‘𝑢)) ∘ ( I ↾ 𝐵)), (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑅) ↦ (((( I ↾ 𝐵)‘𝑥)(𝑤𝑈, 𝑧𝑈 ↦ ( I ↾ ((Base‘𝑧) ↑𝑚 (Base‘𝑤))))(( I ↾ 𝐵)‘𝑦)) ∘ (𝑥(𝑓𝐵, 𝑔𝐵 ↦ ( I ↾ (𝑓 RngHomo 𝑔)))𝑦)))⟩)
79 eqid 2621 . . . . 5 (Base‘𝑅) = (Base‘𝑅)
80 eqid 2621 . . . . . 6 (ExtStrCat‘𝑈) = (ExtStrCat‘𝑈)
81 eqidd 2622 . . . . . 6 (𝜑 → ( I ↾ 𝐵) = ( I ↾ 𝐵))
82 eqidd 2622 . . . . . 6 (𝜑 → (𝑓𝐵, 𝑔𝐵 ↦ ( I ↾ (𝑓 RngHomo 𝑔))) = (𝑓𝐵, 𝑔𝐵 ↦ ( I ↾ (𝑓 RngHomo 𝑔))))
836, 80, 7, 8, 81, 82rngcifuestrc 41301 . . . . 5 (𝜑 → ( I ↾ 𝐵)(𝑅 Func (ExtStrCat‘𝑈))(𝑓𝐵, 𝑔𝐵 ↦ ( I ↾ (𝑓 RngHomo 𝑔))))
84 funcrngcsetcALT.s . . . . . 6 𝑆 = (SetCat‘𝑈)
85 eqid 2621 . . . . . 6 (Base‘(ExtStrCat‘𝑈)) = (Base‘(ExtStrCat‘𝑈))
86 eqid 2621 . . . . . 6 (Base‘𝑆) = (Base‘𝑆)
8780, 8estrcbas 16689 . . . . . . 7 (𝜑𝑈 = (Base‘(ExtStrCat‘𝑈)))
8887mpteq1d 4700 . . . . . 6 (𝜑 → (𝑢𝑈 ↦ (Base‘𝑢)) = (𝑢 ∈ (Base‘(ExtStrCat‘𝑈)) ↦ (Base‘𝑢)))
89 fveq2 6150 . . . . . . . . . . 11 (𝑤 = 𝑢 → (Base‘𝑤) = (Base‘𝑢))
9089oveq2d 6623 . . . . . . . . . 10 (𝑤 = 𝑢 → ((Base‘𝑧) ↑𝑚 (Base‘𝑤)) = ((Base‘𝑧) ↑𝑚 (Base‘𝑢)))
9190reseq2d 5358 . . . . . . . . 9 (𝑤 = 𝑢 → ( I ↾ ((Base‘𝑧) ↑𝑚 (Base‘𝑤))) = ( I ↾ ((Base‘𝑧) ↑𝑚 (Base‘𝑢))))
92 fveq2 6150 . . . . . . . . . . 11 (𝑧 = 𝑣 → (Base‘𝑧) = (Base‘𝑣))
9392oveq1d 6622 . . . . . . . . . 10 (𝑧 = 𝑣 → ((Base‘𝑧) ↑𝑚 (Base‘𝑢)) = ((Base‘𝑣) ↑𝑚 (Base‘𝑢)))
9493reseq2d 5358 . . . . . . . . 9 (𝑧 = 𝑣 → ( I ↾ ((Base‘𝑧) ↑𝑚 (Base‘𝑢))) = ( I ↾ ((Base‘𝑣) ↑𝑚 (Base‘𝑢))))
9591, 94cbvmpt2v 6691 . . . . . . . 8 (𝑤𝑈, 𝑧𝑈 ↦ ( I ↾ ((Base‘𝑧) ↑𝑚 (Base‘𝑤)))) = (𝑢𝑈, 𝑣𝑈 ↦ ( I ↾ ((Base‘𝑣) ↑𝑚 (Base‘𝑢))))
9695a1i 11 . . . . . . 7 (𝜑 → (𝑤𝑈, 𝑧𝑈 ↦ ( I ↾ ((Base‘𝑧) ↑𝑚 (Base‘𝑤)))) = (𝑢𝑈, 𝑣𝑈 ↦ ( I ↾ ((Base‘𝑣) ↑𝑚 (Base‘𝑢)))))
97 eqidd 2622 . . . . . . . 8 (𝜑 → ( I ↾ ((Base‘𝑣) ↑𝑚 (Base‘𝑢))) = ( I ↾ ((Base‘𝑣) ↑𝑚 (Base‘𝑢))))
9887, 87, 97mpt2eq123dv 6673 . . . . . . 7 (𝜑 → (𝑢𝑈, 𝑣𝑈 ↦ ( I ↾ ((Base‘𝑣) ↑𝑚 (Base‘𝑢)))) = (𝑢 ∈ (Base‘(ExtStrCat‘𝑈)), 𝑣 ∈ (Base‘(ExtStrCat‘𝑈)) ↦ ( I ↾ ((Base‘𝑣) ↑𝑚 (Base‘𝑢)))))
9996, 98eqtrd 2655 . . . . . 6 (𝜑 → (𝑤𝑈, 𝑧𝑈 ↦ ( I ↾ ((Base‘𝑧) ↑𝑚 (Base‘𝑤)))) = (𝑢 ∈ (Base‘(ExtStrCat‘𝑈)), 𝑣 ∈ (Base‘(ExtStrCat‘𝑈)) ↦ ( I ↾ ((Base‘𝑣) ↑𝑚 (Base‘𝑢)))))
10080, 84, 85, 86, 8, 88, 99funcestrcsetc 16713 . . . . 5 (𝜑 → (𝑢𝑈 ↦ (Base‘𝑢))((ExtStrCat‘𝑈) Func 𝑆)(𝑤𝑈, 𝑧𝑈 ↦ ( I ↾ ((Base‘𝑧) ↑𝑚 (Base‘𝑤)))))
10179, 83, 100cofuval2 16471 . . . 4 (𝜑 → (⟨(𝑢𝑈 ↦ (Base‘𝑢)), (𝑤𝑈, 𝑧𝑈 ↦ ( I ↾ ((Base‘𝑧) ↑𝑚 (Base‘𝑤))))⟩ ∘func ⟨( I ↾ 𝐵), (𝑓𝐵, 𝑔𝐵 ↦ ( I ↾ (𝑓 RngHomo 𝑔)))⟩) = ⟨((𝑢𝑈 ↦ (Base‘𝑢)) ∘ ( I ↾ 𝐵)), (𝑥 ∈ (Base‘𝑅), 𝑦 ∈ (Base‘𝑅) ↦ (((( I ↾ 𝐵)‘𝑥)(𝑤𝑈, 𝑧𝑈 ↦ ( I ↾ ((Base‘𝑧) ↑𝑚 (Base‘𝑤))))(( I ↾ 𝐵)‘𝑦)) ∘ (𝑥(𝑓𝐵, 𝑔𝐵 ↦ ( I ↾ (𝑓 RngHomo 𝑔)))𝑦)))⟩)
10278, 101eqtr4d 2658 . . 3 (𝜑 → ⟨𝐹, 𝐺⟩ = (⟨(𝑢𝑈 ↦ (Base‘𝑢)), (𝑤𝑈, 𝑧𝑈 ↦ ( I ↾ ((Base‘𝑧) ↑𝑚 (Base‘𝑤))))⟩ ∘func ⟨( I ↾ 𝐵), (𝑓𝐵, 𝑔𝐵 ↦ ( I ↾ (𝑓 RngHomo 𝑔)))⟩))
103 df-br 4616 . . . . 5 (( I ↾ 𝐵)(𝑅 Func (ExtStrCat‘𝑈))(𝑓𝐵, 𝑔𝐵 ↦ ( I ↾ (𝑓 RngHomo 𝑔))) ↔ ⟨( I ↾ 𝐵), (𝑓𝐵, 𝑔𝐵 ↦ ( I ↾ (𝑓 RngHomo 𝑔)))⟩ ∈ (𝑅 Func (ExtStrCat‘𝑈)))
10483, 103sylib 208 . . . 4 (𝜑 → ⟨( I ↾ 𝐵), (𝑓𝐵, 𝑔𝐵 ↦ ( I ↾ (𝑓 RngHomo 𝑔)))⟩ ∈ (𝑅 Func (ExtStrCat‘𝑈)))
105 df-br 4616 . . . . 5 ((𝑢𝑈 ↦ (Base‘𝑢))((ExtStrCat‘𝑈) Func 𝑆)(𝑤𝑈, 𝑧𝑈 ↦ ( I ↾ ((Base‘𝑧) ↑𝑚 (Base‘𝑤)))) ↔ ⟨(𝑢𝑈 ↦ (Base‘𝑢)), (𝑤𝑈, 𝑧𝑈 ↦ ( I ↾ ((Base‘𝑧) ↑𝑚 (Base‘𝑤))))⟩ ∈ ((ExtStrCat‘𝑈) Func 𝑆))
106100, 105sylib 208 . . . 4 (𝜑 → ⟨(𝑢𝑈 ↦ (Base‘𝑢)), (𝑤𝑈, 𝑧𝑈 ↦ ( I ↾ ((Base‘𝑧) ↑𝑚 (Base‘𝑤))))⟩ ∈ ((ExtStrCat‘𝑈) Func 𝑆))
107104, 106cofucl 16472 . . 3 (𝜑 → (⟨(𝑢𝑈 ↦ (Base‘𝑢)), (𝑤𝑈, 𝑧𝑈 ↦ ( I ↾ ((Base‘𝑧) ↑𝑚 (Base‘𝑤))))⟩ ∘func ⟨( I ↾ 𝐵), (𝑓𝐵, 𝑔𝐵 ↦ ( I ↾ (𝑓 RngHomo 𝑔)))⟩) ∈ (𝑅 Func 𝑆))
108102, 107eqeltrd 2698 . 2 (𝜑 → ⟨𝐹, 𝐺⟩ ∈ (𝑅 Func 𝑆))
109 df-br 4616 . 2 (𝐹(𝑅 Func 𝑆)𝐺 ↔ ⟨𝐹, 𝐺⟩ ∈ (𝑅 Func 𝑆))
110108, 109sylibr 224 1 (𝜑𝐹(𝑅 Func 𝑆)𝐺)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3a 1036   = wceq 1480  wcel 1987  Vcvv 3186  cin 3555  cop 4156   class class class wbr 4615  cmpt 4675   I cid 4986  cres 5078  ccom 5080  wf 5845  cfv 5849  (class class class)co 6607  cmpt2 6609  𝑚 cmap 7805  WUnicwun 9469  Basecbs 15784   Func cfunc 16438  func ccofu 16440  SetCatcsetc 16649  ExtStrCatcestrc 16686  Rngcrng 41178   RngHomo crngh 41189  RngCatcrngc 41261
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 4733  ax-sep 4743  ax-nul 4751  ax-pow 4805  ax-pr 4869  ax-un 6905  ax-cnex 9939  ax-resscn 9940  ax-1cn 9941  ax-icn 9942  ax-addcl 9943  ax-addrcl 9944  ax-mulcl 9945  ax-mulrcl 9946  ax-mulcom 9947  ax-addass 9948  ax-mulass 9949  ax-distr 9950  ax-i2m1 9951  ax-1ne0 9952  ax-1rid 9953  ax-rnegex 9954  ax-rrecex 9955  ax-cnre 9956  ax-pre-lttri 9957  ax-pre-lttrn 9958  ax-pre-ltadd 9959  ax-pre-mulgt0 9960
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  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 3419  df-csb 3516  df-dif 3559  df-un 3561  df-in 3563  df-ss 3570  df-pss 3572  df-nul 3894  df-if 4061  df-pw 4134  df-sn 4151  df-pr 4153  df-tp 4155  df-op 4157  df-uni 4405  df-int 4443  df-iun 4489  df-br 4616  df-opab 4676  df-mpt 4677  df-tr 4715  df-eprel 4987  df-id 4991  df-po 4997  df-so 4998  df-fr 5035  df-we 5037  df-xp 5082  df-rel 5083  df-cnv 5084  df-co 5085  df-dm 5086  df-rn 5087  df-res 5088  df-ima 5089  df-pred 5641  df-ord 5687  df-on 5688  df-lim 5689  df-suc 5690  df-iota 5812  df-fun 5851  df-fn 5852  df-f 5853  df-f1 5854  df-fo 5855  df-f1o 5856  df-fv 5857  df-riota 6568  df-ov 6610  df-oprab 6611  df-mpt2 6612  df-om 7016  df-1st 7116  df-2nd 7117  df-wrecs 7355  df-recs 7416  df-rdg 7454  df-1o 7508  df-oadd 7512  df-er 7690  df-map 7807  df-pm 7808  df-ixp 7856  df-en 7903  df-dom 7904  df-sdom 7905  df-fin 7906  df-wun 9471  df-pnf 10023  df-mnf 10024  df-xr 10025  df-ltxr 10026  df-le 10027  df-sub 10215  df-neg 10216  df-nn 10968  df-2 11026  df-3 11027  df-4 11028  df-5 11029  df-6 11030  df-7 11031  df-8 11032  df-9 11033  df-n0 11240  df-z 11325  df-dec 11441  df-uz 11635  df-fz 12272  df-struct 15786  df-ndx 15787  df-slot 15788  df-base 15789  df-sets 15790  df-ress 15791  df-plusg 15878  df-hom 15890  df-cco 15891  df-0g 16026  df-cat 16253  df-cid 16254  df-homf 16255  df-ssc 16394  df-resc 16395  df-subc 16396  df-func 16442  df-idfu 16443  df-cofu 16444  df-full 16488  df-fth 16489  df-setc 16650  df-estrc 16687  df-mgm 17166  df-sgrp 17208  df-mnd 17219  df-mhm 17259  df-grp 17349  df-ghm 17582  df-abl 18120  df-mgp 18414  df-mgmhm 41083  df-rng0 41179  df-rnghomo 41191  df-rngc 41263
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator