Step | Hyp | Ref
| Expression |
1 | | eqid 2610 |
. . . . . 6
⊢
(ExtStrCat‘𝑈)
= (ExtStrCat‘𝑈) |
2 | | funcringcsetc.s |
. . . . . 6
⊢ 𝑆 = (SetCat‘𝑈) |
3 | | eqid 2610 |
. . . . . 6
⊢
(Base‘(ExtStrCat‘𝑈)) = (Base‘(ExtStrCat‘𝑈)) |
4 | | eqid 2610 |
. . . . . 6
⊢
(Base‘𝑆) =
(Base‘𝑆) |
5 | | funcringcsetc.u |
. . . . . 6
⊢ (𝜑 → 𝑈 ∈ WUni) |
6 | 1, 5 | estrcbas 16588 |
. . . . . . 7
⊢ (𝜑 → 𝑈 = (Base‘(ExtStrCat‘𝑈))) |
7 | 6 | mpteq1d 4666 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝑈 ↦ (Base‘𝑥)) = (𝑥 ∈ (Base‘(ExtStrCat‘𝑈)) ↦ (Base‘𝑥))) |
8 | | mpt2eq12 6613 |
. . . . . . 7
⊢ ((𝑈 =
(Base‘(ExtStrCat‘𝑈)) ∧ 𝑈 = (Base‘(ExtStrCat‘𝑈))) → (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑𝑚
(Base‘𝑥)))) = (𝑥 ∈
(Base‘(ExtStrCat‘𝑈)), 𝑦 ∈ (Base‘(ExtStrCat‘𝑈)) ↦ ( I ↾
((Base‘𝑦)
↑𝑚 (Base‘𝑥))))) |
9 | 6, 6, 8 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑𝑚
(Base‘𝑥)))) = (𝑥 ∈
(Base‘(ExtStrCat‘𝑈)), 𝑦 ∈ (Base‘(ExtStrCat‘𝑈)) ↦ ( I ↾
((Base‘𝑦)
↑𝑚 (Base‘𝑥))))) |
10 | 1, 2, 3, 4, 5, 7, 9 | funcestrcsetc 16612 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝑈 ↦ (Base‘𝑥))((ExtStrCat‘𝑈) Func 𝑆)(𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑𝑚
(Base‘𝑥))))) |
11 | | df-br 4584 |
. . . . 5
⊢ ((𝑥 ∈ 𝑈 ↦ (Base‘𝑥))((ExtStrCat‘𝑈) Func 𝑆)(𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑𝑚
(Base‘𝑥)))) ↔
〈(𝑥 ∈ 𝑈 ↦ (Base‘𝑥)), (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑𝑚
(Base‘𝑥))))〉
∈ ((ExtStrCat‘𝑈)
Func 𝑆)) |
12 | 10, 11 | sylib 207 |
. . . 4
⊢ (𝜑 → 〈(𝑥 ∈ 𝑈 ↦ (Base‘𝑥)), (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑𝑚
(Base‘𝑥))))〉
∈ ((ExtStrCat‘𝑈)
Func 𝑆)) |
13 | | funcringcsetc.r |
. . . . . . 7
⊢ 𝑅 = (RingCat‘𝑈) |
14 | | eqid 2610 |
. . . . . . 7
⊢
(Base‘𝑅) =
(Base‘𝑅) |
15 | 13, 14, 5 | ringcbas 41803 |
. . . . . 6
⊢ (𝜑 → (Base‘𝑅) = (𝑈 ∩ Ring)) |
16 | | incom 3767 |
. . . . . 6
⊢ (𝑈 ∩ Ring) = (Ring ∩ 𝑈) |
17 | 15, 16 | syl6eq 2660 |
. . . . 5
⊢ (𝜑 → (Base‘𝑅) = (Ring ∩ 𝑈)) |
18 | | eqid 2610 |
. . . . . 6
⊢ (Hom
‘𝑅) = (Hom
‘𝑅) |
19 | 13, 14, 5, 18 | ringchomfval 41804 |
. . . . 5
⊢ (𝜑 → (Hom ‘𝑅) = ( RingHom ↾
((Base‘𝑅) ×
(Base‘𝑅)))) |
20 | 1, 5, 17, 19 | rhmsubcsetc 41815 |
. . . 4
⊢ (𝜑 → (Hom ‘𝑅) ∈
(Subcat‘(ExtStrCat‘𝑈))) |
21 | 12, 20 | funcres 16379 |
. . 3
⊢ (𝜑 → (〈(𝑥 ∈ 𝑈 ↦ (Base‘𝑥)), (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑𝑚
(Base‘𝑥))))〉
↾f (Hom ‘𝑅)) ∈ (((ExtStrCat‘𝑈) ↾cat (Hom
‘𝑅)) Func 𝑆)) |
22 | | mptexg 6389 |
. . . . . 6
⊢ (𝑈 ∈ WUni → (𝑥 ∈ 𝑈 ↦ (Base‘𝑥)) ∈ V) |
23 | 5, 22 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝑈 ↦ (Base‘𝑥)) ∈ V) |
24 | | fvex 6113 |
. . . . . 6
⊢ (Hom
‘𝑅) ∈
V |
25 | 24 | a1i 11 |
. . . . 5
⊢ (𝜑 → (Hom ‘𝑅) ∈ V) |
26 | | mpt2exga 7135 |
. . . . . 6
⊢ ((𝑈 ∈ WUni ∧ 𝑈 ∈ WUni) → (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑𝑚
(Base‘𝑥)))) ∈
V) |
27 | 5, 5, 26 | syl2anc 691 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑𝑚
(Base‘𝑥)))) ∈
V) |
28 | 15, 19 | rhmresfn 41801 |
. . . . 5
⊢ (𝜑 → (Hom ‘𝑅) Fn ((Base‘𝑅) × (Base‘𝑅))) |
29 | 23, 25, 27, 28 | resfval2 16376 |
. . . 4
⊢ (𝜑 → (〈(𝑥 ∈ 𝑈 ↦ (Base‘𝑥)), (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑𝑚
(Base‘𝑥))))〉
↾f (Hom ‘𝑅)) = 〈((𝑥 ∈ 𝑈 ↦ (Base‘𝑥)) ↾ (Base‘𝑅)), (𝑎 ∈ (Base‘𝑅), 𝑏 ∈ (Base‘𝑅) ↦ ((𝑎(𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑𝑚
(Base‘𝑥))))𝑏) ↾ (𝑎(Hom ‘𝑅)𝑏)))〉) |
30 | | inss1 3795 |
. . . . . . . 8
⊢ (𝑈 ∩ Ring) ⊆ 𝑈 |
31 | 15, 30 | syl6eqss 3618 |
. . . . . . 7
⊢ (𝜑 → (Base‘𝑅) ⊆ 𝑈) |
32 | 31 | resmptd 5371 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ 𝑈 ↦ (Base‘𝑥)) ↾ (Base‘𝑅)) = (𝑥 ∈ (Base‘𝑅) ↦ (Base‘𝑥))) |
33 | | funcringcsetc.f |
. . . . . . 7
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) |
34 | | funcringcsetc.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝑅) |
35 | 34 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 = (Base‘𝑅)) |
36 | 35 | mpteq1d 4666 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)) = (𝑥 ∈ (Base‘𝑅) ↦ (Base‘𝑥))) |
37 | 33, 36 | eqtr2d 2645 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (Base‘𝑅) ↦ (Base‘𝑥)) = 𝐹) |
38 | 32, 37 | eqtrd 2644 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝑈 ↦ (Base‘𝑥)) ↾ (Base‘𝑅)) = 𝐹) |
39 | | funcringcsetc.g |
. . . . . 6
⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RingHom 𝑦)))) |
40 | | oveq1 6556 |
. . . . . . . . 9
⊢ (𝑥 = 𝑎 → (𝑥 RingHom 𝑦) = (𝑎 RingHom 𝑦)) |
41 | 40 | reseq2d 5317 |
. . . . . . . 8
⊢ (𝑥 = 𝑎 → ( I ↾ (𝑥 RingHom 𝑦)) = ( I ↾ (𝑎 RingHom 𝑦))) |
42 | | oveq2 6557 |
. . . . . . . . 9
⊢ (𝑦 = 𝑏 → (𝑎 RingHom 𝑦) = (𝑎 RingHom 𝑏)) |
43 | 42 | reseq2d 5317 |
. . . . . . . 8
⊢ (𝑦 = 𝑏 → ( I ↾ (𝑎 RingHom 𝑦)) = ( I ↾ (𝑎 RingHom 𝑏))) |
44 | 41, 43 | cbvmpt2v 6633 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RingHom 𝑦))) = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ ( I ↾ (𝑎 RingHom 𝑏))) |
45 | 44 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RingHom 𝑦))) = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ ( I ↾ (𝑎 RingHom 𝑏)))) |
46 | 34 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → 𝐵 = (Base‘𝑅)) |
47 | | eqidd 2611 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑𝑚
(Base‘𝑥)))) = (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑𝑚
(Base‘𝑥))))) |
48 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑏 → (Base‘𝑦) = (Base‘𝑏)) |
49 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑎 → (Base‘𝑥) = (Base‘𝑎)) |
50 | 48, 49 | oveqan12rd 6569 |
. . . . . . . . . . . 12
⊢ ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → ((Base‘𝑦) ↑𝑚
(Base‘𝑥)) =
((Base‘𝑏)
↑𝑚 (Base‘𝑎))) |
51 | 50 | reseq2d 5317 |
. . . . . . . . . . 11
⊢ ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → ( I ↾ ((Base‘𝑦) ↑𝑚
(Base‘𝑥))) = ( I
↾ ((Base‘𝑏)
↑𝑚 (Base‘𝑎)))) |
52 | 51 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑥 = 𝑎 ∧ 𝑦 = 𝑏)) → ( I ↾ ((Base‘𝑦) ↑𝑚
(Base‘𝑥))) = ( I
↾ ((Base‘𝑏)
↑𝑚 (Base‘𝑎)))) |
53 | 34, 31 | syl5eqss 3612 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵 ⊆ 𝑈) |
54 | 53 | sseld 3567 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑎 ∈ 𝐵 → 𝑎 ∈ 𝑈)) |
55 | 54 | com12 32 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ 𝐵 → (𝜑 → 𝑎 ∈ 𝑈)) |
56 | 55 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝜑 → 𝑎 ∈ 𝑈)) |
57 | 56 | impcom 445 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝑎 ∈ 𝑈) |
58 | 53 | sseld 3567 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑏 ∈ 𝐵 → 𝑏 ∈ 𝑈)) |
59 | 58 | adantld 482 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝑈)) |
60 | 59 | imp 444 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝑏 ∈ 𝑈) |
61 | | ovex 6577 |
. . . . . . . . . . . 12
⊢
((Base‘𝑏)
↑𝑚 (Base‘𝑎)) ∈ V |
62 | 61 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((Base‘𝑏) ↑𝑚
(Base‘𝑎)) ∈
V) |
63 | 62 | resiexd 6385 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ( I ↾ ((Base‘𝑏) ↑𝑚
(Base‘𝑎))) ∈
V) |
64 | 47, 52, 57, 60, 63 | ovmpt2d 6686 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎(𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑𝑚
(Base‘𝑥))))𝑏) = ( I ↾
((Base‘𝑏)
↑𝑚 (Base‘𝑎)))) |
65 | 64 | reseq1d 5316 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝑎(𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑𝑚
(Base‘𝑥))))𝑏) ↾ (𝑎(Hom ‘𝑅)𝑏)) = (( I ↾ ((Base‘𝑏) ↑𝑚
(Base‘𝑎))) ↾
(𝑎(Hom ‘𝑅)𝑏))) |
66 | 5 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝑈 ∈ WUni) |
67 | | simprl 790 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝑎 ∈ 𝐵) |
68 | | simprr 792 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝑏 ∈ 𝐵) |
69 | 13, 34, 66, 18, 67, 68 | ringchom 41805 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎(Hom ‘𝑅)𝑏) = (𝑎 RingHom 𝑏)) |
70 | 69 | reseq2d 5317 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (( I ↾ ((Base‘𝑏) ↑𝑚
(Base‘𝑎))) ↾
(𝑎(Hom ‘𝑅)𝑏)) = (( I ↾ ((Base‘𝑏) ↑𝑚
(Base‘𝑎))) ↾
(𝑎 RingHom 𝑏))) |
71 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(Base‘𝑎) =
(Base‘𝑎) |
72 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(Base‘𝑏) =
(Base‘𝑏) |
73 | 71, 72 | rhmf 18549 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ (𝑎 RingHom 𝑏) → 𝑓:(Base‘𝑎)⟶(Base‘𝑏)) |
74 | | fvex 6113 |
. . . . . . . . . . . . . 14
⊢
(Base‘𝑏)
∈ V |
75 | | fvex 6113 |
. . . . . . . . . . . . . 14
⊢
(Base‘𝑎)
∈ V |
76 | 74, 75 | pm3.2i 470 |
. . . . . . . . . . . . 13
⊢
((Base‘𝑏)
∈ V ∧ (Base‘𝑎) ∈ V) |
77 | 76 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((Base‘𝑏) ∈ V ∧ (Base‘𝑎) ∈ V)) |
78 | | elmapg 7757 |
. . . . . . . . . . . 12
⊢
(((Base‘𝑏)
∈ V ∧ (Base‘𝑎) ∈ V) → (𝑓 ∈ ((Base‘𝑏) ↑𝑚
(Base‘𝑎)) ↔
𝑓:(Base‘𝑎)⟶(Base‘𝑏))) |
79 | 77, 78 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑓 ∈ ((Base‘𝑏) ↑𝑚
(Base‘𝑎)) ↔
𝑓:(Base‘𝑎)⟶(Base‘𝑏))) |
80 | 73, 79 | syl5ibr 235 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑓 ∈ (𝑎 RingHom 𝑏) → 𝑓 ∈ ((Base‘𝑏) ↑𝑚
(Base‘𝑎)))) |
81 | 80 | ssrdv 3574 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎 RingHom 𝑏) ⊆ ((Base‘𝑏) ↑𝑚
(Base‘𝑎))) |
82 | 81 | resabs1d 5348 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (( I ↾ ((Base‘𝑏) ↑𝑚
(Base‘𝑎))) ↾
(𝑎 RingHom 𝑏)) = ( I ↾ (𝑎 RingHom 𝑏))) |
83 | 65, 70, 82 | 3eqtrrd 2649 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ( I ↾ (𝑎 RingHom 𝑏)) = ((𝑎(𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑𝑚
(Base‘𝑥))))𝑏) ↾ (𝑎(Hom ‘𝑅)𝑏))) |
84 | 35, 46, 83 | mpt2eq123dva 6614 |
. . . . . 6
⊢ (𝜑 → (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ ( I ↾ (𝑎 RingHom 𝑏))) = (𝑎 ∈ (Base‘𝑅), 𝑏 ∈ (Base‘𝑅) ↦ ((𝑎(𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑𝑚
(Base‘𝑥))))𝑏) ↾ (𝑎(Hom ‘𝑅)𝑏)))) |
85 | 39, 45, 84 | 3eqtrrd 2649 |
. . . . 5
⊢ (𝜑 → (𝑎 ∈ (Base‘𝑅), 𝑏 ∈ (Base‘𝑅) ↦ ((𝑎(𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑𝑚
(Base‘𝑥))))𝑏) ↾ (𝑎(Hom ‘𝑅)𝑏))) = 𝐺) |
86 | 38, 85 | opeq12d 4348 |
. . . 4
⊢ (𝜑 → 〈((𝑥 ∈ 𝑈 ↦ (Base‘𝑥)) ↾ (Base‘𝑅)), (𝑎 ∈ (Base‘𝑅), 𝑏 ∈ (Base‘𝑅) ↦ ((𝑎(𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑𝑚
(Base‘𝑥))))𝑏) ↾ (𝑎(Hom ‘𝑅)𝑏)))〉 = 〈𝐹, 𝐺〉) |
87 | 29, 86 | eqtr2d 2645 |
. . 3
⊢ (𝜑 → 〈𝐹, 𝐺〉 = (〈(𝑥 ∈ 𝑈 ↦ (Base‘𝑥)), (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑𝑚
(Base‘𝑥))))〉
↾f (Hom ‘𝑅))) |
88 | 13, 5, 15, 19 | ringcval 41800 |
. . . 4
⊢ (𝜑 → 𝑅 = ((ExtStrCat‘𝑈) ↾cat (Hom ‘𝑅))) |
89 | 88 | oveq1d 6564 |
. . 3
⊢ (𝜑 → (𝑅 Func 𝑆) = (((ExtStrCat‘𝑈) ↾cat (Hom ‘𝑅)) Func 𝑆)) |
90 | 21, 87, 89 | 3eltr4d 2703 |
. 2
⊢ (𝜑 → 〈𝐹, 𝐺〉 ∈ (𝑅 Func 𝑆)) |
91 | | df-br 4584 |
. 2
⊢ (𝐹(𝑅 Func 𝑆)𝐺 ↔ 〈𝐹, 𝐺〉 ∈ (𝑅 Func 𝑆)) |
92 | 90, 91 | sylibr 223 |
1
⊢ (𝜑 → 𝐹(𝑅 Func 𝑆)𝐺) |