| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | funcoppc.o | . . 3
⊢ 𝑂 = (oppCat‘𝐶) | 
| 2 |  | eqid 2736 | . . 3
⊢
(Base‘𝐶) =
(Base‘𝐶) | 
| 3 | 1, 2 | oppcbas 17762 | . 2
⊢
(Base‘𝐶) =
(Base‘𝑂) | 
| 4 |  | funcoppc.p | . . 3
⊢ 𝑃 = (oppCat‘𝐷) | 
| 5 |  | eqid 2736 | . . 3
⊢
(Base‘𝐷) =
(Base‘𝐷) | 
| 6 | 4, 5 | oppcbas 17762 | . 2
⊢
(Base‘𝐷) =
(Base‘𝑃) | 
| 7 |  | eqid 2736 | . 2
⊢ (Hom
‘𝑂) = (Hom
‘𝑂) | 
| 8 |  | eqid 2736 | . 2
⊢ (Hom
‘𝑃) = (Hom
‘𝑃) | 
| 9 |  | eqid 2736 | . 2
⊢
(Id‘𝑂) =
(Id‘𝑂) | 
| 10 |  | eqid 2736 | . 2
⊢
(Id‘𝑃) =
(Id‘𝑃) | 
| 11 |  | eqid 2736 | . 2
⊢
(comp‘𝑂) =
(comp‘𝑂) | 
| 12 |  | eqid 2736 | . 2
⊢
(comp‘𝑃) =
(comp‘𝑃) | 
| 13 |  | funcoppc.f | . . . . . 6
⊢ (𝜑 → 𝐹(𝐶 Func 𝐷)𝐺) | 
| 14 |  | df-br 5143 | . . . . . 6
⊢ (𝐹(𝐶 Func 𝐷)𝐺 ↔ 〈𝐹, 𝐺〉 ∈ (𝐶 Func 𝐷)) | 
| 15 | 13, 14 | sylib 218 | . . . . 5
⊢ (𝜑 → 〈𝐹, 𝐺〉 ∈ (𝐶 Func 𝐷)) | 
| 16 |  | funcrcl 17909 | . . . . 5
⊢
(〈𝐹, 𝐺〉 ∈ (𝐶 Func 𝐷) → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat)) | 
| 17 | 15, 16 | syl 17 | . . . 4
⊢ (𝜑 → (𝐶 ∈ Cat ∧ 𝐷 ∈ Cat)) | 
| 18 | 17 | simpld 494 | . . 3
⊢ (𝜑 → 𝐶 ∈ Cat) | 
| 19 | 1 | oppccat 17766 | . . 3
⊢ (𝐶 ∈ Cat → 𝑂 ∈ Cat) | 
| 20 | 18, 19 | syl 17 | . 2
⊢ (𝜑 → 𝑂 ∈ Cat) | 
| 21 | 4 | oppccat 17766 | . . 3
⊢ (𝐷 ∈ Cat → 𝑃 ∈ Cat) | 
| 22 | 17, 21 | simpl2im 503 | . 2
⊢ (𝜑 → 𝑃 ∈ Cat) | 
| 23 | 2, 5, 13 | funcf1 17912 | . 2
⊢ (𝜑 → 𝐹:(Base‘𝐶)⟶(Base‘𝐷)) | 
| 24 | 2, 13 | funcfn2 17915 | . . 3
⊢ (𝜑 → 𝐺 Fn ((Base‘𝐶) × (Base‘𝐶))) | 
| 25 |  | tposfn 8281 | . . 3
⊢ (𝐺 Fn ((Base‘𝐶) × (Base‘𝐶)) → tpos 𝐺 Fn ((Base‘𝐶) × (Base‘𝐶))) | 
| 26 | 24, 25 | syl 17 | . 2
⊢ (𝜑 → tpos 𝐺 Fn ((Base‘𝐶) × (Base‘𝐶))) | 
| 27 |  | eqid 2736 | . . . 4
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) | 
| 28 |  | eqid 2736 | . . . 4
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) | 
| 29 | 13 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝐹(𝐶 Func 𝐷)𝐺) | 
| 30 |  | simprr 772 | . . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝑦 ∈ (Base‘𝐶)) | 
| 31 |  | simprl 770 | . . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝑥 ∈ (Base‘𝐶)) | 
| 32 | 2, 27, 28, 29, 30, 31 | funcf2 17914 | . . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑦𝐺𝑥):(𝑦(Hom ‘𝐶)𝑥)⟶((𝐹‘𝑦)(Hom ‘𝐷)(𝐹‘𝑥))) | 
| 33 |  | ovtpos 8267 | . . . . 5
⊢ (𝑥tpos 𝐺𝑦) = (𝑦𝐺𝑥) | 
| 34 | 33 | feq1i 6726 | . . . 4
⊢ ((𝑥tpos 𝐺𝑦):(𝑥(Hom ‘𝑂)𝑦)⟶((𝐹‘𝑥)(Hom ‘𝑃)(𝐹‘𝑦)) ↔ (𝑦𝐺𝑥):(𝑥(Hom ‘𝑂)𝑦)⟶((𝐹‘𝑥)(Hom ‘𝑃)(𝐹‘𝑦))) | 
| 35 | 27, 1 | oppchom 17759 | . . . . 5
⊢ (𝑥(Hom ‘𝑂)𝑦) = (𝑦(Hom ‘𝐶)𝑥) | 
| 36 | 28, 4 | oppchom 17759 | . . . . 5
⊢ ((𝐹‘𝑥)(Hom ‘𝑃)(𝐹‘𝑦)) = ((𝐹‘𝑦)(Hom ‘𝐷)(𝐹‘𝑥)) | 
| 37 | 35, 36 | feq23i 6729 | . . . 4
⊢ ((𝑦𝐺𝑥):(𝑥(Hom ‘𝑂)𝑦)⟶((𝐹‘𝑥)(Hom ‘𝑃)(𝐹‘𝑦)) ↔ (𝑦𝐺𝑥):(𝑦(Hom ‘𝐶)𝑥)⟶((𝐹‘𝑦)(Hom ‘𝐷)(𝐹‘𝑥))) | 
| 38 | 34, 37 | bitri 275 | . . 3
⊢ ((𝑥tpos 𝐺𝑦):(𝑥(Hom ‘𝑂)𝑦)⟶((𝐹‘𝑥)(Hom ‘𝑃)(𝐹‘𝑦)) ↔ (𝑦𝐺𝑥):(𝑦(Hom ‘𝐶)𝑥)⟶((𝐹‘𝑦)(Hom ‘𝐷)(𝐹‘𝑥))) | 
| 39 | 32, 38 | sylibr 234 | . 2
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥tpos 𝐺𝑦):(𝑥(Hom ‘𝑂)𝑦)⟶((𝐹‘𝑥)(Hom ‘𝑃)(𝐹‘𝑦))) | 
| 40 |  | eqid 2736 | . . . 4
⊢
(Id‘𝐶) =
(Id‘𝐶) | 
| 41 |  | eqid 2736 | . . . 4
⊢
(Id‘𝐷) =
(Id‘𝐷) | 
| 42 | 13 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝐹(𝐶 Func 𝐷)𝐺) | 
| 43 |  | simpr 484 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → 𝑥 ∈ (Base‘𝐶)) | 
| 44 | 2, 40, 41, 42, 43 | funcid 17916 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑥𝐺𝑥)‘((Id‘𝐶)‘𝑥)) = ((Id‘𝐷)‘(𝐹‘𝑥))) | 
| 45 |  | ovtpos 8267 | . . . . 5
⊢ (𝑥tpos 𝐺𝑥) = (𝑥𝐺𝑥) | 
| 46 | 45 | a1i 11 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (𝑥tpos 𝐺𝑥) = (𝑥𝐺𝑥)) | 
| 47 | 1, 40 | oppcid 17765 | . . . . . . 7
⊢ (𝐶 ∈ Cat →
(Id‘𝑂) =
(Id‘𝐶)) | 
| 48 | 18, 47 | syl 17 | . . . . . 6
⊢ (𝜑 → (Id‘𝑂) = (Id‘𝐶)) | 
| 49 | 48 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (Id‘𝑂) = (Id‘𝐶)) | 
| 50 | 49 | fveq1d 6907 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((Id‘𝑂)‘𝑥) = ((Id‘𝐶)‘𝑥)) | 
| 51 | 46, 50 | fveq12d 6912 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑥tpos 𝐺𝑥)‘((Id‘𝑂)‘𝑥)) = ((𝑥𝐺𝑥)‘((Id‘𝐶)‘𝑥))) | 
| 52 | 4, 41 | oppcid 17765 | . . . . . 6
⊢ (𝐷 ∈ Cat →
(Id‘𝑃) =
(Id‘𝐷)) | 
| 53 | 17, 52 | simpl2im 503 | . . . . 5
⊢ (𝜑 → (Id‘𝑃) = (Id‘𝐷)) | 
| 54 | 53 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → (Id‘𝑃) = (Id‘𝐷)) | 
| 55 | 54 | fveq1d 6907 | . . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((Id‘𝑃)‘(𝐹‘𝑥)) = ((Id‘𝐷)‘(𝐹‘𝑥))) | 
| 56 | 44, 51, 55 | 3eqtr4d 2786 | . 2
⊢ ((𝜑 ∧ 𝑥 ∈ (Base‘𝐶)) → ((𝑥tpos 𝐺𝑥)‘((Id‘𝑂)‘𝑥)) = ((Id‘𝑃)‘(𝐹‘𝑥))) | 
| 57 |  | eqid 2736 | . . . . 5
⊢
(comp‘𝐶) =
(comp‘𝐶) | 
| 58 |  | eqid 2736 | . . . . 5
⊢
(comp‘𝐷) =
(comp‘𝐷) | 
| 59 | 13 | 3ad2ant1 1133 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧))) → 𝐹(𝐶 Func 𝐷)𝐺) | 
| 60 |  | simp23 1208 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧))) → 𝑧 ∈ (Base‘𝐶)) | 
| 61 |  | simp22 1207 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧))) → 𝑦 ∈ (Base‘𝐶)) | 
| 62 |  | simp21 1206 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧))) → 𝑥 ∈ (Base‘𝐶)) | 
| 63 |  | simp3r 1202 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧))) → 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧)) | 
| 64 | 27, 1 | oppchom 17759 | . . . . . 6
⊢ (𝑦(Hom ‘𝑂)𝑧) = (𝑧(Hom ‘𝐶)𝑦) | 
| 65 | 63, 64 | eleqtrdi 2850 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧))) → 𝑔 ∈ (𝑧(Hom ‘𝐶)𝑦)) | 
| 66 |  | simp3l 1201 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧))) → 𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦)) | 
| 67 | 66, 35 | eleqtrdi 2850 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧))) → 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) | 
| 68 | 2, 27, 57, 58, 59, 60, 61, 62, 65, 67 | funcco 17917 | . . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧))) → ((𝑧𝐺𝑥)‘(𝑓(〈𝑧, 𝑦〉(comp‘𝐶)𝑥)𝑔)) = (((𝑦𝐺𝑥)‘𝑓)(〈(𝐹‘𝑧), (𝐹‘𝑦)〉(comp‘𝐷)(𝐹‘𝑥))((𝑧𝐺𝑦)‘𝑔))) | 
| 69 | 2, 57, 1, 62, 61, 60 | oppcco 17761 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧))) → (𝑔(〈𝑥, 𝑦〉(comp‘𝑂)𝑧)𝑓) = (𝑓(〈𝑧, 𝑦〉(comp‘𝐶)𝑥)𝑔)) | 
| 70 | 69 | fveq2d 6909 | . . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧))) → ((𝑧𝐺𝑥)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝑂)𝑧)𝑓)) = ((𝑧𝐺𝑥)‘(𝑓(〈𝑧, 𝑦〉(comp‘𝐶)𝑥)𝑔))) | 
| 71 | 23 | 3ad2ant1 1133 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧))) → 𝐹:(Base‘𝐶)⟶(Base‘𝐷)) | 
| 72 | 71, 62 | ffvelcdmd 7104 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧))) → (𝐹‘𝑥) ∈ (Base‘𝐷)) | 
| 73 | 71, 61 | ffvelcdmd 7104 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧))) → (𝐹‘𝑦) ∈ (Base‘𝐷)) | 
| 74 | 71, 60 | ffvelcdmd 7104 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧))) → (𝐹‘𝑧) ∈ (Base‘𝐷)) | 
| 75 | 5, 58, 4, 72, 73, 74 | oppcco 17761 | . . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧))) → (((𝑧𝐺𝑦)‘𝑔)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘𝑃)(𝐹‘𝑧))((𝑦𝐺𝑥)‘𝑓)) = (((𝑦𝐺𝑥)‘𝑓)(〈(𝐹‘𝑧), (𝐹‘𝑦)〉(comp‘𝐷)(𝐹‘𝑥))((𝑧𝐺𝑦)‘𝑔))) | 
| 76 | 68, 70, 75 | 3eqtr4d 2786 | . . 3
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧))) → ((𝑧𝐺𝑥)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝑂)𝑧)𝑓)) = (((𝑧𝐺𝑦)‘𝑔)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘𝑃)(𝐹‘𝑧))((𝑦𝐺𝑥)‘𝑓))) | 
| 77 |  | ovtpos 8267 | . . . 4
⊢ (𝑥tpos 𝐺𝑧) = (𝑧𝐺𝑥) | 
| 78 | 77 | fveq1i 6906 | . . 3
⊢ ((𝑥tpos 𝐺𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝑂)𝑧)𝑓)) = ((𝑧𝐺𝑥)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝑂)𝑧)𝑓)) | 
| 79 |  | ovtpos 8267 | . . . . 5
⊢ (𝑦tpos 𝐺𝑧) = (𝑧𝐺𝑦) | 
| 80 | 79 | fveq1i 6906 | . . . 4
⊢ ((𝑦tpos 𝐺𝑧)‘𝑔) = ((𝑧𝐺𝑦)‘𝑔) | 
| 81 | 33 | fveq1i 6906 | . . . 4
⊢ ((𝑥tpos 𝐺𝑦)‘𝑓) = ((𝑦𝐺𝑥)‘𝑓) | 
| 82 | 80, 81 | oveq12i 7444 | . . 3
⊢ (((𝑦tpos 𝐺𝑧)‘𝑔)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘𝑃)(𝐹‘𝑧))((𝑥tpos 𝐺𝑦)‘𝑓)) = (((𝑧𝐺𝑦)‘𝑔)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘𝑃)(𝐹‘𝑧))((𝑦𝐺𝑥)‘𝑓)) | 
| 83 | 76, 78, 82 | 3eqtr4g 2801 | . 2
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶) ∧ 𝑧 ∈ (Base‘𝐶)) ∧ (𝑓 ∈ (𝑥(Hom ‘𝑂)𝑦) ∧ 𝑔 ∈ (𝑦(Hom ‘𝑂)𝑧))) → ((𝑥tpos 𝐺𝑧)‘(𝑔(〈𝑥, 𝑦〉(comp‘𝑂)𝑧)𝑓)) = (((𝑦tpos 𝐺𝑧)‘𝑔)(〈(𝐹‘𝑥), (𝐹‘𝑦)〉(comp‘𝑃)(𝐹‘𝑧))((𝑥tpos 𝐺𝑦)‘𝑓))) | 
| 84 | 3, 6, 7, 8, 9, 10,
11, 12, 20, 22, 23, 26, 39, 56, 83 | isfuncd 17911 | 1
⊢ (𝜑 → 𝐹(𝑂 Func 𝑃)tpos 𝐺) |