Step | Hyp | Ref
| Expression |
1 | | eqid 2738 |
. . . . . 6
⊢
(ExtStrCat‘𝑈)
= (ExtStrCat‘𝑈) |
2 | | funcringcsetc.s |
. . . . . 6
⊢ 𝑆 = (SetCat‘𝑈) |
3 | | eqid 2738 |
. . . . . 6
⊢
(Base‘(ExtStrCat‘𝑈)) = (Base‘(ExtStrCat‘𝑈)) |
4 | | eqid 2738 |
. . . . . 6
⊢
(Base‘𝑆) =
(Base‘𝑆) |
5 | | funcringcsetc.u |
. . . . . 6
⊢ (𝜑 → 𝑈 ∈ WUni) |
6 | 1, 5 | estrcbas 17841 |
. . . . . . 7
⊢ (𝜑 → 𝑈 = (Base‘(ExtStrCat‘𝑈))) |
7 | 6 | mpteq1d 5169 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝑈 ↦ (Base‘𝑥)) = (𝑥 ∈ (Base‘(ExtStrCat‘𝑈)) ↦ (Base‘𝑥))) |
8 | | mpoeq12 7348 |
. . . . . . 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 17866 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝑈 ↦ (Base‘𝑥))((ExtStrCat‘𝑈) Func 𝑆)(𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m
(Base‘𝑥))))) |
11 | | df-br 5075 |
. . . . 5
⊢ ((𝑥 ∈ 𝑈 ↦ (Base‘𝑥))((ExtStrCat‘𝑈) Func 𝑆)(𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m
(Base‘𝑥)))) ↔
〈(𝑥 ∈ 𝑈 ↦ (Base‘𝑥)), (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m
(Base‘𝑥))))〉
∈ ((ExtStrCat‘𝑈)
Func 𝑆)) |
12 | 10, 11 | sylib 217 |
. . . 4
⊢ (𝜑 → 〈(𝑥 ∈ 𝑈 ↦ (Base‘𝑥)), (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m
(Base‘𝑥))))〉
∈ ((ExtStrCat‘𝑈)
Func 𝑆)) |
13 | | funcringcsetc.r |
. . . . . . 7
⊢ 𝑅 = (RingCat‘𝑈) |
14 | | eqid 2738 |
. . . . . . 7
⊢
(Base‘𝑅) =
(Base‘𝑅) |
15 | 13, 14, 5 | ringcbas 45569 |
. . . . . 6
⊢ (𝜑 → (Base‘𝑅) = (𝑈 ∩ Ring)) |
16 | | incom 4135 |
. . . . . 6
⊢ (𝑈 ∩ Ring) = (Ring ∩ 𝑈) |
17 | 15, 16 | eqtrdi 2794 |
. . . . 5
⊢ (𝜑 → (Base‘𝑅) = (Ring ∩ 𝑈)) |
18 | | eqid 2738 |
. . . . . 6
⊢ (Hom
‘𝑅) = (Hom
‘𝑅) |
19 | 13, 14, 5, 18 | ringchomfval 45570 |
. . . . 5
⊢ (𝜑 → (Hom ‘𝑅) = ( RingHom ↾
((Base‘𝑅) ×
(Base‘𝑅)))) |
20 | 1, 5, 17, 19 | rhmsubcsetc 45581 |
. . . 4
⊢ (𝜑 → (Hom ‘𝑅) ∈
(Subcat‘(ExtStrCat‘𝑈))) |
21 | 12, 20 | funcres 17611 |
. . 3
⊢ (𝜑 → (〈(𝑥 ∈ 𝑈 ↦ (Base‘𝑥)), (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m
(Base‘𝑥))))〉
↾f (Hom ‘𝑅)) ∈ (((ExtStrCat‘𝑈) ↾cat (Hom
‘𝑅)) Func 𝑆)) |
22 | | mptexg 7097 |
. . . . . 6
⊢ (𝑈 ∈ WUni → (𝑥 ∈ 𝑈 ↦ (Base‘𝑥)) ∈ V) |
23 | 5, 22 | syl 17 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝑈 ↦ (Base‘𝑥)) ∈ V) |
24 | | fvex 6787 |
. . . . . 6
⊢ (Hom
‘𝑅) ∈
V |
25 | 24 | a1i 11 |
. . . . 5
⊢ (𝜑 → (Hom ‘𝑅) ∈ V) |
26 | | mpoexga 7918 |
. . . . . 6
⊢ ((𝑈 ∈ WUni ∧ 𝑈 ∈ WUni) → (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m
(Base‘𝑥)))) ∈
V) |
27 | 5, 5, 26 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m
(Base‘𝑥)))) ∈
V) |
28 | 15, 19 | rhmresfn 45567 |
. . . . 5
⊢ (𝜑 → (Hom ‘𝑅) Fn ((Base‘𝑅) × (Base‘𝑅))) |
29 | 23, 25, 27, 28 | resfval2 17608 |
. . . 4
⊢ (𝜑 → (〈(𝑥 ∈ 𝑈 ↦ (Base‘𝑥)), (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m
(Base‘𝑥))))〉
↾f (Hom ‘𝑅)) = 〈((𝑥 ∈ 𝑈 ↦ (Base‘𝑥)) ↾ (Base‘𝑅)), (𝑎 ∈ (Base‘𝑅), 𝑏 ∈ (Base‘𝑅) ↦ ((𝑎(𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m
(Base‘𝑥))))𝑏) ↾ (𝑎(Hom ‘𝑅)𝑏)))〉) |
30 | | inss1 4162 |
. . . . . . . 8
⊢ (𝑈 ∩ Ring) ⊆ 𝑈 |
31 | 15, 30 | eqsstrdi 3975 |
. . . . . . 7
⊢ (𝜑 → (Base‘𝑅) ⊆ 𝑈) |
32 | 31 | resmptd 5948 |
. . . . . 6
⊢ (𝜑 → ((𝑥 ∈ 𝑈 ↦ (Base‘𝑥)) ↾ (Base‘𝑅)) = (𝑥 ∈ (Base‘𝑅) ↦ (Base‘𝑥))) |
33 | | funcringcsetc.f |
. . . . . . 7
⊢ (𝜑 → 𝐹 = (𝑥 ∈ 𝐵 ↦ (Base‘𝑥))) |
34 | | funcringcsetc.b |
. . . . . . . . 9
⊢ 𝐵 = (Base‘𝑅) |
35 | 34 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 𝐵 = (Base‘𝑅)) |
36 | 35 | mpteq1d 5169 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ 𝐵 ↦ (Base‘𝑥)) = (𝑥 ∈ (Base‘𝑅) ↦ (Base‘𝑥))) |
37 | 33, 36 | eqtr2d 2779 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (Base‘𝑅) ↦ (Base‘𝑥)) = 𝐹) |
38 | 32, 37 | eqtrd 2778 |
. . . . 5
⊢ (𝜑 → ((𝑥 ∈ 𝑈 ↦ (Base‘𝑥)) ↾ (Base‘𝑅)) = 𝐹) |
39 | | funcringcsetc.g |
. . . . . 6
⊢ (𝜑 → 𝐺 = (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RingHom 𝑦)))) |
40 | | oveq1 7282 |
. . . . . . . . 9
⊢ (𝑥 = 𝑎 → (𝑥 RingHom 𝑦) = (𝑎 RingHom 𝑦)) |
41 | 40 | reseq2d 5891 |
. . . . . . . 8
⊢ (𝑥 = 𝑎 → ( I ↾ (𝑥 RingHom 𝑦)) = ( I ↾ (𝑎 RingHom 𝑦))) |
42 | | oveq2 7283 |
. . . . . . . . 9
⊢ (𝑦 = 𝑏 → (𝑎 RingHom 𝑦) = (𝑎 RingHom 𝑏)) |
43 | 42 | reseq2d 5891 |
. . . . . . . 8
⊢ (𝑦 = 𝑏 → ( I ↾ (𝑎 RingHom 𝑦)) = ( I ↾ (𝑎 RingHom 𝑏))) |
44 | 41, 43 | cbvmpov 7370 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RingHom 𝑦))) = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ ( I ↾ (𝑎 RingHom 𝑏))) |
45 | 44 | a1i 11 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ 𝐵, 𝑦 ∈ 𝐵 ↦ ( I ↾ (𝑥 RingHom 𝑦))) = (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ ( I ↾ (𝑎 RingHom 𝑏)))) |
46 | 34 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → 𝐵 = (Base‘𝑅)) |
47 | | eqidd 2739 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m
(Base‘𝑥)))) = (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m
(Base‘𝑥))))) |
48 | | fveq2 6774 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑏 → (Base‘𝑦) = (Base‘𝑏)) |
49 | | fveq2 6774 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑎 → (Base‘𝑥) = (Base‘𝑎)) |
50 | 48, 49 | oveqan12rd 7295 |
. . . . . . . . . . . 12
⊢ ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → ((Base‘𝑦) ↑m (Base‘𝑥)) = ((Base‘𝑏) ↑m
(Base‘𝑎))) |
51 | 50 | reseq2d 5891 |
. . . . . . . . . . 11
⊢ ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → ( I ↾ ((Base‘𝑦) ↑m
(Base‘𝑥))) = ( I
↾ ((Base‘𝑏)
↑m (Base‘𝑎)))) |
52 | 51 | adantl 482 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) ∧ (𝑥 = 𝑎 ∧ 𝑦 = 𝑏)) → ( I ↾ ((Base‘𝑦) ↑m
(Base‘𝑥))) = ( I
↾ ((Base‘𝑏)
↑m (Base‘𝑎)))) |
53 | 34, 31 | eqsstrid 3969 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐵 ⊆ 𝑈) |
54 | 53 | sseld 3920 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑎 ∈ 𝐵 → 𝑎 ∈ 𝑈)) |
55 | 54 | com12 32 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ 𝐵 → (𝜑 → 𝑎 ∈ 𝑈)) |
56 | 55 | adantr 481 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → (𝜑 → 𝑎 ∈ 𝑈)) |
57 | 56 | impcom 408 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝑎 ∈ 𝑈) |
58 | 53 | sseld 3920 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑏 ∈ 𝐵 → 𝑏 ∈ 𝑈)) |
59 | 58 | adantld 491 |
. . . . . . . . . . 11
⊢ (𝜑 → ((𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝑈)) |
60 | 59 | imp 407 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝑏 ∈ 𝑈) |
61 | | ovexd 7310 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((Base‘𝑏) ↑m (Base‘𝑎)) ∈ V) |
62 | 61 | resiexd 7092 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ( I ↾ ((Base‘𝑏) ↑m
(Base‘𝑎))) ∈
V) |
63 | 47, 52, 57, 60, 62 | ovmpod 7425 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎(𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m
(Base‘𝑥))))𝑏) = ( I ↾
((Base‘𝑏)
↑m (Base‘𝑎)))) |
64 | 63 | reseq1d 5890 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((𝑎(𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m
(Base‘𝑥))))𝑏) ↾ (𝑎(Hom ‘𝑅)𝑏)) = (( I ↾ ((Base‘𝑏) ↑m
(Base‘𝑎))) ↾
(𝑎(Hom ‘𝑅)𝑏))) |
65 | 5 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝑈 ∈ WUni) |
66 | | simprl 768 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝑎 ∈ 𝐵) |
67 | | simprr 770 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → 𝑏 ∈ 𝐵) |
68 | 13, 34, 65, 18, 66, 67 | ringchom 45571 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎(Hom ‘𝑅)𝑏) = (𝑎 RingHom 𝑏)) |
69 | 68 | reseq2d 5891 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (( I ↾ ((Base‘𝑏) ↑m
(Base‘𝑎))) ↾
(𝑎(Hom ‘𝑅)𝑏)) = (( I ↾ ((Base‘𝑏) ↑m
(Base‘𝑎))) ↾
(𝑎 RingHom 𝑏))) |
70 | | eqid 2738 |
. . . . . . . . . . . 12
⊢
(Base‘𝑎) =
(Base‘𝑎) |
71 | | eqid 2738 |
. . . . . . . . . . . 12
⊢
(Base‘𝑏) =
(Base‘𝑏) |
72 | 70, 71 | rhmf 19970 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ (𝑎 RingHom 𝑏) → 𝑓:(Base‘𝑎)⟶(Base‘𝑏)) |
73 | | fvex 6787 |
. . . . . . . . . . . . . 14
⊢
(Base‘𝑏)
∈ V |
74 | | fvex 6787 |
. . . . . . . . . . . . . 14
⊢
(Base‘𝑎)
∈ V |
75 | 73, 74 | pm3.2i 471 |
. . . . . . . . . . . . 13
⊢
((Base‘𝑏)
∈ V ∧ (Base‘𝑎) ∈ V) |
76 | 75 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ((Base‘𝑏) ∈ V ∧ (Base‘𝑎) ∈ V)) |
77 | | elmapg 8628 |
. . . . . . . . . . . 12
⊢
(((Base‘𝑏)
∈ V ∧ (Base‘𝑎) ∈ V) → (𝑓 ∈ ((Base‘𝑏) ↑m (Base‘𝑎)) ↔ 𝑓:(Base‘𝑎)⟶(Base‘𝑏))) |
78 | 76, 77 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑓 ∈ ((Base‘𝑏) ↑m (Base‘𝑎)) ↔ 𝑓:(Base‘𝑎)⟶(Base‘𝑏))) |
79 | 72, 78 | syl5ibr 245 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑓 ∈ (𝑎 RingHom 𝑏) → 𝑓 ∈ ((Base‘𝑏) ↑m (Base‘𝑎)))) |
80 | 79 | ssrdv 3927 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (𝑎 RingHom 𝑏) ⊆ ((Base‘𝑏) ↑m (Base‘𝑎))) |
81 | 80 | resabs1d 5922 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → (( I ↾ ((Base‘𝑏) ↑m
(Base‘𝑎))) ↾
(𝑎 RingHom 𝑏)) = ( I ↾ (𝑎 RingHom 𝑏))) |
82 | 64, 69, 81 | 3eqtrrd 2783 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝐵 ∧ 𝑏 ∈ 𝐵)) → ( I ↾ (𝑎 RingHom 𝑏)) = ((𝑎(𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m
(Base‘𝑥))))𝑏) ↾ (𝑎(Hom ‘𝑅)𝑏))) |
83 | 35, 46, 82 | mpoeq123dva 7349 |
. . . . . 6
⊢ (𝜑 → (𝑎 ∈ 𝐵, 𝑏 ∈ 𝐵 ↦ ( I ↾ (𝑎 RingHom 𝑏))) = (𝑎 ∈ (Base‘𝑅), 𝑏 ∈ (Base‘𝑅) ↦ ((𝑎(𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m
(Base‘𝑥))))𝑏) ↾ (𝑎(Hom ‘𝑅)𝑏)))) |
84 | 39, 45, 83 | 3eqtrrd 2783 |
. . . . 5
⊢ (𝜑 → (𝑎 ∈ (Base‘𝑅), 𝑏 ∈ (Base‘𝑅) ↦ ((𝑎(𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m
(Base‘𝑥))))𝑏) ↾ (𝑎(Hom ‘𝑅)𝑏))) = 𝐺) |
85 | 38, 84 | opeq12d 4812 |
. . . 4
⊢ (𝜑 → 〈((𝑥 ∈ 𝑈 ↦ (Base‘𝑥)) ↾ (Base‘𝑅)), (𝑎 ∈ (Base‘𝑅), 𝑏 ∈ (Base‘𝑅) ↦ ((𝑎(𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m
(Base‘𝑥))))𝑏) ↾ (𝑎(Hom ‘𝑅)𝑏)))〉 = 〈𝐹, 𝐺〉) |
86 | 29, 85 | eqtr2d 2779 |
. . 3
⊢ (𝜑 → 〈𝐹, 𝐺〉 = (〈(𝑥 ∈ 𝑈 ↦ (Base‘𝑥)), (𝑥 ∈ 𝑈, 𝑦 ∈ 𝑈 ↦ ( I ↾ ((Base‘𝑦) ↑m
(Base‘𝑥))))〉
↾f (Hom ‘𝑅))) |
87 | 13, 5, 15, 19 | ringcval 45566 |
. . . 4
⊢ (𝜑 → 𝑅 = ((ExtStrCat‘𝑈) ↾cat (Hom ‘𝑅))) |
88 | 87 | oveq1d 7290 |
. . 3
⊢ (𝜑 → (𝑅 Func 𝑆) = (((ExtStrCat‘𝑈) ↾cat (Hom ‘𝑅)) Func 𝑆)) |
89 | 21, 86, 88 | 3eltr4d 2854 |
. 2
⊢ (𝜑 → 〈𝐹, 𝐺〉 ∈ (𝑅 Func 𝑆)) |
90 | | df-br 5075 |
. 2
⊢ (𝐹(𝑅 Func 𝑆)𝐺 ↔ 〈𝐹, 𝐺〉 ∈ (𝑅 Func 𝑆)) |
91 | 89, 90 | sylibr 233 |
1
⊢ (𝜑 → 𝐹(𝑅 Func 𝑆)𝐺) |