| Step | Hyp | Ref
| Expression |
| 1 | | eqid 2737 |
. . . . . 6
⊢
(ExtStrCat‘𝑈)
= (ExtStrCat‘𝑈) |
| 2 | | funcrngcsetc.s |
. . . . . 6
⊢ 𝑆 = (SetCat‘𝑈) |
| 3 | | eqid 2737 |
. . . . . 6
⊢
(Base‘(ExtStrCat‘𝑈)) = (Base‘(ExtStrCat‘𝑈)) |
| 4 | | eqid 2737 |
. . . . . 6
⊢
(Base‘𝑆) =
(Base‘𝑆) |
| 5 | | funcrngcsetc.u |
. . . . . 6
⊢ (𝜑 → 𝑈 ∈ WUni) |
| 6 | 1, 5 | estrcbas 18169 |
. . . . . . 7
⊢ (𝜑 → 𝑈 = (Base‘(ExtStrCat‘𝑈))) |
| 7 | 6 | mpteq1d 5237 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝑈 ↦ (Base‘𝑥)) = (𝑥 ∈ (Base‘(ExtStrCat‘𝑈)) ↦ (Base‘𝑥))) |
| 8 | | mpoeq12 7506 |
. . . . . . 7
⊢ ((𝑈 =
(Base‘(ExtStrCat‘𝑈)) ∧ 𝑈 = (Base‘(ExtStrCat‘𝑈))) → (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m
(Base‘𝑥)))) = (𝑥 ∈
(Base‘(ExtStrCat‘𝑈)), 𝑦 ∈ (Base‘(ExtStrCat‘𝑈)) ↦ ( I ↾
((Base‘𝑦)
↑m (Base‘𝑥))))) |
| 9 | 6, 6, 8 | syl2anc 584 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m
(Base‘𝑥)))) = (𝑥 ∈
(Base‘(ExtStrCat‘𝑈)), 𝑦 ∈ (Base‘(ExtStrCat‘𝑈)) ↦ ( I ↾
((Base‘𝑦)
↑m (Base‘𝑥))))) |
| 10 | 1, 2, 3, 4, 5, 7, 9 | funcestrcsetc 18194 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝑈 ↦ (Base‘𝑥))((ExtStrCat‘𝑈) Func 𝑆)(𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m
(Base‘𝑥))))) |
| 11 | | df-br 5144 |
. . . . 5
⊢ ((𝑥 ∈ 𝑈 ↦ (Base‘𝑥))((ExtStrCat‘𝑈) Func 𝑆)(𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m
(Base‘𝑥)))) ↔
〈(𝑥 ∈ 𝑈 ↦ (Base‘𝑥)), (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m
(Base‘𝑥))))〉
∈ ((ExtStrCat‘𝑈)
Func 𝑆)) |
| 12 | 10, 11 | sylib 218 |
. . . 4
⊢ (𝜑 → 〈(𝑥 ∈ 𝑈 ↦ (Base‘𝑥)), (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m
(Base‘𝑥))))〉
∈ ((ExtStrCat‘𝑈)
Func 𝑆)) |
| 13 | | funcrngcsetc.r |
. . . . . . 7
⊢ 𝑅 = (RngCat‘𝑈) |
| 14 | | eqid 2737 |
. . . . . . 7
⊢
(Base‘𝑅) =
(Base‘𝑅) |
| 15 | 13, 14, 5 | rngcbas 20621 |
. . . . . 6
⊢ (𝜑 → (Base‘𝑅) = (𝑈 ∩ Rng)) |
| 16 | | incom 4209 |
. . . . . 6
⊢ (𝑈 ∩ Rng) = (Rng ∩ 𝑈) |
| 17 | 15, 16 | eqtrdi 2793 |
. . . . 5
⊢ (𝜑 → (Base‘𝑅) = (Rng ∩ 𝑈)) |
| 18 | | eqid 2737 |
. . . . . 6
⊢ (Hom
‘𝑅) = (Hom
‘𝑅) |
| 19 | 13, 14, 5, 18 | rngchomfval 20622 |
. . . . 5
⊢ (𝜑 → (Hom ‘𝑅) = ( RngHom ↾
((Base‘𝑅) ×
(Base‘𝑅)))) |
| 20 | 1, 5, 17, 19 | rnghmsubcsetc 20633 |
. . . 4
⊢ (𝜑 → (Hom ‘𝑅) ∈
(Subcat‘(ExtStrCat‘𝑈))) |
| 21 | 12, 20 | funcres 17941 |
. . 3
⊢ (𝜑 → (〈(𝑥 ∈ 𝑈 ↦ (Base‘𝑥)), (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m
(Base‘𝑥))))〉
↾f (Hom ‘𝑅)) ∈ (((ExtStrCat‘𝑈) ↾cat (Hom
‘𝑅)) Func 𝑆)) |
| 22 | | mptexg 7241 |
. . . . . 6
⊢ (𝑈 ∈ WUni → (𝑥 ∈ 𝑈 ↦ (Base‘𝑥)) ∈ V) |
| 23 | 5, 22 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝑈 ↦ (Base‘𝑥)) ∈ V) |
| 24 | | fvex 6919 |
. . . . . 6
⊢ (Hom
‘𝑅) ∈
V |
| 25 | 24 | a1i 11 |
. . . . 5
⊢ (𝜑 → (Hom ‘𝑅) ∈ V) |
| 26 | | mpoexga 8102 |
. . . . . 6
⊢ ((𝑈 ∈ WUni ∧ 𝑈 ∈ WUni) → (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m
(Base‘𝑥)))) ∈
V) |
| 27 | 5, 5, 26 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m
(Base‘𝑥)))) ∈
V) |
| 28 | 15, 19 | rnghmresfn 20619 |
. . . . 5
⊢ (𝜑 → (Hom ‘𝑅) Fn ((Base‘𝑅) × (Base‘𝑅))) |
| 29 | 23, 25, 27, 28 | resfval2 17938 |
. . . 4
⊢ (𝜑 → (〈(𝑥 ∈ 𝑈 ↦ (Base‘𝑥)), (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m
(Base‘𝑥))))〉
↾f (Hom ‘𝑅)) = 〈((𝑥 ∈ 𝑈 ↦ (Base‘𝑥)) ↾ (Base‘𝑅)), (𝑎 ∈ (Base‘𝑅), 𝑏 ∈ (Base‘𝑅) ↦ ((𝑎(𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m
(Base‘𝑥))))𝑏) ↾ (𝑎(Hom ‘𝑅)𝑏)))〉) |
| 30 | | inss1 4237 |
. . . . . . . 8
⊢ (𝑈 ∩ Rng) ⊆ 𝑈 |
| 31 | 15, 30 | eqsstrdi 4028 |
. . . . . . 7
⊢ (𝜑 → (Base‘𝑅) ⊆ 𝑈) |
| 32 | 31 | resmptd 6058 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ 𝑈 ↦ (Base‘𝑥)) ↾ (Base‘𝑅)) = (𝑥 ∈ (Base‘𝑅) ↦ (Base‘𝑥))) |
| 33 | | funcrngcsetc.f |
. . . . . . 7
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) |
| 34 | | funcrngcsetc.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝑅) |
| 35 | 34 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 = (Base‘𝑅)) |
| 36 | 35 | mpteq1d 5237 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)) = (𝑥 ∈ (Base‘𝑅) ↦ (Base‘𝑥))) |
| 37 | 33, 36 | eqtr2d 2778 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (Base‘𝑅) ↦ (Base‘𝑥)) = 𝐹) |
| 38 | 32, 37 | eqtrd 2777 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝑈 ↦ (Base‘𝑥)) ↾ (Base‘𝑅)) = 𝐹) |
| 39 | | funcrngcsetc.g |
. . . . . 6
⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RngHom 𝑦)))) |
| 40 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑥 = 𝑎 → (𝑥 RngHom 𝑦) = (𝑎 RngHom 𝑦)) |
| 41 | 40 | reseq2d 5997 |
. . . . . . . 8
⊢ (𝑥 = 𝑎 → ( I ↾ (𝑥 RngHom 𝑦)) = ( I ↾ (𝑎 RngHom 𝑦))) |
| 42 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑦 = 𝑏 → (𝑎 RngHom 𝑦) = (𝑎 RngHom 𝑏)) |
| 43 | 42 | reseq2d 5997 |
. . . . . . . 8
⊢ (𝑦 = 𝑏 → ( I ↾ (𝑎 RngHom 𝑦)) = ( I ↾ (𝑎 RngHom 𝑏))) |
| 44 | 41, 43 | cbvmpov 7528 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RngHom 𝑦))) = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ ( I ↾ (𝑎 RngHom 𝑏))) |
| 45 | 44 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RngHom 𝑦))) = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ ( I ↾ (𝑎 RngHom 𝑏)))) |
| 46 | 34 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → 𝐵 = (Base‘𝑅)) |
| 47 | | eqidd 2738 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m
(Base‘𝑥)))) = (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m
(Base‘𝑥))))) |
| 48 | | fveq2 6906 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑏 → (Base‘𝑦) = (Base‘𝑏)) |
| 49 | | fveq2 6906 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑎 → (Base‘𝑥) = (Base‘𝑎)) |
| 50 | 48, 49 | oveqan12rd 7451 |
. . . . . . . . . . . 12
⊢ ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → ((Base‘𝑦) ↑m (Base‘𝑥)) = ((Base‘𝑏) ↑m
(Base‘𝑎))) |
| 51 | 50 | reseq2d 5997 |
. . . . . . . . . . 11
⊢ ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → ( I ↾ ((Base‘𝑦) ↑m
(Base‘𝑥))) = ( I
↾ ((Base‘𝑏)
↑m (Base‘𝑎)))) |
| 52 | 51 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑥 = 𝑎 ∧ 𝑦 = 𝑏)) → ( I ↾ ((Base‘𝑦) ↑m
(Base‘𝑥))) = ( I
↾ ((Base‘𝑏)
↑m (Base‘𝑎)))) |
| 53 | 34, 31 | eqsstrid 4022 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵 ⊆ 𝑈) |
| 54 | 53 | sseld 3982 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑎 ∈ 𝐵 → 𝑎 ∈ 𝑈)) |
| 55 | 54 | com12 32 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ 𝐵 → (𝜑 → 𝑎 ∈ 𝑈)) |
| 56 | 55 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝜑 → 𝑎 ∈ 𝑈)) |
| 57 | 56 | impcom 407 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝑎 ∈ 𝑈) |
| 58 | 53 | sseld 3982 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑏 ∈ 𝐵 → 𝑏 ∈ 𝑈)) |
| 59 | 58 | adantld 490 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝑈)) |
| 60 | 59 | imp 406 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝑏 ∈ 𝑈) |
| 61 | | ovexd 7466 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((Base‘𝑏) ↑m (Base‘𝑎)) ∈ V) |
| 62 | 61 | resiexd 7236 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ( I ↾ ((Base‘𝑏) ↑m
(Base‘𝑎))) ∈
V) |
| 63 | 47, 52, 57, 60, 62 | ovmpod 7585 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎(𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m
(Base‘𝑥))))𝑏) = ( I ↾
((Base‘𝑏)
↑m (Base‘𝑎)))) |
| 64 | 63 | reseq1d 5996 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝑎(𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m
(Base‘𝑥))))𝑏) ↾ (𝑎(Hom ‘𝑅)𝑏)) = (( I ↾ ((Base‘𝑏) ↑m
(Base‘𝑎))) ↾
(𝑎(Hom ‘𝑅)𝑏))) |
| 65 | 5 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝑈 ∈ WUni) |
| 66 | | simprl 771 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝑎 ∈ 𝐵) |
| 67 | | simprr 773 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝑏 ∈ 𝐵) |
| 68 | 13, 34, 65, 18, 66, 67 | rngchom 20623 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎(Hom ‘𝑅)𝑏) = (𝑎 RngHom 𝑏)) |
| 69 | 68 | reseq2d 5997 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (( I ↾ ((Base‘𝑏) ↑m
(Base‘𝑎))) ↾
(𝑎(Hom ‘𝑅)𝑏)) = (( I ↾ ((Base‘𝑏) ↑m
(Base‘𝑎))) ↾
(𝑎 RngHom 𝑏))) |
| 70 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(Base‘𝑎) =
(Base‘𝑎) |
| 71 | | eqid 2737 |
. . . . . . . . . . . 12
⊢
(Base‘𝑏) =
(Base‘𝑏) |
| 72 | 70, 71 | rnghmf 20448 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ (𝑎 RngHom 𝑏) → 𝑓:(Base‘𝑎)⟶(Base‘𝑏)) |
| 73 | | fvex 6919 |
. . . . . . . . . . . . . 14
⊢
(Base‘𝑏)
∈ V |
| 74 | | fvex 6919 |
. . . . . . . . . . . . . 14
⊢
(Base‘𝑎)
∈ V |
| 75 | 73, 74 | pm3.2i 470 |
. . . . . . . . . . . . 13
⊢
((Base‘𝑏)
∈ V ∧ (Base‘𝑎) ∈ V) |
| 76 | 75 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((Base‘𝑏) ∈ V ∧ (Base‘𝑎) ∈ V)) |
| 77 | | elmapg 8879 |
. . . . . . . . . . . 12
⊢
(((Base‘𝑏)
∈ V ∧ (Base‘𝑎) ∈ V) → (𝑓 ∈ ((Base‘𝑏) ↑m (Base‘𝑎)) ↔ 𝑓:(Base‘𝑎)⟶(Base‘𝑏))) |
| 78 | 76, 77 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑓 ∈ ((Base‘𝑏) ↑m (Base‘𝑎)) ↔ 𝑓:(Base‘𝑎)⟶(Base‘𝑏))) |
| 79 | 72, 78 | imbitrrid 246 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑓 ∈ (𝑎 RngHom 𝑏) → 𝑓 ∈ ((Base‘𝑏) ↑m (Base‘𝑎)))) |
| 80 | 79 | ssrdv 3989 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎 RngHom 𝑏) ⊆ ((Base‘𝑏) ↑m (Base‘𝑎))) |
| 81 | 80 | resabs1d 6026 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (( I ↾ ((Base‘𝑏) ↑m
(Base‘𝑎))) ↾
(𝑎 RngHom 𝑏)) = ( I ↾ (𝑎 RngHom 𝑏))) |
| 82 | 64, 69, 81 | 3eqtrrd 2782 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ( I ↾ (𝑎 RngHom 𝑏)) = ((𝑎(𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m
(Base‘𝑥))))𝑏) ↾ (𝑎(Hom ‘𝑅)𝑏))) |
| 83 | 35, 46, 82 | mpoeq123dva 7507 |
. . . . . 6
⊢ (𝜑 → (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ ( I ↾ (𝑎 RngHom 𝑏))) = (𝑎 ∈ (Base‘𝑅), 𝑏 ∈ (Base‘𝑅) ↦ ((𝑎(𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m
(Base‘𝑥))))𝑏) ↾ (𝑎(Hom ‘𝑅)𝑏)))) |
| 84 | 39, 45, 83 | 3eqtrrd 2782 |
. . . . 5
⊢ (𝜑 → (𝑎 ∈ (Base‘𝑅), 𝑏 ∈ (Base‘𝑅) ↦ ((𝑎(𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m
(Base‘𝑥))))𝑏) ↾ (𝑎(Hom ‘𝑅)𝑏))) = 𝐺) |
| 85 | 38, 84 | opeq12d 4881 |
. . . 4
⊢ (𝜑 → 〈((𝑥 ∈ 𝑈 ↦ (Base‘𝑥)) ↾ (Base‘𝑅)), (𝑎 ∈ (Base‘𝑅), 𝑏 ∈ (Base‘𝑅) ↦ ((𝑎(𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m
(Base‘𝑥))))𝑏) ↾ (𝑎(Hom ‘𝑅)𝑏)))〉 = 〈𝐹, 𝐺〉) |
| 86 | 29, 85 | eqtr2d 2778 |
. . 3
⊢ (𝜑 → 〈𝐹, 𝐺〉 = (〈(𝑥 ∈ 𝑈 ↦ (Base‘𝑥)), (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m
(Base‘𝑥))))〉
↾f (Hom ‘𝑅))) |
| 87 | 13, 5, 15, 19 | rngcval 20618 |
. . . 4
⊢ (𝜑 → 𝑅 = ((ExtStrCat‘𝑈) ↾cat (Hom ‘𝑅))) |
| 88 | 87 | oveq1d 7446 |
. . 3
⊢ (𝜑 → (𝑅 Func 𝑆) = (((ExtStrCat‘𝑈) ↾cat (Hom ‘𝑅)) Func 𝑆)) |
| 89 | 21, 86, 88 | 3eltr4d 2856 |
. 2
⊢ (𝜑 → 〈𝐹, 𝐺〉 ∈ (𝑅 Func 𝑆)) |
| 90 | | df-br 5144 |
. 2
⊢ (𝐹(𝑅 Func 𝑆)𝐺 ↔ 〈𝐹, 𝐺〉 ∈ (𝑅 Func 𝑆)) |
| 91 | 89, 90 | sylibr 234 |
1
⊢ (𝜑 → 𝐹(𝑅 Func 𝑆)𝐺) |