Theorem prcof1

Description: The object part of the pre-composition functor. (Contributed by Zhi Wang, 3-Nov-2025)

	Ref	Expression
Hypotheses	prcof1.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝐷 Func 𝐸 ) )
	prcof1.o	⊢ ( 𝜑 → ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) = 𝑂 )
Assertion	prcof1	⊢ ( 𝜑 → ( 𝑂 ‘ 𝐾 ) = ( 𝐾 ∘func 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		prcof1.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝐷 Func 𝐸 ) )
2		prcof1.o	⊢ ( 𝜑 → ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) = 𝑂 )
3	2	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ V ) → ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) = 𝑂 )
4		eqid	⊢ ( 𝐷 Func 𝐸 ) = ( 𝐷 Func 𝐸 )
5		eqid	⊢ ( 𝐷 Nat 𝐸 ) = ( 𝐷 Nat 𝐸 )
6	1	adantr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ V ) → 𝐾 ∈ ( 𝐷 Func 𝐸 ) )
7	6	func1st2nd	⊢ ( ( 𝜑 ∧ 𝐹 ∈ V ) → ( 1st ‘ 𝐾 ) ( 𝐷 Func 𝐸 ) ( 2nd ‘ 𝐾 ) )
8	7	funcrcl2	⊢ ( ( 𝜑 ∧ 𝐹 ∈ V ) → 𝐷 ∈ Cat )
9	7	funcrcl3	⊢ ( ( 𝜑 ∧ 𝐹 ∈ V ) → 𝐸 ∈ Cat )
10		simpr	⊢ ( ( 𝜑 ∧ 𝐹 ∈ V ) → 𝐹 ∈ V )
11	4 5 8 9 10	prcofvala	⊢ ( ( 𝜑 ∧ 𝐹 ∈ V ) → ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) = ⟨ ( 𝑘 ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑘 ∘func 𝐹 ) ) , ( 𝑘 ∈ ( 𝐷 Func 𝐸 ) , 𝑙 ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑎 ∈ ( 𝑘 ( 𝐷 Nat 𝐸 ) 𝑙 ) ↦ ( 𝑎 ∘ ( 1st ‘ 𝐹 ) ) ) ) ⟩ )
12	11	fveq2d	⊢ ( ( 𝜑 ∧ 𝐹 ∈ V ) → ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) = ( 1st ‘ ⟨ ( 𝑘 ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑘 ∘func 𝐹 ) ) , ( 𝑘 ∈ ( 𝐷 Func 𝐸 ) , 𝑙 ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑎 ∈ ( 𝑘 ( 𝐷 Nat 𝐸 ) 𝑙 ) ↦ ( 𝑎 ∘ ( 1st ‘ 𝐹 ) ) ) ) ⟩ ) )
13		ovex	⊢ ( 𝐷 Func 𝐸 ) ∈ V
14	13	mptex	⊢ ( 𝑘 ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑘 ∘func 𝐹 ) ) ∈ V
15	13 13	mpoex	⊢ ( 𝑘 ∈ ( 𝐷 Func 𝐸 ) , 𝑙 ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑎 ∈ ( 𝑘 ( 𝐷 Nat 𝐸 ) 𝑙 ) ↦ ( 𝑎 ∘ ( 1st ‘ 𝐹 ) ) ) ) ∈ V
16	14 15	op1st	⊢ ( 1st ‘ ⟨ ( 𝑘 ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑘 ∘func 𝐹 ) ) , ( 𝑘 ∈ ( 𝐷 Func 𝐸 ) , 𝑙 ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑎 ∈ ( 𝑘 ( 𝐷 Nat 𝐸 ) 𝑙 ) ↦ ( 𝑎 ∘ ( 1st ‘ 𝐹 ) ) ) ) ⟩ ) = ( 𝑘 ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑘 ∘func 𝐹 ) )
17	12 16	eqtrdi	⊢ ( ( 𝜑 ∧ 𝐹 ∈ V ) → ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) = ( 𝑘 ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑘 ∘func 𝐹 ) ) )
18	3 17	eqtr3d	⊢ ( ( 𝜑 ∧ 𝐹 ∈ V ) → 𝑂 = ( 𝑘 ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑘 ∘func 𝐹 ) ) )
19		simpr	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ V ) ∧ 𝑘 = 𝐾 ) → 𝑘 = 𝐾 )
20	19	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝐹 ∈ V ) ∧ 𝑘 = 𝐾 ) → ( 𝑘 ∘func 𝐹 ) = ( 𝐾 ∘func 𝐹 ) )
21		ovexd	⊢ ( ( 𝜑 ∧ 𝐹 ∈ V ) → ( 𝐾 ∘func 𝐹 ) ∈ V )
22	18 20 6 21	fvmptd	⊢ ( ( 𝜑 ∧ 𝐹 ∈ V ) → ( 𝑂 ‘ 𝐾 ) = ( 𝐾 ∘func 𝐹 ) )
23		0fv	⊢ ( ∅ ‘ 𝐾 ) = ∅
24		reldmprcof	⊢ Rel dom −∘F
25	24	ovprc2	⊢ ( ¬ 𝐹 ∈ V → ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) = ∅ )
26	25	fveq2d	⊢ ( ¬ 𝐹 ∈ V → ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) = ( 1st ‘ ∅ ) )
27		1st0	⊢ ( 1st ‘ ∅ ) = ∅
28	26 27	eqtrdi	⊢ ( ¬ 𝐹 ∈ V → ( 1st ‘ ( ⟨ 𝐷 , 𝐸 ⟩ −∘F 𝐹 ) ) = ∅ )
29	2 28	sylan9req	⊢ ( ( 𝜑 ∧ ¬ 𝐹 ∈ V ) → 𝑂 = ∅ )
30	29	fveq1d	⊢ ( ( 𝜑 ∧ ¬ 𝐹 ∈ V ) → ( 𝑂 ‘ 𝐾 ) = ( ∅ ‘ 𝐾 ) )
31		df-cofu	⊢ ∘func = ( 𝑙 ∈ V , 𝑘 ∈ V ↦ ⟨ ( ( 1st ‘ 𝑙 ) ∘ ( 1st ‘ 𝑘 ) ) , ( 𝑎 ∈ dom dom ( 2nd ‘ 𝑘 ) , 𝑏 ∈ dom dom ( 2nd ‘ 𝑘 ) ↦ ( ( ( ( 1st ‘ 𝑘 ) ‘ 𝑎 ) ( 2nd ‘ 𝑙 ) ( ( 1st ‘ 𝑘 ) ‘ 𝑏 ) ) ∘ ( 𝑎 ( 2nd ‘ 𝑘 ) 𝑏 ) ) ) ⟩ )
32	31	reldmmpo	⊢ Rel dom ∘func
33	32	ovprc2	⊢ ( ¬ 𝐹 ∈ V → ( 𝐾 ∘func 𝐹 ) = ∅ )
34	33	adantl	⊢ ( ( 𝜑 ∧ ¬ 𝐹 ∈ V ) → ( 𝐾 ∘func 𝐹 ) = ∅ )
35	23 30 34	3eqtr4a	⊢ ( ( 𝜑 ∧ ¬ 𝐹 ∈ V ) → ( 𝑂 ‘ 𝐾 ) = ( 𝐾 ∘func 𝐹 ) )
36	22 35	pm2.61dan	⊢ ( 𝜑 → ( 𝑂 ‘ 𝐾 ) = ( 𝐾 ∘func 𝐹 ) )