precofvalALT

Description: Alternate proof of precofval . (Contributed by Zhi Wang, 11-Oct-2025) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	precofval.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
	precofval.r	⊢ 𝑅 = ( 𝐷 FuncCat 𝐸 )
	precofval.o	⊢ ( 𝜑 → ⚬ = ( ⟨ 𝑄 , 𝑅 ⟩ curry_F ( ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) ∘_func ( 𝑄 swap_F 𝑅 ) ) ) )
	precofval.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
	precofval.e	⊢ ( 𝜑 → 𝐸 ∈ Cat )
	precofval.k	⊢ ( 𝜑 → 𝐾 = ( ( 1^st ‘ ⚬ ) ‘ 𝐹 ) )
Assertion	precofvalALT	⊢ ( 𝜑 → 𝐾 = ⟨ ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑔 ∘_func 𝐹 ) ) , ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) , ℎ ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑎 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) ) ) ⟩ )

Proof

Step	Hyp	Ref	Expression
1		precofval.q	⊢ 𝑄 = ( 𝐶 FuncCat 𝐷 )
2		precofval.r	⊢ 𝑅 = ( 𝐷 FuncCat 𝐸 )
3		precofval.o	⊢ ( 𝜑 → ⚬ = ( ⟨ 𝑄 , 𝑅 ⟩ curry_F ( ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) ∘_func ( 𝑄 swap_F 𝑅 ) ) ) )
4		precofval.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 Func 𝐷 ) )
5		precofval.e	⊢ ( 𝜑 → 𝐸 ∈ Cat )
6		precofval.k	⊢ ( 𝜑 → 𝐾 = ( ( 1^st ‘ ⚬ ) ‘ 𝐹 ) )
7	1	fucbas	⊢ ( 𝐶 Func 𝐷 ) = ( Base ‘ 𝑄 )
8		relfunc	⊢ Rel ( 𝐶 Func 𝐷 )
9		1st2ndbr	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐹 ∈ ( 𝐶 Func 𝐷 ) ) → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
10	8 4 9	sylancr	⊢ ( 𝜑 → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
11	10	funcrcl2	⊢ ( 𝜑 → 𝐶 ∈ Cat )
12	10	funcrcl3	⊢ ( 𝜑 → 𝐷 ∈ Cat )
13	1 11 12	fuccat	⊢ ( 𝜑 → 𝑄 ∈ Cat )
14	2 12 5	fuccat	⊢ ( 𝜑 → 𝑅 ∈ Cat )
15	2 1	oveq12i	⊢ ( 𝑅 ×_c 𝑄 ) = ( ( 𝐷 FuncCat 𝐸 ) ×_c ( 𝐶 FuncCat 𝐷 ) )
16		eqid	⊢ ( 𝐶 FuncCat 𝐸 ) = ( 𝐶 FuncCat 𝐸 )
17	15 16 11 12 5	fucofunca	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) ∈ ( ( 𝑅 ×_c 𝑄 ) Func ( 𝐶 FuncCat 𝐸 ) ) )
18	2	fucbas	⊢ ( 𝐷 Func 𝐸 ) = ( Base ‘ 𝑅 )
19		eqid	⊢ ( 𝐷 Nat 𝐸 ) = ( 𝐷 Nat 𝐸 )
20	2 19	fuchom	⊢ ( 𝐷 Nat 𝐸 ) = ( Hom ‘ 𝑅 )
21		eqid	⊢ ( Id ‘ 𝑄 ) = ( Id ‘ 𝑄 )
22	3 7 13 14 17 4 6 18 20 21	tposcurf1	⊢ ( 𝜑 → 𝐾 = ⟨ ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑔 ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) ) 𝐹 ) ) , ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) , ℎ ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ↦ ( 𝑎 ( ⟨ 𝑔 , 𝐹 ⟩ ( 2^nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) ) ⟨ ℎ , 𝐹 ⟩ ) ( ( Id ‘ 𝑄 ) ‘ 𝐹 ) ) ) ) ⟩ )
23		df-ov	⊢ ( 𝑔 ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) ) 𝐹 ) = ( ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) ) ‘ ⟨ 𝑔 , 𝐹 ⟩ )
24		eqidd	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) = ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) )
25	11 12 5 24	fucoelvv	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) ∈ ( V × V ) )
26		1st2nd2	⊢ ( ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) ∈ ( V × V ) → ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) = ⟨ ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) ) , ( 2^nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) ) ⟩ )
27	25 26	syl	⊢ ( 𝜑 → ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) = ⟨ ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) ) , ( 2^nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) ) ⟩ )
28	27	adantr	⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐷 Func 𝐸 ) ) → ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) = ⟨ ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) ) , ( 2^nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) ) ⟩ )
29	10	adantr	⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐷 Func 𝐸 ) ) → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
30		relfunc	⊢ Rel ( 𝐷 Func 𝐸 )
31		1st2ndbr	⊢ ( ( Rel ( 𝐷 Func 𝐸 ) ∧ 𝑔 ∈ ( 𝐷 Func 𝐸 ) ) → ( 1^st ‘ 𝑔 ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ 𝑔 ) )
32	30 31	mpan	⊢ ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) → ( 1^st ‘ 𝑔 ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ 𝑔 ) )
33	32	adantl	⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐷 Func 𝐸 ) ) → ( 1^st ‘ 𝑔 ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ 𝑔 ) )
34		1st2nd	⊢ ( ( Rel ( 𝐷 Func 𝐸 ) ∧ 𝑔 ∈ ( 𝐷 Func 𝐸 ) ) → 𝑔 = ⟨ ( 1^st ‘ 𝑔 ) , ( 2^nd ‘ 𝑔 ) ⟩ )
35	30 34	mpan	⊢ ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) → 𝑔 = ⟨ ( 1^st ‘ 𝑔 ) , ( 2^nd ‘ 𝑔 ) ⟩ )
36	35	adantl	⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐷 Func 𝐸 ) ) → 𝑔 = ⟨ ( 1^st ‘ 𝑔 ) , ( 2^nd ‘ 𝑔 ) ⟩ )
37		1st2nd	⊢ ( ( Rel ( 𝐶 Func 𝐷 ) ∧ 𝐹 ∈ ( 𝐶 Func 𝐷 ) ) → 𝐹 = ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ )
38	8 4 37	sylancr	⊢ ( 𝜑 → 𝐹 = ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ )
39	38	adantr	⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐷 Func 𝐸 ) ) → 𝐹 = ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ )
40	36 39	opeq12d	⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐷 Func 𝐸 ) ) → ⟨ 𝑔 , 𝐹 ⟩ = ⟨ ⟨ ( 1^st ‘ 𝑔 ) , ( 2^nd ‘ 𝑔 ) ⟩ , ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ ⟩ )
41	28 29 33 40	fuco11	⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐷 Func 𝐸 ) ) → ( ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) ) ‘ ⟨ 𝑔 , 𝐹 ⟩ ) = ( ⟨ ( 1^st ‘ 𝑔 ) , ( 2^nd ‘ 𝑔 ) ⟩ ∘_func ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ ) )
42	36 39	oveq12d	⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐷 Func 𝐸 ) ) → ( 𝑔 ∘_func 𝐹 ) = ( ⟨ ( 1^st ‘ 𝑔 ) , ( 2^nd ‘ 𝑔 ) ⟩ ∘_func ⟨ ( 1^st ‘ 𝐹 ) , ( 2^nd ‘ 𝐹 ) ⟩ ) )
43	41 42	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐷 Func 𝐸 ) ) → ( ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) ) ‘ ⟨ 𝑔 , 𝐹 ⟩ ) = ( 𝑔 ∘_func 𝐹 ) )
44	23 43	eqtrid	⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐷 Func 𝐸 ) ) → ( 𝑔 ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) ) 𝐹 ) = ( 𝑔 ∘_func 𝐹 ) )
45	44	mpteq2dva	⊢ ( 𝜑 → ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑔 ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) ) 𝐹 ) ) = ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑔 ∘_func 𝐹 ) ) )
46		eqid	⊢ ( Id ‘ 𝐷 ) = ( Id ‘ 𝐷 )
47	1 21 46 4	fucid	⊢ ( 𝜑 → ( ( Id ‘ 𝑄 ) ‘ 𝐹 ) = ( ( Id ‘ 𝐷 ) ∘ ( 1^st ‘ 𝐹 ) ) )
48	47	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ∧ ℎ ∈ ( 𝐷 Func 𝐸 ) ) ) ∧ 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ) → ( ( Id ‘ 𝑄 ) ‘ 𝐹 ) = ( ( Id ‘ 𝐷 ) ∘ ( 1^st ‘ 𝐹 ) ) )
49	48	oveq2d	⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ∧ ℎ ∈ ( 𝐷 Func 𝐸 ) ) ) ∧ 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ) → ( 𝑎 ( ⟨ 𝑔 , 𝐹 ⟩ ( 2^nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) ) ⟨ ℎ , 𝐹 ⟩ ) ( ( Id ‘ 𝑄 ) ‘ 𝐹 ) ) = ( 𝑎 ( ⟨ 𝑔 , 𝐹 ⟩ ( 2^nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) ) ⟨ ℎ , 𝐹 ⟩ ) ( ( Id ‘ 𝐷 ) ∘ ( 1^st ‘ 𝐹 ) ) ) )
50	27	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ∧ ℎ ∈ ( 𝐷 Func 𝐸 ) ) ) ∧ 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ) → ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) = ⟨ ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) ) , ( 2^nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) ) ⟩ )
51		eqidd	⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ∧ ℎ ∈ ( 𝐷 Func 𝐸 ) ) ) ∧ 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ) → ⟨ 𝑔 , 𝐹 ⟩ = ⟨ 𝑔 , 𝐹 ⟩ )
52		eqidd	⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ∧ ℎ ∈ ( 𝐷 Func 𝐸 ) ) ) ∧ 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ) → ⟨ ℎ , 𝐹 ⟩ = ⟨ ℎ , 𝐹 ⟩ )
53		eqid	⊢ ( 𝐶 Nat 𝐷 ) = ( 𝐶 Nat 𝐷 )
54	1 53 46 4	fucidcl	⊢ ( 𝜑 → ( ( Id ‘ 𝐷 ) ∘ ( 1^st ‘ 𝐹 ) ) ∈ ( 𝐹 ( 𝐶 Nat 𝐷 ) 𝐹 ) )
55	54	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ∧ ℎ ∈ ( 𝐷 Func 𝐸 ) ) ) ∧ 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ) → ( ( Id ‘ 𝐷 ) ∘ ( 1^st ‘ 𝐹 ) ) ∈ ( 𝐹 ( 𝐶 Nat 𝐷 ) 𝐹 ) )
56		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ∧ ℎ ∈ ( 𝐷 Func 𝐸 ) ) ) ∧ 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ) → 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) )
57	50 51 52 55 56	fuco22a	⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ∧ ℎ ∈ ( 𝐷 Func 𝐸 ) ) ) ∧ 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ) → ( 𝑎 ( ⟨ 𝑔 , 𝐹 ⟩ ( 2^nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) ) ⟨ ℎ , 𝐹 ⟩ ) ( ( Id ‘ 𝐷 ) ∘ ( 1^st ‘ 𝐹 ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑎 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( ⟨ ( ( 1^st ‘ 𝑔 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝑔 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ ℎ ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝑔 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ‘ ( ( ( Id ‘ 𝐷 ) ∘ ( 1^st ‘ 𝐹 ) ) ‘ 𝑥 ) ) ) ) )
58		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
59		eqid	⊢ ( Base ‘ 𝐸 ) = ( Base ‘ 𝐸 )
60		eqid	⊢ ( Id ‘ 𝐸 ) = ( Id ‘ 𝐸 )
61	10	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ∧ ℎ ∈ ( 𝐷 Func 𝐸 ) ) ) ∧ 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
62	32	adantr	⊢ ( ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ∧ ℎ ∈ ( 𝐷 Func 𝐸 ) ) → ( 1^st ‘ 𝑔 ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ 𝑔 ) )
63	62	ad3antlr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ∧ ℎ ∈ ( 𝐷 Func 𝐸 ) ) ) ∧ 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 1^st ‘ 𝑔 ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ 𝑔 ) )
64		simpr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ∧ ℎ ∈ ( 𝐷 Func 𝐸 ) ) ) ∧ 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑥 ∈ ( Base ‘ 𝐶 ) )
65	58 59 46 60 61 63 64	precofvallem	⊢ ( ( ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ∧ ℎ ∈ ( 𝐷 Func 𝐸 ) ) ) ∧ 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝑔 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ‘ ( ( ( Id ‘ 𝐷 ) ∘ ( 1^st ‘ 𝐹 ) ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐸 ) ‘ ( ( 1^st ‘ 𝑔 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) ∧ ( ( 1^st ‘ 𝑔 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ∈ ( Base ‘ 𝐸 ) ) )
66	65	simpld	⊢ ( ( ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ∧ ℎ ∈ ( 𝐷 Func 𝐸 ) ) ) ∧ 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝑔 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ‘ ( ( ( Id ‘ 𝐷 ) ∘ ( 1^st ‘ 𝐹 ) ) ‘ 𝑥 ) ) = ( ( Id ‘ 𝐸 ) ‘ ( ( 1^st ‘ 𝑔 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) )
67	66	oveq2d	⊢ ( ( ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ∧ ℎ ∈ ( 𝐷 Func 𝐸 ) ) ) ∧ 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝑎 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( ⟨ ( ( 1^st ‘ 𝑔 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝑔 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ ℎ ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝑔 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ‘ ( ( ( Id ‘ 𝐷 ) ∘ ( 1^st ‘ 𝐹 ) ) ‘ 𝑥 ) ) ) = ( ( 𝑎 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( ⟨ ( ( 1^st ‘ 𝑔 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝑔 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ ℎ ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) ( ( Id ‘ 𝐸 ) ‘ ( ( 1^st ‘ 𝑔 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) ) )
68		eqid	⊢ ( Hom ‘ 𝐸 ) = ( Hom ‘ 𝐸 )
69	5	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ∧ ℎ ∈ ( 𝐷 Func 𝐸 ) ) ) ∧ 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝐸 ∈ Cat )
70	65	simprd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ∧ ℎ ∈ ( 𝐷 Func 𝐸 ) ) ) ∧ 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝑔 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ∈ ( Base ‘ 𝐸 ) )
71		eqid	⊢ ( comp ‘ 𝐸 ) = ( comp ‘ 𝐸 )
72		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
73		simpllr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ∧ ℎ ∈ ( 𝐷 Func 𝐸 ) ) ) ∧ 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ∧ ℎ ∈ ( 𝐷 Func 𝐸 ) ) )
74	73	simprd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ∧ ℎ ∈ ( 𝐷 Func 𝐸 ) ) ) ∧ 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ℎ ∈ ( 𝐷 Func 𝐸 ) )
75		1st2ndbr	⊢ ( ( Rel ( 𝐷 Func 𝐸 ) ∧ ℎ ∈ ( 𝐷 Func 𝐸 ) ) → ( 1^st ‘ ℎ ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ ℎ ) )
76	30 74 75	sylancr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ∧ ℎ ∈ ( 𝐷 Func 𝐸 ) ) ) ∧ 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 1^st ‘ ℎ ) ( 𝐷 Func 𝐸 ) ( 2^nd ‘ ℎ ) )
77	72 59 76	funcf1	⊢ ( ( ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ∧ ℎ ∈ ( 𝐷 Func 𝐸 ) ) ) ∧ 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 1^st ‘ ℎ ) : ( Base ‘ 𝐷 ) ⟶ ( Base ‘ 𝐸 ) )
78	10	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ∧ ℎ ∈ ( 𝐷 Func 𝐸 ) ) ) ∧ 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ) → ( 1^st ‘ 𝐹 ) ( 𝐶 Func 𝐷 ) ( 2^nd ‘ 𝐹 ) )
79	58 72 78	funcf1	⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ∧ ℎ ∈ ( 𝐷 Func 𝐸 ) ) ) ∧ 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ) → ( 1^st ‘ 𝐹 ) : ( Base ‘ 𝐶 ) ⟶ ( Base ‘ 𝐷 ) )
80	79	ffvelcdmda	⊢ ( ( ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ∧ ℎ ∈ ( 𝐷 Func 𝐸 ) ) ) ∧ 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐷 ) )
81	77 80	ffvelcdmd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ∧ ℎ ∈ ( 𝐷 Func 𝐸 ) ) ) ∧ 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 1^st ‘ ℎ ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ∈ ( Base ‘ 𝐸 ) )
82	56	adantr	⊢ ( ( ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ∧ ℎ ∈ ( 𝐷 Func 𝐸 ) ) ) ∧ 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) )
83	19 82	nat1st2nd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ∧ ℎ ∈ ( 𝐷 Func 𝐸 ) ) ) ∧ 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → 𝑎 ∈ ( ⟨ ( 1^st ‘ 𝑔 ) , ( 2^nd ‘ 𝑔 ) ⟩ ( 𝐷 Nat 𝐸 ) ⟨ ( 1^st ‘ ℎ ) , ( 2^nd ‘ ℎ ) ⟩ ) )
84	19 83 72 68 80	natcl	⊢ ( ( ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ∧ ℎ ∈ ( 𝐷 Func 𝐸 ) ) ) ∧ 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑎 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ∈ ( ( ( 1^st ‘ 𝑔 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( Hom ‘ 𝐸 ) ( ( 1^st ‘ ℎ ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) )
85	59 68 60 69 70 71 81 84	catrid	⊢ ( ( ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ∧ ℎ ∈ ( 𝐷 Func 𝐸 ) ) ) ∧ 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝑎 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( ⟨ ( ( 1^st ‘ 𝑔 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝑔 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ ℎ ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) ( ( Id ‘ 𝐸 ) ‘ ( ( 1^st ‘ 𝑔 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) ) = ( 𝑎 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) )
86	67 85	eqtrd	⊢ ( ( ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ∧ ℎ ∈ ( 𝐷 Func 𝐸 ) ) ) ∧ 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ) ∧ 𝑥 ∈ ( Base ‘ 𝐶 ) ) → ( ( 𝑎 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( ⟨ ( ( 1^st ‘ 𝑔 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝑔 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ ℎ ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝑔 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ‘ ( ( ( Id ‘ 𝐷 ) ∘ ( 1^st ‘ 𝐹 ) ) ‘ 𝑥 ) ) ) = ( 𝑎 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) )
87	86	mpteq2dva	⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ∧ ℎ ∈ ( 𝐷 Func 𝐸 ) ) ) ∧ 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ) → ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( ( 𝑎 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ( ⟨ ( ( 1^st ‘ 𝑔 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) , ( ( 1^st ‘ 𝑔 ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ⟩ ( comp ‘ 𝐸 ) ( ( 1^st ‘ ℎ ) ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) ( ( ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ( 2^nd ‘ 𝑔 ) ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ‘ ( ( ( Id ‘ 𝐷 ) ∘ ( 1^st ‘ 𝐹 ) ) ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑎 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) )
88	49 57 87	3eqtrd	⊢ ( ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ∧ ℎ ∈ ( 𝐷 Func 𝐸 ) ) ) ∧ 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ) → ( 𝑎 ( ⟨ 𝑔 , 𝐹 ⟩ ( 2^nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) ) ⟨ ℎ , 𝐹 ⟩ ) ( ( Id ‘ 𝑄 ) ‘ 𝐹 ) ) = ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑎 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) )
89	88	mpteq2dva	⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ∧ ℎ ∈ ( 𝐷 Func 𝐸 ) ) ) → ( 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ↦ ( 𝑎 ( ⟨ 𝑔 , 𝐹 ⟩ ( 2^nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) ) ⟨ ℎ , 𝐹 ⟩ ) ( ( Id ‘ 𝑄 ) ‘ 𝐹 ) ) ) = ( 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑎 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) ) )
90	89	3impb	⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐷 Func 𝐸 ) ∧ ℎ ∈ ( 𝐷 Func 𝐸 ) ) → ( 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ↦ ( 𝑎 ( ⟨ 𝑔 , 𝐹 ⟩ ( 2^nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) ) ⟨ ℎ , 𝐹 ⟩ ) ( ( Id ‘ 𝑄 ) ‘ 𝐹 ) ) ) = ( 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑎 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) ) )
91	90	mpoeq3dva	⊢ ( 𝜑 → ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) , ℎ ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ↦ ( 𝑎 ( ⟨ 𝑔 , 𝐹 ⟩ ( 2^nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) ) ⟨ ℎ , 𝐹 ⟩ ) ( ( Id ‘ 𝑄 ) ‘ 𝐹 ) ) ) ) = ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) , ℎ ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑎 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) ) ) )
92	45 91	opeq12d	⊢ ( 𝜑 → ⟨ ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑔 ( 1^st ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) ) 𝐹 ) ) , ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) , ℎ ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ↦ ( 𝑎 ( ⟨ 𝑔 , 𝐹 ⟩ ( 2^nd ‘ ( ⟨ 𝐶 , 𝐷 ⟩ ∘_F 𝐸 ) ) ⟨ ℎ , 𝐹 ⟩ ) ( ( Id ‘ 𝑄 ) ‘ 𝐹 ) ) ) ) ⟩ = ⟨ ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑔 ∘_func 𝐹 ) ) , ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) , ℎ ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑎 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) ) ) ⟩ )
93	22 92	eqtrd	⊢ ( 𝜑 → 𝐾 = ⟨ ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑔 ∘_func 𝐹 ) ) , ( 𝑔 ∈ ( 𝐷 Func 𝐸 ) , ℎ ∈ ( 𝐷 Func 𝐸 ) ↦ ( 𝑎 ∈ ( 𝑔 ( 𝐷 Nat 𝐸 ) ℎ ) ↦ ( 𝑥 ∈ ( Base ‘ 𝐶 ) ↦ ( 𝑎 ‘ ( ( 1^st ‘ 𝐹 ) ‘ 𝑥 ) ) ) ) ) ⟩ )

Metamath Proof Explorer

Theorem precofvalALT

Proof